Added another simplification step after completion.

This commit is contained in:
Patrick Lühne 2017-06-04 14:36:09 +02:00
parent 4ed4458f1b
commit dcc504ebc0
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 10 additions and 3 deletions

View File

@ -79,6 +79,13 @@ void translate(const char *fileName, std::istream &stream, Context &context)
auto completedFormulas = complete(std::move(scopedFormulas));
// TODO: rethink simplification steps
if (context.simplify)
for (auto &completedFormula : completedFormulas)
simplify(completedFormula);
// TODO: remove variables that are not referenced after simplification
for (const auto &completedFormula : completedFormulas)
{
ast::print(context.logger.outputStream(), completedFormula, printContext);

View File

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