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

Added simple unit tests for #show statements.

This commit is contained in:
Patrick Lühne 2017-06-05 03:26:09 +02:00
parent 2cbc3116b8
commit adabe1bf1a
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
1 changed files with 94 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

94
tests/TestHiddenPredicateElimination.cpp Normal file
View File

@ -0,0 +1,94 @@
#include <catch.hpp>
#include <sstream>
#include <anthem/AST.h>
#include <anthem/Context.h>
#include <anthem/Translation.h>
////////////////////////////////////////////////////////////////////////////////////////////////////
TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly eliminated", "[hidden predicate elimination]")
{
std::stringstream input;
std::stringstream output;
std::stringstream errors;
anthem::output::Logger logger(output, errors);
anthem::Context context(std::move(logger));
context.simplify = true;
context.complete = true;
SECTION("simple example (positive 0-ary predicate)")
{
input <<
"p :- q.\n"
"q.\n"
"#show p/0.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"(p <-> #true)\n");
}
SECTION("simple example (negative 0-ary predicate)")
{
input <<
"p :- q.\n"
"#show p/0.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"(p <-> #false)\n");
}
SECTION("simple example (1-ary predicates, hide all but one)")
{
input <<
"a(X) :- b(X), c(X).\n"
"b(X) :- not d(X).\n"
"c(1).\n"
"c(2).\n"
"#show a/1.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (a(V1) <-> (not #false and (V1 = 1 or V1 = 2)))\n");
}
SECTION("simple example (1-ary predicates, show all explicitly)")
{
input <<
"a(X) :- b(X), c(X).\n"
"b(X) :- not d(X).\n"
"c(1).\n"
"c(2).\n"
"#show a/1."
"#show b/1."
"#show c/1."
"#show d/1.";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (a(V1) <-> (b(V1) and c(V1)))\n"
"forall V2 (b(V2) <-> not d(V2))\n"
"forall V3 (c(V3) <-> (V3 = 1 or V3 = 2))\n"
"forall V4 not d(V4)\n");
}
SECTION("simple example (1-ary predicates, show all implicitly)")
{
input <<
"a(X) :- b(X), c(X).\n"
"b(X) :- not d(X).\n"
"c(1).\n"
"c(2).";
anthem::translate("input", input, context);
CHECK(output.str() ==
"forall V1 (a(V1) <-> (b(V1) and c(V1)))\n"
"forall V2 (b(V2) <-> not d(V2))\n"
"forall V3 (c(V3) <-> (V3 = 1 or V3 = 2))\n"
"forall V4 not d(V4)\n");
}
}