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

Add new simplification rule 

This adds the rule “(not F [comparison] G) === (F [negated comparison]
G)” to the simplification rule tableau.
This commit is contained in:
Patrick Lühne 2018-04-11 21:39:27 +02:00
parent b63ef21849
commit 797660d6de
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 56 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

49
src/anthem/Simplification.cpp
View File

@ -466,6 +466,52 @@ struct SimplificationRuleImplicationFromDisjunction
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleNegatedComparison
{
static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] 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::Comparison>())
return SimplificationResult::Unchanged;
auto &comparison = not_.argument.get<ast::Comparison>();
switch (comparison.operator_)
{
case ast::Comparison::Operator::GreaterThan:
comparison.operator_ = ast::Comparison::Operator::LessEqual;
break;
case ast::Comparison::Operator::LessThan:
comparison.operator_ = ast::Comparison::Operator::GreaterEqual;
break;
case ast::Comparison::Operator::LessEqual:
comparison.operator_ = ast::Comparison::Operator::GreaterThan;
break;
case ast::Comparison::Operator::GreaterEqual:
comparison.operator_ = ast::Comparison::Operator::LessThan;
break;
case ast::Comparison::Operator::NotEqual:
comparison.operator_ = ast::Comparison::Operator::Equal;
break;
case ast::Comparison::Operator::Equal:
comparison.operator_ = ast::Comparison::Operator::NotEqual;
break;
}
formula = std::move(comparison);
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
const auto simplifyWithDefaultRules =
simplify
<
@ -479,7 +525,8 @@ const auto simplifyWithDefaultRules =
SimplificationRuleInWithPrimitiveArguments,
SimplificationRuleSubsumptionInBiconditionals,
SimplificationRuleDeMorganForConjunctions,
SimplificationRuleImplicationFromDisjunction
SimplificationRuleImplicationFromDisjunction,
SimplificationRuleNegatedComparison
>;
////////////////////////////////////////////////////////////////////////////////////////////////////

8
tests/TestCompletion.cpp
View File

@ -176,4 +176,12 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
CHECK(output.str() ==
"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
}
SECTION("negated comparisons")
{
input << ":- color(V, C1), color(V, C2), C1 != C2.";
anthem::translate("input", input, context);
CHECK(output.str() == "forall V1, V2 not color(V1, V2)\nforall U1, U2, U3 (not color(U1, U2) or not color(U1, U3) or U2 = U3)\n");
}
}