Major refactoring to uniquely link variables to their declarations (breaks simplification and completion).

2017-05-30 03:53:51 +02:00
parent ce159c7bf0
commit 1c925d661b
23 changed files with 1176 additions and 659 deletions
--- a/src/anthem/ASTCopy.cpp
+++ b/src/anthem/ASTCopy.cpp
@@ -0,0 +1,498 @@
+#include <anthem/ASTCopy.h>
+
+#include <map>
+
+#include <anthem/ASTUtils.h>
+#include <anthem/ASTVisitors.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// ASTCopy
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Replacing Variables
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Replaces all occurrences of a variable in a given term with another term
+struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVariableInTermVisitor>
+{
+	static void accept(ast::Variable &variable, ast::Term &, const ast::VariableDeclaration *original, ast::VariableDeclaration *replacement)
+	{
+		if (variable.declaration == original)
+			variable.declaration = replacement;
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(T &, ast::Term &, const ast::VariableDeclaration *, ast::VariableDeclaration *)
+	{
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Replaces all occurrences of a variable in a given formula with a term
+struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
+{
+	static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration *original, ast::VariableDeclaration *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, ast::VariableDeclaration *replacement)
+	{
+		in.element.accept(ReplaceVariableInTermVisitor(), in.element, 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)
+	{
+		for (auto &argument : predicate.arguments)
+			argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement);
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(T &, ast::Formula &, const ast::VariableDeclaration *, ast::VariableDeclaration *)
+	{
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Preparing Copying
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class Variant>
+struct VariantDeepCopyVisitor
+{
+	template<class T>
+	Variant visit(const T &x)
+	{
+		return prepareCopy(x);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class T>
+std::unique_ptr<T> prepareCopy(const std::unique_ptr<T> &uniquePtr)
+{
+	return std::make_unique<T>(prepareCopy(*uniquePtr));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto prepareCopyVariant =
+	[](const auto &variant) -> typename std::decay<decltype(variant)>::type
+	{
+		using VariantType = typename std::decay<decltype(variant)>::type;
+
+		return variant.accept(VariantDeepCopyVisitor<VariantType>());
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto prepareCopyVariantVector =
+	[](const auto &variantVector) -> typename std::decay<decltype(variantVector)>::type
+	{
+		using Type = typename std::decay<decltype(variantVector)>::type::value_type;
+
+		std::vector<Type> result;
+		result.reserve(variantVector.size());
+
+		for (const auto &variant : variantVector)
+			result.emplace_back(prepareCopyVariant(variant));
+
+		return result;
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto prepareCopyVector =
+	[](const auto &vector) -> typename std::decay<decltype(vector)>::type
+	{
+		using Type = typename std::decay<decltype(vector)>::type::value_type;
+
+		std::vector<Type> result;
+		result.reserve(vector.size());
+
+		for (const auto &element : vector)
+			result.emplace_back(prepareCopy(element));
+
+		return result;
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+BinaryOperation prepareCopy(const BinaryOperation &other)
+{
+	return BinaryOperation(other.operator_, prepareCopy(other.left), prepareCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Boolean prepareCopy(const Boolean &other)
+{
+	return Boolean(other.value);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Comparison prepareCopy(const Comparison &other)
+{
+	return Comparison(other.operator_, prepareCopy(other.left), prepareCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Constant prepareCopy(const Constant &other)
+{
+	return Constant(std::string(other.name));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Function prepareCopy(const Function &other)
+{
+	return Function(std::string(other.name), prepareCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+In prepareCopy(const In &other)
+{
+	return In(prepareCopy(other.element), prepareCopy(other.set));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Integer prepareCopy(const Integer &other)
+{
+	return Integer(other.value);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Interval prepareCopy(const Interval &other)
+{
+	return Interval(prepareCopy(other.from), prepareCopy(other.to));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Predicate prepareCopy(const Predicate &other)
+{
+	return Predicate(std::string(other.name), prepareCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+SpecialInteger prepareCopy(const SpecialInteger &other)
+{
+	return SpecialInteger(other.type);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+String prepareCopy(const String &other)
+{
+	return String(std::string(other.text));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Variable prepareCopy(const Variable &other)
+{
+	return Variable(other.declaration);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+VariableDeclaration prepareCopy(const VariableDeclaration &other)
+{
+	return VariableDeclaration(std::string(other.name), other.type);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+VariableDeclarationPointers prepareCopy(const VariableDeclarationPointers &other)
+{
+	return prepareCopyVector(other);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+And prepareCopy(const And &other)
+{
+	return And(prepareCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Biconditional prepareCopy(const Biconditional &other)
+{
+	return Biconditional(prepareCopy(other.left), prepareCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Exists prepareCopy(const Exists &other)
+{
+	Exists copy(prepareCopy(other.variables), prepareCopy(other.argument));
+
+	// TODO: refactor
+	for (size_t i = 0; i < other.variables.size(); i++)
+		copy.argument.accept(ReplaceVariableInFormulaVisitor(), copy.argument, other.variables[i].get(), copy.variables[i].get());
+
+	return copy;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ForAll prepareCopy(const ForAll &other)
+{
+	ForAll copy(prepareCopy(other.variables), prepareCopy(other.argument));
+
+	// TODO: refactor
+	for (size_t i = 0; i < other.variables.size(); i++)
+		copy.argument.accept(ReplaceVariableInFormulaVisitor(), copy.argument, other.variables[i].get(), copy.variables[i].get());
+
+	return copy;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Implies prepareCopy(const Implies &other)
+{
+	return Implies(prepareCopy(other.antecedent), prepareCopy(other.consequent));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Not prepareCopy(const Not &other)
+{
+	return Not(prepareCopy(other.argument));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Or prepareCopy(const Or &other)
+{
+	return Or(prepareCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Formula prepareCopy(const Formula &formula)
+{
+	return prepareCopyVariant(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Term prepareCopy(const Term &term)
+{
+	return prepareCopyVariant(term);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+std::vector<Term> prepareCopy(const std::vector<Term> &terms)
+{
+	return prepareCopyVariantVector(terms);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+std::vector<Formula> prepareCopy(const std::vector<Formula> &formulas)
+{
+	return prepareCopyVariantVector(formulas);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Fixing Dangling Variables
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Fix all dangling variables in a given term
+struct FixDanglingVariablesInTermVisitor
+{
+	template <class... Arguments>
+	void visit(BinaryOperation &binaryOperation, Arguments &&... arguments)
+	{
+		binaryOperation.left.accept(*this, std::forward<Arguments>(arguments)...);
+		binaryOperation.right.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Boolean &, Arguments &&...)
+	{
+	}
+
+	template <class... Arguments>
+	void visit(Constant &, Arguments &&...)
+	{
+	}
+
+	template <class... Arguments>
+	void visit(Function &function, Arguments &&... arguments)
+	{
+		for (auto &argument : function.arguments)
+			argument.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Integer &, Arguments &&...)
+	{
+	}
+
+	template <class... Arguments>
+	void visit(Interval &interval, Arguments &&... arguments)
+	{
+		interval.from.accept(*this, std::forward<Arguments>(arguments)...);
+		interval.to.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(SpecialInteger &, Arguments &&...)
+	{
+	}
+
+	template <class... Arguments>
+	void visit(String &, Arguments &&...)
+	{
+	}
+
+	void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
+		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
+	{
+		const auto match = replacements.find(variable.declaration);
+
+		// Replace the variable if it is flagged for replacement
+		if (match != replacements.cend())
+		{
+			variable.declaration = match->second;
+			return;
+		}
+
+		// If the variable is not flagged for replacement yet, check whether it is dangling
+		const auto isVariableDangling = !variableStack.contains(*variable.declaration);
+
+		if (!isVariableDangling)
+			return;
+
+		// If the variable is dangling, declare it correctly and flag it for future replacement
+		auto newVariableDeclaration = std::make_unique<VariableDeclaration>(std::string(variable.declaration->name), variable.declaration->type);
+		scopedFormula.freeVariables.emplace_back(std::move(newVariableDeclaration));
+
+		replacements[variable.declaration] = scopedFormula.freeVariables.back().get();
+		variable.declaration = scopedFormula.freeVariables.back().get();
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Fix all dangling variables in a given formula
+struct FixDanglingVariablesInFormulaVisitor
+{
+	template <class... Arguments>
+	void visit(And &and_, Arguments &&... arguments)
+	{
+		for (auto &argument : and_.arguments)
+			argument.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Biconditional &biconditional, Arguments &&... arguments)
+	{
+		biconditional.left.accept(*this, std::forward<Arguments>(arguments)...);
+		biconditional.right.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Boolean &, Arguments &&...)
+	{
+	}
+
+	template <class... Arguments>
+	void visit(Comparison &comparison, Arguments &&... arguments)
+	{
+		comparison.left.accept(FixDanglingVariablesInTermVisitor(), std::forward<Arguments>(arguments)...);
+		comparison.right.accept(FixDanglingVariablesInTermVisitor(), std::forward<Arguments>(arguments)...);
+	}
+
+	void visit(Exists &exists, ScopedFormula &scopedFormula, VariableStack &variableStack,
+		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
+	{
+		variableStack.push(&exists.variables);
+		exists.argument.accept(*this, scopedFormula, variableStack, replacements);
+		variableStack.pop();
+	}
+
+	void visit(ForAll &forAll, ScopedFormula &scopedFormula, VariableStack &variableStack,
+		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
+	{
+		variableStack.push(&forAll.variables);
+		forAll.argument.accept(*this, scopedFormula, variableStack, replacements);
+		variableStack.pop();
+	}
+
+	template <class... Arguments>
+	void visit(Implies &implies, Arguments &&... arguments)
+	{
+		implies.antecedent.accept(*this, std::forward<Arguments>(arguments)...);
+		implies.consequent.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(In &in, Arguments &&... arguments)
+	{
+		in.element.accept(FixDanglingVariablesInTermVisitor(), std::forward<Arguments>(arguments)...);
+		in.set.accept(FixDanglingVariablesInTermVisitor(), std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Not &not_, Arguments &&... arguments)
+	{
+		not_.argument.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Or &or_, Arguments &&... arguments)
+	{
+		for (auto &argument : or_.arguments)
+			argument.accept(*this, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	void visit(Predicate &predicate, Arguments &&... arguments)
+	{
+		for (auto &argument : predicate.arguments)
+			argument.accept(FixDanglingVariablesInTermVisitor(), std::forward<Arguments>(arguments)...);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void fixDanglingVariables(ScopedFormula &scopedFormula)
+{
+	VariableStack variableStack;
+	variableStack.push(&scopedFormula.freeVariables);
+
+	std::map<VariableDeclaration *, VariableDeclaration *> replacements;
+
+	scopedFormula.formula.accept(FixDanglingVariablesInFormulaVisitor(), scopedFormula,
+		variableStack, replacements);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
--- a/src/anthem/ASTUtils.cpp
+++ b/src/anthem/ASTUtils.cpp
@@ -27,21 +27,43 @@ void VariableStack::pop()

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-bool VariableStack::contains(const ast::Variable &variable) const
+std::experimental::optional<ast::VariableDeclaration *> VariableStack::findVariableDeclaration(const char *variableName) const
 {
-	const auto variableMatches =
-		[&variable](const auto &otherVariable)
+	const auto variableNameMatches =
+		[&variableName](const auto &variableDeclaration)
 		{
-			return variable.name == otherVariable.name;
+			return variableDeclaration->name == variableName;
 		};

-	const auto layerContainsVariable =
-		[&variable, &variableMatches](const auto &layer)
+	for (auto i = m_layers.rbegin(); i != m_layers.rend(); i++)
+	{
+		auto &layer = **i;
+		const auto matchingVariableDeclaration = std::find_if(layer.begin(), layer.end(), variableNameMatches);
+
+		if (matchingVariableDeclaration != layer.end())
+			return matchingVariableDeclaration->get();
+	}
+
+	return std::experimental::nullopt;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool VariableStack::contains(const ast::VariableDeclaration &variableDeclaration) const
+{
+	const auto variableDeclarationMatches =
+		[&variableDeclaration](const auto &other)
 		{
-			return (std::find_if(layer->cbegin(), layer->cend(), variableMatches) != layer->cend());
+			return variableDeclaration.name == other->name;
 		};

-	return (std::find_if(m_layers.cbegin(), m_layers.cend(), layerContainsVariable) != m_layers.cend());
+	const auto layerContainsVariableDeclaration =
+		[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
+		{
+			return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
+		};
+
+	return (std::find_if(m_layers.cbegin(), m_layers.cend(), layerContainsVariableDeclaration) != m_layers.cend());
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -52,68 +74,68 @@ struct CollectFreeVariablesVisitor
 	// Formulas
 	////////////////////////////////////////////////////////////////////////////////////////////////

-	void visit(const ast::And &and_, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::And &and_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
-		for (const auto &argument : and_.arguments)
+		for (auto &argument : and_.arguments)
 			argument.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Biconditional &biconditional, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Biconditional &biconditional, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		biconditional.left.accept(*this, variableStack, freeVariables);
 		biconditional.right.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Boolean &, VariableStack &, std::vector<ast::Variable> &)
+	void visit(ast::Boolean &, VariableStack &, std::vector<ast::VariableDeclaration *> &)
 	{
 	}

-	void visit(const ast::Comparison &comparison, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Comparison &comparison, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		comparison.left.accept(*this, variableStack, freeVariables);
 		comparison.right.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Exists &exists, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Exists &exists, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		variableStack.push(&exists.variables);
 		exists.argument.accept(*this, variableStack, freeVariables);
 		variableStack.pop();
 	}

-	void visit(const ast::ForAll &forAll, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::ForAll &forAll, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		variableStack.push(&forAll.variables);
 		forAll.argument.accept(*this, variableStack, freeVariables);
 		variableStack.pop();
 	}

-	void visit(const ast::Implies &implies, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Implies &implies, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		implies.antecedent.accept(*this, variableStack, freeVariables);
 		implies.consequent.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::In &in, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::In &in, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		in.element.accept(*this, variableStack, freeVariables);
 		in.set.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Not &not_, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Not &not_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		not_.argument.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Or &or_, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Or &or_, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
-		for (const auto &argument : or_.arguments)
+		for (auto &argument : or_.arguments)
 			argument.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Predicate &predicate, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Predicate &predicate, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
-		for (const auto &argument : predicate.arguments)
+		for (auto &argument : predicate.arguments)
 			argument.accept(*this, variableStack, freeVariables);
 	}

@@ -121,61 +143,55 @@ struct CollectFreeVariablesVisitor
 	// Terms
 	////////////////////////////////////////////////////////////////////////////////////////////////

-	void visit(const ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::BinaryOperation &binaryOperation, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		binaryOperation.left.accept(*this, variableStack, freeVariables);
 		binaryOperation.right.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Constant &, VariableStack &, std::vector<ast::Variable> &)
+	void visit(ast::Constant &, VariableStack &, std::vector<ast::VariableDeclaration *> &)
 	{
 	}

-	void visit(const ast::Function &function, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Function &function, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
-		for (const auto &argument : function.arguments)
+		for (auto &argument : function.arguments)
 			argument.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::Integer &, VariableStack &, std::vector<ast::Variable> &)
+	void visit(ast::Integer &, VariableStack &, std::vector<ast::VariableDeclaration *> &)
 	{
 	}

-	void visit(const ast::Interval &interval, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Interval &interval, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
 		interval.from.accept(*this, variableStack, freeVariables);
 		interval.to.accept(*this, variableStack, freeVariables);
 	}

-	void visit(const ast::SpecialInteger &, VariableStack &, std::vector<ast::Variable> &)
+	void visit(ast::SpecialInteger &, VariableStack &, std::vector<ast::VariableDeclaration *> &)
 	{
 	}

-	void visit(const ast::String &, VariableStack &, std::vector<ast::Variable> &)
+	void visit(ast::String &, VariableStack &, std::vector<ast::VariableDeclaration *> &)
 	{
 	}

-	void visit(const ast::Variable &variable, VariableStack &variableStack, std::vector<ast::Variable> &freeVariables)
+	void visit(ast::Variable &variable, VariableStack &variableStack, std::vector<ast::VariableDeclaration *> &freeVariables)
 	{
-		if (variableStack.contains(variable))
+		if (variableStack.contains(*variable.declaration))
 			return;

-		const auto &variableMatches =
-			[&variable](auto &otherVariable)
-			{
-				return variable.name == otherVariable.name;
-			};
-
-		if (std::find_if(freeVariables.cbegin(), freeVariables.cend(), variableMatches) != freeVariables.cend())
+		if (std::find(freeVariables.cbegin(), freeVariables.cend(), variable.declaration) != freeVariables.cend())
 			return;

-		freeVariables.emplace_back(ast::deepCopy(variable));
+		freeVariables.emplace_back(variable.declaration);
 	}
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula)
+std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula)
 {
 	ast::VariableStack variableStack;
 	return collectFreeVariables(formula, variableStack);
@@ -183,9 +199,9 @@ std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula)

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack)
+std::vector<ast::VariableDeclaration *> collectFreeVariables(ast::Formula &formula, ast::VariableStack &variableStack)
 {
-	std::vector<ast::Variable> freeVariables;
+	std::vector<ast::VariableDeclaration *> freeVariables;

 	formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables);

--- a/src/anthem/Completion.cpp
+++ b/src/anthem/Completion.cpp
@@ -1,5 +1,6 @@
-#include <anthem/Completion.h>
+	#include <anthem/Completion.h>

+#include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
 #include <anthem/ASTVisitors.h>
 #include <anthem/Utils.h>
@@ -14,16 +15,17 @@ namespace anthem
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Copies the parameters of a predicate
-std::vector<ast::Variable> copyParameters(const ast::Predicate &predicate)
+std::vector<std::unique_ptr<ast::VariableDeclaration>> copyParameters(const ast::Predicate &predicate)
 {
-	std::vector<ast::Variable> parameters;
-	parameters.reserve(predicate.arity());
+	std::vector<std::unique_ptr<ast::VariableDeclaration>> parameters;
+	/*parameters.reserve(predicate.arity());

-	for (const auto &parameter : predicate.arguments)
+	for (const auto &argument : predicate.arguments)
 	{
-		assert(parameter.is<ast::Variable>());
-		parameters.emplace_back(ast::deepCopy(parameter.get<ast::Variable>()));
-	}
+		assert(argument.is<ast::Variable>());
+		// TODO: reimplement
+		//parameters.emplace_back(ast::deepCopy(parameter.get<ast::VariableDeclaration>()));
+	}*/

 	return parameters;
 }
@@ -31,18 +33,18 @@ std::vector<ast::Variable> copyParameters(const ast::Predicate &predicate)
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Builds the conjunction within the completed formula for a given predicate
-ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const std::vector<ast::Variable> &parameters, const std::vector<ast::Formula> &formulas)
+ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, std::vector<std::unique_ptr<ast::VariableDeclaration>> &parameters, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
 	auto disjunction = ast::Formula::make<ast::Or>();

-	ast::VariableStack variableStack;
+	/*ast::VariableStack variableStack;
 	variableStack.push(&parameters);

 	// Build the conjunction of all formulas with the predicate as consequent
-	for (const auto &formula : formulas)
+	for (auto &scopedFormula : scopedFormulas)
 	{
-		assert(formula.is<ast::Implies>());
-		const auto &implies = formula.get<ast::Implies>();
+		assert(scopedFormula.formula.is<ast::Implies>());
+		auto &implies = scopedFormula.formula.get<ast::Implies>();

 		if (!implies.consequent.is<ast::Predicate>())
 			continue;
@@ -55,6 +57,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 		auto variables = ast::collectFreeVariables(implies.antecedent, variableStack);

 		// TODO: avoid deep copies
+		// TODO: reimplement
 		if (variables.empty())
 			disjunction.get<ast::Or>().arguments.emplace_back(ast::deepCopy(implies.antecedent));
 		else
@@ -62,7 +65,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 			auto exists = ast::Formula::make<ast::Exists>(std::move(variables), ast::deepCopy(implies.antecedent));
 			disjunction.get<ast::Or>().arguments.emplace_back(std::move(exists));
 		}
-	}
+	}*/

 	return disjunction;
 }
@@ -74,7 +77,7 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 {
 	assert(innerFormula.is<ast::Or>());

-	if (innerFormula.get<ast::Or>().arguments.empty())
+	/*if (innerFormula.get<ast::Or>().arguments.empty())
 		return ast::Formula::make<ast::Not>(std::move(predicate));

 	if (innerFormula.get<ast::Or>().arguments.size() == 1)
@@ -88,17 +91,17 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 			return std::move(predicate);
 		else
 			return ast::Formula::make<ast::Not>(std::move(predicate));
-	}
+	}*/

 	return ast::Formula::make<ast::Biconditional>(std::move(predicate), std::move(innerFormula));
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-void completePredicate(ast::Predicate &&predicate, const std::vector<ast::Formula> &formulas, std::vector<ast::Formula> &completedFormulas)
+void completePredicate(ast::Predicate &&predicate, std::vector<ast::ScopedFormula> &scopedFormulas, std::vector<ast::ScopedFormula> &completedScopedFormulas)
 {
-	auto parameters = copyParameters(predicate);
-	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, formulas);
+	/*auto parameters = copyParameters(predicate);
+	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, scopedFormulas);
 	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction));

 	if (parameters.empty())
@@ -108,14 +111,14 @@ void completePredicate(ast::Predicate &&predicate, const std::vector<ast::Formul
 	}

 	auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(parameters), std::move(completedFormulaQuantified));
-	completedFormulas.emplace_back(std::move(completedFormula));
+	completedFormulas.emplace_back(std::move(completedFormula));*/
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-void completeIntegrityConstraint(const ast::Formula &formula, std::vector<ast::Formula> &completedFormulas)
+void completeIntegrityConstraint(ast::Formula &formula, std::vector<ast::ScopedFormula> &)
 {
-	assert(formula.is<ast::Implies>());
+	/*assert(formula.is<ast::Implies>());
 	auto &implies = formula.get<ast::Implies>();
 	assert(implies.consequent.is<ast::Boolean>());
 	assert(implies.consequent.get<ast::Boolean>().value == false);
@@ -123,6 +126,7 @@ void completeIntegrityConstraint(const ast::Formula &formula, std::vector<ast::F
 	auto variables = ast::collectFreeVariables(implies.antecedent);

 	// TODO: avoid deep copies
+	// TODO: reimplement
 	auto argument = ast::Formula::make<ast::Not>(ast::deepCopy(implies.antecedent));

 	if (variables.empty())
@@ -132,20 +136,20 @@ void completeIntegrityConstraint(const ast::Formula &formula, std::vector<ast::F
 	}

 	auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
-	completedFormulas.emplace_back(std::move(completedFormula));
+	completedFormulas.emplace_back(std::move(completedFormula));*/
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-void complete(std::vector<ast::Formula> &formulas)
+void complete(std::vector<ast::ScopedFormula> &scopedFormulas)
 {
-	// Check whether formulas are in normal form
-	for (const auto &formula : formulas)
+	/*// Check whether formulas are in normal form
+	for (const auto &scopedFormula : scopedFormulas)
 	{
-		if (!formula.is<ast::Implies>())
+		if (!scopedFormula.formula.is<ast::Implies>())
 			throw std::runtime_error("cannot perform completion, formula not in normal form");

-		auto &implies = formula.get<ast::Implies>();
+		auto &implies = scopedFormula.formula.get<ast::Implies>();

 		if (!implies.consequent.is<ast::Predicate>() && !implies.consequent.is<ast::Boolean>())
 			throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
@@ -153,8 +157,8 @@ void complete(std::vector<ast::Formula> &formulas)

 	std::vector<const ast::Predicate *> predicates;

-	for (const auto &formula : formulas)
-		ast::collectPredicates(formula, predicates);
+	for (const auto &scopedFormula : scopedFormulas)
+		ast::collectPredicates(scopedFormula.formula, predicates);

 	std::sort(predicates.begin(), predicates.end(),
 		[](const auto *lhs, const auto *rhs)
@@ -167,7 +171,7 @@ void complete(std::vector<ast::Formula> &formulas)
 			return lhs->arity() < rhs->arity();
 		});

-	std::vector<ast::Formula> completedFormulas;
+	std::vector<ast::ScopedFormula> completedScopedFormulas;

 	// Complete predicates
 	for (const auto *predicate : predicates)
@@ -176,19 +180,20 @@ void complete(std::vector<ast::Formula> &formulas)
 		ast::Predicate signature(std::string(predicate->name));
 		signature.arguments.reserve(predicate->arguments.size());

+		// TODO: reimplement
 		for (std::size_t i = 0; i < predicate->arguments.size(); i++)
 		{
 			auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1);
-			signature.arguments.emplace_back(ast::Term::make<ast::Variable>(std::move(variableName), ast::Variable::Type::Reserved));
+			signature.arguments.emplace_back(ast::Term::make<ast::Variable>(std::move(variableName), ast::VariableDeclaration::Type::Reserved));
 		}

-		completePredicate(std::move(signature), formulas, completedFormulas);
+		completePredicate(std::move(signature), scopedFormulas, completedScopedFormulas);
 	}

 	// Complete integrity constraints
-	for (const auto &formula : formulas)
+	for (auto &scopedFormula : scopedFormulas)
 	{
-		auto &implies = formula.get<ast::Implies>();
+		auto &implies = scopedFormula.formula.get<ast::Implies>();

 		if (!implies.consequent.is<ast::Boolean>())
 			continue;
@@ -199,10 +204,10 @@ void complete(std::vector<ast::Formula> &formulas)
 		if (boolean.value == true)
 			continue;

-		completeIntegrityConstraint(formula, completedFormulas);
+		completeIntegrityConstraint(scopedFormula.formula, completedScopedFormulas);
 	}

-	std::swap(formulas, completedFormulas);
+	std::swap(scopedFormulas, completedScopedFormulas);*/
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -1,5 +1,7 @@
 #include <anthem/Simplification.h>

+#include <experimental/optional>
+
 #include <anthem/ASTVisitors.h>

 namespace anthem
@@ -12,21 +14,19 @@ namespace anthem
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Determines whether a term is a specific variable
-bool matchesVariable(const ast::Term &term, const ast::Variable &variable)
+bool matchesVariableDeclaration(const ast::Term &term, const ast::VariableDeclaration &variableDeclaration)
 {
 	if (!term.is<ast::Variable>())
 		return false;

-	const auto &otherVariable = term.get<ast::Variable>();
-
-	return variable.name == otherVariable.name;
+	return term.get<ast::Variable>().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<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::Variable &variable)
+std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula, const ast::VariableDeclaration &variableDeclaration)
 {
 	if (!formula.is<ast::Comparison>())
 		return std::experimental::nullopt;
@@ -36,10 +36,10 @@ std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula
 	if (comparison.operator_ != ast::Comparison::Operator::Equal)
 		return std::experimental::nullopt;

-	if (matchesVariable(comparison.left, variable))
+	if (matchesVariableDeclaration(comparison.left, variableDeclaration))
 		return std::move(comparison.right);

-	if (matchesVariable(comparison.right, variable))
+	if (matchesVariableDeclaration(comparison.right, variableDeclaration))
 		return std::move(comparison.left);

 	return std::experimental::nullopt;
@@ -50,15 +50,16 @@ std::experimental::optional<ast::Term> extractAssignedTerm(ast::Formula &formula
 // Replaces all occurrences of a variable in a given term with another term
 struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVariableInTermVisitor>
 {
-	static void accept(ast::Variable &variable, ast::Term &term, const ast::Variable &variableToReplace, const ast::Term &replacementTerm)
+	static void accept(ast::Variable &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &)
 	{
-		if (variable.name == variableToReplace.name)
-			term = ast::deepCopy(replacementTerm);
+		// TODO: reimplement
+		//if (variable.name == variableToReplace.name)
+		//	term = ast::deepCopy(replacementTerm);
 	}

 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(T &, ast::Term &, const ast::Variable &, const ast::Term &)
+	static void accept(T &, ast::Term &, const ast::VariableDeclaration &, const ast::Term &)
 	{
 	}
 };
@@ -68,27 +69,27 @@ struct ReplaceVariableInTermVisitor : public ast::RecursiveTermVisitor<ReplaceVa
 // Replaces all occurrences of a variable in a given formula with a term
 struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
 {
-	static void accept(ast::Comparison &comparison, ast::Formula &, const ast::Variable &variable, const ast::Term &term)
+	static void accept(ast::Comparison &comparison, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term)
 	{
-		comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variable, term);
-		comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, variable, term);
+		comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, variableDeclaration, term);
+		comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, variableDeclaration, term);
 	}

-	static void accept(ast::In &in, ast::Formula &, const ast::Variable &variable, const ast::Term &term)
+	static void accept(ast::In &in, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term)
 	{
-		in.element.accept(ReplaceVariableInTermVisitor(), in.element, variable, term);
-		in.set.accept(ReplaceVariableInTermVisitor(), in.set, variable, term);
+		in.element.accept(ReplaceVariableInTermVisitor(), in.element, variableDeclaration, term);
+		in.set.accept(ReplaceVariableInTermVisitor(), in.set, variableDeclaration, term);
 	}

-	static void accept(ast::Predicate &predicate, ast::Formula &, const ast::Variable &variable, const ast::Term &term)
+	static void accept(ast::Predicate &predicate, ast::Formula &, const ast::VariableDeclaration &variableDeclaration, const ast::Term &term)
 	{
 		for (auto &argument : predicate.arguments)
-			argument.accept(ReplaceVariableInTermVisitor(), argument, variable, term);
+			argument.accept(ReplaceVariableInTermVisitor(), argument, variableDeclaration, term);
 	}

 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(T &, ast::Formula &, const ast::Variable &, const ast::Term &)
+	static void accept(T &, ast::Formula &, const ast::VariableDeclaration &, const ast::Term &)
 	{
 	}
 };
@@ -108,7 +109,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();)
 	{
-		auto &variable = *i;
+		auto &variableDeclaration = *i->get();

 		bool wasVariableReplaced = false;

@@ -117,7 +118,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 		{
 			auto &argument = *j;
 			// Find term that is equivalent to the given variable
-			auto assignedTerm = extractAssignedTerm(argument, variable);
+			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);

 			if (!assignedTerm)
 				continue;
@@ -129,7 +130,7 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 					continue;

 				auto &otherArgument = *k;
-				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variable, assignedTerm.value());
+				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
 			}

 			arguments.erase(j);
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -40,12 +40,12 @@ void translate(const char *fileName, std::istream &stream, Context &context)

 	auto fileContent = std::string(std::istreambuf_iterator<char>(stream), {});

-	std::vector<ast::Formula> formulas;
+	std::vector<ast::ScopedFormula> scopedFormulas;

 	const auto translateStatement =
-		[&formulas, &context](const Clingo::AST::Statement &statement)
+		[&scopedFormulas, &context](const Clingo::AST::Statement &statement)
 		{
-			statement.data.accept(StatementVisitor(), statement, formulas, context);
+			statement.data.accept(StatementVisitor(), statement, scopedFormulas, context);
 		};

 	const auto logger =
@@ -57,14 +57,19 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	Clingo::parse_program(fileContent.c_str(), translateStatement, logger);

 	if (context.simplify)
-		for (auto &formula : formulas)
-			simplify(formula);
+		for (auto &scopedFormula : scopedFormulas)
+			simplify(scopedFormula.formula);

 	if (context.complete)
-		complete(formulas);
+		complete(scopedFormulas);

-	for (const auto &formula : formulas)
-		context.logger.outputStream() << formula << std::endl;
+	ast::PrintContext printContext;
+
+	for (const auto &scopedFormula : scopedFormulas)
+	{
+		ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
+		context.logger.outputStream() << std::endl;
+	}
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////