From cae09487638daee761ea478dd425747feb6db534 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 23 Mar 2017 15:02:06 +0100 Subject: [PATCH] Completed implementing simplification with deep variable replacement. --- include/anthem/ASTVisitors.h | 69 +++++++++++++++++++++++++++++++ src/anthem/Simplification.cpp | 77 ++++++++++++++++++++--------------- 2 files changed, 114 insertions(+), 32 deletions(-) diff --git a/include/anthem/ASTVisitors.h b/include/anthem/ASTVisitors.h index 5d603b7..49db5d7 100644 --- a/include/anthem/ASTVisitors.h +++ b/include/anthem/ASTVisitors.h @@ -107,6 +107,75 @@ struct RecursiveFormulaVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// +template +struct RecursiveTermVisitor +{ + template + void visit(ast::BinaryOperation &binaryOperation, ast::Term &term, Arguments &&... arguments) + { + binaryOperation.left.accept(*this, binaryOperation.left, std::forward(arguments)...); + binaryOperation.right.accept(*this, binaryOperation.left, std::forward(arguments)...); + + return T::accept(binaryOperation, term, std::forward(arguments)...); + } + + template + void visit(ast::Boolean &boolean, ast::Term &term, Arguments &&... arguments) + { + return T::accept(boolean, term, std::forward(arguments)...); + } + + template + void visit(ast::Constant &constant, ast::Term &term, Arguments &&... arguments) + { + return T::accept(constant, term, std::forward(arguments)...); + } + + template + void visit(ast::Function &function, ast::Term &term, Arguments &&... arguments) + { + for (auto &argument : function.arguments) + argument.accept(*this, argument, std::forward(arguments)...); + + return T::accept(function, term, std::forward(arguments)...); + } + + template + void visit(ast::Integer &integer, ast::Term &term, Arguments &&... arguments) + { + return T::accept(integer, term, std::forward(arguments)...); + } + + template + void visit(ast::Interval &interval, ast::Term &term, Arguments &&... arguments) + { + interval.from.accept(*this, interval.from, std::forward(arguments)...); + interval.to.accept(*this, interval.to, std::forward(arguments)...); + + return T::accept(interval, term, std::forward(arguments)...); + } + + template + void visit(ast::SpecialInteger &specialInteger, ast::Term &term, Arguments &&... arguments) + { + return T::accept(specialInteger, term, std::forward(arguments)...); + } + + template + void visit(ast::String &string, ast::Term &term, Arguments &&... arguments) + { + return T::accept(string, term, std::forward(arguments)...); + } + + template + void visit(ast::Variable &variable, ast::Term &term, Arguments &&... arguments) + { + return T::accept(variable, term, std::forward(arguments)...); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } } diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index f03a19a..ae57a14 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -57,42 +57,48 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula //////////////////////////////////////////////////////////////////////////////////////////////////// -// Replaces all occurrences of a variable with a term in a given formula -struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor +// Replaces all occurrences of a variable in a given term with another term +struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Comparison &comparison, ast::Formula &, const ast::Variable &variable, ast::Term &term) + static void accept(ast::Variable &variable, ast::Term &term, const ast::Variable &variableToReplace, const ast::Term &replacementTerm) { - if (matchesVariable(comparison.left, variable)) - comparison.left = ast::deepCopy(term); - - if (matchesVariable(comparison.right, variable)) - comparison.right = ast::deepCopy(term); - } - - static void accept(ast::In &in, ast::Formula &, const ast::Variable &variable, ast::Term &term) - { - if (matchesVariable(in.element, variable)) - in.element = ast::deepCopy(term); - - if (matchesVariable(in.set, variable)) - in.set = ast::deepCopy(term); - } - - static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, ast::Term &term) - { - for (auto &argument : predicate.arguments) - { - if (!matchesVariable(argument, variable)) - continue; - - // TODO: optimize (one less deep copy possible) - argument = ast::deepCopy(term); - } + if (variable.name == variableToReplace.name) + term = ast::deepCopy(replacementTerm); } // Ignore all other types of expressions template - static void accept(T &, ast::Formula &, const ast::Variable &, ast::Term &) + static void accept(T &, ast::Term &, const ast::Variable &, const ast::Term &) + { + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +// Replaces all occurrences of a variable in a given formula with a term +struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor +{ + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + { + comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variable, term); + comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.left, variable, term); + } + + static void accept(ast::In &in, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + { + in.element.accept(ReplaceVariableInTermVisitor(), in.element, variable, term); + in.set.accept(ReplaceVariableInTermVisitor(), in.set, variable, term); + } + + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, const ast::Term &term) + { + for (auto &argument : predicate.arguments) + argument.accept(ReplaceVariableInTermVisitor(), argument, variable, term); + } + + // Ignore all other types of expressions + template + static void accept(T &, ast::Formula &, const ast::Variable &, const ast::Term &) { } }; @@ -116,6 +122,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) bool wasVariableReplaced = false; + // TODO: refactor for (auto j = arguments.begin(); j != arguments.end(); j++) { auto &argument = *j; @@ -126,8 +133,14 @@ void simplify(ast::Exists &exists, ast::Formula &formula) continue; // Replace all occurrences of the variable with the equivalent term - for (auto &otherArgument : arguments) - otherArgument.accept(ReplaceVariableWithTermVisitor(), otherArgument, variable, assignedTerm.value()); + for (auto k = arguments.begin(); k != arguments.end(); k++) + { + if (k == j) + continue; + + auto &otherArgument = *k; + otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variable, assignedTerm.value()); + } arguments.erase(j); wasVariableReplaced = true;