From ab71e8eb0a4e216945e24f086270201106ac6d5f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 4 Jun 2017 14:47:53 +0200 Subject: [PATCH] Minor refactoring. --- src/anthem/Simplification.cpp | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index f221306..a95caf9 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -15,19 +15,19 @@ namespace anthem //////////////////////////////////////////////////////////////////////////////////////////////////// // Determines whether a term is a specific variable -bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration *variableDeclaration) +bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration &variableDeclaration) { if (!term.is()) return false; - return term.get().declaration == variableDeclaration; + return term.get().declaration == &variableDeclaration; } //////////////////////////////////////////////////////////////////////////////////////////////////// // Extracts the term t if the given formula is of the form “X = t” and X matches the given variable // The input formula is not usable if a term is returned -std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration *variableDeclaration) +std::experimental::optional extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration) { if (!formula.is()) return std::experimental::nullopt; @@ -51,16 +51,16 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula // Replaces all occurrences of a variable in a given term with another term struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Variable &variable, ast::Term &term, const ast::VariableDeclaration *original, const ast::Term &replacement) + static void accept(ast::Variable &variable, ast::Term &term, const ast::VariableDeclaration &original, const ast::Term &replacement) { - if (variable.declaration == original) + if (variable.declaration == &original) // No dangling variables can result from this operation, and hence, fixing them is not necessary term = ast::prepareCopy(replacement); } // Ignore all other types of expressions template - static void accept(T &, ast::Term &, const ast::VariableDeclaration *, const ast::Term &) + static void accept(T &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &) { } }; @@ -70,19 +70,19 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor { - static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &replacement) + static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &original, const ast::Term &replacement) { comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); } - static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &term) + static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &original, const ast::Term &term) { in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, term); in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, term); } - static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration *original, const ast::Term &replacement) + static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &original, const ast::Term &replacement) { for (auto &argument : predicate.arguments) argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); @@ -90,7 +90,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor - static void accept(T &, ast::Formula &, const ast::VariableDeclaration *, const ast::Term &) + static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, const ast::Term &) { } }; @@ -110,7 +110,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula) // Simplify formulas of type “exists X (X = t and F(X))” to “F(t)” for (auto i = exists.variables.begin(); i != exists.variables.end();) { - const auto *variableDeclaration = i->get(); + const auto &variableDeclaration = **i; bool wasVariableReplaced = false;