From e0509f725a6e8ea8712f83d83317f84d019bc420 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Fri, 27 Apr 2018 23:37:13 +0200 Subject: [PATCH] Replace SimplificationResult with OperationResult This replaces the SimplificationResult enum class with OperationResult. The rationale is that this type, which just reports whether or not an operation actually changed the input data, is not simplification- specific and will be used for integer variable detection as well. --- include/anthem/Simplification.h | 8 -- include/anthem/SimplificationVisitors.h | 97 +++++++++---------- include/anthem/Utils.h | 8 ++ src/anthem/Simplification.cpp | 118 ++++++++++++------------ 4 files changed, 116 insertions(+), 115 deletions(-) diff --git a/include/anthem/Simplification.h b/include/anthem/Simplification.h index 2169971..162559f 100644 --- a/include/anthem/Simplification.h +++ b/include/anthem/Simplification.h @@ -12,14 +12,6 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -enum class SimplificationResult -{ - Simplified, - Unchanged, -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - void simplify(ast::Formula &formula); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/SimplificationVisitors.h b/include/anthem/SimplificationVisitors.h index e32b60e..a467274 100644 --- a/include/anthem/SimplificationVisitors.h +++ b/include/anthem/SimplificationVisitors.h @@ -3,6 +3,7 @@ #include #include +#include namespace anthem { @@ -19,96 +20,96 @@ template struct FormulaSimplificationVisitor { template - SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments) + OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments) { for (auto &argument : and_.arguments) - if (argument.accept(*this, argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (argument.accept(*this, argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments) + OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments) { - if (biconditional.left.accept(*this, biconditional.left, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (biconditional.left.accept(*this, biconditional.left, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; - if (biconditional.right.accept(*this, biconditional.right, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (biconditional.right.accept(*this, biconditional.right, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments) + OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments) { return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments) + OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments) { return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments) + OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments) { - if (exists.argument.accept(*this, exists.argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (exists.argument.accept(*this, exists.argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments) + OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments) { - if (forAll.argument.accept(*this, forAll.argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (forAll.argument.accept(*this, forAll.argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments) + OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments) { - if (implies.antecedent.accept(*this, implies.antecedent, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (implies.antecedent.accept(*this, implies.antecedent, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; - if (implies.consequent.accept(*this, implies.consequent, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (implies.consequent.accept(*this, implies.consequent, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments) + OperationResult visit(In &, Formula &formula, Arguments &&... arguments) { return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments) + OperationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments) { - if (not_.argument.accept(*this, not_.argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (not_.argument.accept(*this, not_.argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments) + OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments) { for (auto &argument : or_.arguments) - if (argument.accept(*this, argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (argument.accept(*this, argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(formula, std::forward(arguments)...); } template - SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments) + OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments) { return T::accept(formula, std::forward(arguments)...); } @@ -116,69 +117,69 @@ struct FormulaSimplificationVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -template +template struct TermSimplificationVisitor { template - SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments) + OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments) { - if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; - if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments) + OperationResult visit(Boolean &, Term &term, Arguments &&... arguments) { return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments) + OperationResult visit(Function &function, Term &term, Arguments &&... arguments) { for (auto &argument : function.arguments) - if (argument.accept(*this, argument, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (argument.accept(*this, argument, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments) + OperationResult visit(Integer &, Term &term, Arguments &&... arguments) { return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments) + OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments) { - if (interval.from.accept(*this, interval.from, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (interval.from.accept(*this, interval.from, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; - if (interval.to.accept(*this, interval.to, std::forward(arguments)...) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (interval.to.accept(*this, interval.to, std::forward(arguments)...) == OperationResult::Changed) + return OperationResult::Changed; return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments) + OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments) { return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(String &, Term &term, Arguments &&... arguments) + OperationResult visit(String &, Term &term, Arguments &&... arguments) { return T::accept(term, std::forward(arguments)...); } template - SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments) + OperationResult visit(Variable &, Term &term, Arguments &&... arguments) { return T::accept(term, std::forward(arguments)...); } diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index 161ed92..11e9b35 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -32,6 +32,14 @@ enum class Tristate //////////////////////////////////////////////////////////////////////////////////////////////////// +enum class OperationResult +{ + Unchanged, + Changed, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } #endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 188fd6e..aa9129b 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -100,7 +100,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor -SimplificationResult simplify(ast::Formula &formula) +OperationResult simplify(ast::Formula &formula) { return SimplificationRule::apply(formula); } @@ -108,10 +108,10 @@ SimplificationResult simplify(ast::Formula &formula) //////////////////////////////////////////////////////////////////////////////////////////////////// template -SimplificationResult simplify(ast::Formula &formula) +OperationResult simplify(ast::Formula &formula) { - if (simplify(formula) == SimplificationResult::Simplified) - return SimplificationResult::Simplified; + if (simplify(formula) == OperationResult::Changed) + return OperationResult::Changed; return simplify(formula); } @@ -122,19 +122,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables { static constexpr const auto Description = "exists () (F) === F"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &exists = formula.get(); if (!exists.variables.empty()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = std::move(exists.argument); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -144,20 +144,20 @@ struct SimplificationRuleTrivialAssignmentInExists { static constexpr const auto Description = "exists X (X = Y) === #true"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; const auto &exists = formula.get(); if (!exists.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; const auto &comparison = exists.argument.get(); if (comparison.operator_ != ast::Comparison::Operator::Equal) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(), [&](const auto &variableDeclaration) @@ -167,11 +167,11 @@ struct SimplificationRuleTrivialAssignmentInExists }); if (matchingAssignment == exists.variables.cend()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = ast::Formula::make(true); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -181,20 +181,20 @@ struct SimplificationRuleAssignmentInExists { static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &exists = formula.get(); if (!exists.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &and_ = exists.argument.get(); auto &arguments = and_.arguments; - auto simplificationResult = SimplificationResult::Unchanged; + auto simplificationResult = OperationResult::Unchanged; for (auto i = exists.variables.begin(); i != exists.variables.end();) { @@ -225,7 +225,7 @@ struct SimplificationRuleAssignmentInExists arguments.erase(j); wasVariableReplaced = true; - simplificationResult = SimplificationResult::Simplified; + simplificationResult = OperationResult::Changed; break; } @@ -249,19 +249,19 @@ struct SimplificationRuleEmptyConjunction { static constexpr const auto Description = "[empty conjunction] === #true"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &and_ = formula.get(); if (!and_.arguments.empty()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = ast::Formula::make(true); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -271,19 +271,19 @@ struct SimplificationRuleOneElementConjunction { static constexpr const auto Description = "[conjunction of only F] === F"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &and_ = formula.get(); if (and_.arguments.size() != 1) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = std::move(and_.arguments.front()); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -293,19 +293,19 @@ struct SimplificationRuleTrivialExists { static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &exists = formula.get(); if (!exists.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = std::move(exists.argument); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -315,21 +315,21 @@ struct SimplificationRuleInWithPrimitiveArguments { static constexpr const auto Description = "[primitive A] in [primitive B] === A = B"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &in = formula.get(); assert(ast::isPrimitive(in.element)); if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set)) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set)); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -339,10 +339,10 @@ struct SimplificationRuleSubsumptionInBiconditionals { static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &biconditional = formula.get(); @@ -353,7 +353,7 @@ struct SimplificationRuleSubsumptionInBiconditionals const auto rightIsAnd = biconditional.right.is(); if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd)) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right); auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left); @@ -367,13 +367,13 @@ struct SimplificationRuleSubsumptionInBiconditionals }); if (matchingPredicate == and_.arguments.cend()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; and_.arguments.erase(matchingPredicate); formula = ast::Formula::make(std::move(predicateSide), std::move(andSide)); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -383,21 +383,21 @@ struct SimplificationRuleDoubleNegation { static constexpr const auto Description = "not not F === F"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto ¬_ = formula.get(); if (!not_.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto ¬Not = not_.argument.get(); formula = std::move(notNot.argument); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -407,15 +407,15 @@ struct SimplificationRuleDeMorganForConjunctions { static constexpr const auto Description = "(not (F and G)) === (not F or not G)"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto ¬_ = formula.get(); if (!not_.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &and_ = not_.argument.get(); @@ -424,7 +424,7 @@ struct SimplificationRuleDeMorganForConjunctions formula = ast::Formula::make(std::move(and_.arguments)); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -434,21 +434,21 @@ struct SimplificationRuleImplicationFromDisjunction { static constexpr const auto Description = "(not F or G) === (F -> G)"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &or_ = formula.get(); if (or_.arguments.size() != 2) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; const auto leftIsNot = or_.arguments[0].is(); const auto rightIsNot = or_.arguments[1].is(); if (leftIsNot == rightIsNot) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1]; auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0]; @@ -460,7 +460,7 @@ struct SimplificationRuleImplicationFromDisjunction formula = ast::Formula::make(std::move(negativeSideArgument), std::move(positiveSide)); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -470,15 +470,15 @@ struct SimplificationRuleNegatedComparison { static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)"; - static SimplificationResult apply(ast::Formula &formula) + static OperationResult apply(ast::Formula &formula) { if (!formula.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto ¬_ = formula.get(); if (!not_.argument.is()) - return SimplificationResult::Unchanged; + return OperationResult::Unchanged; auto &comparison = not_.argument.get(); @@ -506,7 +506,7 @@ struct SimplificationRuleNegatedComparison formula = std::move(comparison); - return SimplificationResult::Simplified; + return OperationResult::Changed; } }; @@ -535,7 +535,7 @@ const auto simplifyWithDefaultRules = struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor { // Do nothing for all other types of expressions - static SimplificationResult accept(ast::Formula &formula) + static OperationResult accept(ast::Formula &formula) { return simplifyWithDefaultRules(formula); } @@ -545,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor