patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Add new simplification rule

Browse Source 
This adds the rule “(F <-> (F and G)) === (F -> G)” to the
simplification rule tableau.
This commit is contained in:
Patrick Lühne
2018-04-09 23:13:21 +02:00
parent 00ab975c2d
commit b18ddcc575
5 changed files with 469 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
tests/TestCompletion.cpp
View File

@@ -152,7 +152,7 @@ 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 and in(V2, V3)))\n"
"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
"forall U2 not (U2 in 1..n and not covered(U2))\n"
"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
}

5
tests/TestHiddenPredicateElimination.cpp
View File

@@ -164,10 +164,9 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
"#show t/0.";
anthem::translate("input", input, context);
// TODO: simplify further
CHECK(output.str() ==
"(s <-> (not #false and s))\n"
"(t <-> (not #false and t))\n"
"(s -> not #false)\n"
"(t -> not #false)\n"
"not (s and not t)\n"
"not (not #false and not #false and #false)\n");
}

2
tests/TestPlaceholders.cpp
View File

@@ -55,7 +55,7 @@ TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1, V2 (color(V1, V2) <-> (vertex(V1) and color(V2) and color(V1, V2)))\n"
"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
"forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n"
"forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n");
}