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

Removed unnecessary namespace identifiers.

Browse Source
This commit is contained in:
Patrick Lühne 2017-05-30 18:13:31 +02:00
parent 664a57ec68
commit 1de0486989
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
4 changed files with 67 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
include/anthem/ASTUtils.h
View File

@ -20,14 +20,14 @@ namespace ast
class VariableStack class VariableStack
{ {
public: public:
using Layer = ast::VariableDeclarationPointers *; using Layer = VariableDeclarationPointers *;
public: public:
void push(Layer layer); void push(Layer layer);
void pop(); void pop();
std::experimental::optional<ast::VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const; std::experimental::optional<VariableDeclaration *> findUserVariableDeclaration(const char *variableName) const;
bool contains(const ast::VariableDeclaration &variableDeclaration) const; bool contains(const VariableDeclaration &variableDeclaration) const;
private: private:
std::vector<Layer> m_layers; std::vector<Layer> m_layers;
@ -35,11 +35,11 @@ class VariableStack
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula); std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula);
std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula, ast::VariableStack &variableStack); std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula, VariableStack &variableStack);
bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs); bool matches(const Predicate &lhs, const Predicate &rhs);
void collectPredicates(const ast::Formula &formula, std::vector<const ast::Predicate *> &predicates); void collectPredicates(const Formula &formula, std::vector<const Predicate *> &predicates);
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////

47
include/anthem/ASTVisitors.h
View File

@ -5,6 +5,8 @@
namespace anthem namespace anthem
{ {
namespace ast
{
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
// //
@ -12,16 +14,11 @@ namespace anthem
// //
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
namespace ast
{
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class T> template<class T>
struct RecursiveFormulaVisitor struct RecursiveFormulaVisitor
{ {
template <class... Arguments> template <class... Arguments>
void visit(ast::And &and_, ast::Formula &formula, Arguments &&... arguments) void visit(And &and_, Formula &formula, Arguments &&... arguments)
{ {
for (auto &argument : and_.arguments) for (auto &argument : and_.arguments)
argument.accept(*this, argument, std::forward<Arguments>(arguments)...); argument.accept(*this, argument, std::forward<Arguments>(arguments)...);
@ -30,7 +27,7 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Biconditional &biconditional, ast::Formula &formula, Arguments &&... arguments) void visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
{ {
biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...); biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...);
biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...); biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...);
@ -39,19 +36,19 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Boolean &boolean, ast::Formula &formula, Arguments &&... arguments) void visit(Boolean &boolean, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(boolean, formula, std::forward<Arguments>(arguments)...); return T::accept(boolean, formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Comparison &comparison, ast::Formula &formula, Arguments &&... arguments) void visit(Comparison &comparison, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(comparison, formula, std::forward<Arguments>(arguments)...); return T::accept(comparison, formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Exists &exists, ast::Formula &formula, Arguments &&... arguments) void visit(Exists &exists, Formula &formula, Arguments &&... arguments)
{ {
exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...); exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...);
@ -59,7 +56,7 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::ForAll &forAll, ast::Formula &formula, Arguments &&... arguments) void visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
{ {
forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...); forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...);
@ -67,7 +64,7 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Implies &implies, ast::Formula &formula, Arguments &&... arguments) void visit(Implies &implies, Formula &formula, Arguments &&... arguments)
{ {
implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...); implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...);
implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...); implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...);
@ -76,13 +73,13 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::In &in, ast::Formula &formula, Arguments &&... arguments) void visit(In &in, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(in, formula, std::forward<Arguments>(arguments)...); return T::accept(in, formula, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Not &not_, ast::Formula &formula, Arguments &&... arguments) void visit(Not &not_, Formula &formula, Arguments &&... arguments)
{ {
not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...); not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...);
@ -90,7 +87,7 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Or &or_, ast::Formula &formula, Arguments &&... arguments) void visit(Or &or_, Formula &formula, Arguments &&... arguments)
{ {
for (auto &argument : or_.arguments) for (auto &argument : or_.arguments)
argument.accept(*this, argument, std::forward<Arguments>(arguments)...); argument.accept(*this, argument, std::forward<Arguments>(arguments)...);
@ -99,7 +96,7 @@ struct RecursiveFormulaVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Predicate &predicate, ast::Formula &formula, Arguments &&... arguments) void visit(Predicate &predicate, Formula &formula, Arguments &&... arguments)
{ {
return T::accept(predicate, formula, std::forward<Arguments>(arguments)...); return T::accept(predicate, formula, std::forward<Arguments>(arguments)...);
} }
@ -112,7 +109,7 @@ struct RecursiveTermVisitor
{ {
// TODO: return type is incorrect // TODO: return type is incorrect
template <class... Arguments> template <class... Arguments>
void visit(ast::BinaryOperation &binaryOperation, ast::Term &term, Arguments &&... arguments) void visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
{ {
binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...); binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...);
binaryOperation.right.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...); binaryOperation.right.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...);
@ -121,19 +118,19 @@ struct RecursiveTermVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Boolean &boolean, ast::Term &term, Arguments &&... arguments) void visit(Boolean &boolean, Term &term, Arguments &&... arguments)
{ {
return T::accept(boolean, term, std::forward<Arguments>(arguments)...); return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Constant &constant, ast::Term &term, Arguments &&... arguments) void visit(Constant &constant, Term &term, Arguments &&... arguments)
{ {
return T::accept(constant, term, std::forward<Arguments>(arguments)...); return T::accept(constant, term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Function &function, ast::Term &term, Arguments &&... arguments) void visit(Function &function, Term &term, Arguments &&... arguments)
{ {
for (auto &argument : function.arguments) for (auto &argument : function.arguments)
argument.accept(*this, argument, std::forward<Arguments>(arguments)...); argument.accept(*this, argument, std::forward<Arguments>(arguments)...);
@ -142,13 +139,13 @@ struct RecursiveTermVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Integer &integer, ast::Term &term, Arguments &&... arguments) void visit(Integer &integer, Term &term, Arguments &&... arguments)
{ {
return T::accept(integer, term, std::forward<Arguments>(arguments)...); return T::accept(integer, term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Interval &interval, ast::Term &term, Arguments &&... arguments) void visit(Interval &interval, Term &term, Arguments &&... arguments)
{ {
interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...); interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...);
interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...); interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...);
@ -157,19 +154,19 @@ struct RecursiveTermVisitor
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::SpecialInteger &specialInteger, ast::Term &term, Arguments &&... arguments) void visit(SpecialInteger &specialInteger, Term &term, Arguments &&... arguments)
{ {
return T::accept(specialInteger, term, std::forward<Arguments>(arguments)...); return T::accept(specialInteger, term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::String &string, ast::Term &term, Arguments &&... arguments) void visit(String &string, Term &term, Arguments &&... arguments)
{ {
return T::accept(string, term, std::forward<Arguments>(arguments)...); return T::accept(string, term, std::forward<Arguments>(arguments)...);
} }
template <class... Arguments> template <class... Arguments>
void visit(ast::Variable &variable, ast::Term &term, Arguments &&... arguments) void visit(Variable &variable, Term &term, Arguments &&... arguments)
{ {
return T::accept(variable, term, std::forward<Arguments>(arguments)...); return T::accept(variable, term, std::forward<Arguments>(arguments)...);
} }

16
src/anthem/ASTCopy.cpp
View File

@ -21,9 +21,9 @@ namespace ast
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
// Replaces all occurrences of a variable in a given term with another term // Replaces all occurrences of a variable in a given term with another term
struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVariableInTermVisitor> struct ReplaceVariableInTermVisitor : public RecursiveTermVisitor<ReplaceVariableInTermVisitor>
{ {
static void accept(ast::Variable &variable, ast::Term &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) static void accept(Variable &variable, Term &, const VariableDeclaration *original, VariableDeclaration *replacement)
{ {
if (variable.declaration == original) if (variable.declaration == original)
variable.declaration = replacement; variable.declaration = replacement;
@ -31,7 +31,7 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVa
// Ignore all other types of expressions // Ignore all other types of expressions
template<class T> template<class T>
static void accept(T &, ast::Term &, const ast::VariableDeclaration *, ast::VariableDeclaration *) static void accept(T &, Term &, const VariableDeclaration *, VariableDeclaration *)
{ {
} }
}; };
@ -39,21 +39,21 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVa
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
// Replaces all occurrences of a variable in a given formula with a term // Replaces all occurrences of a variable in a given formula with a term
struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor> struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
{ {
static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) static void accept(Comparison &comparison, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
{ {
comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement); comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement);
comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement); comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement);
} }
static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) static void accept(In &in, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
{ {
in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement); in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement);
in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement); in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement);
} }
static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement) static void accept(Predicate &predicate, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
{ {
for (auto &argument : predicate.arguments) for (auto &argument : predicate.arguments)
argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement); argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement);
@ -61,7 +61,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
// Ignore all other types of expressions // Ignore all other types of expressions
template<class T> template<class T>
static void accept(T &, ast::Formula &, const ast::VariableDeclaration *, ast::VariableDeclaration *) static void accept(T &, Formula &, const VariableDeclaration *, VariableDeclaration *)
{ {
} }
}; };

60
src/anthem/ASTUtils.cpp
View File

@ -27,7 +27,7 @@ void VariableStack::pop()
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
std::experimental::optional<ast::VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const std::experimental::optional<VariableDeclaration *> VariableStack::findUserVariableDeclaration(const char *variableName) const
{ {
const auto variableDeclarationMatches = const auto variableDeclarationMatches =
[&variableName](const auto &variableDeclaration) [&variableName](const auto &variableDeclaration)
@ -50,7 +50,7 @@ std::experimental::optional<ast::VariableDeclaration *> VariableStack::findUserV
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
bool VariableStack::contains(const ast::VariableDeclaration &variableDeclaration) const bool VariableStack::contains(const VariableDeclaration &variableDeclaration) const
{ {
const auto variableDeclarationMatches = const auto variableDeclarationMatches =
[&variableDeclaration](const auto &other) [&variableDeclaration](const auto &other)
@ -75,66 +75,66 @@ struct CollectFreeVariablesVisitor
// Formulas // Formulas
//////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////
void visit(ast::And &and_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(And &and_, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
for (auto &argument : and_.arguments) for (auto &argument : and_.arguments)
argument.accept(*this, variableStack, freeVariables); argument.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Biconditional &biconditional, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Biconditional &biconditional, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
biconditional.left.accept(*this, variableStack, freeVariables); biconditional.left.accept(*this, variableStack, freeVariables);
biconditional.right.accept(*this, variableStack, freeVariables); biconditional.right.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Boolean &, VariableStack &, std::vector<ast::VariableDeclaration *> &) void visit(Boolean &, VariableStack &, std::vector<VariableDeclaration *> &)
{ {
} }
void visit(ast::Comparison &comparison, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Comparison &comparison, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
comparison.left.accept(*this, variableStack, freeVariables); comparison.left.accept(*this, variableStack, freeVariables);
comparison.right.accept(*this, variableStack, freeVariables); comparison.right.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Exists &exists, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Exists &exists, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
variableStack.push(&exists.variables); variableStack.push(&exists.variables);
exists.argument.accept(*this, variableStack, freeVariables); exists.argument.accept(*this, variableStack, freeVariables);
variableStack.pop(); variableStack.pop();
} }
void visit(ast::ForAll &forAll, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(ForAll &forAll, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
variableStack.push(&forAll.variables); variableStack.push(&forAll.variables);
forAll.argument.accept(*this, variableStack, freeVariables); forAll.argument.accept(*this, variableStack, freeVariables);
variableStack.pop(); variableStack.pop();
} }
void visit(ast::Implies &implies, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Implies &implies, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
implies.antecedent.accept(*this, variableStack, freeVariables); implies.antecedent.accept(*this, variableStack, freeVariables);
implies.consequent.accept(*this, variableStack, freeVariables); implies.consequent.accept(*this, variableStack, freeVariables);
} }
void visit(ast::In &in, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(In &in, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
in.element.accept(*this, variableStack, freeVariables); in.element.accept(*this, variableStack, freeVariables);
in.set.accept(*this, variableStack, freeVariables); in.set.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Not &not_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Not &not_, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
not_.argument.accept(*this, variableStack, freeVariables); not_.argument.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Or &or_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Or &or_, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
for (auto &argument : or_.arguments) for (auto &argument : or_.arguments)
argument.accept(*this, variableStack, freeVariables); argument.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Predicate &predicate, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Predicate &predicate, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
for (auto &argument : predicate.arguments) for (auto &argument : predicate.arguments)
argument.accept(*this, variableStack, freeVariables); argument.accept(*this, variableStack, freeVariables);
@ -144,41 +144,41 @@ struct CollectFreeVariablesVisitor
// Terms // Terms
//////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////
void visit(ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
binaryOperation.left.accept(*this, variableStack, freeVariables); binaryOperation.left.accept(*this, variableStack, freeVariables);
binaryOperation.right.accept(*this, variableStack, freeVariables); binaryOperation.right.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Constant &, VariableStack &, std::vector<ast::VariableDeclaration *> &) void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
{ {
} }
void visit(ast::Function &function, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
for (auto &argument : function.arguments) for (auto &argument : function.arguments)
argument.accept(*this, variableStack, freeVariables); argument.accept(*this, variableStack, freeVariables);
} }
void visit(ast::Integer &, VariableStack &, std::vector<ast::VariableDeclaration *> &) void visit(Integer &, VariableStack &, std::vector<VariableDeclaration *> &)
{ {
} }
void visit(ast::Interval &interval, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Interval &interval, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
interval.from.accept(*this, variableStack, freeVariables); interval.from.accept(*this, variableStack, freeVariables);
interval.to.accept(*this, variableStack, freeVariables); interval.to.accept(*this, variableStack, freeVariables);
} }
void visit(ast::SpecialInteger &, VariableStack &, std::vector<ast::VariableDeclaration *> &) void visit(SpecialInteger &, VariableStack &, std::vector<VariableDeclaration *> &)
{ {
} }
void visit(ast::String &, VariableStack &, std::vector<ast::VariableDeclaration *> &) void visit(String &, VariableStack &, std::vector<VariableDeclaration *> &)
{ {
} }
void visit(ast::Variable &variable, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables) void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
{ {
if (variableStack.contains(*variable.declaration)) if (variableStack.contains(*variable.declaration))
return; return;
@ -192,17 +192,17 @@ struct CollectFreeVariablesVisitor
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula) std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula)
{ {
ast::VariableStack variableStack; VariableStack variableStack;
return collectFreeVariables(formula, variableStack); return collectFreeVariables(formula, variableStack);
} }
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula, ast::VariableStack &variableStack) std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula, VariableStack &variableStack)
{ {
std::vector<ast::VariableDeclaration *> freeVariables; std::vector<VariableDeclaration *> freeVariables;
formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables); formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables);
@ -213,7 +213,7 @@ std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formu
struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicatesVisitor> struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicatesVisitor>
{ {
static void accept(const ast::Predicate &predicate, const ast::Formula &, std::vector<const ast::Predicate *> &predicates) static void accept(const Predicate &predicate, const Formula &, std::vector<const Predicate *> &predicates)
{ {
const auto predicateMatches = const auto predicateMatches =
[&predicate](const auto *otherPredicate) [&predicate](const auto *otherPredicate)
@ -227,14 +227,14 @@ struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicat
// Ignore all other types of expressions // Ignore all other types of expressions
template<class T> template<class T>
static void accept(const T &, const ast::Formula &, std::vector<const ast::Predicate *> &) static void accept(const T &, const Formula &, std::vector<const Predicate *> &)
{ {
} }
}; };
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs) bool matches(const Predicate &lhs, const Predicate &rhs)
{ {
return (lhs.name == rhs.name && lhs.arity() == rhs.arity()); return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
} }
@ -242,9 +242,9 @@ bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs)
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
// TODO: remove const_cast // TODO: remove const_cast
void collectPredicates(const ast::Formula &formula, std::vector<const ast::Predicate *> &predicates) void collectPredicates(const Formula &formula, std::vector<const Predicate *> &predicates)
{ {
auto &formulaMutable = const_cast<ast::Formula &>(formula); auto &formulaMutable = const_cast<Formula &>(formula);
formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates); formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates);
} }