From 574130a8ec2549f00f6af7ad347d072f965bd36b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 23 Mar 2017 13:44:55 +0100 Subject: [PATCH] Minor clarifications in simplification code annotations. --- src/anthem/Simplification.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 &) {