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.
This commit is contained in:
Patrick Lühne 2018-04-27 23:37:13 +02:00
parent 48cf8ee3e0
commit e0509f725a
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 116 additions and 115 deletions

View File

@ -12,14 +12,6 @@ namespace anthem
// //
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
enum class SimplificationResult
{
Simplified,
Unchanged,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
void simplify(ast::Formula &formula); void simplify(ast::Formula &formula);
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -3,6 +3,7 @@
#include <anthem/AST.h> #include <anthem/AST.h>
#include <anthem/Simplification.h> #include <anthem/Simplification.h>
#include <anthem/Utils.h>
namespace anthem namespace anthem
{ {
@ -19,96 +20,96 @@ template<class T>
struct FormulaSimplificationVisitor struct FormulaSimplificationVisitor
{ {
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments) OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
{ {
for (auto &argument : and_.arguments) for (auto &argument : and_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments) OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments) OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments) OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments) OperationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
{ {
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments) OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
{ {
for (auto &argument : or_.arguments) for (auto &argument : or_.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments) OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(formula, std::forward<Arguments>(arguments)...); return T::accept(formula, std::forward<Arguments>(arguments)...);
} }
@ -116,69 +117,69 @@ struct FormulaSimplificationVisitor
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
template<class T, class SimplificationResult = void> template<class T, class OperationResult = void>
struct TermSimplificationVisitor struct TermSimplificationVisitor
{ {
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments) OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
{ {
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments) OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
{ {
for (auto &argument : function.arguments) for (auto &argument : function.arguments)
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments) OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
{ {
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
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>(arguments)...) == SimplificationResult::Simplified) if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified) if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments) OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
{ {
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(String &, Term &term, Arguments &&... arguments) OperationResult visit(String &, Term &term, Arguments &&... arguments)
{ {
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments) OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
{ {
return T::accept(term, std::forward<Arguments>(arguments)...); return T::accept(term, std::forward<Arguments>(arguments)...);
} }

View File

@ -32,6 +32,14 @@ enum class Tristate
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
enum class OperationResult
{
Unchanged,
Changed,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
} }
#endif #endif

View File

@ -100,7 +100,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
template<class SimplificationRule> template<class SimplificationRule>
SimplificationResult simplify(ast::Formula &formula) OperationResult simplify(ast::Formula &formula)
{ {
return SimplificationRule::apply(formula); return SimplificationRule::apply(formula);
} }
@ -108,10 +108,10 @@ SimplificationResult simplify(ast::Formula &formula)
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules> template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
SimplificationResult simplify(ast::Formula &formula) OperationResult simplify(ast::Formula &formula)
{ {
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified) if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
return SimplificationResult::Simplified; return OperationResult::Changed;
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula); return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
} }
@ -122,19 +122,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
{ {
static constexpr const auto Description = "exists () (F) === F"; static constexpr const auto Description = "exists () (F) === F";
static SimplificationResult apply(ast::Formula &formula) static OperationResult apply(ast::Formula &formula)
{ {
if (!formula.is<ast::Exists>()) if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &exists = formula.get<ast::Exists>(); auto &exists = formula.get<ast::Exists>();
if (!exists.variables.empty()) if (!exists.variables.empty())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
formula = std::move(exists.argument); 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 constexpr const auto Description = "exists X (X = Y) === #true";
static SimplificationResult apply(ast::Formula &formula) static OperationResult apply(ast::Formula &formula)
{ {
if (!formula.is<ast::Exists>()) if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
const auto &exists = formula.get<ast::Exists>(); const auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Comparison>()) if (!exists.argument.is<ast::Comparison>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
const auto &comparison = exists.argument.get<ast::Comparison>(); const auto &comparison = exists.argument.get<ast::Comparison>();
if (comparison.operator_ != ast::Comparison::Operator::Equal) 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 matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
[&](const auto &variableDeclaration) [&](const auto &variableDeclaration)
@ -167,11 +167,11 @@ struct SimplificationRuleTrivialAssignmentInExists
}); });
if (matchingAssignment == exists.variables.cend()) if (matchingAssignment == exists.variables.cend())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true); formula = ast::Formula::make<ast::Boolean>(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 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<ast::Exists>()) if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &exists = formula.get<ast::Exists>(); auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::And>()) if (!exists.argument.is<ast::And>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &and_ = exists.argument.get<ast::And>(); auto &and_ = exists.argument.get<ast::And>();
auto &arguments = and_.arguments; auto &arguments = and_.arguments;
auto simplificationResult = SimplificationResult::Unchanged; auto simplificationResult = OperationResult::Unchanged;
for (auto i = exists.variables.begin(); i != exists.variables.end();) for (auto i = exists.variables.begin(); i != exists.variables.end();)
{ {
@ -225,7 +225,7 @@ struct SimplificationRuleAssignmentInExists
arguments.erase(j); arguments.erase(j);
wasVariableReplaced = true; wasVariableReplaced = true;
simplificationResult = SimplificationResult::Simplified; simplificationResult = OperationResult::Changed;
break; break;
} }
@ -249,19 +249,19 @@ struct SimplificationRuleEmptyConjunction
{ {
static constexpr const auto Description = "[empty conjunction] === #true"; static constexpr const auto Description = "[empty conjunction] === #true";
static SimplificationResult apply(ast::Formula &formula) static OperationResult apply(ast::Formula &formula)
{ {
if (!formula.is<ast::And>()) if (!formula.is<ast::And>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &and_ = formula.get<ast::And>(); auto &and_ = formula.get<ast::And>();
if (!and_.arguments.empty()) if (!and_.arguments.empty())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
formula = ast::Formula::make<ast::Boolean>(true); formula = ast::Formula::make<ast::Boolean>(true);
return SimplificationResult::Simplified; return OperationResult::Changed;
} }
}; };
@ -271,19 +271,19 @@ struct SimplificationRuleOneElementConjunction
{ {
static constexpr const auto Description = "[conjunction of only F] === F"; 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<ast::And>()) if (!formula.is<ast::And>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &and_ = formula.get<ast::And>(); auto &and_ = formula.get<ast::And>();
if (and_.arguments.size() != 1) if (and_.arguments.size() != 1)
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
formula = std::move(and_.arguments.front()); 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 constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
static SimplificationResult apply(ast::Formula &formula) static OperationResult apply(ast::Formula &formula)
{ {
if (!formula.is<ast::Exists>()) if (!formula.is<ast::Exists>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &exists = formula.get<ast::Exists>(); auto &exists = formula.get<ast::Exists>();
if (!exists.argument.is<ast::Boolean>()) if (!exists.argument.is<ast::Boolean>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
formula = std::move(exists.argument); 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 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<ast::In>()) if (!formula.is<ast::In>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &in = formula.get<ast::In>(); auto &in = formula.get<ast::In>();
assert(ast::isPrimitive(in.element)); assert(ast::isPrimitive(in.element));
if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set)) 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)); 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 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<ast::Biconditional>()) if (!formula.is<ast::Biconditional>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &biconditional = formula.get<ast::Biconditional>(); auto &biconditional = formula.get<ast::Biconditional>();
@ -353,7 +353,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
const auto rightIsAnd = biconditional.right.is<ast::And>(); const auto rightIsAnd = biconditional.right.is<ast::And>();
if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd)) if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right); auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left); auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
@ -367,13 +367,13 @@ struct SimplificationRuleSubsumptionInBiconditionals
}); });
if (matchingPredicate == and_.arguments.cend()) if (matchingPredicate == and_.arguments.cend())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
and_.arguments.erase(matchingPredicate); and_.arguments.erase(matchingPredicate);
formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide)); formula = ast::Formula::make<ast::Implies>(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 constexpr const auto Description = "not not F === F";
static SimplificationResult apply(ast::Formula &formula) static OperationResult apply(ast::Formula &formula)
{ {
if (!formula.is<ast::Not>()) if (!formula.is<ast::Not>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>(); auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Not>()) if (!not_.argument.is<ast::Not>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &notNot = not_.argument.get<ast::Not>(); auto &notNot = not_.argument.get<ast::Not>();
formula = std::move(notNot.argument); 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 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<ast::Not>()) if (!formula.is<ast::Not>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>(); auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::And>()) if (!not_.argument.is<ast::And>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &and_ = not_.argument.get<ast::And>(); auto &and_ = not_.argument.get<ast::And>();
@ -424,7 +424,7 @@ struct SimplificationRuleDeMorganForConjunctions
formula = ast::Formula::make<ast::Or>(std::move(and_.arguments)); formula = ast::Formula::make<ast::Or>(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 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<ast::Or>()) if (!formula.is<ast::Or>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &or_ = formula.get<ast::Or>(); auto &or_ = formula.get<ast::Or>();
if (or_.arguments.size() != 2) if (or_.arguments.size() != 2)
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
const auto leftIsNot = or_.arguments[0].is<ast::Not>(); const auto leftIsNot = or_.arguments[0].is<ast::Not>();
const auto rightIsNot = or_.arguments[1].is<ast::Not>(); const auto rightIsNot = or_.arguments[1].is<ast::Not>();
if (leftIsNot == rightIsNot) if (leftIsNot == rightIsNot)
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1]; auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0]; auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
@ -460,7 +460,7 @@ struct SimplificationRuleImplicationFromDisjunction
formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide)); formula = ast::Formula::make<ast::Implies>(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 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<ast::Not>()) if (!formula.is<ast::Not>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &not_ = formula.get<ast::Not>(); auto &not_ = formula.get<ast::Not>();
if (!not_.argument.is<ast::Comparison>()) if (!not_.argument.is<ast::Comparison>())
return SimplificationResult::Unchanged; return OperationResult::Unchanged;
auto &comparison = not_.argument.get<ast::Comparison>(); auto &comparison = not_.argument.get<ast::Comparison>();
@ -506,7 +506,7 @@ struct SimplificationRuleNegatedComparison
formula = std::move(comparison); formula = std::move(comparison);
return SimplificationResult::Simplified; return OperationResult::Changed;
} }
}; };
@ -535,7 +535,7 @@ const auto simplifyWithDefaultRules =
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor> struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
{ {
// Do nothing for all other types of expressions // Do nothing for all other types of expressions
static SimplificationResult accept(ast::Formula &formula) static OperationResult accept(ast::Formula &formula)
{ {
return simplifyWithDefaultRules(formula); return simplifyWithDefaultRules(formula);
} }
@ -545,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
void simplify(ast::Formula &formula) void simplify(ast::Formula &formula)
{ {
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified); while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
} }
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////