From ddbd4061e43c77f7423a094fef9086c81854ca04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 23 Mar 2017 13:28:09 +0100 Subject: [PATCH] Moved recursive formula visitor to separate header file. --- include/anthem/ASTVisitors.h | 113 ++++++++++++++++++++++++++++++++++ src/anthem/Simplification.cpp | 96 ++--------------------------- 2 files changed, 117 insertions(+), 92 deletions(-) create mode 100644 include/anthem/ASTVisitors.h diff --git a/include/anthem/ASTVisitors.h b/include/anthem/ASTVisitors.h new file mode 100644 index 0000000..5d603b7 --- /dev/null +++ b/include/anthem/ASTVisitors.h @@ -0,0 +1,113 @@ +#ifndef __ANTHEM__AST_VISITORS_H +#define __ANTHEM__AST_VISITORS_H + +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// AST Visitors +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +namespace ast +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct RecursiveFormulaVisitor +{ + template + void visit(ast::And &and_, ast::Formula &formula, Arguments &&... arguments) + { + for (auto &argument : and_.arguments) + argument.accept(*this, argument, std::forward(arguments)...); + + return T::accept(and_, formula, std::forward(arguments)...); + } + + template + void visit(ast::Biconditional &biconditional, ast::Formula &formula, Arguments &&... arguments) + { + biconditional.left.accept(*this, biconditional.left, std::forward(arguments)...); + biconditional.right.accept(*this, biconditional.right, std::forward(arguments)...); + + return T::accept(biconditional, formula, std::forward(arguments)...); + } + + template + void visit(ast::Boolean &boolean, ast::Formula &formula, Arguments &&... arguments) + { + return T::accept(boolean, formula, std::forward(arguments)...); + } + + template + void visit(ast::Comparison &comparison, ast::Formula &formula, Arguments &&... arguments) + { + return T::accept(comparison, formula, std::forward(arguments)...); + } + + template + void visit(ast::Exists &exists, ast::Formula &formula, Arguments &&... arguments) + { + exists.argument.accept(*this, exists.argument, std::forward(arguments)...); + + return T::accept(exists, formula, std::forward(arguments)...); + } + + template + void visit(ast::ForAll &forAll, ast::Formula &formula, Arguments &&... arguments) + { + forAll.argument.accept(*this, forAll.argument, std::forward(arguments)...); + + return T::accept(forAll, formula, std::forward(arguments)...); + } + + template + void visit(ast::Implies &implies, ast::Formula &formula, Arguments &&... arguments) + { + implies.antecedent.accept(*this, implies.antecedent, std::forward(arguments)...); + implies.consequent.accept(*this, implies.consequent, std::forward(arguments)...); + + return T::accept(implies, formula, std::forward(arguments)...); + } + + template + void visit(ast::In &in, ast::Formula &formula, Arguments &&... arguments) + { + return T::accept(in, formula, std::forward(arguments)...); + } + + template + void visit(ast::Not ¬_, ast::Formula &formula, Arguments &&... arguments) + { + not_.argument.accept(*this, not_.argument, std::forward(arguments)...); + + return T::accept(not_, formula, std::forward(arguments)...); + } + + template + void visit(ast::Or &or_, ast::Formula &formula, Arguments &&... arguments) + { + for (auto &argument : or_.arguments) + argument.accept(*this, argument, std::forward(arguments)...); + + return T::accept(or_, formula, std::forward(arguments)...); + } + + template + void visit(ast::Predicate &predicate, ast::Formula &formula, Arguments &&... arguments) + { + return T::accept(predicate, formula, std::forward(arguments)...); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} +} + +#endif diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index e6f16b7..c05f5ba 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -1,5 +1,7 @@ #include +#include + namespace anthem { @@ -16,96 +18,6 @@ bool isPrimitiveTerm(const ast::Term &term) //////////////////////////////////////////////////////////////////////////////////////////////////// -template -struct RecursiveFormulaVisitor -{ - template - void visit(ast::And &and_, ast::Formula &formula, Arguments &&... arguments) - { - for (auto &argument : and_.arguments) - argument.accept(*this, argument, std::forward(arguments)...); - - return T::accept(and_, formula, std::forward(arguments)...); - } - - template - void visit(ast::Biconditional &biconditional, ast::Formula &formula, Arguments &&... arguments) - { - biconditional.left.accept(*this, biconditional.left, std::forward(arguments)...); - biconditional.right.accept(*this, biconditional.right, std::forward(arguments)...); - - return T::accept(biconditional, formula, std::forward(arguments)...); - } - - template - void visit(ast::Boolean &boolean, ast::Formula &formula, Arguments &&... arguments) - { - return T::accept(boolean, formula, std::forward(arguments)...); - } - - template - void visit(ast::Comparison &comparison, ast::Formula &formula, Arguments &&... arguments) - { - return T::accept(comparison, formula, std::forward(arguments)...); - } - - template - void visit(ast::Exists &exists, ast::Formula &formula, Arguments &&... arguments) - { - exists.argument.accept(*this, exists.argument, std::forward(arguments)...); - - return T::accept(exists, formula, std::forward(arguments)...); - } - - template - void visit(ast::ForAll &forAll, ast::Formula &formula, Arguments &&... arguments) - { - forAll.argument.accept(*this, forAll.argument, std::forward(arguments)...); - - return T::accept(forAll, formula, std::forward(arguments)...); - } - - template - void visit(ast::Implies &implies, ast::Formula &formula, Arguments &&... arguments) - { - implies.antecedent.accept(*this, implies.antecedent, std::forward(arguments)...); - implies.consequent.accept(*this, implies.consequent, std::forward(arguments)...); - - return T::accept(implies, formula, std::forward(arguments)...); - } - - template - void visit(ast::In &in, ast::Formula &formula, Arguments &&... arguments) - { - return T::accept(in, formula, std::forward(arguments)...); - } - - template - void visit(ast::Not ¬_, ast::Formula &formula, Arguments &&... arguments) - { - not_.argument.accept(*this, not_.argument, std::forward(arguments)...); - - return T::accept(not_, formula, std::forward(arguments)...); - } - - template - void visit(ast::Or &or_, ast::Formula &formula, Arguments &&... arguments) - { - for (auto &argument : or_.arguments) - argument.accept(*this, argument, std::forward(arguments)...); - - return T::accept(or_, formula, std::forward(arguments)...); - } - - template - void visit(ast::Predicate &predicate, ast::Formula &formula, Arguments &&... arguments) - { - return T::accept(predicate, formula, std::forward(arguments)...); - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - bool matchesVariable(const ast::Term &term, const ast::Variable &variable) { if (!term.is()) @@ -139,7 +51,7 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula //////////////////////////////////////////////////////////////////////////////////////////////////// -struct ReplaceVariableWithTermVisitor : public RecursiveFormulaVisitor +struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor { static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, ast::Term &&term) { @@ -226,7 +138,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) //////////////////////////////////////////////////////////////////////////////////////////////////// -struct SimplifyFormulaVisitor : public RecursiveFormulaVisitor +struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor { static void accept(ast::Exists &exists, ast::Formula &formula) {