From 107dae72878e5fc3c6581aa9dba412995895e09a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 25 Mar 2018 19:42:55 +0200 Subject: [PATCH] Move simplification rule to tableau MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This moves the rule “exists () (F) === F” to the simplification rule tableau. --- src/anthem/Simplification.cpp | 29 +++++++++++++++++++++++------ 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index e85a369..29eeb5d 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -124,6 +124,28 @@ SimplificationResult simplify(ast::Formula &formula) //////////////////////////////////////////////////////////////////////////////////////////////////// +struct SimplificationRuleExistsWithoutQuantifiedVariables +{ + static constexpr const auto Description = "exists () (F) === F"; + + static SimplificationResult apply(ast::Formula &formula) + { + if (!formula.is()) + return SimplificationResult::Unchanged; + + auto &exists = formula.get(); + + if (!exists.variables.empty()) + return SimplificationResult::Unchanged; + + formula = std::move(exists.argument); + + return SimplificationResult::Simplified; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct SimplificationRuleTrivialAssignmentInExists { static constexpr const auto Description = "exists X (X = Y) === #true"; @@ -304,12 +326,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) SimplificationRuleTrivialExists::apply(formula); SimplificationRuleOneElementConjunction::apply(exists.argument); - // If there are still remaining variables, simplification is over - if (!exists.variables.empty()) - return; - - // If there is more than one element in the conjunction, replace the input formula with the conjunction - formula = std::move(exists.argument); + SimplificationRuleExistsWithoutQuantifiedVariables::apply(formula); } ////////////////////////////////////////////////////////////////////////////////////////////////////