Skip to content

Commit

Permalink
added simple explanations for user input
Browse files Browse the repository at this point in the history
  • Loading branch information
nrueh committed Nov 30, 2024
1 parent ccbe10e commit 97fca11
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 9 deletions.
29 changes: 26 additions & 3 deletions src/coomsuite/application.py
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,25 @@ def preprocess(self, files: List[str]) -> List[str]:

return facts

def parse_unsat(self, unsat: Symbol) -> str:
type = unsat.arguments[0].string
info = unsat.arguments[1]

if type == "not exists":
variable = info.string
msg = f"Variable {variable} does not exists in the model."
elif type == "not part":
variable = info.string
msg = f"Variable {variable} cannot be added."
elif type == "not attribute":
variable = info.string
msg = f"No value can be set for variable {variable}."
elif type == "outside domain":
variable = info.arguments[0].string
value = info.arguments[1].string
msg = f"Value '{value}' is not in domain of variable {variable}."
return msg

def check_user_input(self, facts: list[str]) -> SolveResult:
"""
Checks if the user input is valid and returns a clingo.SolveResult
Expand All @@ -180,7 +199,9 @@ def check_user_input(self, facts: list[str]) -> SolveResult:
user_input_ctl.load(get_encoding("user-check.lp"))
user_input_ctl.add("".join(facts))
user_input_ctl.ground()
return user_input_ctl.solve()
with user_input_ctl.solve(yield_=True) as handle:
unsat = [self.parse_unsat(s) for s in handle.model().symbols(shown=True)]
return unsat

def main(self, control: Control, files: Sequence[str]) -> None:
"""
Expand All @@ -190,8 +211,10 @@ def main(self, control: Control, files: Sequence[str]) -> None:
if self._show:
print("\n".join(processed_facts)) # nocoverage
else:
if self.check_user_input(processed_facts).unsatisfiable:
raise ValueError("User input not valid.")
user_input_check = self.check_user_input(processed_facts)
if user_input_check != []:
error_msg = "User input not valid.\n" + "\n".join(user_input_check)
raise ValueError(error_msg)

encoding = get_encoding(f"encoding-base-{self._solver}.lp")
facts = "".join(processed_facts)
Expand Down
16 changes: 10 additions & 6 deletions src/coomsuite/encodings/user-check.lp
Original file line number Diff line number Diff line change
@@ -1,12 +1,16 @@
% Check that variables exist
:- user_value(X,_), not type(X,_).
:- user_include(X), not type(X,_).
unsat("not exists",X) :- user_value(X,_), not type(X,_).
unsat("not exists",X) :- user_include(X), not type(X,_).

% Check variable type
:- user_include(X), type(X,T), not part(T).
:- user_value(X,V), type(X,T), #false : discrete(T); #false : integer(T).
unsat("not part",X) :- user_include(X), type(X,T), not part(T).
unsat("not attribute",X) :- user_value(X,V), type(X,T), #false : discrete(T); #false : integer(T).

% Check valid domain
:- user_value(X,V), type(X,T), not domain(T,V).

unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), discrete(T), not domain(T,V).
unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V < Min.
unsat("outside domain",(X,V)) :- user_value(X,V), type(X,T), integer(T), range(T,Min,Max), V > Max.
% Check max cardinality not exceeded
% For now this is covered by line 3 (only max amount of objects is grounded)

#show unsat/2.

0 comments on commit 97fca11

Please sign in to comment.