From 544a2e241962cabc8e5a738b274fa149bf3e25e8 Mon Sep 17 00:00:00 2001 From: Lute Lillo <65786380+lute47lillo@users.noreply.github.com> Date: Sat, 7 Oct 2023 10:35:42 -0500 Subject: [PATCH] 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 --- logs_error.txt | 57 ----------- noxfile.py | 4 - src/eclingo/config.py | 7 +- src/eclingo/control.py | 21 ++++- src/eclingo/grounder.py | 1 - src/eclingo/main.py | 37 +++++--- src/eclingo/parsing/parser.py | 17 ++-- .../parsing/transformers/parser_negations.py | 8 +- .../transformers/theory_parser_epistemic.py | 48 ++++------ src/eclingo/solver/candidate.py | 2 +- src/eclingo/solver/tester.py | 20 +--- src/eclingo/solver/world_view_builder.py | 94 ++++++++++--------- tests/_test_generator.py | 59 ------------ tests/prog/input/prog00.lp | 1 + tests/test_app.py | 29 ++++++ tests/test_generator_reification.py | 1 - tests/test_reification.py | 2 +- tests/test_reification5.py | 2 +- tests/test_transformers.py | 2 +- tests/test_util.py | 27 ++++++ 20 files changed, 188 insertions(+), 251 deletions(-) delete mode 100644 logs_error.txt delete mode 100644 tests/_test_generator.py create mode 100644 tests/prog/input/prog00.lp diff --git a/logs_error.txt b/logs_error.txt deleted file mode 100644 index 616b49c..0000000 --- a/logs_error.txt +++ /dev/null @@ -1,57 +0,0 @@ -LOGS of ERRORS while adapting tests to reification version. - - -Error 3: - - File: test_eclingo.py - - Test: TestEclingoAggregates - - Program: """{fact}. - :- not fact. - a :- not &k{ not a}. - b :- #sum{1:fact; 25:a} >= 24. - c :- &k{b}. - d :- &k{c}.""" - - Old solution: [[], ["&m{a}", "&k{b}", "&k{c}"]] - - Current solution given reification: [[], ["&m{a}"]] - - Hypothesis: Does the new implementation account for aggregates (?) - -Error 7 (SAME as error 1) - - File: test_app.py (input -> prog02.lp, output -> sol02.txt) - - Test: TestExamples.test_prog_g94 - - Program: - """ - a :- not &k{ b }. - b :- not &k{ a }. - """ - - Old solution: [[&k{a}],[&k{b}]] - - Current solution given reification: [[],[&k{a}],[&k{b}]] - - Hypothesis: CHECK LOG FOR ERROR 1 - - -Error 8: - - Lines - # self.assert_world_views( - # command, [elegible_path, input_path], output_path, external_call=False - # ) - - of TestExamples.test_eligible_g94 - - cause it to fail on sol_eligible2.txt, eligible2.lp - - - - - - diff --git a/noxfile.py b/noxfile.py index 53934de..c3427ec 100644 --- a/noxfile.py +++ b/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", diff --git a/src/eclingo/config.py b/src/eclingo/config.py index 8b33c9c..28aa274 100644 --- a/src/eclingo/config.py +++ b/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 diff --git a/src/eclingo/control.py b/src/eclingo/control.py index 285c917..5a40650 100644 --- a/src/eclingo/control.py +++ b/src/eclingo/control.py @@ -5,9 +5,25 @@ 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: @@ -15,9 +31,10 @@ def __init__(self, control, config=None): 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): diff --git a/src/eclingo/grounder.py b/src/eclingo/grounder.py index e86cf97..45f303c 100644 --- a/src/eclingo/grounder.py +++ b/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() diff --git a/src/eclingo/main.py b/src/eclingo/main.py index d57bad8..7234294 100644 --- a/src/eclingo/main.py +++ b/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="", ) + options.add( + group=group, + option="output-e", + description="Rewrites the program using reification", + parser=self._parse_string(self.config, "eclingo_rewritten"), + argument="", + ) + 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") diff --git a/src/eclingo/parsing/parser.py b/src/eclingo/parsing/parser.py index 958769d..56ccf4f 100644 --- a/src/eclingo/parsing/parser.py +++ b/src/eclingo/parsing/parser.py @@ -63,13 +63,15 @@ def __init__( begin=Position(filename="", line=1, column=1), end=Position(filename="", 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 ( diff --git a/src/eclingo/parsing/transformers/parser_negations.py b/src/eclingo/parsing/transformers/parser_negations.py index 1ed9e27..25c7988 100644 --- a/src/eclingo/parsing/transformers/parser_negations.py +++ b/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: diff --git a/src/eclingo/parsing/transformers/theory_parser_epistemic.py b/src/eclingo/parsing/transformers/theory_parser_epistemic.py index 0321e23..0dcf529 100644 --- a/src/eclingo/parsing/transformers/theory_parser_epistemic.py +++ b/src/eclingo/parsing/transformers/theory_parser_epistemic.py @@ -26,19 +26,18 @@ class ApplyToEpistemicAtomsElementsTransformer(Transformer): - def __init__(self, fun, reification, update_fun=None): + def __init__(self, fun, update_fun=None): self.fun = fun self.update_fun = update_fun - self.reification = reification def visit_TheoryAtom(self, atom, loc="body"): if atom.term.name == "k" and not atom.term.arguments: if self.update_fun is None: - new_elements = [self.fun(self.reification, e) for e in atom.elements] + new_elements = [self.fun(e) for e in atom.elements] else: new_elements = [] for element in atom.elements: - new_element, update = self.fun(self.reification, element) + new_element, update = self.fun(element) new_elements.append(new_element) self.update_fun(update) atom.elements = new_elements @@ -48,24 +47,23 @@ def visit_TheoryAtom(self, atom, loc="body"): #################################################################################### -def _theory_term_to_literal_adapter(reification: bool, element: AST) -> AST: +def _theory_term_to_literal_adapter(element: AST) -> AST: assert len(element.terms) == 1 new_element = copy(element) new_element.terms[0] = theory_term_to_literal(element.terms[0]) return new_element -def parse_epistemic_literals_elements(rule, reification): - return ApplyToEpistemicAtomsElementsTransformer( - _theory_term_to_literal_adapter, reification=True - )(rule) +def parse_epistemic_literals_elements(rule): + return ApplyToEpistemicAtomsElementsTransformer(_theory_term_to_literal_adapter)( + rule + ) #################################################################################### def make_strong_negation_auxiliar_in_epistemic_literals( - use_reification: bool, stm: Iterable[ast.AST], ) -> Tuple[Iterable[ast.AST], SnReplacementType]: """ @@ -79,7 +77,7 @@ def make_strong_negation_auxiliar_in_epistemic_literals( """ replacement: SnReplacementType = set() trn = ApplyToEpistemicAtomsElementsTransformer( - make_strong_negations_auxiliar, use_reification, replacement.update + make_strong_negations_auxiliar, replacement.update ) stm = trn.visit_sequence(cast(ASTSequence, stm)) return (stm, replacement) @@ -89,7 +87,6 @@ def make_strong_negation_auxiliar_in_epistemic_literals( def make_default_negation_auxiliar_in_epistemic_literals( - use_reification: bool, stm: Iterable[ast.AST], ) -> Tuple[Iterable[ast.AST], Iterable[ast.AST]]: """ @@ -103,7 +100,6 @@ def make_default_negation_auxiliar_in_epistemic_literals( replacement: Set[ast.AST] = set() trn = ApplyToEpistemicAtomsElementsTransformer( make_default_negation_auxiliar, - use_reification, lambda x: replacement.add(x) if x is not None else None, ) stm = trn.visit_sequence(cast(ASTSequence, stm)) @@ -126,8 +122,7 @@ def build_guard(body): class EpistemicLiteralNegationsToAuxiliarTransformer(Transformer): - def __init__(self, use_reification, user_prefix="u"): - self.reification = use_reification + def __init__(self, user_prefix="u"): self.user_prefix = user_prefix self.sn_replacement = set() self.aux_rules = [] @@ -136,11 +131,11 @@ def visit_Rule(self, rule): head = rule.head body = rule.body body, self.sn_replacement = make_strong_negation_auxiliar_in_epistemic_literals( - self.reification, body + body ) guard = build_guard(body) body, not_replacement = make_default_negation_auxiliar_in_epistemic_literals( - self.reification, body + body ) self.aux_rules.extend( default_negation_auxiliary_rule_replacement( @@ -154,7 +149,7 @@ def visit_Rule(self, rule): def replace_negations_by_auxiliary_atoms_in_epistemic_literals( - stm: ast.AST, use_reification: bool, user_prefix: str = "u" + stm: ast.AST, user_prefix: str = "u" ) -> Tuple[List[ast.AST], SnReplacementType]: """ Replaces strong and default negations by an auxiliary atom inside epistemic literals of the rule. @@ -166,7 +161,7 @@ def replace_negations_by_auxiliary_atoms_in_epistemic_literals( - the second element is a list of rules relating the auxiliary atoms used to replace default negation with their original literals - the third element contains the information about the replacements corresponding to strong negation """ - trn = EpistemicLiteralNegationsToAuxiliarTransformer(use_reification, user_prefix) + trn = EpistemicLiteralNegationsToAuxiliarTransformer(user_prefix) rule = trn.visit(stm) return ([rule] + trn.aux_rules, trn.sn_replacement) @@ -190,11 +185,10 @@ def ensure_literals(stms): class EClingoTransformer(Transformer): - def __init__(self, use_reification, k_prefix="k"): + def __init__(self, k_prefix="k"): self.k_prefix = k_prefix self.epistemic_replacements = [] self.aux_rules = [] - self.reification = use_reification def visit_Rule(self, x, loc="body"): head = ensure_literals(self.visit(x.head, loc="head")) @@ -227,24 +221,20 @@ def visit_TheoryAtom(self, atom, loc="body"): def _replace_epistemic_literals_by_auxiliary_atoms( - stm: ast.AST, use_reification: bool, k_prefix: str = "k" + stm: ast.AST, k_prefix: str = "k" ) -> List[ast.AST]: - trans = EClingoTransformer(use_reification, k_prefix) + trans = EClingoTransformer(k_prefix) rule = trans(stm) rules = [rule] + trans.aux_rules return rules def replace_epistemic_literals_by_auxiliary_atoms( - stms: Iterable[ast.AST], use_reification: bool, k_prefix: str = "k" + stms: Iterable[ast.AST], k_prefix: str = "k" ) -> List[ast.AST]: rules = [] for stm in stms: - rules.extend( - _replace_epistemic_literals_by_auxiliary_atoms( - stm, use_reification, k_prefix - ) - ) + rules.extend(_replace_epistemic_literals_by_auxiliary_atoms(stm, k_prefix)) return rules diff --git a/src/eclingo/solver/candidate.py b/src/eclingo/solver/candidate.py index be6b20e..7247242 100644 --- a/src/eclingo/solver/candidate.py +++ b/src/eclingo/solver/candidate.py @@ -1,4 +1,4 @@ -from typing import List, NamedTuple, Sequence +from typing import NamedTuple, Sequence from clingo import Symbol diff --git a/src/eclingo/solver/tester.py b/src/eclingo/solver/tester.py index ab2f9cf..af8f8bf 100644 --- a/src/eclingo/solver/tester.py +++ b/src/eclingo/solver/tester.py @@ -43,13 +43,6 @@ def __init__(self, config: AppConfig, reified_program: str): hold(L) :- k(A), output(k(A), B), literal_tuple(B, L). :- hold(L) , not k(A), output(k(A), B), literal_tuple(B, L). - - %%symbolic_atom(SA, A) :- output(SA,LT), #count{LL : literal_tuple(LT, LL)} = 1, literal_tuple(LT, A). - %%epistemic_atom_info(SKA, KA, SA, A) :- symbolic_atom(SA, A), SKA=k(SA), symbolic_atom(SKA, KA). - %%show_statement(SA) :- symbolic_atom(show_statement(SA), _). - %%hold(L) : show_statment(SA), output(k(A), B), literal_tuple(B, L). - %% #project hold(L) : output(k(A), B), literal_tuple(B, L). - %% #project hold(L) : show_statment(SA), output(k(A), B), literal_tuple(B, L). """ self.control.add("base", [], self.reified_program) @@ -77,20 +70,13 @@ def __call__(self, candidate: Candidate) -> bool: literal = literal.arguments[0] candidate_neg.append(literal) - for literal in candidate.extra_assumptions.neg: - assumption = (literal, False) - candidate_assumptions.append(assumption) + # for literal in candidate.extra_assumptions.neg: + # assumption = (literal, False) + # candidate_assumptions.append(assumption) cast(Configuration, self.control.configuration.solve).models = 0 cast(Configuration, self.control.configuration.solve).project = "no" - # print("\nTESTER") - # print("Candidate assumptions:\n", candidate_assumptions) - # print( - # "Candidate assumptions:\n", - # "\n".join(str((str(a), v)) for a, v in candidate_assumptions), - # ) - with cast( clingo.SolveHandle, self.control.solve(yield_=True, assumptions=candidate_assumptions), diff --git a/src/eclingo/solver/world_view_builder.py b/src/eclingo/solver/world_view_builder.py index 1eac782..44780f4 100644 --- a/src/eclingo/solver/world_view_builder.py +++ b/src/eclingo/solver/world_view_builder.py @@ -44,8 +44,6 @@ def generate_k_symbol(self, epistemic_literal): for args in literal_symbol.arguments: arguments.append(args) - # print("The args: ", literal_symbol.arguments[0]) - new_symbol = Function(literal_symbol.name, arguments, is_explicit) literal = Literal(new_symbol, sign) @@ -68,20 +66,14 @@ def generate_m_symbol(self, epistemic_literal): def world_view_from_candidate(self, candidate: Candidate): epistemic_literals = [] k_symbols = [] - epistemic_show_literals = [] for epistemic_literal in candidate.pos: - # print("\n The epistemic literal POS: ", epistemic_literal) show_literal = self.generate_k_symbol(epistemic_literal) if show_literal is not None: epistemic_literals.append(show_literal) k_symbols.append(show_literal.objective_literal) - if epistemic_literal in self.show_statements: - epistemic_show_literals.append(show_literal) - for epistemic_literal in candidate.neg: - # print("\n The epistemic literal NEG: ", epistemic_literal) show_literal = self.generate_m_symbol(epistemic_literal) if ( @@ -90,12 +82,6 @@ def world_view_from_candidate(self, candidate: Candidate): ): epistemic_literals.append(show_literal) - if epistemic_literal in self.show_statements: - epistemic_show_literals.append(show_literal) - - if epistemic_show_literals: - return WorldView(epistemic_show_literals) - return WorldView(epistemic_literals) @@ -108,10 +94,35 @@ def __init__(self, reified_program): self.show_statements: Sequence[Symbol] = [] program_meta_encoding = """ + conjunction(B) :- literal_tuple(B), + hold(L) : literal_tuple(B, L), L > 0; + not hold(L) : literal_tuple(B, -L), L > 0. + + body(normal(B)) :- rule(_, normal(B)), conjunction (B). + + body(sum(B, G)) :- rule (_sum(B,G)), + #sum { + W,L : hold(L), weighted_literal_tuple(B, L,W), L>0; + W,L : not hold(L), weighted_literal_tuple(B, -L,W), L>0} >= G. + + hold(A) : atom_tuple(H,A) :- rule(disjunction(H), B), body(B). + + {hold(A) : atom_tuple(H,A)} :- rule(choice(H), B), body(B). + + u(A) :- output(u(A), B), conjunction(B). + not1(A) :- output(not1(A), B), conjunction(B). + not2(A) :- output(not2(A), B), conjunction(B). + symbolic_atom(SA, A) :- output(SA,LT), #count{LL : literal_tuple(LT, LL)} = 1, literal_tuple(LT, A). + epistemic_atom_info(SKA, KA, SA, A) :- symbolic_atom(SA, A), SKA=k(SA), symbolic_atom(SKA, KA). show_statement(SA) :- symbolic_atom(show_statement(SA), _). + not1(u(SA)) :- show_statement(SA), not u(SA). + {k(A)} :- output(k(A), _). + + hold(L) :- k(A), output(k(A), B), literal_tuple(B, L). + :- hold(L) , not k(A), output(k(A), B), literal_tuple(B, L). """ self.control.add("base", [], self.reified_program) @@ -140,6 +151,7 @@ def world_view_from_candidate(self, candidate: Candidate): cast(Configuration, self.control.configuration.solve).models = 0 cast(Configuration, self.control.configuration.solve).project = "no" + cast(Configuration, self.control.configuration.solve).enum_mode = "cautious" with cast( SolveHandle, @@ -150,41 +162,31 @@ def world_view_from_candidate(self, candidate: Candidate): pass assert model is not None - self.epistemic_show_statements(model, cand_show) + ret = self.epistemic_show_statements(model) + if ret is not None: + candidate = ret - return super().world_view_from_candidate( - Candidate(candidate_pos, candidate_neg) - ) + return super().world_view_from_candidate(candidate) """ Check in model for show_statement(X) facts for all X atoms. """ - def epistemic_show_statements(self, model, candidates_show): - show_name: str = "show_statement" - - for atom in candidates_show: - show_arguments: Sequence[Symbol] = [] - atom_arguments: Sequence[Symbol] = [] - - if ( - atom.name == "not1" or atom.name == "not2" - ): # Check if it is a negative atom - atom_show = atom.arguments[0].arguments[0] - else: - atom_show = atom.arguments[0] - - # Check for arguments of atom - if atom_show.arguments: - for args in atom_show.arguments: - atom_arguments.append(args) - - show_arguments.append( - Function(atom_show.name, atom_arguments, atom.arguments[0].positive) - ) - - show_stm = Function(show_name, show_arguments, True) - - k_atom = Function("k", [atom], atom.arguments[0].positive) - if model.contains(show_stm) and k_atom not in self.show_statements: - self.show_statements.append(k_atom) + def epistemic_show_statements(self, model): + candidate_pos = [] + candidate_neg = [] + with_show_statement = False + for atom in model.symbols(atoms=True): + if atom.name == "show_statement": + with_show_statement = True + uatom = Function("u", [atom.arguments[0]]) + katom = Function("k", [uatom]) + natom = Function("not1", [uatom]) + knatom = Function("k", [natom]) + if model.contains(uatom): + candidate_pos.append(katom) + elif not model.contains(natom): + candidate_neg.append(knatom) + if with_show_statement: + return Candidate(candidate_pos, candidate_neg) + return None diff --git a/tests/_test_generator.py b/tests/_test_generator.py deleted file mode 100644 index 9bcaa81..0000000 --- a/tests/_test_generator.py +++ /dev/null @@ -1,59 +0,0 @@ -import unittest - -import clingo -from clingo.symbol import Function - -import eclingo as _eclingo -from eclingo.config import AppConfig -from eclingo.control import Control -from eclingo.solver.candidate import Candidate -from eclingo.solver.generator import CandidateGenerator - - -class CandidateGeneratorTest(Control): - def generator_solve(self): - self.prepare_solver() - - candidates = [] - for candidate in self.solver.generate_candidates(): - candidates.append(candidate) - return candidates - - -""" Helper function to generate candidates for a given program """ - - -def generate(program): - # Initialize - control = clingo.Control(message_limit=0) - control.configuration.solve.models = 0 - config = _eclingo.config.AppConfig() - config.eclingo_semantics = "c19-1" - - control.add_program(program) - control.ground([("base", [])]) - - candidate_generator = CandidateGenerator(config, control) - - candidates = list(candidate_generator()) - - return sorted(candidates) - - -class TestCase(unittest.TestCase): - def assert_models(self, models, expected): - self.assertEqual(models, expected) - - -class TestEclingoGenerator(TestCase): - def test_generator01(self): - self.assert_models( - generate("u_b :- k_u_a. u_a. {k_u_a}."), - [ - Candidate(pos=[], neg=[Function("k_u_a", [], True)]), - Candidate(pos=[Function("k_u_a", [], True)], neg=[]), - ], - ) - - # def test_generator02(self): - # self.assert_models(generate("u_a. u_b :- k_u_a. u_c :- k_u_b."), [Candidate(pos=[Function('k_u_a', [], True)], neg=[Function('k_u_b', [], True)]), Candidate(pos=[Function('k_u_a', [], True), Function('k_u_b', [], True)], neg=[])]) diff --git a/tests/prog/input/prog00.lp b/tests/prog/input/prog00.lp new file mode 100644 index 0000000..fa41827 --- /dev/null +++ b/tests/prog/input/prog00.lp @@ -0,0 +1 @@ +{a}. b :- &k{a}. diff --git a/tests/test_app.py b/tests/test_app.py index 66e514b..08a46a1 100644 --- a/tests/test_app.py +++ b/tests/test_app.py @@ -147,3 +147,32 @@ def test_yale_g94(self): command, [yale_path, input_path], output_path, external_call=False ) self.assert_world_views(command, [yale_path, input_path], output_path) + + +class PrintRewrittenTestCase(unittest.TestCase): + def test_print_rewritten(self): + command = 'echo "{a}. b :- &k{a}." | eclingo --output-e=rewritten' + process = subprocess.Popen( + command, stdout=subprocess.PIPE, stderr=subprocess.PIPE, shell=True + ) + stdout, stderr = process.communicate() + output = stdout.decode("utf-8") + self.assertEqual( + output.strip(), + """\ +{ u(a) }. +u(b) :- k(u(a)). +{ k(u(a)) } :- u(a).""", + ) + + def test_print_rewrittenpatch(self): + path = os.path.dirname(os.path.realpath(__file__)) + input_path = os.path.join(path, INPUT_PROG_PATH) + input_path = os.path.join(input_path, f"prog00.lp") + command = ["eclingo", input_path, "--output-e=rewritten"] + with ( + contextlib.redirect_stdout(io.StringIO()) as stdout, + patch.object(sys, "argv", command), + ): + eclingo_main() + output = stdout.getvalue() diff --git a/tests/test_generator_reification.py b/tests/test_generator_reification.py index 2df0ca8..bcbb1b5 100644 --- a/tests/test_generator_reification.py +++ b/tests/test_generator_reification.py @@ -21,7 +21,6 @@ def generate(program): candidate_generator = GeneratorReification(config, program) candidates = list(candidate_generator()) - # print(sorted(candidates)) return sorted(candidates) diff --git a/tests/test_reification.py b/tests/test_reification.py index 1cf1895..604d9e9 100644 --- a/tests/test_reification.py +++ b/tests/test_reification.py @@ -27,7 +27,7 @@ def parse_program(stm, parameters=[], name="base"): ret.append, parameters, name, - config=AppConfig(semantics="c19-1", verbose=0, use_reification=True), + config=AppConfig(semantics="c19-1", verbose=0), ) return flatten(ret) diff --git a/tests/test_reification5.py b/tests/test_reification5.py index 3277331..e7e465b 100644 --- a/tests/test_reification5.py +++ b/tests/test_reification5.py @@ -31,7 +31,7 @@ def parse_program(stm, parameters=[], name="base"): ret.append, parameters, name, - config=AppConfig(semantics="c19-1", verbose=0, use_reification=True), + config=AppConfig(semantics="c19-1", verbose=0), ) return flatten(ret) diff --git a/tests/test_transformers.py b/tests/test_transformers.py index d57e786..c4c5d47 100644 --- a/tests/test_transformers.py +++ b/tests/test_transformers.py @@ -66,7 +66,7 @@ def test_epistemic_atom(self): else: self.assertEqual(ast_type(term), _ast.ASTType.SymbolicTerm) - result = _parse_epistemic_literals_elements(statement, reification=False) + result = _parse_epistemic_literals_elements(statement) self.assertEqual(len(result.elements), 1) element = result.elements[0] self.assertEqual(ast_type(element), _ast.ASTType.TheoryAtomElement) diff --git a/tests/test_util.py b/tests/test_util.py index b6fd5c2..1db4eaa 100644 --- a/tests/test_util.py +++ b/tests/test_util.py @@ -1,6 +1,26 @@ from unittest import TestCase +import clingo +from clingox.testing.ast import ASTTestCase + from eclingo import util +from eclingo.config import AppConfig +from eclingo.control import Control + +# python -m unittest tests.test_util.TestRewritten + + +class TestCase(ASTTestCase): + def assert_equal_program_rewritten(self, program, expected): + control = clingo.Control(message_limit=0) + config = AppConfig(eclingo_rewritten="rewritten") + eclingo_control = Control(control, config) + eclingo_control.add_program(program) + + parsed_prg = [] + for i in range(1, len(eclingo_control.rewritten_program)): + parsed_prg.append(str(eclingo_control.rewritten_program[i])) + self.assertListEqual(parsed_prg, expected) class TestPartition(TestCase): @@ -55,3 +75,10 @@ def test_size_more(self): ), ([2, 4, 6, 8, 10, 12], [7], [9], [11], [13], [1, 3, 5]), ) + + +class TestRewritten(TestCase): + def test_rewritten(self): + self.assert_equal_program_rewritten( + "a. b :- &k{a}.", ["u(a).", "u(b) :- k(u(a)).", "{ k(u(a)) } :- u(a)."] + )