From b88393655a20d44c308f557178d83f0878df3859 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 25 Mar 2018 23:49:39 +0200 Subject: [PATCH] Iteratively apply simplification tableau rules With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached. --- examples/schur-numbers.lp | 2 + include/anthem/Simplification.h | 8 + include/anthem/SimplificationVisitors.h | 198 ++++++++++++++++++++++++ src/anthem/Simplification.cpp | 58 +++---- 4 files changed, 227 insertions(+), 39 deletions(-) create mode 100644 include/anthem/SimplificationVisitors.h diff --git a/examples/schur-numbers.lp b/examples/schur-numbers.lp index eed2755..cdbbca9 100644 --- a/examples/schur-numbers.lp +++ b/examples/schur-numbers.lp @@ -3,3 +3,5 @@ covered(I) :- in(I, S). :- I = 1..n, not covered(I). :- in(I, S), in(J, S), in(I + J, S). + +#show in/2. diff --git a/include/anthem/Simplification.h b/include/anthem/Simplification.h index 162559f..2169971 100644 --- a/include/anthem/Simplification.h +++ b/include/anthem/Simplification.h @@ -12,6 +12,14 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// +enum class SimplificationResult +{ + Simplified, + Unchanged, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + void simplify(ast::Formula &formula); //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/SimplificationVisitors.h b/include/anthem/SimplificationVisitors.h new file mode 100644 index 0000000..bca0f30 --- /dev/null +++ b/include/anthem/SimplificationVisitors.h @@ -0,0 +1,198 @@ +#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H +#define __ANTHEM__SIMPLIFICATION_VISITORS_H + +#include +#include + +namespace anthem +{ +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Simplification Visitor +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct FormulaSimplificationVisitor +{ + template + SimplificationResult 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; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments) + { + if (biconditional.left.accept(*this, biconditional.left, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + if (biconditional.right.accept(*this, biconditional.right, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments) + { + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments) + { + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments) + { + if (exists.argument.accept(*this, exists.argument, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments) + { + if (forAll.argument.accept(*this, forAll.argument, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments) + { + if (implies.antecedent.accept(*this, implies.antecedent, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + if (implies.consequent.accept(*this, implies.consequent, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments) + { + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments) + { + if (not_.argument.accept(*this, not_.argument, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult 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; + + return T::accept(formula, std::forward(arguments)...); + } + + template + SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments) + { + return T::accept(formula, std::forward(arguments)...); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct TermSimplificationVisitor +{ + template + SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments) + { + if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult 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; + + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments) + { + if (interval.from.accept(*this, interval.from, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + if (interval.to.accept(*this, interval.to, std::forward(arguments)...) == SimplificationResult::Simplified) + return SimplificationResult::Simplified; + + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(String &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } + + template + SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments) + { + return T::accept(term, std::forward(arguments)...); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 2f2ab52..a7654ad 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -3,7 +3,7 @@ #include #include -#include +#include namespace anthem { @@ -97,14 +97,6 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor SimplificationResult simplify(ast::Formula &formula) { @@ -113,13 +105,13 @@ SimplificationResult simplify(ast::Formula &formula) //////////////////////////////////////////////////////////////////////////////////////////////////// -template +template SimplificationResult simplify(ast::Formula &formula) { - if (SimplificationRule::apply(formula) == SimplificationResult::Simplified) + if (simplify(formula) == SimplificationResult::Simplified) return SimplificationResult::Simplified; - return simplify(formula); + return simplify(formula); } //////////////////////////////////////////////////////////////////////////////////////////////////// @@ -341,39 +333,27 @@ struct SimplificationRuleInWithPrimitiveArguments //////////////////////////////////////////////////////////////////////////////////////////////////// -void simplify(ast::Exists &exists, ast::Formula &formula) -{ - SimplificationRuleTrivialAssignmentInExists::apply(formula); - SimplificationRuleAssignmentInExists::apply(formula); - - SimplificationRuleEmptyConjunction::apply(exists.argument); - SimplificationRuleTrivialExists::apply(formula); - SimplificationRuleOneElementConjunction::apply(exists.argument); - - SimplificationRuleExistsWithoutQuantifiedVariables::apply(formula); -} +const auto simplifyWithDefaultRules = + simplify + < + SimplificationRuleTrivialAssignmentInExists, + SimplificationRuleAssignmentInExists, + SimplificationRuleEmptyConjunction, + SimplificationRuleTrivialExists, + SimplificationRuleOneElementConjunction, + SimplificationRuleExistsWithoutQuantifiedVariables, + SimplificationRuleInWithPrimitiveArguments + >; //////////////////////////////////////////////////////////////////////////////////////////////////// // Performs the different simplification techniques -struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor +struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor { - // Forward exists statements to the dedicated simplification function - static void accept(ast::Exists &exists, ast::Formula &formula) - { - simplify(exists, formula); - } - - // Simplify formulas of type “A in B” to “A = B” if A and B are primitive - static void accept(ast::In &, ast::Formula &formula) - { - SimplificationRuleInWithPrimitiveArguments::apply(formula); - } - // Do nothing for all other types of expressions - template - static void accept(T &, ast::Formula &) + static SimplificationResult accept(ast::Formula &formula) { + return simplifyWithDefaultRules(formula); } }; @@ -381,7 +361,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor