patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Minor clarifications in simplification code annotations.

Browse Source
This commit is contained in:
Patrick Lühne 2017-03-23 13:44:55 +01:00
parent 188a24f5b5
commit 574130a8ec
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/anthem/Simplification.cpp
View File

@ -57,9 +57,10 @@ std::experimental::optional<ast::Term> 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<ReplaceVariableWithTermVisitor> struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor<ReplaceVariableWithTermVisitor>
{ {
// Perform replacement in predicates only
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, ast::Term &&term) static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, ast::Term &&term)
{ {
for (auto &argument : predicate.arguments) for (auto &argument : predicate.arguments)
@ -72,6 +73,7 @@ struct ReplaceVariableWithTermVisitor : public ast::RecursiveFormulaVisitor<Repl
} }
} }
// Ignore all other types of expressions
template<class T> template<class T>
static void accept(T &, ast::Formula &, const ast::Variable &, ast::Term &&) static void accept(T &, ast::Formula &, const ast::Variable &, ast::Term &&)
{ {
@ -165,6 +167,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set)); formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
} }
// Do nothing for all other types of expressions
template<class T> template<class T>
static void accept(T &, ast::Formula &) static void accept(T &, ast::Formula &)
{ {