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

Move simplification rule to tableau

Browse Source 
This moves the rule “exists ... ([#true/#false]) === [#true/#false]” to
the simplification rule tableau along with “[empty conjunction] ===
This commit is contained in:
Patrick Lühne 2018-03-25 19:29:46 +02:00
parent 7e3fc007c8
commit 4a85fc4b23
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 48 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
src/anthem/Simplification.cpp
View File

@ -124,7 +124,7 @@ SimplificationResult simplify(ast::Formula &formula)
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialExists struct SimplificationRuleTrivialAssignmentInExists
{ {
static constexpr const auto Description = "exists X (X = Y) === #true"; static constexpr const auto Description = "exists X (X = Y) === #true";
@ -229,9 +229,53 @@ struct SimplificationRuleAssignmentInExists
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleEmptyConjunction
{
static constexpr const auto Description = "[empty conjunction] === #true";
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::And>())
return SimplificationResult::Unchanged;
auto &and_ = formula.get<ast::And>();
if (!and_.arguments.empty())
return SimplificationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true);
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialExists
{
static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged;
auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Boolean>())
return SimplificationResult::Unchanged;
formula = std::move(exists.argument);
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
void simplify(ast::Exists &exists, ast::Formula &formula) void simplify(ast::Exists &exists, ast::Formula &formula)
{ {
SimplificationRuleTrivialExists::apply(formula); SimplificationRuleTrivialAssignmentInExists::apply(formula);
SimplificationRuleAssignmentInExists::apply(formula); SimplificationRuleAssignmentInExists::apply(formula);
if (!exists.argument.is<ast::And>()) if (!exists.argument.is<ast::And>())
@ -240,13 +284,8 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
auto &and_ = exists.argument.get<ast::And>(); auto &and_ = exists.argument.get<ast::And>();
auto &arguments = and_.arguments; auto &arguments = and_.arguments;
// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)” SimplificationRuleEmptyConjunction::apply(exists.argument);
// Such exists statements are useless and can be safely replaced with “#true” SimplificationRuleTrivialExists::apply(formula);
if (arguments.empty())
{
formula = ast::Formula::make<ast::Boolean>(true);
return;
}
// If the argument now is a conjunction with just one element, directly replace the input formula with the argument // If the argument now is a conjunction with just one element, directly replace the input formula with the argument
if (arguments.size() == 1) if (arguments.size() == 1)