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

Implement simplification rule tableau

Browse Source 
This implements a tableau containing simplification rules that can be
iteratively applied to input formulas until they remain unchanged.

First, this moves the rule “exists X (X = Y) === #true” to the tableau
as a reference implementation.
This commit is contained in:
Patrick Lühne 2018-03-25 18:52:36 +02:00
parent eaabeb0c55
commit 5c5411c0ff
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 54 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
src/anthem/Simplification.cpp
View File

@ -97,18 +97,51 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
////////////////////////////////////////////////////////////////////////////////////////////////////
// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
// The exists statement has to be of the form “exists <variables> <conjunction>”
void simplify(ast::Exists &exists, ast::Formula &formula)
enum class SimplificationResult
{
// Simplify formulas like “exists X (X = Y)” to “#true”
// TODO: check that this covers all cases
if (exists.argument.is<ast::Comparison>())
Simplified,
Unchanged,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class SimplificationRule>
SimplificationResult simplify(ast::Formula &formula)
{
return SimplificationRule::apply(formula);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class SimplificationRule, class... OtherSimplificationRules>
SimplificationResult simplify(ast::Formula &formula)
{
if (SimplificationRule::apply(formula) == SimplificationResult::Simplified)
return SimplificationResult::Simplified;
return simplify<OtherSimplificationRules...>(formula);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
struct SimplificationRuleTrivialExists
{
static constexpr const auto Description = "exists X (X = Y) === #true";
static SimplificationResult apply(ast::Formula &formula)
{
if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged;
const auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Comparison>())
return SimplificationResult::Unchanged;
const auto &comparison = exists.argument.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal)
return;
return SimplificationResult::Unchanged;
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
[&](const auto &variableDeclaration)
@ -117,11 +150,22 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
});
if (matchingAssignment != exists.variables.cend())
if (matchingAssignment == exists.variables.cend())
return SimplificationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true);
return;
return SimplificationResult::Simplified;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
// The exists statement has to be of the form “exists <variables> <conjunction>”
void simplify(ast::Exists &exists, ast::Formula &formula)
{
SimplificationRuleTrivialExists::apply(formula);
if (!exists.argument.is<ast::And>())
return;