diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 0493bba..f221306 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -2,6 +2,7 @@ #include +#include #include namespace anthem @@ -14,19 +15,19 @@ namespace anthem //////////////////////////////////////////////////////////////////////////////////////////////////// // Determines whether a term is a specific variable -bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration &variableDeclaration) +bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration *variableDeclaration) { if (!term.is()) return false; - return term.get().declaration == &variableDeclaration; + return term.get().declaration == variableDeclaration; } //////////////////////////////////////////////////////////////////////////////////////////////////// // Extracts the term t if the given formula is of the form “X = t” and X matches the given variable // The input formula is not usable if a term is returned -std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration) +std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration *variableDeclaration) { if (!formula.is()) return std::experimental::nullopt; @@ -50,16 +51,16 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula // Replaces all occurrences of a variable in a given term with another term struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Variable &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &) + static void accept(ast::Variable &variable, ast::Term &term, const ast::VariableDeclaration *original, const ast::Term &replacement) { - // TODO: reimplement - //if (variable.name == variableToReplace.name) - // term = ast::deepCopy(replacementTerm); + if (variable.declaration == original) + // No dangling variables can result from this operation, and hence, fixing them is not necessary + term = ast::prepareCopy(replacement); } // Ignore all other types of expressions template - static void accept(T &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &) + static void accept(T &, ast::Term &, const ast::VariableDeclaration *, const ast::Term &) { } }; @@ -69,27 +70,27 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &replacement) { - comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variableDeclaration, term); - comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, variableDeclaration, term); + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); } - static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) + static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &term) { - in.element.accept(ReplaceVariableInTermVisitor(), in.element, variableDeclaration, term); - in.set.accept(ReplaceVariableInTermVisitor(), in.set, variableDeclaration, term); + in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, term); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, term); } - static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term) + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &replacement) { for (auto &argument : predicate.arguments) - argument.accept(ReplaceVariableInTermVisitor(), argument, variableDeclaration, term); + argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); } // Ignore all other types of expressions template - static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, const ast::Term &) + static void accept(T &, ast::Formula &, const ast::VariableDeclaration *, const ast::Term &) { } }; @@ -109,7 +110,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) // Simplify formulas of type “exists X (X = t and F(X))” to “F(t)” for (auto i = exists.variables.begin(); i != exists.variables.end();) { - auto &variableDeclaration = *i->get(); + const auto *variableDeclaration = i->get(); bool wasVariableReplaced = false; diff --git a/tests/TestSimplification.cpp b/tests/TestSimplification.cpp index 0ec2f5c..8748c72 100644 --- a/tests/TestSimplification.cpp +++ b/tests/TestSimplification.cpp @@ -8,14 +8,14 @@ //////////////////////////////////////////////////////////////////////////////////////////////////// -/*TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") +TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") { std::stringstream input; std::stringstream output; std::stringstream errors; anthem::output::Logger logger(output, errors); - anthem::Context context = {logger, {}}; + anthem::Context context(std::move(logger)); context.simplify = true; context.complete = false; @@ -24,7 +24,7 @@ input << ":- in(I, S), in(J, S), in(I + J, S)."; anthem::translate("input", input, context); - CHECK(output.str() == "((in(I, S) and in(J, S) and exists X5 (X5 in (I + J) and in(X5, S))) -> #false)\n"); + CHECK(output.str() == "((in(U1, U2) and in(U3, U2) and exists X1 (X1 in (U1 + U3) and in(X1, U2))) -> #false)\n"); } SECTION("example 2") @@ -32,7 +32,7 @@ input << "covered(I) :- in(I, S)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 = I and in(I, S)) -> covered(V1))\n"); + CHECK(output.str() == "((V1 = U1 and in(U1, U2)) -> covered(V1))\n"); } SECTION("example 3") @@ -40,7 +40,7 @@ input << ":- not covered(I), I = 1..n."; anthem::translate("input", input, context); - CHECK(output.str() == "((not covered(I) and I in 1..n) -> #false)\n"); + CHECK(output.str() == "((not covered(U1) and U1 in 1..n) -> #false)\n"); } SECTION("comparisons") @@ -48,7 +48,6 @@ input << ":- M > N."; anthem::translate("input", input, context); - CHECK(output.str() == "(M > N -> #false)\n"); + CHECK(output.str() == "(U1 > U2 -> #false)\n"); } } -*/