diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index 6ddadf2..8f62d90 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -34,6 +34,9 @@ class VariableStack std::vector collectFreeVariables(const ast::Formula &formula); std::vector collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack); +bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs); +void collectPredicates(const ast::Formula &formula, std::vector &predicates); + //////////////////////////////////////////////////////////////////////////////////////////////////// } diff --git a/src/anthem/ASTUtils.cpp b/src/anthem/ASTUtils.cpp index ddb34e0..af8a43d 100644 --- a/src/anthem/ASTUtils.cpp +++ b/src/anthem/ASTUtils.cpp @@ -194,5 +194,44 @@ std::vector collectFreeVariables(const ast::Formula &formula, ast //////////////////////////////////////////////////////////////////////////////////////////////////// +struct CollectPredicatesVisitor : public RecursiveFormulaVisitor +{ + static void accept(const ast::Predicate &predicate, const ast::Formula &, std::vector &predicates) + { + const auto predicateMatches = + [&predicate](const auto *otherPredicate) + { + return matches(predicate, *otherPredicate); + }; + + if (std::find_if(predicates.cbegin(), predicates.cend(), predicateMatches) == predicates.cend()) + predicates.emplace_back(&predicate); + } + + // Ignore all other types of expressions + template + static void accept(const T &, const ast::Formula &, std::vector &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs) +{ + return (lhs.name == rhs.name && lhs.arity() == rhs.arity()); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// TODO: remove const_cast +void collectPredicates(const ast::Formula &formula, std::vector &predicates) +{ + auto &formulaMutable = const_cast(formula); + formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } } diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp index 4adce41..6f90437 100644 --- a/src/anthem/Completion.cpp +++ b/src/anthem/Completion.cpp @@ -2,6 +2,7 @@ #include #include +#include namespace anthem { @@ -12,163 +13,133 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -// Checks that two matching predicates (same name, same arity) have the same arguments -void checkMatchingPredicates(const ast::Term &lhs, const ast::Term &rhs) +// Copies the parameters of a predicate +std::vector copyParameters(const ast::Predicate &predicate) { - if (!lhs.is() || !rhs.is()) - throw std::runtime_error("cannot preform completion, only variables supported in predicates currently"); + std::vector parameters; + parameters.reserve(predicate.arity()); - if (lhs.get().name != rhs.get().name) - throw std::runtime_error("cannot perform completion, inconsistent predicate argument naming"); + for (const auto ¶meter : predicate.arguments) + { + assert(parameter.is()); + parameters.emplace_back(ast::deepCopy(parameter.get())); + } + + return parameters; } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completePredicate(const ast::Predicate &predicate, std::vector &formulas, std::size_t &formulaIndex) +// Builds the conjunction within the completed formula for a given predicate +ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const std::vector ¶meters, const std::vector &formulas) { - // Check that predicate is in normal form - for (auto i = formulaIndex; i < formulas.size(); i++) - { - auto &formula = formulas[i]; - assert(formula.is()); - auto &implies = formula.get(); + auto disjunction = ast::Formula::make(); - if (!implies.consequent.is()) - continue; - - auto &otherPredicate = implies.consequent.get(); - - if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name) - continue; - - for (std::size_t i = 0; i < predicate.arguments.size(); i++) - checkMatchingPredicates(predicate.arguments[i], otherPredicate.arguments[i]); - } - - // Copy the predicate’s arguments for the completed formula - std::vector variables; - variables.reserve(predicate.arguments.size()); - - for (const auto &argument : predicate.arguments) - { - assert(argument.is()); - variables.emplace_back(ast::deepCopy(argument.get())); - } - - auto or_ = ast::Formula::make(); + ast::VariableStack variableStack; + variableStack.push(¶meters); // Build the conjunction of all formulas with the predicate as consequent - for (auto i = formulaIndex; i < formulas.size();) + for (const auto &formula : formulas) { - auto &formula = formulas[i]; assert(formula.is()); auto &implies = formula.get(); if (!implies.consequent.is()) - { - i++; continue; - } auto &otherPredicate = implies.consequent.get(); - if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name) - { - i++; + if (!ast::matches(predicate, otherPredicate)) continue; - } - - ast::VariableStack variableStack; - variableStack.push(&variables); auto variables = ast::collectFreeVariables(implies.antecedent, variableStack); + // TODO: avoid deep copies if (variables.empty()) - or_.get().arguments.emplace_back(std::move(implies.antecedent)); + disjunction.get().arguments.emplace_back(ast::deepCopy(implies.antecedent)); else { - auto exists = ast::Formula::make(std::move(variables), std::move(implies.antecedent)); - or_.get().arguments.emplace_back(std::move(exists)); + auto exists = ast::Formula::make(std::move(variables), ast::deepCopy(implies.antecedent)); + disjunction.get().arguments.emplace_back(std::move(exists)); } - - if (i > formulaIndex) - formulas.erase(formulas.begin() + i); - else - i++; } - auto biconditionalRight = std::move(or_); - - // If the disjunction contains only one element, drop the enclosing disjunction - if (biconditionalRight.get().arguments.size() == 1) - biconditionalRight = biconditionalRight.get().arguments.front(); - - // If the biconditional would be of the form “F <-> true” or “F <-> false,” simplify the output - if (biconditionalRight.is()) - { - const auto &boolean = biconditionalRight.get(); - - if (boolean.value == true) - formulas[formulaIndex] = ast::deepCopy(predicate); - else - formulas[formulaIndex] = ast::Formula::make(ast::deepCopy(predicate)); - - formulaIndex++; - return; - } - - // Build the biconditional within the completed formula - auto biconditional = ast::Formula::make(ast::deepCopy(predicate), std::move(biconditionalRight)); - - if (predicate.arguments.empty()) - { - formulas[formulaIndex] = std::move(biconditional); - formulaIndex++; - return; - } - - auto completedFormula = ast::Formula::make(std::move(variables), std::move(biconditional)); - - formulas[formulaIndex] = std::move(completedFormula); - formulaIndex++; + return disjunction; } //////////////////////////////////////////////////////////////////////////////////////////////////// -void completeBoolean(std::vector &formulas, std::size_t &formulaIndex) +// Builds the quantified inner part of the completed formula +ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Formula &&innerFormula) +{ + assert(innerFormula.is()); + + if (innerFormula.get().arguments.empty()) + return ast::Formula::make(std::move(predicate)); + + if (innerFormula.get().arguments.size() == 1) + innerFormula = std::move(innerFormula.get().arguments.front()); + + if (innerFormula.is()) + { + const auto &boolean = innerFormula.get(); + + if (boolean.value == true) + return std::move(predicate); + else + return ast::Formula::make(std::move(predicate)); + } + + return ast::Formula::make(std::move(predicate), std::move(innerFormula)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void completePredicate(ast::Predicate &&predicate, const std::vector &formulas, std::vector &completedFormulas) +{ + auto parameters = copyParameters(predicate); + auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, formulas); + auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction)); + + if (parameters.empty()) + { + completedFormulas.emplace_back(std::move(completedFormulaQuantified)); + return; + } + + auto completedFormula = ast::Formula::make(std::move(parameters), std::move(completedFormulaQuantified)); + completedFormulas.emplace_back(std::move(completedFormula)); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void completeIntegrityConstraint(const ast::Formula &formula, std::vector &completedFormulas) { - auto &formula = formulas[formulaIndex]; assert(formula.is()); auto &implies = formula.get(); assert(implies.consequent.is()); - auto &boolean = implies.consequent.get(); + assert(implies.consequent.get().value == false); auto variables = ast::collectFreeVariables(implies.antecedent); - // Implications of the form “T -> true” are useless - if (boolean.value == true) - { - formulas.erase(formulas.begin() + formulaIndex); - return; - } - - auto argument = ast::Formula::make(std::move(implies.antecedent)); + // TODO: avoid deep copies + auto argument = ast::Formula::make(ast::deepCopy(implies.antecedent)); if (variables.empty()) { - formula = std::move(argument); - formulaIndex++; + completedFormulas.emplace_back(std::move(argument)); return; } - formula = ast::Formula::make(std::move(variables), std::move(argument)); - formulaIndex++; + auto completedFormula = ast::Formula::make(std::move(variables), std::move(argument)); + completedFormulas.emplace_back(std::move(completedFormula)); } //////////////////////////////////////////////////////////////////////////////////////////////////// void complete(std::vector &formulas) { + // Check whether formulas are in normal form for (const auto &formula : formulas) { if (!formula.is()) @@ -180,19 +151,58 @@ void complete(std::vector &formulas) throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently"); } - for (std::size_t i = 0; i < formulas.size();) + std::vector predicates; + + for (const auto &formula : formulas) + ast::collectPredicates(formula, predicates); + + std::sort(predicates.begin(), predicates.end(), + [](const auto *lhs, const auto *rhs) + { + const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str()); + + if (order != 0) + return order < 0; + + return lhs->arity() < rhs->arity(); + }); + + std::vector completedFormulas; + + // Complete predicates + for (const auto *predicate : predicates) + { + // Create the signature of the predicate + ast::Predicate signature(std::string(predicate->name)); + signature.arguments.reserve(predicate->arguments.size()); + + for (std::size_t i = 0; i < predicate->arguments.size(); i++) + { + auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1); + signature.arguments.emplace_back(ast::Term::make(std::move(variableName), ast::Variable::Type::Reserved)); + } + + completePredicate(std::move(signature), formulas, completedFormulas); + } + + // Complete integrity constraints + for (const auto &formula : formulas) { - auto &formula = formulas[i]; auto &implies = formula.get(); - if (implies.consequent.is()) - { - auto &predicate = implies.consequent.get(); - completePredicate(predicate, formulas, i); - } - else if (implies.consequent.is()) - completeBoolean(formulas, i); + if (!implies.consequent.is()) + continue; + + const auto &boolean = implies.consequent.get(); + + // Rules of the form “F -> #true” are useless + if (boolean.value == true) + continue; + + completeIntegrityConstraint(formula, completedFormulas); } + + std::swap(formulas, completedFormulas); } //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index dbad868..bfc2743 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -21,76 +21,127 @@ TEST_CASE("[completion] Rules are completed", "[completion]") SECTION("predicate in single rule head") { input << "p :- q."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); - CHECK(output.str() == "(p <-> q)\n"); + CHECK(output.str() == + "(p <-> q)\n" + "not q\n"); } SECTION("predicate in multiple rule heads") { - input << "p :- q.\n" + input << + "p :- q.\n" "p :- r.\n" "p :- s."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); - CHECK(output.str() == "(p <-> (q or r or s))\n"); + CHECK(output.str() == + "(p <-> (q or r or s))\n" + "not q\n" + "not r\n" + "not s\n"); } SECTION("multiple predicates are correctly separated") { - input << "p :- s.\n" + input << + "p :- s.\n" "q :- t.\n" "p :- q.\n" "r :- t.\n" "q :- r."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); - CHECK(output.str() == "(p <-> (s or q))\n(q <-> (t or r))\n(r <-> t)\n"); + CHECK(output.str() == + "(p <-> (s or q))\n" + "(q <-> (t or r))\n" + "(r <-> t)\n" + "not s\n" + "not t\n"); } SECTION("integrity constraints") { - input << ":- q.\n" - ":- s(5).\n" + input << + ":- q.\n" + ":- r(5).\n" + ":- s(N).\n" "#false :- t.\n" - "#false :- v(5)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + "#false :- u(5)."; + anthem::translate("input", input, context); - CHECK(output.str() == "not q\nnot s(5)\nnot t\nnot v(5)\n"); + CHECK(output.str() == + "not q\n" + "forall V1 not r(V1)\n" + "forall V1 not s(V1)\n" + "not t\n" + "forall V1 not u(V1)\n" + "not q\n" + "not r(5)\n" + "forall N not s(N)\n" + "not t\n" + "not u(5)\n"); + } + + SECTION("Booleans") + { + input << + "#true :- #true.\n" + "#true :- #false.\n" + "#false :- #true.\n" + "#false :- #false.\n"; + anthem::translate("input", input, context); + + CHECK(output.str() == + "not #true\n" + "not #false\n"); } SECTION("facts") { - input << "q.\n" + input << + "q.\n" "r.\n" - "t :- #true.\n" - "s :- #true."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + "s :- #true.\n" + "t :- #true."; + anthem::translate("input", input, context); - CHECK(output.str() == "q\nr\nt\ns\n"); + CHECK(output.str() == + "q\n" + "r\n" + "s\n" + "t\n"); } SECTION("useless implications") { - input << "#true :- p, q(N), t(1, 2).\n" + input << + "#true :- p, q(N), t(1, 2).\n" "#true.\n" - "h :- #false."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + "v :- #false."; + anthem::translate("input", input, context); // TODO: implement completion for unused predicates - CHECK(output.str() == "not h\n"); + CHECK(output.str() == + "not p\n" + "forall V1 not q(V1)\n" + "forall V1, V2 not t(V1, V2)\n" + "not v\n"); } SECTION("example") { - input << "{in(1..n, 1..r)}.\n" + input << + "{in(1..n, 1..r)}.\n" "covered(I) :- in(I, S).\n" ":- I = 1..n, not covered(I).\n" ":- in(I, S), in(J, S), in(I + J, S)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); - CHECK(output.str() == "forall V1, V2 (in(V1, V2) <-> (V1 in 1..n and V2 in 1..r and in(V1, V2)))\n" + CHECK(output.str() == "forall V1 (covered(V1) <-> exists I, S (V1 = I and in(I, S)))\n" + "forall V1, V2 (in(V1, V2) <-> (V1 in 1..n and V2 in 1..r and in(V1, V2)))\n" "forall I not (I in 1..n and not covered(I))\n" "forall I, S, J not (in(I, S) and in(J, S) and exists X5 (X5 in (I + J) and in(X5, S)))\n"); } diff --git a/tests/TestSimplification.cpp b/tests/TestSimplification.cpp index f8b8698..fa16bbb 100644 --- a/tests/TestSimplification.cpp +++ b/tests/TestSimplification.cpp @@ -21,7 +21,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") SECTION("example 1") { input << ":- in(I, S), in(J, S), in(I + J, S)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + 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"); } @@ -29,7 +29,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") SECTION("example 2") { input << "covered(I) :- in(I, S)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 = I and in(I, S)) -> covered(V1))\n"); } @@ -37,7 +37,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") SECTION("example 3") { input << ":- not covered(I), I = 1..n."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((not covered(I) and I in 1..n) -> #false)\n"); } @@ -45,7 +45,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") SECTION("comparisons") { input << ":- M > N."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(M > N -> #false)\n"); } diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index 4dfec3b..1cd6fd5 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -21,7 +21,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("simple example 1") { input << "p(1..5)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(V1 in 1..5 -> p(V1))\n"); } @@ -29,7 +29,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("simple example 2") { input << "p(N) :- N = 1..5."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1))\n"); } @@ -37,7 +37,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("simple example 3") { input << "p(N + 1) :- q(N)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in (N + 1) and exists X1 (X1 in N and q(X1))) -> p(V1))\n"); } @@ -45,7 +45,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("n-ary head") { input << "p(N, 1, 2) :- N = 1..5."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n"); } @@ -54,7 +54,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") { // TODO: check why order of disjunctive literals is inverted input << "q(3, N); p(N, 1, 2) :- N = 1..5."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } @@ -63,7 +63,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") { // TODO: check why order of disjunctive literals is inverted input << "q(3, N), p(N, 1, 2) :- N = 1..5."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } @@ -71,7 +71,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("escaping conflicting variable names") { input << "p(X1, V1, A1) :- q(X1), q(V1), q(A1)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in _X1 and V2 in _V1 and V3 in _A1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2)) and exists X3 (X3 in _A1 and q(X3))) -> p(V1, V2, V3))\n"); } @@ -79,7 +79,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("fact") { input << "p(42)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(V1 in 42 -> p(V1))\n"); } @@ -87,7 +87,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("0-ary fact") { input << "p."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(#true -> p)\n"); } @@ -95,7 +95,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("function") { input << ":- not p(I), I = 1..n."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((exists X1 (X1 in I and not p(X1)) and exists X2, X3 (X2 in I and X3 in 1..n and X2 = X3)) -> #false)\n"); } @@ -103,7 +103,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("disjunctive fact (no arguments)") { input << "q; p."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(#true -> (p or q))\n"); } @@ -111,7 +111,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("disjunctive fact (arguments)") { input << "q; p(42)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(V1 in 42 -> (p(V1) or q))\n"); } @@ -119,7 +119,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("integrity constraint (no arguments)") { input << ":- p, q."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((p and q) -> #false)\n"); } @@ -127,7 +127,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("contradiction") { input << ":-."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(#true -> #false)\n"); } @@ -135,7 +135,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("integrity constraint (arguments)") { input << ":- p(42), q."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((exists X1 (X1 in 42 and p(X1)) and q) -> #false)\n"); } @@ -143,7 +143,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("inf/sup") { input << "p(X, #inf) :- q(X, #sup)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in #inf and exists X1, X2 (X1 in X and X2 in #sup and q(X1, X2))) -> p(V1, V2))\n"); } @@ -151,7 +151,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("strings") { input << "p(X, \"foo\") :- q(X, \"bar\")."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in \"foo\" and exists X1, X2 (X1 in X and X2 in \"bar\" and q(X1, X2))) -> p(V1, V2))\n"); } @@ -159,7 +159,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("tuples") { input << "p(X, (1, 2, 3)) :- q(X, (4, 5))."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in (1, 2, 3) and exists X1, X2 (X1 in X and X2 in (4, 5) and q(X1, X2))) -> p(V1, V2))\n"); } @@ -167,7 +167,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("1-ary tuples") { input << "p(X, (1,)) :- q(X, (2,))."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in (1,) and exists X1, X2 (X1 in X and X2 in (2,) and q(X1, X2))) -> p(V1, V2))\n"); } @@ -175,7 +175,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("intervals") { input << "p(X, 1..10) :- q(X, 6..12)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in 1..10 and exists X1, X2 (X1 in X and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n"); } @@ -183,7 +183,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("comparisons") { input << "p(M, N, O, P) :- M < N, P != O."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in M and V2 in N and V3 in O and V4 in P and exists X1, X2 (X1 in M and X2 in N and X1 < X2) and exists X3, X4 (X3 in P and X4 in O and X3 != X4)) -> p(V1, V2, V3, V4))\n"); } @@ -191,7 +191,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("single negation") { input << "not p(X, 1) :- not q(X, 2)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2))) -> not p(V1, V2))\n"); } @@ -200,7 +200,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") { // TODO: check why order of disjunctive literals is inverted input << "f; q(A1, A2); p(A3, r(A4)); g(g(A5)) :- g(A3), f, q(A4, A1), p(A2, A5)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in _A1 and V2 in _A2 and V3 in _A3 and V4 in r(_A4) and V5 in g(_A5)" " and exists X1 (X1 in _A3 and g(X1)) and f and exists X2, X3 (X2 in _A4 and X3 in _A1 and q(X2, X3)) and exists X4, X5 (X4 in _A2 and X5 in _A5 and p(X4, X5)))" @@ -210,7 +210,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("nested functions") { input << "p(q(s(t(X1))), u(X2)) :- u(v(w(X2)), z(X1))."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in q(s(t(_X1))) and V2 in u(_X2) and exists X1, X2 (X1 in v(w(_X2)) and X2 in z(_X1) and u(X1, X2))) -> p(V1, V2))\n"); } @@ -218,7 +218,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule (simple)") { input << "{p}."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(p -> p)\n"); } @@ -226,7 +226,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule (two elements)") { input << "{p; q}."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "(p -> p)\n(q -> q)\n"); } @@ -234,7 +234,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule (n-ary elements)") { input << "{p(1..3, N); q(2..4)}."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V1 in 1..3 and V2 in N and V3 in 2..4 and q(V3)) -> q(V3))\n"); } @@ -242,7 +242,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule with body") { input << "{p(M, N); q(P)} :- s(M, N, P)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and p(V1, V2)) -> p(V1, V2))\n((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and q(V3)) -> q(V3))\n"); } @@ -250,7 +250,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule with negation") { input << "{not p(X, 1)} :- not q(X, 2)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n"); } @@ -258,7 +258,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("choice rule with negation (two elements)") { input << "{not p(X, 1); not s} :- not q(X, 2)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not s) -> not s)\n"); } @@ -266,7 +266,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") SECTION("anonymous variables") { input << "p(_, _) :- q(_, _)."; - REQUIRE_NOTHROW(anthem::translate("input", input, context)); + anthem::translate("input", input, context); CHECK(output.str() == "((V1 in A1 and V2 in A2 and exists X1, X2 (X1 in A3 and X2 in A4 and q(X1, X2))) -> p(V1, V2))\n"); }