From 0ce4e54d1a1eaf1965fca9dda592faf40d9283c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 4 May 2018 15:30:44 +0200 Subject: [PATCH] Fix precedence of interval operator The interval operator has a lower precedence than, for example, binary operations. This was unexpected and incorrectly implemented in the output functions. For now, this is fixed by enclosing intervals in parentheses to avoid misinterpretations. The existing unit tests are adjusted to the updated output format. --- include/anthem/output/AST.h | 6 +++--- tests/TestCompletion.cpp | 8 ++++---- tests/TestHiddenPredicateElimination.cpp | 2 +- tests/TestIntegerDetection.cpp | 12 ++++++------ tests/TestSimplification.cpp | 2 +- tests/TestTranslation.cpp | 22 +++++++++++----------- 6 files changed, 26 insertions(+), 26 deletions(-) diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index 20e04eb..0a8fa61 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -219,16 +219,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Integer &in //////////////////////////////////////////////////////////////////////////////////////////////////// -inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool) +inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses) { - if (printContext.context.parenthesisStyle == ParenthesisStyle::Full) + if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full) stream << "("; print(stream, interval.from, printContext); stream << ".."; print(stream, interval.to, printContext); - if (printContext.context.parenthesisStyle == ParenthesisStyle::Full) + if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full) stream << ")"; return stream; diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index e26584b..00cdb6b 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]") anthem::translate("input", input, context); CHECK(output.str() == - "forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in 1..5))\n"); + "forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in (1..5)))\n"); } SECTION("useless implications") @@ -152,8 +152,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]") CHECK(output.str() == "forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n" - "forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n" - "forall U2 (U2 in 1..n -> covered(U2))\n" + "forall V2, V3 (in(V2, V3) -> (V2 in (1..n) and V3 in (1..r)))\n" + "forall U2 (U2 in (1..n) -> covered(U2))\n" "forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n"); } @@ -190,6 +190,6 @@ TEST_CASE("[completion] Rules are completed", "[completion]") input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1."; anthem::translate("input", input, context); - CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n"); + CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in (1..n) and V2 in (1..n) and |V1 - V2| = 1))\n"); } } diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp index 3e33c30..5e2fea4 100644 --- a/tests/TestHiddenPredicateElimination.cpp +++ b/tests/TestHiddenPredicateElimination.cpp @@ -150,7 +150,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin // TODO: simplify further CHECK(output.str() == - "forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n"); + "forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in (1..4)))\n"); } SECTION("simple propositions are hidden correctly") diff --git a/tests/TestIntegerDetection.cpp b/tests/TestIntegerDetection.cpp index 203c628..de34700 100644 --- a/tests/TestIntegerDetection.cpp +++ b/tests/TestIntegerDetection.cpp @@ -26,7 +26,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall N1 (p(N1) <-> N1 in 1..5)\n" + "forall N1 (p(N1) <-> N1 in (1..5))\n" "int(p/1@1)\n"); } @@ -38,7 +38,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall V1 (p(V1) <-> (V1 in 1..5 or V1 = error))\n"); + "forall V1 (p(V1) <-> (V1 in (1..5) or V1 = error))\n"); } SECTION("integer parameter with arithmetics") @@ -47,7 +47,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall N1 (p(N1) <-> N1 in ((2 + 1..5) * 2))\n" + "forall N1 (p(N1) <-> N1 in ((2 + (1..5)) * 2))\n" "int(p/1@1)\n"); } @@ -59,7 +59,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall N1 (p(N1) <-> N1 in 1..5)\n" + "forall N1 (p(N1) <-> N1 in (1..5))\n" "forall N2 (q(N2) <-> exists N3 (p(N3) and N2 in ((N3 + 5) / 3)))\n" "int(p/1@1)\n" "int(q/1@1)\n"); @@ -74,7 +74,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall N1 (p(N1) <-> N1 in 1..5)\n" + "forall N1 (p(N1) <-> N1 in (1..5))\n" "forall V1 (q(V1) <-> V1 = error)\n" "forall N2, V2, N3 (r(N2, V2, N3) <-> exists N4 (p(N4) and N2 = (N4 ** 2) and q(V2) and p(N3)))\n" "int(p/1@1)\n" @@ -89,7 +89,7 @@ TEST_CASE("[integer detection] Integer variables are correctly detected", "[inte anthem::translate("input", input, context); CHECK(output.str() == - "forall N1 (p(N1) <-> N1 in 2..n)\n" + "forall N1 (p(N1) <-> N1 in (2..n))\n" "int(p/1@1)\n"); } diff --git a/tests/TestSimplification.cpp b/tests/TestSimplification.cpp index b760c12..63ed564 100644 --- a/tests/TestSimplification.cpp +++ b/tests/TestSimplification.cpp @@ -40,7 +40,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]") input << ":- not covered(I), I = 1..n."; anthem::translate("input", input, context); - CHECK(output.str() == "((not covered(U1) and U1 in 1..n) -> #false)\n"); + CHECK(output.str() == "((not covered(U1) and U1 in (1..n)) -> #false)\n"); } SECTION("comparisons") diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index c55f543..945be61 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -24,7 +24,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(1..5)."; anthem::translate("input", input, context); - CHECK(output.str() == "(V1 in 1..5 -> p(V1))\n"); + CHECK(output.str() == "(V1 in (1..5) -> p(V1))\n"); } SECTION("simple example 2") @@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1))\n"); + CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1))\n"); } SECTION("simple example 3") @@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1, V2, V3))\n"); } SECTION("disjunctive head") @@ -57,7 +57,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q(3, N); p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } SECTION("disjunctive head (alternative syntax)") @@ -66,7 +66,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "q(3, N), p(N, 1, 2) :- N = 1..5."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n"); } SECTION("escaping conflicting variable names") @@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- not p(I), I = 1..n."; anthem::translate("input", input, context); - CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in 1..n and X2 = X3)) -> #false)\n"); + CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in (1..n) and X2 = X3)) -> #false)\n"); } SECTION("disjunctive fact (no arguments)") @@ -178,7 +178,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(X, 1..10) :- q(X, 6..12)."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in (1..10) and exists X1, X2 (X1 in U1 and X2 in (6..12) and q(X1, X2))) -> p(V1, V2))\n"); } SECTION("intervals with variable") @@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- q(N), 1 = 1..N."; anthem::translate("input", input, context); - CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in 1..U1 and X2 = X3)) -> #false)\n"); + CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in (1..U1) and X2 = X3)) -> #false)\n"); } SECTION("intervals with two variables") @@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << ":- q(M, N), M = 1..N."; anthem::translate("input", input, context); - CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in 1..U2 and X3 = X4)) -> #false)\n"); + CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in (1..U2) and X3 = X4)) -> #false)\n"); } SECTION("comparisons") @@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") anthem::translate("input", input, context); // TODO: eliminate V5: not needed - CHECK(output.str() == "((V1 in 1..3 and V2 in U1 and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V4 in 1..3 and V5 in U2 and V6 in 2..4 and q(V6)) -> q(V6))\n"); + CHECK(output.str() == "((V1 in (1..3) and V2 in U1 and V3 in (2..4) and p(V1, V2)) -> p(V1, V2))\n((V4 in (1..3) and V5 in U2 and V6 in (2..4) and q(V6)) -> q(V6))\n"); } SECTION("choice rule with body") @@ -302,6 +302,6 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") input << "p(N, N ** N) :- N = 1..n."; anthem::translate("input", input, context); - CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in 1..n and X1 = X2)) -> p(V1, V2))\n"); + CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in (1..n) and X1 = X2)) -> p(V1, V2))\n"); } }