Browse Source

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.
master
Patrick Lühne 4 years ago
parent
commit
0ce4e54d1a
Signed by: patrick GPG Key ID: 05F3611E97A70ABF
  1. 6
      include/anthem/output/AST.h
  2. 8
      tests/TestCompletion.cpp
  3. 2
      tests/TestHiddenPredicateElimination.cpp
  4. 12
      tests/TestIntegerDetection.cpp
  5. 2
      tests/TestSimplification.cpp
  6. 22
      tests/TestTranslation.cpp

6
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;

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

2
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")

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

2
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")

22
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");
}
}
Loading…
Cancel
Save