Lute/fixing branches (#66)

* Add output-e=rewritten & Remove reification AppConfig

* Return only reify program if using --option=reify

* grouping eclingo options

* fix UNSATISFIABLE

* show fixed

* Fixing branches (Output rewritten, show stms)

---------

Co-authored-by: jorgefandinno <[email protected]>

noxfile.py

@@ -49,15 +49,11 @@ def tests(session: nox.Session):
         "tests/test_reification3.py",
         "tests/test_reification4.py",
         "tests/test_reification5.py",
-        # "tests/test_app.py",
         "tests/test_eclingo.py",
-        # "tests/test_eclingo_examples.py",
         # "tests/test_grounder.py",
         "tests/test_generator_reification.py",
         "tests/test_literals.py",
-        # "tests/test_internal_control_ground_program.py",
         "tests/test_parsing.py",
-        # "tests/test_show.py",
         "tests/test_solver_reification.py",
         "tests/test_worldview_builder_reification.py",
         "tests/test_tester_reification.py",

src/eclingo/config.py

@@ -3,7 +3,10 @@ class AppConfig(object):
     Class for application specific options.
     """
 
-    def __init__(self, semantics="g94", verbose=0, use_reification=True):
+    def __init__(
+        self, semantics="g94", verbose=0, eclingo_rewritten="no", rewritten_program=[]
+    ):
         self.eclingo_verbose = verbose
         self.eclingo_semantics = semantics
-        self.eclingo_reification = use_reification
+        self.eclingo_rewritten = eclingo_rewritten
+        self.rewritten_program = rewritten_program

src/eclingo/control.py

@@ -5,19 +5,36 @@
 
 from eclingo.config import AppConfig
 from eclingo.grounder import Grounder
+from eclingo.parsing import parser
 from eclingo.solver import SolverReification
 
 
+def parse_program(stm, parameters=None, name="base"):
+    """Helping function to parse program for flag: --output-e=rewritten"""
+    if parameters is None:
+        parameters = []
+    ret = []
+    parser.parse_program(
+        stm,
+        ret.append,
+        parameters,
+        name,
+        config=AppConfig(semantics="c19-1", verbose=0),
+    )
+    return ret
+
+
 class Control(object):
     def __init__(self, control, config=None):
         # if control is not None:
         self.project = control.configuration.solve.project
         self.max_models = int(control.configuration.solve.models)
         control.configuration.solve.project = "auto,3"
         control.configuration.solve.models = 0
+        self.rewritten_program = None
         self.control = control
         if config is None:
-            config = AppConfig(semantics="c19-1", use_reification=True)
+            config = AppConfig(semantics="c19-1")
         self.config = config
 
         if self.max_models == 0:
@@ -29,6 +46,8 @@ def __init__(self, control, config=None):
         self.solver = None
 
     def add_program(self, program):
+        if self.config.eclingo_rewritten == "rewritten":
+            self.rewritten_program = parse_program(program)
         self.grounder.add_program(program)
 
     def load(self, input_path):

src/eclingo/grounder.py

@@ -16,7 +16,6 @@ class Grounder:
     def __init__(self, control: Control, config: AppConfig = AppConfig()):
         self.control = control
         self.config = config
-        self.reification = self.config.eclingo_reification
         self.facts: List[Symbol] = []
         self.reified_facts: str
         self.atom_to_symbol: Dict[int, Symbol] = dict()

src/eclingo/main.py

@@ -42,23 +42,22 @@ def register_options(self, options) -> None:
         """
         group = "Eclingo Options"
 
-        options.add_flag(
-            group=group,
-            option="reification",
-            description="Applies reification to the program",
-            target=reification_flag,
-        )
-
-        group = "Semantics Options"
-
         options.add(
             group=group,
             option="semantics",
-            description="Sets Eclingo to use specified semantics",
+            description="Sets eclingo to use an specified semantics",
             parser=self._parse_string(self.config, "eclingo_semantics"),
             argument="<ELP_semantics>",
         )
 
+        options.add(
+            group=group,
+            option="output-e",
+            description="Rewrites the program using reification",
+            parser=self._parse_string(self.config, "eclingo_rewritten"),
+            argument="<rewritten>",
+        )
+
     def _read(self, path):
         if path == "-":
             return sys.stdin.read()
@@ -80,18 +79,28 @@ def main(self, control: Control, files: Sequence[str]) -> None:
         for path in files:
             eclingo_control.add_program(self._read(path))
 
+        if self.config.eclingo_rewritten == "rewritten":
+            for stm in eclingo_control.rewritten_program[1:]:
+                sys.stdout.write(str(stm))
+                sys.stdout.write("\n")
+            return
+
         eclingo_control.ground()
+
+        # Command check
+        if "--output=reify" in set(arg.replace(" ", "") for arg in sys.argv):
+            return
+
         eclingo_control.preprocess()
         eclingo_control.prepare_solver()
 
         sys.stdout.write("Solving...\n")
-        wv_number = 1
-        for world_view in eclingo_control.solve():
+        wv_number = 0
+        for wv_number, world_view in enumerate(eclingo_control.solve(), 1):
             sys.stdout.write("World view: %d\n" % wv_number)
             sys.stdout.write(str(world_view))
             sys.stdout.write("\n")
-            wv_number += 1
-        if wv_number > 1:
+        if wv_number >= 1:
             sys.stdout.write("SATISFIABLE\n")
         else:
             sys.stdout.write("UNSATISFIABLE\n")

src/eclingo/parsing/parser.py

@@ -63,13 +63,15 @@ def __init__(
             begin=Position(filename="<string>", line=1, column=1),
             end=Position(filename="<string>", line=1, column=1),
         )
+        self.config = config
         self.program = program
         self.callback = callback
         self.parameters = [ast.Id(self.initial_location, x) for x in parameters]
         self.name = name
         self.strong_negation_replacements = StrongNegationReplacement()
-        self.semantics = config.eclingo_semantics
-        self.reification = config.eclingo_reification
+        self.semantics = self.config.eclingo_semantics
+        self.rewritten_prg = self.config.rewritten_program
+        self.rewritten = self.config.eclingo_rewritten
         self.theory_parser = parse_theory(_ProgramParser.eclingo_theory)
 
     def __call__(self) -> None:
@@ -81,7 +83,7 @@ def __call__(self) -> None:
 
     def _parse_statement(self, statement: ast.AST) -> None:
         statement = self.theory_parser(statement)
-        statement = parse_epistemic_literals_elements(statement, self.reification)
+        statement = parse_epistemic_literals_elements(statement)
 
         statement = reify_symbolic_atoms(statement, U_NAME, reify_strong_negation=True)
 
@@ -111,14 +113,9 @@ def _parse_rule(self, rule: ast.AST) -> Iterable[ast.AST]:
         (
             rules,
             sn_replacement,
-        ) = replace_negations_by_auxiliary_atoms_in_epistemic_literals(
-            rule, self.reification
-        )
+        ) = replace_negations_by_auxiliary_atoms_in_epistemic_literals(rule)
         self.strong_negation_replacements.update(sn_replacement)
-
-        return replace_epistemic_literals_by_auxiliary_atoms(
-            rules, self.reification, "k"
-        )
+        return replace_epistemic_literals_by_auxiliary_atoms(rules, "k")
 
     def _parse_program_statement(self, statement: ast.AST) -> List[ast.AST]:
         if (

src/eclingo/parsing/transformers/parser_negations.py

@@ -71,9 +71,7 @@ def simplify_strong_negations(stm: ast.AST) -> ast.AST:
     return SimplifyStrongNegationsTransformer().visit(stm)
 
 
-def make_strong_negations_auxiliar(
-    reification: bool, stm: ast.AST
-) -> Tuple[ast.AST, SnReplacementType]:
+def make_strong_negations_auxiliar(stm: ast.AST) -> Tuple[ast.AST, SnReplacementType]:
     """
     Replaces strong negation by an auxiliary atom.
     Returns a pair:
@@ -110,9 +108,7 @@ def _make_default_negation_auxiliar(
 NotReplacementType = Optional[Tuple[ast.AST, ast.AST]]
 
 
-def make_default_negation_auxiliar(
-    use_reification: bool, stm: ast.AST
-) -> Tuple[ast.AST, NotReplacementType]:
+def make_default_negation_auxiliar(stm: ast.AST) -> Tuple[ast.AST, NotReplacementType]:
     """
     Replaces default negation by an auxiliary atom.
     Returns a pair: