diff --git a/CHANGELOG.md b/CHANGELOG.md index 1f58dd3..5d45bda 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ Features: Bug Fixes: * adds missing error message when attempting to read inaccessible file +* removes unnecessary parentheses after simplification ## 0.1.5 (2017-05-04) diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index f4df751..7a95734 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -170,19 +170,16 @@ void simplify(ast::Exists &exists, ast::Formula &formula) 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 (!exists.variables.empty()) return; 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 formula = std::move(exists.argument); } diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp index 1d301dc..14b59b1 100644 --- a/tests/TestCompletion.cpp +++ b/tests/TestCompletion.cpp @@ -140,7 +140,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]") anthem::translate("input", input, context); 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 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");