diff --git a/tests/TestSimplification.cpp b/tests/TestSimplification.cpp new file mode 100644 index 0000000..4456fc0 --- /dev/null +++ b/tests/TestSimplification.cpp @@ -0,0 +1,44 @@ +#include + +#include + +#include +#include +#include + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +TEST_CASE("[simplification] Rules are simplified correctly", "[simplified]") +{ + std::stringstream input; + std::stringstream output; + std::stringstream errors; + + anthem::output::Logger logger(output, errors); + anthem::Context context = {logger, {}}; + context.simplify = true; + + SECTION("example 1") + { + input << ":- in(I, S), in(J, S), in(I + J, S)."; + anthem::translate("input", input, context); + + REQUIRE(output.str() == "((in(I, S) and in(J, S) and exists X5 (X5 in (I + J) and in(X5, S))) -> #false)\n"); + } + + SECTION("example 2") + { + input << "covered(I) :- in(I, S)."; + anthem::translate("input", input, context); + + REQUIRE(output.str() == "((V1 = I and in(I, S)) -> covered(V1))\n"); + } + + SECTION("example 3") + { + input << ":- not covered(I), I = 1..n."; + anthem::translate("input", input, context); + + REQUIRE(output.str() == "((not covered(I) and I in 1..n) -> #false)\n"); + } +} diff --git a/tests/TestTranslation.cpp b/tests/TestTranslation.cpp index 224577f..19b66d8 100644 --- a/tests/TestTranslation.cpp +++ b/tests/TestTranslation.cpp @@ -14,7 +14,8 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]") std::stringstream errors; anthem::output::Logger logger(output, errors); - anthem::Context context = {logger, {}, 1}; + anthem::Context context = {logger, {}}; + context.simplify = false; SECTION("simple example 1") {