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

Add new simplification rule

Browse Source 
This adds the rule “(not (F and G)) === (not F or not G)” to the
simplification rule tableau.
This commit is contained in:
Patrick Lühne 2018-04-09 23:38:58 +02:00
parent 23624007ec
commit 6f7b021712
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 35 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/anthem/Simplification.cpp
View File

@ -403,6 +403,33 @@ struct SimplificationRuleDoubleNegation
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleDeMorganForConjunctions
{
static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Not>())
return SimplificationResult::Unchanged;
auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::And>())
return SimplificationResult::Unchanged;
auto &and_ = not_.argument.get<ast::And>();
for (auto &argument : and_.arguments)
argument = ast::Formula::make<ast::Not>(std::move(argument));
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
const auto simplifyWithDefaultRules =
simplify
<
@ -414,7 +441,8 @@ const auto simplifyWithDefaultRules =
SimplificationRuleOneElementConjunction,
SimplificationRuleExistsWithoutQuantifiedVariables,
SimplificationRuleInWithPrimitiveArguments,
SimplificationRuleSubsumptionInBiconditionals
SimplificationRuleSubsumptionInBiconditionals,
SimplificationRuleDeMorganForConjunctions
>;
////////////////////////////////////////////////////////////////////////////////////////////////////

4
tests/TestCompletion.cpp
View File

@ -153,8 +153,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
CHECK(output.str() ==
"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))\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 U2 (not U2 in 1..n or covered(U2))\n"
"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
}
SECTION("binary operations with multiple variables")

4
tests/TestHiddenPredicateElimination.cpp
View File

@ -168,8 +168,8 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
CHECK(output.str() ==
"(s -> not #false)\n"
"(t -> not #false)\n"
"not (s and not t)\n"
"not (not #false and not #false and #false)\n");
"(not s or t)\n"
"(#false or #false or not #false)\n");
}
SECTION("predicate with more than one argument is hidden correctly")

4
tests/TestPlaceholders.cpp
View File

@ -56,7 +56,7 @@ TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "
CHECK(output.str() ==
"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
"forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n"
"forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n");
"forall U1 (not vertex(U1) or exists U2 color(U1, U2))\n"
"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
}
}