Merge pull request #28 from potassco/nico/user-input-new

Nico/user input new

README.md

@@ -122,6 +122,15 @@ Modify [this line](src/coomsuite/application.py#L182) to insert your own
 encoding. Note that you might also have to disable/modify the preprocessing
 encoding [here](<(src/coomsuite/application.py#L159)>).
 
+#### Generate ANTLR4 Python files
+
+From the corresponding folder run (possibly replacing the version number and
+grammar file name)
+
+```
+antlr4 -v 4.9.3 -Dlanguage=Python3 Grammar.g4 -visitor
+```
+
 ## Development
 
 To improve code quality, we use [nox] to run linters, type checkers, unit

examples/coom/user-input.coom

@@ -0,0 +1,4 @@
+
+set color[0] = "Yellow"
+// add basket
+add 2 carrier[0].bag

noxfile.py

@@ -5,9 +5,9 @@
 nox.options.sessions = "lint_pylint", "typecheck", "test"
 
 EDITABLE_TESTS = True
-PYTHON_VERSIONS = ["3.9", "3.11"]
+PYTHON_VERSIONS = ["3.12"]
 if "GITHUB_ACTIONS" in os.environ:
-    # PYTHON_VERSIONS = ["3.9", "3.11"]
+    PYTHON_VERSIONS = ["3.9", "3.11"]
     EDITABLE_TESTS = False
 
 

src/coomsuite/__init__.py

@@ -15,21 +15,26 @@
 SOLVERS = ["clingo", "fclingo"]
 
 
-def convert_instance(coom_file: str, outdir: Optional[str] = None) -> str:  # nocoverage
+def convert_instance(coom_file: str, grammar: str, outdir: Optional[str] = None) -> str:  # nocoverage
     """
     Converts a COOM instance into ASP
     Args:
         coom_file (str): COOM file .coom
         output_dir (str, optional): Name of the output directory, by default the same of coom_file is used
     """
     input_stream = FileStream(coom_file, encoding="utf-8")
-    asp_instance = "\n".join([f"coom_{a}" if a != "" else a for a in run_antlr4_visitor(input_stream)])
+    asp_instance = "\n".join([f"coom_{a}" if a != "" else a for a in run_antlr4_visitor(input_stream, grammar=grammar)])
 
     if outdir is not None:
         filename = splitext(basename(coom_file))[0] + "-coom.lp"
         output_lp_file = join(outdir, filename)
 
         with open(output_lp_file, "w", encoding="utf8") as f:
+            if grammar == "model":
+                f.write("%%% COOM model\n")
+            elif grammar == "user":
+                f.write("%%% User Input\n")
+
             f.write(asp_instance)
             f.write("\n")
         log.info("ASP file saved in %s", output_lp_file)

src/coomsuite/__main__.py

@@ -29,14 +29,26 @@ def main():
     # log.error("error")
 
     if args.command == "convert":
-        asp_instance = convert_instance(args.input, args.output)
+        asp_instance = convert_instance(args.input, "model", args.output)
+
+        if args.user_input:
+            output_user_lp_file = convert_instance(args.user_input, "user", args.output)
+
         if args.output is None:
             print(asp_instance)
+            if args.user_input:
+                print("")
+                print(output_user_lp_file)
 
     elif args.command == "solve":
         log.info("Converting and solving COOM file %s", args.input)
         with TemporaryDirectory() as temp_dir:
-            options = [convert_instance(args.input, temp_dir)] + unknown_args
+            options = (
+                [convert_instance(args.input, "model", temp_dir)]
+                + ([convert_instance(args.user_input, "user", temp_dir)] if args.user_input else [])
+                + unknown_args
+            )
+
             if args.show:
                 options.append("--outf=3")
 

src/coomsuite/application.py

@@ -171,6 +171,45 @@ def preprocess(self, files: List[str]) -> List[str]:
 
         return facts
 
+    def parse_user_input_unsat(self, unsat: Symbol) -> str:
+        """
+        Parses the unsat/2 predicates of the user input check
+        """
+        unsat_type = unsat.arguments[0].string
+        info = unsat.arguments[1]
+
+        if unsat_type == "not exists":
+            variable = info.string
+            msg = f"Variable {variable} is not valid."
+        elif unsat_type == "not part":
+            variable = info.string
+            msg = f"Variable {variable} cannot be added."
+        elif unsat_type == "not attribute":
+            variable = info.string
+            msg = f"No value can be set for variable {variable}."
+        elif unsat_type == "outside domain":
+            variable = info.arguments[0].string
+            if str(info.arguments[1].type) == "SymbolType.Number":
+                value = str(info.arguments[1].number)
+            else:
+                value = info.arguments[1].string
+            msg = f"Value '{value}' is not in domain of variable {variable}."
+        else:
+            raise ValueError(f"Unknown unsat type: {unsat_type}")  # nocoverage
+        return msg
+
+    def check_user_input(self, facts: list[str]) -> list[str]:
+        """
+        Checks if the user input is valid and returns a clingo.SolveResult
+        """
+        user_input_ctl = Control(message_limit=0)
+        user_input_ctl.load(get_encoding("user-check.lp"))
+        user_input_ctl.add("".join(facts))
+        user_input_ctl.ground()
+        with user_input_ctl.solve(yield_=True) as handle:
+            unsat = [self.parse_user_input_unsat(s) for s in handle.model().symbols(shown=True)]
+        return unsat
+
     def main(self, control: Control, files: Sequence[str]) -> None:
         """
         Main function ran on call.
@@ -179,6 +218,11 @@ def main(self, control: Control, files: Sequence[str]) -> None:
         if self._show:
             print("\n".join(processed_facts))  # nocoverage
         else:
+            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)
             if self._solver == "clingo":

src/coomsuite/encodings/base/clingo/user.lp

@@ -0,0 +1,2 @@
+value(X,V) :- user_value(X,V).
+include(X) :- user_include(X).

src/coomsuite/encodings/base/defined.lp

@@ -24,3 +24,6 @@
 #defined number/2.
 
 #defined function/3.
+
+#defined user_include/1.
+#defined user_value/2.

src/coomsuite/encodings/base/fclingo/user.lp

@@ -0,0 +1,3 @@
+value(X,V)     :- user_value(X,V), type(X,T), discrete(T).
+&in{V..V} =: X :- user_value(X,V), type(X,T), integer(T).
+include(X)     :- user_include(X).

src/coomsuite/encodings/encoding-base-clingo.lp

@@ -3,3 +3,5 @@
 #include "base/structure.lp".
 #include "base/attributes.lp".
 #include "base/constraints.lp".
+
+#include "base/clingo/user.lp".

src/coomsuite/encodings/encoding-base-fclingo.lp

@@ -3,3 +3,5 @@
 #include "base/structure.lp".
 #include "base/attributes-fclingo.lp".
 #include "base/constraints-fclingo.lp".
+
+#include "base/fclingo/user.lp".

src/coomsuite/encodings/preprocess/defined.lp

@@ -20,3 +20,6 @@
 
 #defined coom_function/4.
 #defined coom_imply/3.
+
+#defined coom_user_include/1.
+#defined coom_user_value/2.

src/coomsuite/encodings/preprocess/output.lp

@@ -97,3 +97,10 @@ number(C,N) :- coom_number(C,N).
 
 #show constant/1.
 #show number/2.
+
+% User input
+user_include(X) :- coom_user_include(X).
+user_value(X,V) :- coom_user_value(X,V).
+
+#show user_include/1.
+#show user_value/2.

src/coomsuite/encodings/user-check.lp

@@ -0,0 +1,16 @@
+% Check that variables exist
+unsat("not exists",X) :- user_value(X,_), not type(X,_).
+unsat("not exists",X) :- user_include(X), not type(X,_).
+
+% Check variable type
+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
+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.

src/coomsuite/utils/__init__.py

@@ -8,10 +8,12 @@
 from antlr4 import CommonTokenStream, InputStream
 from clingo import Symbol
 
-from coomsuite.utils.parse_coom import ASPVisitor
+from coomsuite.utils.parse_coom import ASPModelVisitor, ASPUserInputVisitor
 
-from .coom_grammar.ModelLexer import ModelLexer
-from .coom_grammar.ModelParser import ModelParser
+from .coom_grammar.model.ModelLexer import ModelLexer
+from .coom_grammar.model.ModelParser import ModelParser
+from .coom_grammar.user.UserInputLexer import UserInputLexer
+from .coom_grammar.user.UserInputParser import UserInputParser
 
 # mypy: allow-untyped-calls
 
@@ -29,7 +31,7 @@ def get_encoding(file_name: str) -> str:  # nocoverage
         return str(file)
 
 
-def run_antlr4_visitor(coom_input_stream: InputStream) -> List[str]:
+def run_antlr4_visitor(coom_input_stream: InputStream, grammar: str) -> List[str]:
     """Runs the ANTLR4 Visitor.
 
     Args:
@@ -39,12 +41,20 @@ def run_antlr4_visitor(coom_input_stream: InputStream) -> List[str]:
         List[str]: The converted ASP instance
 
     """
-    lexer = ModelLexer(coom_input_stream)
-    stream = CommonTokenStream(lexer)
-    parser = ModelParser(stream)
-    tree = parser.root()
-    visitor = ASPVisitor()
-    visitor.visitRoot(tree)
+    if grammar == "model":
+        lexer = ModelLexer(coom_input_stream)
+        stream = CommonTokenStream(lexer)
+        parser = ModelParser(stream)
+        tree = parser.root()
+        visitor = ASPModelVisitor()
+        visitor.visitRoot(tree)
+    elif grammar == "user":
+        lexer = UserInputLexer(coom_input_stream)
+        stream = CommonTokenStream(lexer)
+        parser = UserInputParser(stream)
+        tree = parser.user_input()
+        visitor = ASPUserInputVisitor()
+        visitor.visitUser_input(tree)
     return visitor.output_asp
 
 

src/coomsuite/utils/coom_grammar/__init__.py

@@ -1,3 +1,3 @@
 """
-COOM model files
+COOM grammar files
 """

src/coomsuite/utils/coom_grammar/model/__init__.py

@@ -0,0 +1,3 @@
+"""
+COOM model grammar files
+"""

src/coomsuite/utils/coom_grammar/user/Base.g4

@@ -0,0 +1,65 @@
+grammar Base;
+
+@parser::header {}
+
+@parser::members {
+def wasNewline(self):
+    for index in reversed(range(self.getCurrentToken().tokenIndex)):
+        # stop on default channel
+        token = self.getTokenStream().get(index)
+        if token.channel == 0:
+            break
+
+        # if the token is blank and contains newline, we found it
+        if len(token.text) == 0:
+            continue
+        if token.text.startswith("\n") or token.text.startswith("\r"):
+            return True
+
+    return False
+}
+
+floating:
+	'-'? (FLOATING | INTEGER | '\u221e'); // == infinity symbol
+// define path expressions
+path: path_item ('.' path_item)*;
+path_item: name ('[' path_index ('..' path_index)? ']')?;
+path_index: INTEGER | ('last' ('-' INTEGER)?);
+
+name: NAME; // | FUNCTION | KEYWORD;
+stmt_end: ';' | {self.wasNewline()};
+
+NAME: (ALPHA ALPHANUMERIC*) | QUOTED_SINGLE | QUOTED_DOUBLE;
+
+formula_atom:
+	atom_true = 'true'
+	| atom_false = 'false'
+	| atom_num = floating
+	| atom_path = path;
+
+fragment ALPHANUMERIC: ALPHA | DIGIT;
+fragment ALPHA:
+	[_a-zA-Z$\u00A2-\u00A5\u00C0-\u00D6\u00D8-\u00F6\u00F8-\u02FF\u0370-\u037D\u037F-\u1FFF\u200C-\u200D\u2070-\u218F\u2C00-\u2FEF\u3001-\uD7FF\uF900-\uFDCF\uFDF0-\uFFFD]
+		;
+fragment DIGIT: [0-9];
+
+fragment QUOTED_SINGLE: '\'' (ESC | ~['\\\u0000-\u001F])* '\'';
+fragment QUOTED_DOUBLE: '"' (ESC | ~["\\\u0000-\u001F])* '"';
+
+fragment ESC: '\\' (["\\/bfnrt] | UNICODE);
+fragment UNICODE: 'u' HEX HEX HEX HEX;
+fragment HEX: [0-9a-fA-F];
+
+INTEGER: DIGIT+;
+FLOATING: DIGIT+ ('.' DIGIT+)?;
+
+// skip whitespaces, but get the newlines in a spearate channel
+
+NEWLINE: [\r\n]+ -> channel(HIDDEN);
+WHITESPACE: [ \t]+ -> skip;
+
+// allow java-like comments, direct them into the comment channel
+
+COMMENT: '//' ~[\n\r]* ( [\n\r] | EOF) -> channel(HIDDEN);
+MULTILINE_COMMENT:
+	'/*' (MULTILINE_COMMENT | .)*? ('*/' | EOF) -> channel(HIDDEN);

src/coomsuite/utils/coom_grammar/user/UserInput.g4

@@ -0,0 +1,15 @@
+/*
+ Grammar to define user input (customer product requirements)
+ */
+
+grammar UserInput;
+import Base;
+
+user_input: (input_block | input_operation)* EOF;
+
+input_block: 'blockinput' path '{' input_operation* '}';
+
+input_operation: set_value | add_instance;
+
+set_value: op = 'set' path '=' formula_atom;
+add_instance: op = 'add' INTEGER? path;