diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp index 52758e5..525d1d3 100644 --- a/src/anthem/Simplification.cpp +++ b/src/anthem/Simplification.cpp @@ -57,9 +57,10 @@ std::experimental::optional extractAssignedTerm(ast::Formula &formula //////////////////////////////////////////////////////////////////////////////////////////////////// -// Replaces all occurrences of a variable with a term in a given formula +// Replaces the first occurrence of a variable with a term in a given formula struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor { + // Perform replacement in predicates only static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, ast::Term &&term) { for (auto &argument : predicate.arguments) @@ -72,6 +73,7 @@ struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor static void accept(T &, ast::Formula &, const ast::Variable &, ast::Term &&) { @@ -165,6 +167,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor static void accept(T &, ast::Formula &) {