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"); } }