Implemented explicit syntax tree representation for first-order formulas.

include/anthem/AST.h

@@ -22,10 +22,20 @@ struct BinaryOperation
 {
 	enum class Operator
 	{
-		Add,
-		Subtract
+		Plus,
+		Minus,
+		Multiplication,
+		Division,
+		Modulo
 	};
 
+	BinaryOperation(Operator operator_, Term &&left, Term &&right)
+	:	operator_{operator_},
+		left{std::move(left)},
+		right{std::move(right)}
+	{
+	}
+
 	Operator operator_;
 	Term left;
 	Term right;
@@ -35,53 +45,173 @@ struct BinaryOperation
 
 struct Boolean
 {
+	Boolean(bool value)
+	:	value{value}
+	{
+	}
+
 	bool value = false;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct Equals
+struct Comparison
 {
+	enum class Operator
+	{
+		GreaterThan,
+		LessThan,
+		LessEqual,
+		GreaterEqual,
+		NotEqual,
+		Equal
+	};
+
+	Comparison(Operator operator_, Term &&left, Term &&right)
+	:	operator_{operator_},
+		left{std::move(left)},
+		right{std::move(right)}
+	{
+	}
+
+	Operator operator_;
 	Term left;
 	Term right;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct Constant
+{
+	Constant(std::string &&name)
+	:	name{std::move(name)}
+	{
+	}
+
+	std::string name;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct Function
 {
-	const char *name = nullptr;
+	Function(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
+		arguments{std::move(arguments)}
+	{
+	}
+
+	std::string name;
 	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct In
+{
+	In(Term &&element, Term &&set)
+	:	element{std::move(element)},
+		set{std::move(set)}
+	{
+	}
+
+	Term element;
+	Term set;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct Integer
 {
+	Integer(int value)
+	:	value{value}
+	{
+	}
+
 	int value;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct IntegerRange
+struct Interval
 {
-	Integer from;
-	Integer to;
+	Interval(Term &&from, Term &&to)
+	:	from{std::move(from)},
+		to{std::move(to)}
+	{
+	}
+
+	Term from;
+	Term to;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct Predicate
 {
-	const char *name = nullptr;
+	Predicate(std::string &&name)
+	:	name{std::move(name)}
+	{
+	}
+
+	Predicate(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
+		arguments{std::move(arguments)}
+	{
+	}
+
+	std::string name;
 	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SpecialInteger
+{
+	enum class Type
+	{
+		Infimum,
+		Supremum
+	};
+
+	SpecialInteger(Type type)
+	:	type{type}
+	{
+	}
+
+	Type type;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct String
+{
+	String(std::string &&text)
+	:	text{std::move(text)}
+	{
+	}
+
+	std::string text;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct Variable
 {
-	const char *name = nullptr;
+	enum class Type
+	{
+		UserDefined,
+		Reserved
+	};
+
+	Variable(std::string &&name, Type type)
+	:	name{std::move(name)},
+		type{type}
+	{
+	}
+
+	std::string name;
+	Type type;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -90,6 +220,13 @@ struct Variable
 
 struct And
 {
+	And() = default;
+
+	And(std::vector<Formula> &&arguments)
+	:	arguments{std::move(arguments)}
+	{
+	}
+
 	std::vector<Formula> arguments;
 };
 
@@ -97,6 +234,12 @@ struct And
 
 struct Biconditional
 {
+	Biconditional(Formula &&left, Formula &&right)
+	:	left{std::move(left)},
+		right{std::move(right)}
+	{
+	}
+
 	Formula left;
 	Formula right;
 };
@@ -105,22 +248,40 @@ struct Biconditional
 
 struct Exists
 {
+	Exists(std::vector<VariablePointer> &&variables, Formula &&argument)
+	:	variables{std::move(variables)},
+		argument{std::move(argument)}
+	{
+	}
+
 	std::vector<VariablePointer> variables;
-	Formula formula;
+	Formula argument;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct ForAll
 {
+	ForAll(std::vector<VariablePointer> &&variables, Formula &&argument)
+	:	variables{std::move(variables)},
+		argument{std::move(argument)}
+	{
+	}
+
 	std::vector<VariablePointer> variables;
-	Formula formula;
+	Formula argument;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct Implies
 {
+	Implies(Formula &&antecedent, Formula &&consequent)
+	:	antecedent{std::move(antecedent)},
+		consequent{std::move(consequent)}
+	{
+	}
+
 	Formula antecedent;
 	Formula consequent;
 };
@@ -129,6 +290,11 @@ struct Implies
 
 struct Not
 {
+	Not(Formula &&argument)
+	:	argument{std::move(argument)}
+	{
+	}
+
 	Formula argument;
 };
 
@@ -136,12 +302,261 @@ struct Not
 
 struct Or
 {
+	Or() = default;
+
+	Or(std::vector<Formula> &&arguments)
+	:	arguments{std::move(arguments)}
+	{
+	}
+
 	std::vector<Formula> arguments;
 };
 
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Deep Copying
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+BinaryOperation deepCopy(const BinaryOperation &other);
+Boolean deepCopy(const Boolean &other);
+Comparison deepCopy(const Comparison &other);
+Constant deepCopy(const Constant &other);
+Function deepCopy(const Function &other);
+Integer deepCopy(const Integer &other);
+Interval deepCopy(const Interval &other);
+Predicate deepCopy(const Predicate &other);
+SpecialInteger deepCopy(const SpecialInteger &other);
+String deepCopy(const String &other);
+Variable deepCopy(const Variable &other);
+std::vector<VariablePointer> deepCopy(const std::vector<VariablePointer> &other);
+And deepCopy(const And &other);
+Biconditional deepCopy(const Biconditional &other);
+Exists deepCopy(const Exists &other);
+ForAll deepCopy(const ForAll &other);
+Implies deepCopy(const Implies &other);
+Not deepCopy(const Not &other);
+Or deepCopy(const Or &other);
 
+Formula deepCopy(const Formula &formula);
+std::vector<Formula> deepCopy(const std::vector<Formula> &formulas);
+Term deepCopy(const Term &term);
+std::vector<Term> deepCopy(const std::vector<Term> &terms);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto deepCopyUniquePtr =
+	[](const auto &uniquePtr) -> typename std::decay<decltype(uniquePtr)>::type
+	{
+		using Type = typename std::decay<decltype(uniquePtr)>::type::element_type;
+		return std::make_unique<Type>(deepCopy(*uniquePtr));
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto deepCopyUniquePtrVector =
+	[](const auto &uniquePtrVector) -> typename std::decay<decltype(uniquePtrVector)>::type
+	{
+		using Type = typename std::decay<decltype(uniquePtrVector)>::type::value_type;
+
+		std::vector<Type> result;
+		result.reserve(uniquePtrVector.size());
+
+		for (const auto &uniquePtr : uniquePtrVector)
+			result.emplace_back(deepCopyUniquePtr(uniquePtr));
+
+		return result;
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto deepCopyVariant =
+	[](const auto &variant) -> typename std::decay<decltype(variant)>::type
+	{
+		return variant.match([](const auto &x) -> typename std::decay<decltype(variant)>::type {return deepCopyUniquePtr(x);});
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto deepCopyVariantVector =
+	[](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(deepCopyVariant(variant));
+
+		return result;
+	};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+BinaryOperation deepCopy(const BinaryOperation &other)
+{
+	return BinaryOperation(other.operator_, deepCopy(other.left), deepCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Boolean deepCopy(const Boolean &other)
+{
+	return Boolean(other.value);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Comparison deepCopy(const Comparison &other)
+{
+	return Comparison(other.operator_, deepCopy(other.left), deepCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Constant deepCopy(const Constant &other)
+{
+	return Constant(std::string(other.name));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Function deepCopy(const Function &other)
+{
+	return Function(std::string(other.name), deepCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Integer deepCopy(const Integer &other)
+{
+	return Integer(other.value);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Interval deepCopy(const Interval &other)
+{
+	return Interval(deepCopy(other.from), deepCopy(other.to));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Predicate deepCopy(const Predicate &other)
+{
+	return Predicate(std::string(other.name), deepCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+SpecialInteger deepCopy(const SpecialInteger &other)
+{
+	return SpecialInteger(other.type);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+String deepCopy(const String &other)
+{
+	return String(std::string(other.text));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Variable deepCopy(const Variable &other)
+{
+	return Variable(std::string(other.name), other.type);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+std::vector<VariablePointer> deepCopy(const std::vector<VariablePointer> &other)
+{
+	return deepCopyUniquePtrVector(other);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+And deepCopy(const And &other)
+{
+	return And(deepCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Biconditional deepCopy(const Biconditional &other)
+{
+	return Biconditional(deepCopy(other.left), deepCopy(other.right));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Exists deepCopy(const Exists &other)
+{
+	return Exists(deepCopy(other.variables), deepCopy(other.argument));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ForAll deepCopy(const ForAll &other)
+{
+	return ForAll(deepCopy(other.variables), deepCopy(other.argument));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+In deepCopy(const In &other)
+{
+	return In(deepCopy(other.element), deepCopy(other.set));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Implies deepCopy(const Implies &other)
+{
+	return Implies(deepCopy(other.antecedent), deepCopy(other.consequent));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Not deepCopy(const Not &other)
+{
+	return Not(deepCopy(other.argument));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Or deepCopy(const Or &other)
+{
+	return Or(deepCopy(other.arguments));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Formula deepCopy(const Formula &formula)
+{
+	return deepCopyVariant(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+std::vector<Formula> deepCopy(const std::vector<Formula> &formulas)
+{
+	return deepCopyVariantVector(formulas);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Term deepCopy(const Term &term)
+{
+	return deepCopyVariant(term);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+std::vector<Term> deepCopy(const std::vector<Term> &terms)
+{
+	return deepCopyVariantVector(terms);
+}
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

include/anthem/ASTForward.h

@@ -24,60 +24,55 @@ struct And;
 struct BinaryOperation;
 struct Biconditional;
 struct Boolean;
+struct Comparison;
 struct Constant;
-struct Equals;
 struct Exists;
 struct ForAll;
 struct Function;
 struct Implies;
+struct In;
 struct Integer;
-struct IntegerRange;
+struct Interval;
 struct Not;
 struct Or;
 struct Predicate;
+struct SpecialInteger;
+struct String;
 struct Variable;
 
 using AndPointer = std::unique_ptr<And>;
 using BinaryOperationPointer = std::unique_ptr<BinaryOperation>;
 using BiconditionalPointer = std::unique_ptr<Biconditional>;
 using BooleanPointer = std::unique_ptr<Boolean>;
+using ComparisonPointer = std::unique_ptr<Comparison>;
 using ConstantPointer = std::unique_ptr<Constant>;
-using EqualsPointer = std::unique_ptr<Equals>;
 using ExistsPointer = std::unique_ptr<Exists>;
 using ForAllPointer = std::unique_ptr<ForAll>;
 using FunctionPointer = std::unique_ptr<Function>;
 using ImpliesPointer = std::unique_ptr<Implies>;
+using InPointer = std::unique_ptr<In>;
 using IntegerPointer = std::unique_ptr<Integer>;
-using IntegerRangePointer = std::unique_ptr<IntegerRange>;
+using IntervalPointer = std::unique_ptr<Interval>;
 using NotPointer = std::unique_ptr<Not>;
 using OrPointer = std::unique_ptr<Or>;
 using PredicatePointer = std::unique_ptr<Predicate>;
+using SpecialIntegerPointer = std::unique_ptr<SpecialInteger>;
+using StringPointer = std::unique_ptr<String>;
 using VariablePointer = std::unique_ptr<Variable>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Variants
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-using TermT = mapbox::util::variant<
-	BinaryOperationPointer,
-	ConstantPointer,
-	IntegerPointer,
-	FunctionPointer,
-	VariablePointer>;
-
-class Term : public TermT
-{
-	using TermT::TermT;
-};
-
 using FormulaT = mapbox::util::variant<
 	AndPointer,
 	BiconditionalPointer,
 	BooleanPointer,
-	EqualsPointer,
+	ComparisonPointer,
 	ExistsPointer,
 	ForAllPointer,
 	ImpliesPointer,
+	InPointer,
 	NotPointer,
 	OrPointer,
 	PredicatePointer>;
@@ -87,7 +82,21 @@ class Formula : public FormulaT
 	using FormulaT::FormulaT;
 };
 
-using Formulas = std::vector<Formula>;
+using TermT = mapbox::util::variant<
+	BinaryOperationPointer,
+	BooleanPointer,
+	ConstantPointer,
+	FunctionPointer,
+	IntegerPointer,
+	IntervalPointer,
+	SpecialIntegerPointer,
+	StringPointer,
+	VariablePointer>;
+
+class Term : public TermT
+{
+	using TermT::TermT;
+};
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

include/anthem/Body.h

@@ -3,9 +3,9 @@
 
 #include <algorithm>
 
-#include <anthem/Context.h>
+#include <anthem/AST.h>
+#include <anthem/Term.h>
 #include <anthem/Utils.h>
-#include <anthem/output/ClingoOutput.h>
 #include <anthem/output/Formatting.h>
 
 namespace anthem
@@ -17,204 +17,199 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct TermPrintVisitor
+ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOperator)
 {
-	void visit(const Clingo::Symbol &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	switch (comparisonOperator)
+	{
+		case Clingo::AST::ComparisonOperator::GreaterThan:
+			return ast::Comparison::Operator::GreaterThan;
+		case Clingo::AST::ComparisonOperator::LessThan:
+			return ast::Comparison::Operator::LessThan;
+		case Clingo::AST::ComparisonOperator::LessEqual:
+			return ast::Comparison::Operator::LessEqual;
+		case Clingo::AST::ComparisonOperator::GreaterEqual:
+			return ast::Comparison::Operator::GreaterEqual;
+		case Clingo::AST::ComparisonOperator::NotEqual:
+			return ast::Comparison::Operator::NotEqual;
+		case Clingo::AST::ComparisonOperator::Equal:
+			return ast::Comparison::Operator::Equal;
+	}
+
+	return ast::Comparison::Operator::NotEqual;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ast::VariablePointer makeAuxiliaryBodyVariable(const int i)
+{
+	auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(i);
+
+	return std::make_unique<ast::Variable>(std::move(variableName), ast::Variable::Type::Reserved);
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct BodyTermTranslateVisitor
+{
+	std::experimental::optional<ast::Formula> visit(const Clingo::Symbol &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“symbol” terms currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Variable &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Variable &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“variable” terms currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Interval &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Interval &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“interval” terms currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	// TODO: check correctness
-	void visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context)
+	// TODO: refactor
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context);
 
-		auto &outputStream = context.logger.outputStream();
-
 		if (function.arguments.empty())
+			return std::make_unique<ast::Predicate>(std::string(function.name));
+
+		std::vector<ast::VariablePointer> variables;
+		variables.reserve(function.arguments.size());
+
+		for (size_t i = 0; i < function.arguments.size(); i++)
+			variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i));
+
+		auto conjunction = std::make_unique<ast::And>();
+
+		for (size_t i = 0; i < function.arguments.size(); i++)
 		{
-			outputStream << output::Function(function.name);
-			return;
+			const auto &argument = function.arguments[i];
+			conjunction->arguments.emplace_back(std::make_unique<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i), translate(argument, context)));
 		}
 
-		outputStream << output::Keyword("exists") << " ";
+		auto predicate = std::make_unique<ast::Predicate>(std::string(function.name));
+		predicate->arguments.reserve(function.arguments.size());
 
-		for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
-		{
-			if (i != function.arguments.cbegin())
-				outputStream << ", ";
+		for (size_t i = 0; i < function.arguments.size(); i++)
+			predicate->arguments.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + i));
 
-			const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin());
-
-			outputStream << output::Variable(variableName.c_str());
-		}
-
-		outputStream << " (";
-
-		for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
-		{
-			const auto &argument = *i;
-
-			if (i != function.arguments.cbegin())
-				outputStream << " " << Clingo::AST::BinaryOperator::And << " ";
-
-			const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin());
-
-			outputStream
-				<< output::Variable(variableName.c_str())
-				<< " " << output::Keyword("in") << " "
-				<< argument;
-		}
-
-		outputStream
-			<< " " << Clingo::AST::BinaryOperator::And << " "
-			<< literal.sign
-			<< output::Function(function.name) << "(";
-
-		for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
-		{
-			if (i != function.arguments.cbegin())
-				outputStream << ", ";
-
-			const auto variableName = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + i - function.arguments.cbegin());
-
-			outputStream << output::Variable(variableName.c_str());
-		}
-
-		outputStream << "))";
+		if (literal.sign == Clingo::AST::Sign::None)
+			conjunction->arguments.emplace_back(std::move(predicate));
+		else
+			conjunction->arguments.emplace_back(std::make_unique<ast::Not>(std::move(predicate)));
 
 		context.auxiliaryBodyLiteralID += function.arguments.size();
+
+		return std::make_unique<ast::Exists>(std::move(variables), std::move(conjunction));
 	}
 
-	void visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct LiteralPrintVisitor
+struct BodyLiteralTranslateVisitor
 {
-	void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, Context &context)
 	{
 		throwErrorAtLocation(literal.location, "“boolean” literals currently unsupported in this context", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, Context &context)
 	{
-		term.data.accept(TermPrintVisitor(), literal, term, context);
+		return term.data.accept(BodyTermTranslateVisitor(), literal, term, context);
+		return std::experimental::nullopt;
 	}
 
 	// TODO: refactor
-	void visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, Context &context)
 	{
 		assert(literal.sign == Clingo::AST::Sign::None);
 
-		const char *operatorName = "";
+		const auto operator_ = translate(comparison.comparison);
 
-		switch (comparison.comparison)
-		{
-			case Clingo::AST::ComparisonOperator::GreaterThan:
-				operatorName = ">";
-				break;
-			case Clingo::AST::ComparisonOperator::LessThan:
-				operatorName = "<";
-				break;
-			case Clingo::AST::ComparisonOperator::LessEqual:
-				operatorName = "<=";
-				break;
-			case Clingo::AST::ComparisonOperator::GreaterEqual:
-				operatorName = ">=";
-				break;
-			case Clingo::AST::ComparisonOperator::NotEqual:
-				operatorName = "!=";
-				break;
-			case Clingo::AST::ComparisonOperator::Equal:
-				operatorName = "=";
-				break;
-		}
+		std::vector<ast::VariablePointer> variables;
+		variables.reserve(2);
+		variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID));
+		variables.emplace_back(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1));
 
-		const auto variableName1 = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID);
-		const auto variableName2 = std::string(AuxiliaryBodyVariablePrefix) + std::to_string(context.auxiliaryBodyLiteralID + 1);
-
-		context.logger.outputStream()
-			<< output::Keyword("exists") << " " << output::Variable(variableName1.c_str())
-			<< ", " << output::Variable(variableName2.c_str())
-			<< " ("
-			<< output::Variable(variableName1.c_str())
-			<< " " << output::Keyword("in") << " " << comparison.left
-			<< " " << Clingo::AST::BinaryOperator::And << " "
-			<< output::Variable(variableName2.c_str())
-			<< " " << output::Keyword("in") << " " << comparison.right
-			<< " " << Clingo::AST::BinaryOperator::And << " "
-			<< output::Variable(variableName1.c_str())
-			<< " " << output::Operator(operatorName) << " "
-			<< output::Variable(variableName2.c_str())
-			<< ")";
+		auto conjunction = std::make_unique<ast::And>();
+		conjunction->arguments.reserve(3);
+		conjunction->arguments.emplace_back(std::make_unique<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), translate(comparison.left, context)));
+		conjunction->arguments.emplace_back(std::make_unique<ast::In>(makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1), translate(comparison.right, context)));
+		conjunction->arguments.emplace_back(std::make_unique<ast::Comparison>(operator_, makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID), makeAuxiliaryBodyVariable(context.auxiliaryBodyLiteralID + 1)));
 
 		context.auxiliaryBodyLiteralID += 2;
+
+		return std::make_unique<ast::Exists>(std::move(variables), std::move(conjunction));
 	}
 
-	void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
 	{
 		throwErrorAtLocation(literal.location, "CSP literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct BodyLiteralPrintVisitor
+struct BodyBodyLiteralTranslateVisitor
 {
-	void visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &, Context &context)
 	{
-		literal.data.accept(LiteralPrintVisitor(), literal, context);
+		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, context);
 	}
 
-	void visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
 	{
 		throwErrorAtLocation(bodyLiteral.location, "“conditional literal” body literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
 	{
 		throwErrorAtLocation(bodyLiteral.location, "“aggregate” body literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
 	{
 		throwErrorAtLocation(bodyLiteral.location, "“body aggregate” body literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
 	{
 		throwErrorAtLocation(bodyLiteral.location, "“theory atom” body literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
 	{
 		throwErrorAtLocation(bodyLiteral.location, "“disjoint” body literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 };
 

include/anthem/Head.h

@@ -3,8 +3,8 @@
 
 #include <algorithm>
 
+#include <anthem/AST.h>
 #include <anthem/Utils.h>
-#include <anthem/output/ClingoOutput.h>
 #include <anthem/output/Formatting.h>
 
 namespace anthem
@@ -139,155 +139,179 @@ struct HeadLiteralCollectFunctionTermsVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct TermPrintSubstitutedVisitor
+struct FunctionTermTranslateVisitor
 {
-	void visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected", context);
+		return std::experimental::nullopt;
 	}
 
 	// TODO: check correctness
-	void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context)
 	{
 		if (function.external)
 			throwErrorAtLocation(term.location, "external functions currently unsupported", context);
 
-		auto &outputStream = context.logger.outputStream();
-
-		outputStream << output::Function(function.name);
-
-		if (function.arguments.empty())
-			return;
-
-		outputStream << "(";
+		std::vector<ast::Term> arguments;
+		arguments.reserve(function.arguments.size());
 
 		for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
 		{
-			if (i != function.arguments.cbegin())
-				outputStream << ", ";
-
 			const auto &argument = *i;
-
 			const auto matchingTerm = std::find(context.headTerms.cbegin(), context.headTerms.cend(), &argument);
 
 			assert(matchingTerm != context.headTerms.cend());
 
-			const auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1);
-
-			outputStream << output::Variable(variableName.c_str());
+			auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(matchingTerm - context.headTerms.cbegin() + 1);
+			arguments.emplace_back(std::make_unique<ast::Variable>(std::move(variableName), ast::Variable::Type::Reserved));
 		}
 
-		outputStream << ")";
+		return std::make_unique<ast::Predicate>(function.name, std::move(arguments));
 	}
 
-	void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context)
 	{
 		throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected", context);
+		return std::experimental::nullopt;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct LiteralPrintSubstitutedVisitor
+struct LiteralTranslateVisitor
 {
-	void visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &)
 	{
-		context.logger.outputStream() << boolean;
+		return std::make_unique<ast::Boolean>(boolean.value);
 	}
 
-	void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context)
 	{
-		term.data.accept(TermPrintSubstitutedVisitor(), term, context);
+		return term.data.accept(FunctionTermTranslateVisitor(), term, context);
 	}
 
-	void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context)
 	{
 		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
 	{
 		throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
+		return std::experimental::nullopt;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct HeadLiteralPrintSubstitutedVisitor
+struct HeadLiteralTranslateToConsequentVisitor
 {
-	void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, Context &context)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
-			throwErrorAtLocation(literal.location, "double-negated literals currently unsupported", context);
+			throwErrorAtLocation(literal.location, "double-negated head literals currently unsupported", context);
 
-		context.logger.outputStream() << literal.sign;
+		auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, context);
 
-		literal.data.accept(LiteralPrintSubstitutedVisitor(), literal, context);
+		if (literal.sign == Clingo::AST::Sign::None)
+			return translatedLiteral;
+
+		if (!translatedLiteral)
+			return std::experimental::nullopt;
+
+		return std::make_unique<ast::Not>(std::move(translatedLiteral.value()));
 	}
 
-	void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
 	{
-		for (auto i = disjunction.elements.cbegin(); i != disjunction.elements.cend(); i++)
-		{
-			const auto &conditionalLiteral = *i;
+		std::vector<ast::Formula> arguments;
+		arguments.reserve(disjunction.elements.size());
 
+		for (const auto &conditionalLiteral : disjunction.elements)
+		{
 			if (!conditionalLiteral.condition.empty())
 				throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context);
 
-			if (i != disjunction.elements.cbegin())
-				context.logger.outputStream() << " " << Clingo::AST::BinaryOperator::Or << " ";
+			auto argument = visit(conditionalLiteral.literal, headLiteral, context);
 
-			visit(conditionalLiteral.literal, headLiteral, context);
+			if (!argument)
+				throwErrorAtLocation(headLiteral.location, "could not parse argument", context);
+
+			arguments.emplace_back(std::move(argument.value()));
 		}
+
+		return std::make_unique<ast::Or>(std::move(arguments));
 	}
 
-	void visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
 	{
 		if (aggregate.left_guard || aggregate.right_guard)
 			throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards not allowed", context);
 
-		for (auto i = aggregate.elements.cbegin(); i != aggregate.elements.cend(); i++)
+		const auto translateConditionalLiteral =
+			[&](const auto &conditionalLiteral)
+			{
+				if (!conditionalLiteral.condition.empty())
+					throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context);
+
+				return this->visit(conditionalLiteral.literal, headLiteral, context);
+			};
+
+		if (aggregate.elements.size() == 1)
+			return translateConditionalLiteral(aggregate.elements[0]);
+
+		std::vector<ast::Formula> arguments;
+		arguments.reserve(aggregate.elements.size());
+
+		for (const auto &conditionalLiteral : aggregate.elements)
 		{
-			const auto &conditionalLiteral = *i;
+			auto argument = translateConditionalLiteral(conditionalLiteral);
 
-			if (!conditionalLiteral.condition.empty())
-				throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported", context);
+			if (!argument)
+				throwErrorAtLocation(headLiteral.location, "could not parse argument", context);
 
-			if (i != aggregate.elements.cbegin())
-				context.logger.outputStream() << " " << Clingo::AST::BinaryOperator::Or << " ";
-
-			visit(conditionalLiteral.literal, headLiteral, context);
+			arguments.emplace_back(std::move(argument.value()));
 		}
+
+		return std::make_unique<ast::Or>(std::move(arguments));
 	}
 
-	void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
 	{
 		throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
 	{
 		throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 };
 

include/anthem/StatementVisitor.h

@@ -1,10 +1,11 @@
 #ifndef __ANTHEM__STATEMENT_VISITOR_H
 #define __ANTHEM__STATEMENT_VISITOR_H
 
+#include <anthem/AST.h>
 #include <anthem/Body.h>
 #include <anthem/Head.h>
+#include <anthem/Term.h>
 #include <anthem/Utils.h>
-#include <anthem/output/ClingoOutput.h>
 
 namespace anthem
 {
@@ -17,37 +18,46 @@ namespace anthem
 
 struct StatementVisitor
 {
-	void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
 	{
 		// TODO: refactor
 		context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str());
 
 		if (!program.parameters.empty())
 			throwErrorAtLocation(statement.location, "program parameters currently unsupported", context);
+
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
 	{
 		context.reset();
 
-		auto &outputStream = context.logger.outputStream();
-
 		// Concatenate all head terms
 		rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context);
 
+		auto antecedent = std::make_unique<ast::And>();
+
+		// Compute consequent
+		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context);
+
+		if (!consequent)
+		{
+			context.logger.log(output::Priority::Error, "could not translate formula consequent");
+			return std::experimental::nullopt;
+		}
+
 		// Print auxiliary variables replacing the head atom’s arguments
 		for (auto i = context.headTerms.cbegin(); i != context.headTerms.cend(); i++)
 		{
 			const auto &headTerm = **i;
 
-			if (i != context.headTerms.cbegin())
-				outputStream << " " << Clingo::AST::BinaryOperator::And << " ";
+			auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1);
+			auto element = std::make_unique<ast::Variable>(std::move(variableName), ast::Variable::Type::Reserved);
+			auto set = translate(headTerm, context);
+			auto in = std::make_unique<ast::In>(std::move(element), std::move(set));
 
-			const auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1);
-
-			outputStream
-				<< output::Variable(variableName.c_str())
-				<< " " << output::Keyword("in") << " " << headTerm;
+			antecedent->arguments.emplace_back(std::move(in));
 		}
 
 		// Print translated body literals
@@ -55,97 +65,94 @@ struct StatementVisitor
 		{
 			const auto &bodyLiteral = *i;
 
-			if (!context.headTerms.empty() || i != rule.body.cbegin())
-				outputStream << " " << Clingo::AST::BinaryOperator::And << " ";
-
 			if (bodyLiteral.sign != Clingo::AST::Sign::None)
 				throwErrorAtLocation(bodyLiteral.location, "only positive literals currently supported", context);
 
-			bodyLiteral.data.accept(BodyLiteralPrintVisitor(), bodyLiteral, context);
+			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, context);
+
+			if (!argument)
+				throwErrorAtLocation(bodyLiteral.location, "could not translate body literal", context);
+
+			antecedent->arguments.emplace_back(std::move(argument.value()));
 		}
 
 		// Handle choice rules
 		if (context.isChoiceRule)
-		{
-			const bool isFirstOutput = rule.body.empty() && context.headTerms.empty();
+			antecedent->arguments.emplace_back(ast::deepCopy(consequent.value()));
 
-			if (!isFirstOutput)
-				outputStream << " " << Clingo::AST::BinaryOperator::And << " ";
+		// Use “true” as the consequent in case it is empty
+		if (antecedent->arguments.empty())
+			return std::make_unique<ast::Implies>(std::make_unique<ast::Boolean>(true), std::move(consequent.value()));
+		else if (antecedent->arguments.size() == 1)
+			return std::make_unique<ast::Implies>(std::move(antecedent->arguments[0]), std::move(consequent.value()));
 
-			if (context.numberOfHeadLiterals > 1 && !isFirstOutput)
-				outputStream << "(";
-
-			rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, context);
-
-			if (context.numberOfHeadLiterals > 1 && !isFirstOutput)
-				outputStream << ")";
-		}
-
-		// Print “true” on the left side of the formula in case there is nothing else
-		if (rule.body.empty() && context.headTerms.empty() && !context.isChoiceRule)
-			outputStream << Clingo::AST::Boolean({true});
-
-		outputStream << " " << output::Operator("->") << " ";
-
-		// Print consequent of the implication
-		rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, context);
-
-		outputStream << std::endl;
+		return std::make_unique<ast::Implies>(std::move(antecedent), std::move(consequent.value()));
 	}
 
-	void visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“definition” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“show signature” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“show term” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“minimize” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“script” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“external” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“edge” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“heuristic” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“project atom” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“project signature” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 
-	void visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
+	std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
 	{
 		throwErrorAtLocation(statement.location, "“theory definition” statements currently unsupported", context);
+		return std::experimental::nullopt;
 	}
 };
 

include/anthem/Term.h

@@ -0,0 +1,132 @@
+#ifndef __ANTHEM__TERM_H
+#define __ANTHEM__TERM_H
+
+#include <algorithm>
+
+#include <anthem/AST.h>
+#include <anthem/Utils.h>
+#include <anthem/output/Formatting.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Term
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOperator, const Clingo::AST::Term &term, Context &context)
+{
+	switch (binaryOperator)
+	{
+		case Clingo::AST::BinaryOperator::Plus:
+			return ast::BinaryOperation::Operator::Plus;
+		case Clingo::AST::BinaryOperator::Minus:
+			return ast::BinaryOperation::Operator::Minus;
+		case Clingo::AST::BinaryOperator::Multiplication:
+			return ast::BinaryOperation::Operator::Multiplication;
+		case Clingo::AST::BinaryOperator::Division:
+			return ast::BinaryOperation::Operator::Division;
+		case Clingo::AST::BinaryOperator::Modulo:
+			return ast::BinaryOperation::Operator::Modulo;
+		default:
+			throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported", context);
+	}
+
+	return ast::BinaryOperation::Operator::Plus;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ast::Term translate(const Clingo::AST::Term &term, Context &context);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct TermTranslateVisitor
+{
+	std::experimental::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, Context &context)
+	{
+		switch (symbol.type())
+		{
+			case Clingo::SymbolType::Number:
+				return std::make_unique<ast::Integer>(symbol.number());
+			case Clingo::SymbolType::Infimum:
+				return std::make_unique<ast::SpecialInteger>(ast::SpecialInteger::Type::Infimum);
+			case Clingo::SymbolType::Supremum:
+				return std::make_unique<ast::SpecialInteger>(ast::SpecialInteger::Type::Supremum);
+			case Clingo::SymbolType::String:
+				return std::make_unique<ast::String>(std::string(symbol.string()));
+			default:
+				throwErrorAtLocation(term.location, "only numeric “symbol” terms allowed", context);
+		}
+
+		return std::experimental::nullopt;
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, Context &)
+	{
+		return std::make_unique<ast::Variable>(std::string(variable.name), ast::Variable::Type::UserDefined);
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context)
+	{
+		throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported", context);
+		return std::experimental::nullopt;
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, Context &context)
+	{
+		const auto operator_ = translate(binaryOperation.binary_operator, term, context);
+		auto left = translate(binaryOperation.left, context);
+		auto right = translate(binaryOperation.right, context);
+
+		return std::make_unique<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, Context &context)
+	{
+		auto left = translate(interval.left, context);
+		auto right = translate(interval.right, context);
+
+		return std::make_unique<ast::Interval>(std::move(left), std::move(right));
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context)
+	{
+		if (function.external)
+			throwErrorAtLocation(term.location, "external functions currently unsupported", context);
+
+		std::vector<ast::Term> arguments;
+		arguments.reserve(function.arguments.size());
+
+		for (const auto &argument : function.arguments)
+			arguments.emplace_back(translate(argument, context));
+
+		return std::make_unique<ast::Function>(function.name, std::move(arguments));
+	}
+
+	std::experimental::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context)
+	{
+		throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context);
+		return std::experimental::nullopt;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+ast::Term translate(const Clingo::AST::Term &term, Context &context)
+{
+	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, context);
+
+	if (!translatedTerm)
+		throwErrorAtLocation(term.location, "could not translate term", context);
+
+	return std::move(translatedTerm.value());
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#endif

include/anthem/output/AST.h

@@ -0,0 +1,345 @@
+#ifndef __ANTHEM__OUTPUT__AST_H
+#define __ANTHEM__OUTPUT__AST_H
+
+#include <cassert>
+
+#include <anthem/AST.h>
+#include <anthem/Utils.h>
+#include <anthem/output/ColorStream.h>
+#include <anthem/output/Formatting.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// AST
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_);
+output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation);
+output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean);
+output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison);
+output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant);
+output::ColorStream &operator<<(output::ColorStream &stream, const Function &function);
+output::ColorStream &operator<<(output::ColorStream &stream, const In &in);
+output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer);
+output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval);
+output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate);
+output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger);
+output::ColorStream &operator<<(output::ColorStream &stream, const String &string);
+output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable);
+
+output::ColorStream &operator<<(output::ColorStream &stream, const And &and_);
+output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional);
+output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists);
+output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll);
+output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies);
+output::ColorStream &operator<<(output::ColorStream &stream, const Not &not_);
+output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_);
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula);
+output::ColorStream &operator<<(output::ColorStream &stream, const Term &term);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Primitives
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, BinaryOperation::Operator operator_)
+{
+	switch (operator_)
+	{
+		case BinaryOperation::Operator::Plus:
+			return (stream << output::Operator("+"));
+		case BinaryOperation::Operator::Minus:
+			return (stream << output::Operator("-"));
+		case BinaryOperation::Operator::Multiplication:
+			return (stream << output::Operator("*"));
+		case BinaryOperation::Operator::Division:
+			return (stream << output::Operator("/"));
+		case BinaryOperation::Operator::Modulo:
+			return (stream << output::Operator("%"));
+	}
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const BinaryOperation &binaryOperation)
+{
+	return (stream << "(" << binaryOperation.left << " " << binaryOperation.operator_ << " " << binaryOperation.right << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Boolean &boolean)
+{
+	if (boolean.value)
+		return (stream << output::Boolean("#true"));
+
+	return (stream << output::Boolean("#false"));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, Comparison::Operator operator_)
+{
+	switch (operator_)
+	{
+		case Comparison::Operator::GreaterThan:
+			return (stream << output::Operator(">"));
+		case Comparison::Operator::LessThan:
+			return (stream << output::Operator("<"));
+		case Comparison::Operator::LessEqual:
+			return (stream << output::Operator("<="));
+		case Comparison::Operator::GreaterEqual:
+			return (stream << output::Operator(">="));
+		case Comparison::Operator::NotEqual:
+			return (stream << output::Operator("!="));
+		case Comparison::Operator::Equal:
+			return (stream << output::Operator("="));
+	}
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Comparison &comparison)
+{
+	return (stream << comparison.left << " " << comparison.operator_ << " " << comparison.right);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Constant &constant)
+{
+	return (stream << constant.name);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Function &function)
+{
+	stream << function.name;
+
+	if (function.arguments.empty())
+		return stream;
+
+	stream << "(";
+
+	for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++)
+	{
+		if (i != function.arguments.cbegin())
+			stream << ", ";
+
+		stream << (*i);
+	}
+
+	if (function.name.empty() && function.arguments.size() == 1)
+		stream << ",";
+
+	return (stream << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const In &in)
+{
+	return (stream << in.element << " " << output::Keyword("in") << " " << in.set);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Integer &integer)
+{
+	return (stream << output::Number<int>(integer.value));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Interval &interval)
+{
+	return (stream << interval.from << ".." << interval.to);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Predicate &predicate)
+{
+	stream << predicate.name;
+
+	if (predicate.arguments.empty())
+		return stream;
+
+	stream << "(";
+
+	for (auto i = predicate.arguments.cbegin(); i != predicate.arguments.cend(); i++)
+	{
+		if (i != predicate.arguments.cbegin())
+			stream << ", ";
+
+		stream << (*i);
+	}
+
+	return (stream << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const SpecialInteger &specialInteger)
+{
+	switch (specialInteger.type)
+	{
+		case SpecialInteger::Type::Infimum:
+			return (stream << output::Number<std::string>("#inf"));
+		case SpecialInteger::Type::Supremum:
+			return (stream << output::Number<std::string>("#sup"));
+	}
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const String &string)
+{
+	return (stream << output::String(string.text.c_str()));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Variable &variable)
+{
+	assert(!variable.name.empty());
+	assert(variable.name[0] >= 65 && variable.name[0] <= 90);
+
+	if (variable.type == ast::Variable::Type::Reserved || !isReservedVariableName(variable.name.c_str()))
+		return (stream << output::Variable(variable.name.c_str()));
+
+	const auto variableName = std::string(UserVariablePrefix) + variable.name;
+
+	return (stream << output::Variable(variableName.c_str()));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Expressions
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const And &and_)
+{
+	stream << "(";
+
+	for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
+	{
+		if (i != and_.arguments.cbegin())
+			stream << " " << output::Keyword("and") << " ";
+
+		stream << (*i);
+	}
+
+	return (stream << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Biconditional &biconditional)
+{
+	return (stream << "(" << biconditional.left << " <-> " << biconditional.right << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Exists &exists)
+{
+	stream << output::Keyword("exists") << " ";
+
+	for (auto i = exists.variables.cbegin(); i != exists.variables.cend(); i++)
+	{
+		if (i != exists.variables.cbegin())
+			stream << ", ";
+
+		stream << (**i);
+	}
+
+	return (stream << " " << exists.argument);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const ForAll &forAll)
+{
+	stream << output::Keyword("forall") << " ";
+
+	for (auto i = forAll.variables.cbegin(); i != forAll.variables.cend(); i++)
+	{
+		if (i != forAll.variables.cbegin())
+			stream << ", ";
+
+		stream << (**i);
+	}
+
+	return (stream << " " << forAll.argument);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Implies &implies)
+{
+	return (stream << "(" << implies.antecedent << " -> " << implies.consequent << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Not &not_)
+{
+	return (stream << output::Keyword("not ") << not_.argument);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Or &or_)
+{
+	stream << "(";
+
+	for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
+	{
+		if (i != or_.arguments.cbegin())
+			stream << " " << output::Keyword("or") << " ";
+
+		stream << (*i);
+	}
+
+	return (stream << ")");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Variants
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Formula &formula)
+{
+	formula.match([&](const auto &x){stream << *x;});
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+output::ColorStream &operator<<(output::ColorStream &stream, const Term &term)
+{
+	term.match([&](const auto &x){stream << *x;});
+
+	return stream;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif

include/anthem/output/ClingoOutput.h

@@ -1,36 +0,0 @@
-#ifndef __ANTHEM__OUTPUT__CLINGO_OUTPUT_H
-#define __ANTHEM__OUTPUT__CLINGO_OUTPUT_H
-
-#include <clingo.hh>
-
-#include <anthem/output/ColorStream.h>
-
-namespace anthem
-{
-namespace output
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// ClingoOutput
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::Symbol &symbol);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Sign &sign);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Boolean &boolean);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Variable &variable);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperator &binaryOperator);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::UnaryOperation &unaryOperation);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperation &binaryOperation);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Interval &interval);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Function &function);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Pool &pool);
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Term &term);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}
-
-#endif

include/anthem/output/Formatting.h

@@ -118,7 +118,7 @@ struct Keyword
 inline ColorStream &operator<<(ColorStream &stream, const Keyword &keyword)
 {
 	return (stream
-		<< Format({Color::Blue, FontWeight::Bold})
+		<< Format({Color::Blue, FontWeight::Normal})
 		<< keyword.name
 		<< ResetFormat());
 }

src/anthem/Translation.cpp

@@ -8,6 +8,7 @@
 
 #include <anthem/Context.h>
 #include <anthem/StatementVisitor.h>
+#include <anthem/output/AST.h>
 
 namespace anthem
 {
@@ -40,7 +41,12 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	const auto translateStatement =
 		[&context](const Clingo::AST::Statement &statement)
 		{
-			statement.data.accept(StatementVisitor(), statement, context);
+			const auto formula = statement.data.accept(StatementVisitor(), statement, context);
+
+			if (!formula)
+				return;
+
+			context.logger.outputStream() << formula.value() << std::endl;
 		};
 
 	const auto logger =

src/anthem/output/ClingoOutput.cpp

@@ -1,257 +0,0 @@
-#include <anthem/output/ClingoOutput.h>
-
-#include <anthem/Utils.h>
-#include <anthem/output/Formatting.h>
-
-namespace anthem
-{
-namespace output
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// ClingoOutput
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-const auto printCollection = [](auto &stream, const auto &collection,
-	const auto &preToken, const auto &delimiter, const auto &postToken, bool printTokensIfEmpty)
-{
-	if (collection.empty() && !printTokensIfEmpty)
-		return;
-
-	if (collection.empty() && printTokensIfEmpty)
-	{
-		stream << preToken << postToken;
-		return;
-	}
-
-	stream << preToken;
-
-	// TODO: use cbegin/cend (requires support by Clingo::SymbolSpan)
-	for (auto i = collection.begin(); i != collection.end(); i++)
-	{
-		if (i != collection.begin())
-			stream << delimiter;
-
-		stream << *i;
-	}
-
-	stream << postToken;
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::Symbol &symbol)
-{
-	switch (symbol.type())
-	{
-		case Clingo::SymbolType::Infimum:
-			return (stream << Keyword("#inf"));
-		case Clingo::SymbolType::Supremum:
-			return (stream << Keyword("#sup"));
-		case Clingo::SymbolType::Number:
-			return (stream << Number<decltype(symbol.number())>(symbol.number()));
-		case Clingo::SymbolType::String:
-			return (stream << String(symbol.string()));
-		case Clingo::SymbolType::Function:
-		{
-			const auto isNegative = symbol.is_negative();
-			assert(isNegative != symbol.is_positive());
-
-			const auto isUnaryTuple = (symbol.name()[0] == '\0' && symbol.arguments().size() == 1);
-			const auto printIfEmpty = (symbol.name()[0] == '\0' || !symbol.arguments().empty());
-
-			if (isNegative)
-				stream << Operator("-");
-
-			stream << Function(symbol.name());
-
-			const auto postToken = (isUnaryTuple ? ",)" : ")");
-
-			printCollection(stream, symbol.arguments(), "(", ", ", postToken, printIfEmpty);
-
-			return stream;
-		}
-	}
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Sign &sign)
-{
-	switch (sign)
-	{
-		case Clingo::AST::Sign::None:
-			return stream;
-		case Clingo::AST::Sign::Negation:
-			return (stream << Keyword("not") << " ");
-		case Clingo::AST::Sign::DoubleNegation:
-			return (stream << Keyword("not") << " " << Keyword("not") << " ");
-	}
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Boolean &boolean)
-{
-	if (boolean.value == true)
-		return (stream << Boolean("#true"));
-
-	return (stream << Boolean("#false"));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Variable &variable)
-{
-	if (!isReservedVariableName(variable.name))
-		return (stream << Variable(variable.name));
-
-	const auto variableName = std::string(UserVariablePrefix) + variable.name;
-
-	return (stream << Variable(variableName.c_str()));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperator &binaryOperator)
-{
-	switch (binaryOperator)
-	{
-		case Clingo::AST::BinaryOperator::XOr:
-			return (stream << Keyword("xor"));
-		case Clingo::AST::BinaryOperator::Or:
-			return (stream << Keyword("or"));
-		case Clingo::AST::BinaryOperator::And:
-			return (stream << Keyword("and"));
-		case Clingo::AST::BinaryOperator::Plus:
-			return (stream << Operator("+"));
-		case Clingo::AST::BinaryOperator::Minus:
-			return (stream << Operator("-"));
-		case Clingo::AST::BinaryOperator::Multiplication:
-			return (stream << Operator("*"));
-		case Clingo::AST::BinaryOperator::Division:
-			return (stream << Operator("/"));
-		case Clingo::AST::BinaryOperator::Modulo:
-			return (stream << Operator("\\"));
-	}
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::UnaryOperation &unaryOperation)
-{
-	return (stream
-		<< Keyword(Clingo::AST::left_hand_side(unaryOperation.unary_operator))
-		<< unaryOperation.argument
-		<< Keyword(Clingo::AST::right_hand_side(unaryOperation.unary_operator)));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::BinaryOperation &binaryOperation)
-{
-	return (stream << "(" << binaryOperation.left
-		<< " " << binaryOperation.binary_operator
-		<< " " << binaryOperation.right << ")");
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Interval &interval)
-{
-	return (stream << "(" << interval.left << Operator("..") << interval.right << ")");
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Function &function)
-{
-	const auto isUnaryTuple = (function.name[0] == '\0' && function.arguments.size() == 1);
-	const auto printIfEmpty = (function.name[0] == '\0' || !function.arguments.empty());
-
-	if (function.external)
-		stream << Operator("@");
-
-	stream << output::Function(function.name);
-
-	const auto postToken = (isUnaryTuple ? ",)" : ")");
-
-	printCollection(stream, function.arguments, "(", ", ", postToken, printIfEmpty);
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Pool &pool)
-{
-	// Note: There is no representation for an empty pool
-	if (pool.arguments.empty())
-		return (stream << "(" << Number<int>(1) << "/" << Number<int>(0) << ")");
-
-	printCollection(stream, pool.arguments, "(", ";", ")", true);
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct TermOutputVisitor
-{
-	void visit(const Clingo::Symbol &symbol, ColorStream &stream)
-	{
-		stream << symbol;
-	}
-
-	void visit(const Clingo::AST::Variable &variable, ColorStream &stream)
-	{
-		stream << variable;
-	}
-
-	void visit(const Clingo::AST::UnaryOperation &unaryOperation, ColorStream &stream)
-	{
-		stream << unaryOperation;
-	}
-
-	void visit(const Clingo::AST::BinaryOperation &binaryOperation, ColorStream &stream)
-	{
-		stream << binaryOperation;
-	}
-
-	void visit(const Clingo::AST::Interval &interval, ColorStream &stream)
-	{
-		stream << interval;
-	}
-
-	void visit(const Clingo::AST::Function &function, ColorStream &stream)
-	{
-		stream << function;
-	}
-
-	void visit(const Clingo::AST::Pool &pool, ColorStream &stream)
-	{
-		stream << pool;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ColorStream &operator<<(ColorStream &stream, const Clingo::AST::Term &term)
-{
-	term.data.accept(TermOutputVisitor(), stream);
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}

tests/TestTranslation.cpp

@@ -21,7 +21,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(1..5).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in (1..5) -> p(V1)\n");
+		REQUIRE(output.str() == "(V1 in 1..5 -> p(V1))\n");
 	}
 
 	SECTION("simple example 2")
@@ -29,7 +29,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(N) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in N and exists X1, X2 (X1 in N and X2 in (1..5) and X1 = X2) -> p(V1)\n");
+		REQUIRE(output.str() == "((V1 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1))\n");
 	}
 
 	SECTION("simple example 3")
@@ -37,7 +37,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(N + 1) :- q(N).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in (N + 1) and exists X1 (X1 in N and q(X1)) -> p(V1)\n");
+		REQUIRE(output.str() == "((V1 in (N + 1) and exists X1 (X1 in N and q(X1))) -> p(V1))\n");
 	}
 
 	SECTION("n-ary head")
@@ -45,7 +45,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in N and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in N and X2 in (1..5) and X1 = X2) -> p(V1, V2, V3)\n");
+		REQUIRE(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n");
 	}
 
 	SECTION("disjunctive head")
@@ -54,7 +54,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in (1..5) and X1 = X2) -> p(V1, V2, V3) or q(V4, V5)\n");
+		REQUIRE(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
 	}
 
 	SECTION("disjunctive head (alternative syntax)")
@@ -63,7 +63,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in (1..5) and X1 = X2) -> p(V1, V2, V3) or q(V4, V5)\n");
+		REQUIRE(output.str() == "((V1 in N and V2 in 1 and V3 in 2 and V4 in 3 and V5 in N and exists X1, X2 (X1 in N and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
 	}
 
 	SECTION("escaping conflicting variable names")
@@ -71,7 +71,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X1, V1) :- q(X1), q(V1).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in _X1 and V2 in _V1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in _X1 and V2 in _V1 and exists X1 (X1 in _X1 and q(X1)) and exists X2 (X2 in _V1 and q(X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("fact")
@@ -79,7 +79,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(42).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in 42 -> p(V1)\n");
+		REQUIRE(output.str() == "(V1 in 42 -> p(V1))\n");
 	}
 
 	SECTION("0-ary fact")
@@ -87,7 +87,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "#true -> p\n");
+		REQUIRE(output.str() == "(#true -> p)\n");
 	}
 
 	SECTION("disjunctive fact (no arguments)")
@@ -95,7 +95,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q; p.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "#true -> p or q\n");
+		REQUIRE(output.str() == "(#true -> (p or q))\n");
 	}
 
 	SECTION("disjunctive fact (arguments)")
@@ -103,7 +103,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q; p(42).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in 42 -> p(V1) or q\n");
+		REQUIRE(output.str() == "(V1 in 42 -> (p(V1) or q))\n");
 	}
 
 	SECTION("integrity constraint (no arguments)")
@@ -111,7 +111,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":- p, q.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "p and q -> #false\n");
+		REQUIRE(output.str() == "((p and q) -> #false)\n");
 	}
 
 	SECTION("contradiction")
@@ -119,7 +119,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":-.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "#true -> #false\n");
+		REQUIRE(output.str() == "(#true -> #false)\n");
 	}
 
 	SECTION("integrity constraint (arguments)")
@@ -127,7 +127,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":- p(42), q.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "exists X1 (X1 in 42 and p(X1)) and q -> #false\n");
+		REQUIRE(output.str() == "((exists X1 (X1 in 42 and p(X1)) and q) -> #false)\n");
 	}
 
 	SECTION("inf/sup")
@@ -135,7 +135,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, #inf) :- q(X, #sup).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in #inf and exists X1, X2 (X1 in X and X2 in #sup and q(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in #inf and exists X1, X2 (X1 in X and X2 in #sup and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("strings")
@@ -143,7 +143,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, \"foo\") :- q(X, \"bar\").";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in \"foo\" and exists X1, X2 (X1 in X and X2 in \"bar\" and q(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in \"foo\" and exists X1, X2 (X1 in X and X2 in \"bar\" and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("tuples")
@@ -151,7 +151,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, (1, 2, 3)) :- q(X, (4, 5)).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in (1, 2, 3) and exists X1, X2 (X1 in X and X2 in (4, 5) and q(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in (1, 2, 3) and exists X1, X2 (X1 in X and X2 in (4, 5) and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("1-ary tuples")
@@ -159,7 +159,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, (1,)) :- q(X, (2,)).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in (1,) and exists X1, X2 (X1 in X and X2 in (2,) and q(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in (1,) and exists X1, X2 (X1 in X and X2 in (2,) and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("intervals")
@@ -167,7 +167,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, 1..10) :- q(X, 6..12).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in (1..10) and exists X1, X2 (X1 in X and X2 in (6..12) and q(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in 1..10 and exists X1, X2 (X1 in X and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("comparisons")
@@ -175,7 +175,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(M, N, O, P) :- M < N, P != O.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in M and V2 in N and V3 in O and V4 in P and exists X1, X2 (X1 in M and X2 in N and X1 < X2) and exists X3, X4 (X3 in P and X4 in O and X3 != X4) -> p(V1, V2, V3, V4)\n");
+		REQUIRE(output.str() == "((V1 in M and V2 in N and V3 in O and V4 in P and exists X1, X2 (X1 in M and X2 in N and X1 < X2) and exists X3, X4 (X3 in P and X4 in O and X3 != X4)) -> p(V1, V2, V3, V4))\n");
 	}
 
 	SECTION("single negation")
@@ -183,7 +183,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "not p(X, 1) :- not q(X, 2).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) -> not p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2))) -> not p(V1, V2))\n");
 	}
 
 	SECTION("variable numbering")
@@ -192,9 +192,9 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "f; q(A1, A2); p(A3, r(A4)); g(g(A5)) :- g(A3), f, q(A4, A1), p(A2, A5).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in A1 and V2 in A2 and V3 in A3 and V4 in r(A4) and V5 in g(A5)"
-		        " and exists X1 (X1 in A3 and g(X1)) and f and exists X2, X3 (X2 in A4 and X3 in A1 and q(X2, X3)) and exists X4, X5 (X4 in A2 and X5 in A5 and p(X4, X5))"
-		        " -> q(V1, V2) or p(V3, V4) or g(V5) or f\n");
+		REQUIRE(output.str() == "((V1 in A1 and V2 in A2 and V3 in A3 and V4 in r(A4) and V5 in g(A5)"
+		        " and exists X1 (X1 in A3 and g(X1)) and f and exists X2, X3 (X2 in A4 and X3 in A1 and q(X2, X3)) and exists X4, X5 (X4 in A2 and X5 in A5 and p(X4, X5)))"
+		        " -> (q(V1, V2) or p(V3, V4) or g(V5) or f))\n");
 	}
 
 	SECTION("nested functions")
@@ -202,7 +202,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(q(s(t(X1))), u(X2)) :- u(v(w(X2)), z(X1)).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in q(s(t(_X1))) and V2 in u(_X2) and exists X1, X2 (X1 in v(w(_X2)) and X2 in z(_X1) and u(X1, X2)) -> p(V1, V2)\n");
+		REQUIRE(output.str() == "((V1 in q(s(t(_X1))) and V2 in u(_X2) and exists X1, X2 (X1 in v(w(_X2)) and X2 in z(_X1) and u(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("choice rule (simple)")
@@ -210,7 +210,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p}.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "p -> p\n");
+		REQUIRE(output.str() == "(p -> p)\n");
 	}
 
 	SECTION("choice rule (two elements)")
@@ -218,7 +218,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p; q}.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "p or q -> p or q\n");
+		REQUIRE(output.str() == "((p or q) -> (p or q))\n");
 	}
 
 	SECTION("choice rule (n-ary elements)")
@@ -226,7 +226,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p(1..3, N); q(2..4)}.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in (1..3) and V2 in N and V3 in (2..4) and (p(V1, V2) or q(V3)) -> p(V1, V2) or q(V3)\n");
+		REQUIRE(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and (p(V1, V2) or q(V3))) -> (p(V1, V2) or q(V3)))\n");
 	}
 
 	SECTION("choice rule with body")
@@ -234,6 +234,22 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p(M, N); q(P)} :- s(M, N, P).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and (p(V1, V2) or q(V3)) -> p(V1, V2) or q(V3)\n");
+		REQUIRE(output.str() == "((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and (p(V1, V2) or q(V3))) -> (p(V1, V2) or q(V3)))\n");
+	}
+
+	SECTION("choice rule with negation")
+	{
+		input << "{not p(X, 1)} :- not q(X, 2).";
+		anthem::translate("input", input, context);
+
+		REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n");
+	}
+
+	SECTION("choice rule with negation (two elements)")
+	{
+		input << "{not p(X, 1); not s} :- not q(X, 2).";
+		anthem::translate("input", input, context);
+
+		REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and (not p(V1, V2) or not s)) -> (not p(V1, V2) or not s))\n");
 	}
 }