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

Removed unnecessary parentheses after simplification.

Browse Source
This commit is contained in:
Patrick Lühne 2017-06-05 03:58:39 +02:00
parent 3b26580815
commit 7ae0a1f289
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
3 changed files with 6 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CHANGELOG.md
View File

@ -11,6 +11,7 @@ Features:
Bug Fixes: Bug Fixes:
* adds missing error message when attempting to read inaccessible file * adds missing error message when attempting to read inaccessible file
* removes unnecessary parentheses after simplification
## 0.1.5 (2017-05-04) ## 0.1.5 (2017-05-04)

11
src/anthem/Simplification.cpp
View File

@ -170,19 +170,16 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
i++; i++;
} }
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
if (arguments.size() == 1)
exists.argument = std::move(arguments.front());
// If there are still remaining variables, simplification is over // If there are still remaining variables, simplification is over
if (!exists.variables.empty()) if (!exists.variables.empty())
return; return;
assert(!arguments.empty()); assert(!arguments.empty());
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
if (arguments.size() == 1)
{
formula = std::move(arguments.front());
return;
}
// If there is more than one element in the conjunction, replace the input formula with the conjunction // If there is more than one element in the conjunction, replace the input formula with the conjunction
formula = std::move(exists.argument); formula = std::move(exists.argument);
} }

2
tests/TestCompletion.cpp
View File

@ -140,7 +140,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
anthem::translate("input", input, context); anthem::translate("input", input, context);
CHECK(output.str() == CHECK(output.str() ==
"forall V1 (covered(V1) <-> exists U1 (in(V1, U1)))\n" "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 and in(V2, V3)))\n"
"forall U2 not (U2 in 1..n and not covered(U2))\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"); "forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");