Iteratively apply simplification tableau rules
With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached.
This commit is contained in:
parent
c4c3156e77
commit
b88393655a
GPG Key ID:
05F3611E97A70ABF
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -12,6 +12,14 @@ namespace anthem
|
|||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class SimplificationResult
|
||||
{
|
||||
Simplified,
|
||||
Unchanged,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void simplify(ast::Formula &formula);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -0,0 +1,198 @@
|
|||
#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
|
||||
#define __ANTHEM__SIMPLIFICATION_VISITORS_H
|
||||
|
||||
#include <anthem/AST.h>
|
||||
#include <anthem/Simplification.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
namespace ast
|
||||
{
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
//
|
||||
// Simplification Visitor
|
||||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class T>
|
||||
struct FormulaSimplificationVisitor
|
||||
{
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : and_.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Not ¬_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : or_.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(formula, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class T, class SimplificationResult = void>
|
||||
struct TermSimplificationVisitor
|
||||
{
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
for (auto &argument : function.arguments)
|
||||
if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
|
||||
template <class... Arguments>
|
||||
SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
|
||||
{
|
||||
return T::accept(term, std::forward<Arguments>(arguments)...);
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
@ -3,7 +3,7 @@
|
|||
#include <optional>
|
||||
|
||||
#include <anthem/ASTCopy.h>
|
||||
#include <anthem/ASTVisitors.h>
|
||||
#include <anthem/SimplificationVisitors.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
|
|
@ -97,14 +97,6 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
|
|||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
enum class SimplificationResult
|
||||
{
|
||||
Simplified,
|
||||
Unchanged,
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class SimplificationRule>
|
||||
SimplificationResult simplify(ast::Formula &formula)
|
||||
{
|
||||
|
|
@ -113,13 +105,13 @@ SimplificationResult simplify(ast::Formula &formula)
|
|||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class SimplificationRule, class... OtherSimplificationRules>
|
||||
template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
|
||||
SimplificationResult simplify(ast::Formula &formula)
|
||||
{
|
||||
if (SimplificationRule::apply(formula) == SimplificationResult::Simplified)
|
||||
if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
|
||||
return SimplificationResult::Simplified;
|
||||
|
||||
return simplify<OtherSimplificationRules...>(formula);
|
||||
return simplify<SecondSimplificationRule, OtherSimplificationRules...>(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<SimplifyFormulaVisitor>
|
||||
struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
|
||||
{
|
||||
// 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<class T>
|
||||
static void accept(T &, ast::Formula &)
|
||||
static SimplificationResult accept(ast::Formula &formula)
|
||||
{
|
||||
return simplifyWithDefaultRules(formula);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -381,7 +361,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
|
|||
|
||||
void simplify(ast::Formula &formula)
|
||||
{
|
||||
formula.accept(SimplifyFormulaVisitor(), formula);
|
||||
while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
Loading…
Reference in New Issue