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

Move simplification rule to tableau

Browse Source 
This moves the rule “[conjunction of only F] === F” to the
simplification rule tableau.
This commit is contained in:
Patrick Lühne 2018-03-25 19:33:07 +02:00
parent 4a85fc4b23
commit 827d6e40fe
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 23 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/anthem/Simplification.cpp
View File

@ -251,6 +251,28 @@ struct SimplificationRuleEmptyConjunction
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleOneElementConjunction
{
static constexpr const auto Description = "[conjunction of only F] === F";
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return SimplificationResult::Unchanged;
auto &and_ = formula.get<ast::And>();
if (and_.arguments.size() != 1)
return SimplificationResult::Unchanged;
formula = std::move(and_.arguments.front());
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialExists
{
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
@ -278,25 +300,14 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
SimplificationRuleTrivialAssignmentInExists::apply(formula);
SimplificationRuleAssignmentInExists::apply(formula);
if (!exists.argument.is<ast::And>())
return;
auto &and_ = exists.argument.get<ast::And>();
auto &arguments = and_.arguments;
SimplificationRuleEmptyConjunction::apply(exists.argument);
SimplificationRuleTrivialExists::apply(formula);
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
if (arguments.size() == 1)
exists.argument = std::move(arguments.front());
SimplificationRuleOneElementConjunction::apply(exists.argument);
// If there are still remaining variables, simplification is over
if (!exists.variables.empty())
return;
assert(!arguments.empty());
// If there is more than one element in the conjunction, replace the input formula with the conjunction
formula = std::move(exists.argument);
}