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

Added simplification rule “exists X (X = Y)” → “#true.”

Browse Source
This commit is contained in:
Patrick Lühne 2017-06-05 02:41:17 +02:00
parent 7bf5d3867d
commit 4fd143ef64
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/anthem/Simplification.cpp
View File

@ -101,6 +101,28 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
// The exists statement has to be of the form “exists <variables> <conjunction>”
void simplify(ast::Exists &exists, ast::Formula &formula)
{
// Simplify formulas like “exists X (X = Y)” to “#true”
// TODO: check that this covers all cases
if (exists.argument.is<ast::Comparison>())
{
const auto &comparison = exists.argument.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal)
return;
const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
[&](const auto &variableDeclaration)
{
return matchesVariableDeclaration(comparison.left, *variableDeclaration)
|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
});
if (matchingAssignment != exists.variables.cend())
formula = ast::Formula::make<ast::Boolean>(true);
return;
}
if (!exists.argument.is<ast::And>())
return;