Version bump for release 0.1.8 RC 1

Add new simplification rule
This adds the rule “(not F or G) === (F -> G)” to the simplification rule tableau.
2018-04-10 00:19:55 +02:00 · 2018-04-09 23:48:04 +02:00 · 2018-04-09 23:39:29 +02:00 · 2018-04-09 23:36:16 +02:00 · 2018-04-09 23:27:38 +02:00 · 2018-04-08 22:24:14 +02:00
36 changed files with 445 additions and 1438 deletions
--- a/.ci/Dockerfile-ubuntu-18.04
+++ b/.ci/Dockerfile-ubuntu-18.04
@@ -3,7 +3,7 @@ FROM ubuntu:18.04
 ARG toolchain

 RUN apt-get update
-RUN apt-get install -y bison cmake git ninja-build re2c
+RUN apt-get install -y cmake git ninja-build re2c
 RUN if [ "${toolchain}" = "gcc" ]; then apt-get install -y g++; fi
 RUN if [ "${toolchain}" = "clang" ]; then apt-get install -y clang; fi

--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,19 +1,10 @@
 # Change Log

-## 0.1.9 RC 1 (2018-04-20)
+## 0.1.8 RC 1 (2018-04-10)

 ### Features

-* optional detection of integer variables and integer predicate parameters
-* command-line option `--detect-integers` to enable integer variable detection
-
-## 0.1.8 (2018-04-20)
-
-### Features
-
-* more and advanced simplification rules
-* adds support for exponentiation (power) and modulus (absolute value)
-* new examples: prime numbers, permutation generator, and graph coloring (extended)
+* more, advanced simplification rules

 ## 0.1.7 (2018-04-08)

--- a/README.md
+++ b/README.md
@@ -9,11 +9,10 @@
 ## Usage

 ```bash
-$ anthem [--complete] [--simplify] file...
+$ anthem [--simplify] file...
 ```

-`--complete` instructs `anthem` to perform Clark’s completion on the translated formulas.
-With the option `--simplify`, the output formulas are simplified by applying several basic transformation rules.
+With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.

 ## Building

--- a/app/main.cpp
+++ b/app/main.cpp
@@ -18,7 +18,6 @@ int main(int argc, char **argv)
 		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
 		("s,simplify", "Simplify the output")
 		("c,complete", "Perform completion")
-		("d,detect-integers", "Detect integer variables")
 		("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
 		("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
 		("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
@@ -51,7 +50,6 @@ int main(int argc, char **argv)

 		context.performSimplification = (parseResult.count("simplify") > 0);
 		context.performCompletion = (parseResult.count("complete") > 0);
-		context.performIntegerDetection = (parseResult.count("detect-integers") > 0);
 		colorPolicyString = parseResult["color"].as<std::string>();
 		parenthesisStyleString = parseResult["parentheses"].as<std::string>();
 		logPriorityString = parseResult["log-priority"].as<std::string>();
@@ -72,7 +70,7 @@ int main(int argc, char **argv)

 	if (version)
 	{
-		std::cout << "anthem version 0.1.9-rc.1" << std::endl;
+		std::cout << "anthem version 0.1.8-rc.1" << std::endl;
 		return EXIT_SUCCESS;
 	}

--- a/examples/graph-coloring.lp
+++ b/examples/graph-coloring.lp
@@ -3,8 +3,7 @@
 #external vertex(1).
 #show color/2.

-{color(V, C)} :- vertex(V), color(C).
+{color(V,C)} :- vertex(V), color(C).
 covered(V) :- color(V, _).
 :- vertex(V), not covered(V).
-:- color(V1, C), color(V2, C), edge(V1, V2).
-:- color(V, C1), color(V, C2), C1 != C2.
+:- color(V1,C), color(V2,C), edge(V1,V2).
--- a/examples/permutations.lp
+++ b/examples/permutations.lp
@@ -1,13 +0,0 @@
-#show p/2.
-#external integer(n(0)).
-
-{p(1..n, 1..n)}.
-
-:- p(X, Y1), p(X, Y2), Y1 != Y2.
-:- p(X1, Y), p(X2, Y), X1 != X2.
-
-q1(X) :- p(X, _).
-q2(Y) :- p(_, Y).
-
-:- not q1(X), X = 1..n.
-:- not q2(Y), Y = 1..n.
--- a/examples/prime.lp
+++ b/examples/prime.lp
@@ -1,5 +0,0 @@
-#show prime/1.
-#external integer(n(0)).
-
-composite(I * J) :- I = 2..n, J = 2..n.
-prime(N) :- N = 2..n, not composite(N).
--- a/examples/schur-numbers.lp
+++ b/examples/schur-numbers.lp
@@ -1,9 +1,7 @@
-#show in/2.
-#external integer(n(0)).
-#external integer(r(0)).
-
 {in(1..n, 1..r)}.
 covered(I) :- in(I, S).

 :- I = 1..n, not covered(I).
 :- in(I, S), in(J, S), in(I + J, S).
+
+#show in/2.
--- a/include/anthem/AST.h
+++ b/include/anthem/AST.h
@@ -2,8 +2,6 @@
 #define __ANTHEM__AST_H

 #include <anthem/ASTForward.h>
-#include <anthem/Domain.h>
-#include <anthem/Tristate.h>

 namespace anthem
 {
@@ -34,8 +32,7 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo,
-		Power
+		Modulo
 	};

 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@@ -105,15 +102,32 @@ struct Comparison

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

-struct Function
+struct Constant
 {
-	explicit Function(FunctionDeclaration *declaration)
-	:	declaration{declaration}
+	explicit Constant(std::string &&name)
+	:	name{std::move(name)}
 	{
 	}

-	explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
-	:	declaration{declaration},
+	Constant(const Constant &other) = delete;
+	Constant &operator=(const Constant &other) = delete;
+	Constant(Constant &&other) = default;
+	Constant &operator=(Constant &&other) = default;
+
+	std::string name;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Function
+{
+	explicit Function(std::string &&name)
+	:	name{std::move(name)}
+	{
+	}
+
+	explicit Function(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -123,33 +137,8 @@ struct Function
 	Function(Function &&other) noexcept = default;
 	Function &operator=(Function &&other) noexcept = default;

-	FunctionDeclaration *declaration;
-	std::vector<Term> arguments;
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct FunctionDeclaration
-{
-	explicit FunctionDeclaration(std::string &&name)
-	:	name{std::move(name)}
-	{
-	}
-
-	explicit FunctionDeclaration(std::string &&name, size_t arity)
-	:	name{std::move(name)},
-		arity{arity}
-	{
-	}
-
-	FunctionDeclaration(const FunctionDeclaration &other) = delete;
-	FunctionDeclaration &operator=(const FunctionDeclaration &other) = delete;
-	FunctionDeclaration(FunctionDeclaration &&other) noexcept = default;
-	FunctionDeclaration &operator=(FunctionDeclaration &&other) noexcept = default;
-
 	std::string name;
-	size_t arity;
-	Domain domain{Domain::General};
+	std::vector<Term> arguments;
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -214,13 +203,13 @@ struct Interval

 struct Predicate
 {
-	explicit Predicate(PredicateDeclaration *declaration)
-	:	declaration{declaration}
+	explicit Predicate(std::string &&name)
+	:	name{std::move(name)}
 	{
 	}

-	explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
-	:	declaration{declaration},
+	explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -230,47 +219,35 @@ struct Predicate
 	Predicate(Predicate &&other) noexcept = default;
 	Predicate &operator=(Predicate &&other) noexcept = default;

-	PredicateDeclaration *declaration{nullptr};
+	std::size_t arity() const
+	{
+		return arguments.size();
+	}
+
+	std::string name;
 	std::vector<Term> arguments;
 };

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

-struct PredicateDeclaration
+// TODO: make more use of this class
+struct PredicateSignature
 {
-	enum class Visibility
-	{
-		Default,
-		Visible,
-		Hidden
-	};
-
-	struct Parameter
-	{
-		Domain domain{Domain::Unknown};
-	};
-
-	explicit PredicateDeclaration(std::string &&name, size_t arity)
+	explicit PredicateSignature(std::string &&name, size_t arity)
 	:	name{std::move(name)},
-		parameters{std::vector<Parameter>(arity)}
+		arity{arity}
 	{
 	}

-	PredicateDeclaration(const PredicateDeclaration &other) = delete;
-	PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
-	PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
-	PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
-
-	size_t arity() const noexcept
-	{
-		return parameters.size();
-	}
+	PredicateSignature(const PredicateSignature &other) = delete;
+	PredicateSignature &operator=(const PredicateSignature &other) = delete;
+	// TODO: make noexcept again
+	// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
+	PredicateSignature(PredicateSignature &&other) = default;
+	PredicateSignature &operator=(PredicateSignature &&other) = default;

 	std::string name;
-	std::vector<Parameter> parameters;
-	bool isUsed{false};
-	bool isExternal{false};
-	Visibility visibility{Visibility::Default};
+	size_t arity;
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -315,30 +292,6 @@ struct String

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

-struct UnaryOperation
-{
-	enum class Operator
-	{
-		Absolute
-	};
-
-	explicit UnaryOperation(Operator operator_, Term &&argument)
-	:	operator_{operator_},
-		argument{std::move(argument)}
-	{
-	}
-
-	UnaryOperation(const UnaryOperation &other) = delete;
-	UnaryOperation &operator=(const UnaryOperation &other) = delete;
-	UnaryOperation(UnaryOperation &&other) noexcept = default;
-	UnaryOperation &operator=(UnaryOperation &&other) noexcept = default;
-
-	Operator operator_;
-	Term argument;
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct Variable
 {
 	explicit Variable(VariableDeclaration *declaration)
@@ -382,7 +335,6 @@ struct VariableDeclaration
 	VariableDeclaration &operator=(VariableDeclaration &&other) = default;

 	Type type;
-	Domain domain{Domain::Unknown};
 	std::string name;
 };

--- a/include/anthem/ASTCopy.h
+++ b/include/anthem/ASTCopy.h
@@ -22,6 +22,7 @@ namespace ast
 BinaryOperation prepareCopy(const BinaryOperation &other);
 Boolean prepareCopy(const Boolean &other);
 Comparison prepareCopy(const Comparison &other);
+Constant prepareCopy(const Constant &other);
 Function prepareCopy(const Function &other);
 In prepareCopy(const In &other);
 Integer prepareCopy(const Integer &other);
--- a/include/anthem/ASTForward.h
+++ b/include/anthem/ASTForward.h
@@ -24,10 +24,10 @@ struct BinaryOperation;
 struct Biconditional;
 struct Boolean;
 struct Comparison;
+struct Constant;
 struct Exists;
 struct ForAll;
 struct Function;
-struct FunctionDeclaration;
 struct Implies;
 struct In;
 struct Integer;
@@ -35,10 +35,8 @@ struct Interval;
 struct Not;
 struct Or;
 struct Predicate;
-struct PredicateDeclaration;
 struct SpecialInteger;
 struct String;
-struct UnaryOperation;
 struct Variable;
 struct VariableDeclaration;
 using VariableDeclarationPointer = std::unique_ptr<VariableDeclaration>;
@@ -64,12 +62,12 @@ using Formula = Clingo::Variant<
 using Term = Clingo::Variant<
 	BinaryOperation,
 	Boolean,
+	Constant,
 	Function,
 	Integer,
 	Interval,
 	SpecialInteger,
 	String,
-	UnaryOperation,
 	Variable>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/ASTUtils.h
+++ b/include/anthem/ASTUtils.h
@@ -36,6 +36,12 @@ class VariableStack
 		std::vector<Layer> m_layers;
 };

+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &lhs, const Predicate &rhs);
+bool matches(const Predicate &predicate, const PredicateSignature &signature);
+bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context);

 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables
--- a/include/anthem/ASTVisitors.h
+++ b/include/anthem/ASTVisitors.h
@@ -123,6 +123,12 @@ struct RecursiveTermVisitor
 		return T::accept(boolean, term, std::forward<Arguments>(arguments)...);
 	}

+	template <class... Arguments>
+	ReturnType visit(Constant &constant, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(constant, term, std::forward<Arguments>(arguments)...);
+	}
+
 	template <class... Arguments>
 	ReturnType visit(Function &function, Term &term, Arguments &&... arguments)
 	{
@@ -159,14 +165,6 @@ struct RecursiveTermVisitor
 		return T::accept(string, term, std::forward<Arguments>(arguments)...);
 	}

-	template <class... Arguments>
-	ReturnType visit(UnaryOperation &unaryOperation, Term &term, Arguments &&... arguments)
-	{
-		unaryOperation.argument.accept(*this, unaryOperation.argument, std::forward<Arguments>(arguments)...);
-
-		return T::accept(unaryOperation, term, std::forward<Arguments>(arguments)...);
-	}
-
 	template <class... Arguments>
 	ReturnType visit(Variable &variable, Term &term, Arguments &&... arguments)
 	{
--- a/include/anthem/Body.h
+++ b/include/anthem/Body.h
@@ -43,22 +43,19 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
 struct BodyTermTranslateVisitor
 {
 	// TODO: refactor
-	std::optional<ast::Formula> visit(const Clingo::AST::Function &function,
-		const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext,
-		Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throw TranslationException(literal.location, "double-negated literals currently unsupported");

-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
-		predicateDeclaration->isUsed = true;
-
 		if (function.arguments.empty())
 		{
+			auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
+
 			if (literal.sign == Clingo::AST::Sign::None)
-				return ast::Predicate(predicateDeclaration);
+				return std::move(predicate);
 			else if (literal.sign == Clingo::AST::Sign::Negation)
-				return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
+				return ast::Formula::make<ast::Not>(std::move(predicate));
 		}

 		// Create new body variable declarations
@@ -76,12 +73,12 @@ struct BodyTermTranslateVisitor
 		for (size_t i = 0; i < function.arguments.size(); i++)
 		{
 			auto &argument = function.arguments[i];
-			conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
+			conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
 		}

 		variableStack.pop();

-		ast::Predicate predicate(predicateDeclaration);
+		ast::Predicate predicate(std::string(function.name));
 		predicate.arguments.reserve(function.arguments.size());

 		for (size_t i = 0; i < function.arguments.size(); i++)
@@ -96,8 +93,7 @@ struct BodyTermTranslateVisitor
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
-		const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
 	{
 		assert(!term.data.is<Clingo::AST::Function>());

@@ -110,18 +106,18 @@ struct BodyTermTranslateVisitor

 struct BodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
 	{
 		return ast::Formula::make<ast::Boolean>(boolean.value);
 	}

-	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
-		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
+		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
 	}

 	// TODO: refactor
-	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
 		if (literal.sign != Clingo::AST::Sign::None)
@@ -136,15 +132,15 @@ struct BodyLiteralTranslateVisitor

 		ast::And conjunction;
 		conjunction.arguments.reserve(3);
-		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, context, variableStack)));
-		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, context, variableStack)));
+		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, variableStack)));
+		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, variableStack)));
 		conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));

 		return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
 		return std::nullopt;
@@ -155,16 +151,16 @@ struct BodyLiteralTranslateVisitor

 struct BodyBodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (bodyLiteral.sign != Clingo::AST::Sign::None)
 			throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");

-		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
+		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
 		return std::nullopt;
--- a/include/anthem/Context.h
+++ b/include/anthem/Context.h
@@ -16,9 +16,9 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-struct PredicateDeclarationMeta
+struct PredicateSignatureMeta
 {
-	ast::PredicateDeclaration *declaration;
+	ast::PredicateSignature predicateSignature;
 	bool used{false};
 };

@@ -33,59 +33,13 @@ struct Context
 	{
 	}

-	ast::PredicateDeclaration *findOrCreatePredicateDeclaration(const char *name, size_t arity)
-	{
-		const auto matchesExistingPredicateDeclaration =
-			[&](const auto &predicateDeclaration)
-			{
-				return (predicateDeclaration->arity() == arity
-					&& strcmp(predicateDeclaration->name.c_str(), name) == 0);
-			};
-
-		auto matchingPredicateDeclaration = std::find_if(predicateDeclarations.begin(),
-			predicateDeclarations.end(), matchesExistingPredicateDeclaration);
-
-		if (matchingPredicateDeclaration != predicateDeclarations.end())
-			return matchingPredicateDeclaration->get();
-
-		predicateDeclarations.emplace_back(std::make_unique<ast::PredicateDeclaration>(name, arity));
-
-		return predicateDeclarations.back().get();
-	}
-
-	ast::FunctionDeclaration *findOrCreateFunctionDeclaration(const char *name, size_t arity)
-	{
-		const auto matchesExistingFunctionDeclaration =
-			[&](const auto &functionDeclarations)
-			{
-				return (functionDeclarations->arity == arity
-					&& strcmp(functionDeclarations->name.c_str(), name) == 0);
-			};
-
-		auto matchingFunctionDeclaration = std::find_if(functionDeclarations.begin(),
-			functionDeclarations.end(), matchesExistingFunctionDeclaration);
-
-		if (matchingFunctionDeclaration != functionDeclarations.end())
-			return matchingFunctionDeclaration->get();
-
-		functionDeclarations.emplace_back(std::make_unique<ast::FunctionDeclaration>(name, arity));
-
-		return functionDeclarations.back().get();
-	}
-
 	output::Logger logger;

-	bool performSimplification{false};
-	bool performCompletion{false};
-	bool performIntegerDetection{false};
+	bool performSimplification = false;
+	bool performCompletion = false;

-	std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
-	ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
-
-	std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
-
-	bool externalStatementsUsed{false};
-	bool showStatementsUsed{false};
+	std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
+	std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;

 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };
--- a/include/anthem/Domain.h
+++ b/include/anthem/Domain.h
@@ -1,27 +0,0 @@
-#ifndef __ANTHEM__DOMAIN_H
-#define __ANTHEM__DOMAIN_H
-
-namespace anthem
-{
-namespace ast
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Domain
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class Domain
-{
-	General,
-	Integer,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}
-
-#endif
--- a/include/anthem/Equality.h
+++ b/include/anthem/Equality.h
@@ -3,7 +3,6 @@

 #include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
-#include <anthem/Tristate.h>

 namespace anthem
 {
@@ -16,6 +15,16 @@ namespace ast
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////

+// TODO: move to separate class
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 Tristate equal(const Formula &lhs, const Formula &rhs);
 Tristate equal(const Term &lhs, const Term &rhs);

@@ -228,7 +237,7 @@ struct FormulaEqualityVisitor

 		const auto &otherPredicate = otherFormula.get<Predicate>();

-		if (predicate.declaration != otherPredicate.declaration)
+		if (!matches(predicate, otherPredicate))
 			return Tristate::False;

 		assert(predicate.arguments.size() == otherPredicate.arguments.size());
@@ -289,6 +298,18 @@ struct TermEqualityVisitor
 			: Tristate::False;
 	}

+	Tristate visit(const Constant &constant, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Constant>())
+			return Tristate::Unknown;
+
+		const auto &otherConstant = otherTerm.get<Constant>();
+
+		return (constant.name == otherConstant.name)
+			? Tristate::True
+			: Tristate::False;
+	}
+
 	Tristate visit(const Function &function, const Term &otherTerm)
 	{
 		if (!otherTerm.is<Function>())
@@ -296,7 +317,7 @@ struct TermEqualityVisitor

 		const auto &otherFunction = otherTerm.get<Function>();

-		if (function.declaration != otherFunction.declaration)
+		if (function.name != otherFunction.name)
 			return Tristate::False;

 		if (function.arguments.size() != otherFunction.arguments.size())
@@ -361,19 +382,6 @@ struct TermEqualityVisitor
 			: Tristate::False;
 	}

-	Tristate visit(const UnaryOperation &unaryOperation, const Term &otherTerm)
-	{
-		if (!otherTerm.is<UnaryOperation>())
-			return Tristate::Unknown;
-
-		const auto &otherUnaryOperation = otherTerm.get<UnaryOperation>();
-
-		if (unaryOperation.operator_ != otherUnaryOperation.operator_)
-			return Tristate::Unknown;
-
-		return equal(unaryOperation.argument, otherUnaryOperation.argument);
-	}
-
 	Tristate visit(const Variable &variable, const Term &otherTerm)
 	{
 		if (!otherTerm.is<Variable>())
--- a/include/anthem/Head.h
+++ b/include/anthem/Head.h
@@ -118,7 +118,8 @@ struct HeadLiteralCollectFunctionTermsVisitor

 struct FunctionTermTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
+	// TODO: check correctness
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -129,14 +130,11 @@ struct FunctionTermTranslateVisitor
 		for (size_t i = 0; i < function.arguments.size(); i++)
 			arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));

-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
-		predicateDeclaration->isUsed = true;
-
-		return ast::Predicate(predicateDeclaration, std::move(arguments));
+		return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
 	{
 		throw TranslationException(term.location, "term currently unsupported in this context, function expected");
 		return std::nullopt;
@@ -147,18 +145,18 @@ struct FunctionTermTranslateVisitor

 struct LiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, size_t &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
 	{
 		return ast::Formula::make<ast::Boolean>(boolean.value);
 	}

-	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
-		return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
+		return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
 	{
 		throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
 		return std::nullopt;
@@ -169,12 +167,12 @@ struct LiteralTranslateVisitor

 struct HeadLiteralTranslateToConsequentVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throw TranslationException(literal.location, "double-negated head literals currently unsupported");

-		auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
+		auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, headVariableIndex);

 		if (literal.sign == Clingo::AST::Sign::None)
 			return translatedLiteral;
@@ -185,7 +183,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 		return ast::Formula::make<ast::Not>(std::move(translatedLiteral.value()));
 	}

-	std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		std::vector<ast::Formula> arguments;
 		arguments.reserve(disjunction.elements.size());
@@ -195,7 +193,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 			if (!conditionalLiteral.condition.empty())
 				throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");

-			auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
+			auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);

 			if (!argument)
 				throw TranslationException(headLiteral.location, "could not parse argument");
@@ -206,7 +204,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 		return ast::Formula::make<ast::Or>(std::move(arguments));
 	}

-	std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (aggregate.left_guard || aggregate.right_guard)
 			throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
@@ -217,7 +215,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 				if (!conditionalLiteral.condition.empty())
 					throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");

-				return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
+				return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
 			};

 		if (aggregate.elements.size() == 1)
@@ -240,7 +238,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 	}

 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
 	{
 		throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
 		return std::nullopt;
--- a/include/anthem/HiddenPredicateElimination.h
+++ b/include/anthem/HiddenPredicateElimination.h
@@ -13,7 +13,7 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
+void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);

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

--- a/include/anthem/IntegerVariableDetection.h
+++ b/include/anthem/IntegerVariableDetection.h
@@ -1,22 +0,0 @@
-#ifndef __ANTHEM__INTEGER_VARIABLE_DETECTION_H
-#define __ANTHEM__INTEGER_VARIABLE_DETECTION_H
-
-#include <anthem/AST.h>
-#include <anthem/Context.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// IntegerVariableDetection
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif
--- a/include/anthem/SimplificationVisitors.h
+++ b/include/anthem/SimplificationVisitors.h
@@ -137,6 +137,12 @@ struct TermSimplificationVisitor
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

+	template <class... Arguments>
+	SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
 	template <class... Arguments>
 	SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
 	{
--- a/include/anthem/StatementVisitor.h
+++ b/include/anthem/StatementVisitor.h
@@ -73,7 +73,7 @@ struct StatementVisitor

 		// Compute consequent
 		auto headVariableIndex = ruleContext.headVariablesStartIndex;
-		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
+		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);

 		assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);

@@ -87,7 +87,7 @@ struct StatementVisitor

 			const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
 			auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
-			auto set = translate(headTerm, ruleContext, context, variableStack);
+			auto set = translate(headTerm, ruleContext, variableStack);
 			auto in = ast::In(std::move(element), std::move(set));

 			antecedent.arguments.emplace_back(std::move(in));
@@ -98,7 +98,7 @@ struct StatementVisitor
 		{
 			const auto &bodyLiteral = *i;

-			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
+			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);

 			if (!argument)
 				throw TranslationException(bodyLiteral.location, "could not translate body literal");
@@ -165,8 +165,8 @@ struct StatementVisitor
 		if (signature.negative())
 			throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");

-		context.showStatementsUsed = true;
-		context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
+		if (!context.visiblePredicateSignatures)
+			context.visiblePredicateSignatures.emplace();

 		if (std::strlen(signature.name()) == 0)
 		{
@@ -176,8 +176,8 @@ struct StatementVisitor

 		context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";

-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
-		predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
+		auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
+		context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}

 	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@@ -190,7 +190,7 @@ struct StatementVisitor
 		const auto fail =
 			[&]()
 			{
-				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” or “#external integer(<function name>(<arity>)).” supported");
+				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” supported");
 			};

 		if (!external.body.empty())
@@ -204,47 +204,6 @@ struct StatementVisitor
 		if (predicate.arguments.size() != 1)
 			fail();

-		const auto handleIntegerDeclaration =
-			[&]()
-			{
-				// Integer function declarations are treated separately if applicable
-				if (strcmp(predicate.name, "integer") != 0)
-					return false;
-
-				if (predicate.arguments.size() != 1)
-					return false;
-
-				const auto &functionArgument = predicate.arguments.front();
-
-				if (!functionArgument.data.is<Clingo::AST::Function>())
-					return false;
-
-				const auto &function = functionArgument.data.get<Clingo::AST::Function>();
-
-				if (function.arguments.size() != 1)
-					return false;
-
-				const auto &arityArgument = function.arguments.front();
-
-				if (!arityArgument.data.is<Clingo::Symbol>())
-					return false;
-
-				const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
-
-				if (aritySymbol.type() != Clingo::SymbolType::Number)
-					return false;
-
-				const size_t arity = aritySymbol.number();
-
-				auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
-				functionDeclaration->domain = ast::Domain::Integer;
-
-				return true;
-			};
-
-		if (handleIntegerDeclaration())
-			return;
-
 		const auto &arityArgument = predicate.arguments.front();

 		if (!arityArgument.data.is<Clingo::Symbol>())
@@ -255,12 +214,13 @@ struct StatementVisitor
 		if (aritySymbol.type() != Clingo::SymbolType::Number)
 			fail();

-		context.externalStatementsUsed = true;
+		const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();

-		const size_t arity = aritySymbol.number();
+		if (!context.externalPredicateSignatures)
+			context.externalPredicateSignatures.emplace();

-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
-		predicateDeclaration->isExternal = true;
+		auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
+		context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}

 	template<class T>
--- a/include/anthem/Term.h
+++ b/include/anthem/Term.h
@@ -23,12 +23,6 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 {
 	switch (binaryOperator)
 	{
-		case Clingo::AST::BinaryOperator::XOr:
-			throw TranslationException(term.location, "binary operation “xor” currently unsupported");
-		case Clingo::AST::BinaryOperator::Or:
-			throw TranslationException(term.location, "binary operation “or” currently unsupported");
-		case Clingo::AST::BinaryOperator::And:
-			throw TranslationException(term.location, "binary operation “and” currently unsupported");
 		case Clingo::AST::BinaryOperator::Plus:
 			return ast::BinaryOperation::Operator::Plus;
 		case Clingo::AST::BinaryOperator::Minus:
@@ -39,39 +33,22 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 			return ast::BinaryOperation::Operator::Division;
 		case Clingo::AST::BinaryOperator::Modulo:
 			return ast::BinaryOperation::Operator::Modulo;
-		case Clingo::AST::BinaryOperator::Power:
-			return ast::BinaryOperation::Operator::Power;
+		default:
+			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
 	}

-	throw TranslationException(term.location, "unknown binary operation");
+	return ast::BinaryOperation::Operator::Plus;
 }

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

-ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator, const Clingo::AST::Term &term)
-{
-	switch (unaryOperator)
-	{
-		case Clingo::AST::UnaryOperator::Absolute:
-			return ast::UnaryOperation::Operator::Absolute;
-		case Clingo::AST::UnaryOperator::Minus:
-			throw TranslationException(term.location, "binary operation “minus” currently unsupported");
-		case Clingo::AST::UnaryOperator::Negation:
-			throw TranslationException(term.location, "binary operation “negation” currently unsupported");
-	}
-
-	throw TranslationException(term.location, "unknown unary operation");
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack);
+ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack);

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

 struct TermTranslateVisitor
 {
-	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		switch (symbol.type())
 		{
@@ -85,19 +62,19 @@ struct TermTranslateVisitor
 				return ast::Term::make<ast::String>(std::string(symbol.string()));
 			case Clingo::SymbolType::Function:
 			{
-				auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
-
-				auto function = ast::Function(functionDeclaration);
-				function.arguments.reserve(symbol.arguments().size());
+				auto function = ast::Term::make<ast::Function>(symbol.name());
+				// TODO: remove workaround
+				auto &functionRaw = function.get<ast::Function>();
+				functionRaw.arguments.reserve(symbol.arguments().size());

 				for (const auto &argument : symbol.arguments())
 				{
-					auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
+					auto translatedArgument = visit(argument, term, ruleContext, variableStack);

 					if (!translatedArgument)
 						throw TranslationException(term.location, "could not translate argument");

-					function.arguments.emplace_back(std::move(translatedArgument.value()));
+					functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
 				}

 				return std::move(function);
@@ -107,7 +84,7 @@ struct TermTranslateVisitor
 		return std::nullopt;
 	}

-	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
 		const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@@ -120,36 +97,33 @@ struct TermTranslateVisitor
 		auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
 		ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));

-		// TODO: ast::Term::make is unnecessary and can be removed
 		return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
 	}

-	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
+	{
+		throw TranslationException(term.location, "“unary operation” terms currently unsupported");
+		return std::nullopt;
+	}
+
+	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
-		auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
-		auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
+		auto left = translate(binaryOperation.left, ruleContext, variableStack);
+		auto right = translate(binaryOperation.right, ruleContext, variableStack);

 		return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
 	}

-	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
-		const auto operator_ = translate(unaryOperation.unary_operator, term);
-		auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
-
-		return ast::Term::make<ast::UnaryOperation>(operator_, std::move(argument));
-	}
-
-	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
-	{
-		auto left = translate(interval.left, ruleContext, context, variableStack);
-		auto right = translate(interval.right, ruleContext, context, variableStack);
+		auto left = translate(interval.left, ruleContext, variableStack);
+		auto right = translate(interval.right, ruleContext, variableStack);

 		return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
 	}

-	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -158,14 +132,12 @@ struct TermTranslateVisitor
 		arguments.reserve(function.arguments.size());

 		for (const auto &argument : function.arguments)
-			arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
+			arguments.emplace_back(translate(argument, ruleContext, variableStack));

-		auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
-
-		return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
+		return ast::Term::make<ast::Function>(function.name, std::move(arguments));
 	}

-	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
+	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
 	{
 		throw TranslationException(term.location, "“pool” terms currently unsupported");
 		return std::nullopt;
@@ -174,9 +146,9 @@ struct TermTranslateVisitor

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

-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 {
-	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
+	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);

 	if (!translatedTerm)
 		throw TranslationException(term.location, "could not translate term");
--- a/include/anthem/Tristate.h
+++ b/include/anthem/Tristate.h
@@ -1,24 +0,0 @@
-#ifndef __ANTHEM__TRISTATE_H
-#define __ANTHEM__TRISTATE_H
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Tristate
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class Tristate
-{
-	True,
-	False,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif
--- a/include/anthem/output/AST.h
+++ b/include/anthem/output/AST.h
@@ -41,39 +41,37 @@ struct PrintContext

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

-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);

-output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext);

-output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);

 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Primitives
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
 {
 	switch (operator_)
 	{
@@ -87,8 +85,6 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
 			return (stream << output::Operator("/"));
 		case BinaryOperation::Operator::Modulo:
 			return (stream << output::Operator("%"));
-		case BinaryOperation::Operator::Power:
-			return (stream << output::Operator("**"));
 	}

 	return stream;
@@ -96,26 +92,22 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::

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

-inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << "(";
-
+	stream << "(";
 	print(stream, binaryOperation.left, printContext);
 	stream << " ";
 	print(stream, binaryOperation.operator_, printContext);
 	stream << " ";
 	print(stream, binaryOperation.right, printContext);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	stream << ")";

 	return stream;
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
 {
 	if (boolean.value)
 		return (stream << output::Boolean("#true"));
@@ -125,7 +117,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo

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

-inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
 {
 	switch (operator_)
 	{
@@ -148,7 +140,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera

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

-inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -167,9 +159,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison

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

-inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
 {
-	stream << function.declaration->name;
+	return (stream << constant.name);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
+{
+	stream << function.name;

 	if (function.arguments.empty())
 		return stream;
@@ -184,7 +183,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
 		print(stream, *i, printContext);
 	}

-	if (function.declaration->name.empty() && function.arguments.size() == 1)
+	if (function.name.empty() && function.arguments.size() == 1)
 		stream << ",";

 	stream << ")";
@@ -194,7 +193,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f

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

-inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -211,14 +210,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri

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

-inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
 {
 	return (stream << output::Number<int>(integer.value));
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -235,9 +234,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i

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

-inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext)
 {
-	stream << predicate.declaration->name;
+	stream << predicate.name;

 	if (predicate.arguments.empty())
 		return stream;
@@ -259,14 +258,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &

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

-inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool)
-{
-	return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity());
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
 {
 	switch (specialInteger.type)
 	{
@@ -281,37 +273,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte

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

-inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
 {
 	return (stream << output::String(string.text.c_str()));
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool)
-{
-	switch (unaryOperation.operator_)
-	{
-		case UnaryOperation::Operator::Absolute:
-			stream << "|";
-			break;
-	}
-
-	print(stream, unaryOperation.argument, printContext, true);
-
-	switch (unaryOperation.operator_)
-	{
-		case UnaryOperation::Operator::Absolute:
-			stream << "|";
-			break;
-	}
-
-	return stream;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
 {
 	assert(variable.declaration != nullptr);

@@ -320,26 +289,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v

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

-inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext)
 {
-	const auto domainSuffix =
-		[&variableDeclaration]()
-		{
-			switch (variableDeclaration.domain)
-			{
-				case Domain::Unknown:
-					return "";
-				case Domain::General:
-					return "g";
-				case Domain::Integer:
-					return "i";
-			}
-
-			return "";
-		};
-
 	const auto printVariableDeclaration =
-		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
+		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
 			auto matchingVariableID = variableIDs.find(&variableDeclaration);

@@ -350,7 +303,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 				matchingVariableID = emplaceResult.first;
 			}

-			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
+			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);

 			return (stream << output::Variable(variableName.c_str()));
 		};
@@ -372,10 +325,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 // Expressions
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << "(";
+	stream << "(";

 	for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
 	{
@@ -385,32 +337,27 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
 		print(stream, *i, printContext);
 	}

-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	stream << ")";

 	return stream;
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << "(";
-
+	stream << "(";
 	print(stream, biconditional.left, printContext);
 	stream << " <-> ";
 	print(stream, biconditional.right, printContext);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	stream << ")";

 	return stream;
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -436,7 +383,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi

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

-inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -462,24 +409,20 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for

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

-inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << "(";
-
+	stream << "(";
 	print(stream, implies.antecedent, printContext);
 	stream << " -> ";
 	print(stream, implies.consequent, printContext);
-
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	stream << ")";

 	return stream;
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool)
+inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -495,10 +438,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not &not_,

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

-inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << "(";
+	stream << "(";

 	for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
 	{
@@ -508,8 +450,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
 		print(stream, *i, printContext);
 	}

-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
-		stream << ")";
+	stream << ")";

 	return stream;
 }
@@ -522,24 +463,24 @@ template<class Variant>
 struct VariantPrintVisitor
 {
 	template<class T>
-	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
+	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
 	{
-		return print(stream, x, printContext, omitParentheses);
+		return print(stream, x, printContext);
 	}
 };

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

-inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
 {
-	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
+	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
 }

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

-inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
 {
-	return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
+	return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/lib/clingo
+++ b/lib/clingo
--- a/lib/cxxopts
+++ b/lib/cxxopts
--- a/src/anthem/ASTCopy.cpp
+++ b/src/anthem/ASTCopy.cpp
@@ -103,9 +103,16 @@ Comparison prepareCopy(const Comparison &other)

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

+Constant prepareCopy(const Constant &other)
+{
+	return Constant(std::string(other.name));
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 Function prepareCopy(const Function &other)
 {
-	return Function(other.declaration, prepareCopy(other.arguments));
+	return Function(std::string(other.name), prepareCopy(other.arguments));
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -133,7 +140,7 @@ Interval prepareCopy(const Interval &other)

 Predicate prepareCopy(const Predicate &other)
 {
-	return Predicate(other.declaration, prepareCopy(other.arguments));
+	return Predicate(std::string(other.name), prepareCopy(other.arguments));
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -152,13 +159,6 @@ String prepareCopy(const String &other)

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

-UnaryOperation prepareCopy(const UnaryOperation &other)
-{
-	return UnaryOperation(other.operator_, prepareCopy(other.argument));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 Variable prepareCopy(const Variable &other)
 {
 	return Variable(other.declaration);
@@ -286,6 +286,11 @@ struct FixDanglingVariablesInTermVisitor
 	{
 	}

+	template <class... Arguments>
+	void visit(Constant &, Arguments &&...)
+	{
+	}
+
 	template <class... Arguments>
 	void visit(Function &function, Arguments &&... arguments)
 	{
@@ -315,12 +320,6 @@ struct FixDanglingVariablesInTermVisitor
 	{
 	}

-	template <class... Arguments>
-	void visit(UnaryOperation &unaryOperation, Arguments &&... arguments)
-	{
-		unaryOperation.argument.accept(*this, std::forward<Arguments>(arguments)...);
-	}
-
 	void visit(Variable &variable, ScopedFormula &scopedFormula, VariableStack &variableStack,
 		std::map<VariableDeclaration *, VariableDeclaration *> &replacements)
 	{
--- a/src/anthem/ASTUtils.cpp
+++ b/src/anthem/ASTUtils.cpp
@@ -150,6 +150,10 @@ struct CollectFreeVariablesVisitor
 		binaryOperation.right.accept(*this, variableStack, freeVariables);
 	}

+	void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
+	{
+	}
+
 	void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
 	{
 		for (auto &argument : function.arguments)
@@ -174,11 +178,6 @@ struct CollectFreeVariablesVisitor
 	{
 	}

-	void visit(UnaryOperation &unaryOperation, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
-	{
-		unaryOperation.argument.accept(*this, variableStack, freeVariables);
-	}
-
 	void visit(Variable &variable, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
 	{
 		if (variableStack.contains(*variable.declaration))
@@ -193,5 +192,84 @@ struct CollectFreeVariablesVisitor

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

+struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
+{
+	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+	{
+		const auto predicateSignatureMatches =
+			[&predicate](const auto &predicateSignature)
+			{
+				return matches(predicate, predicateSignature);
+			};
+
+		if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
+			return;
+
+		// TODO: avoid copies
+		auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
+
+		// Ignore predicates that are declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+				};
+
+			auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
+			{
+				matchingExternalPredicateSignature->used = true;
+				return;
+			}
+		}
+
+		predicateSignatures.emplace_back(std::move(predicateSignature));
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
+	{
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &lhs, const Predicate &rhs)
+{
+	return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &predicate, const PredicateSignature &signature)
+{
+	return (predicate.name == signature.name && predicate.arity() == signature.arity);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
+{
+	return (lhs.name == rhs.name && lhs.arity == rhs.arity);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// TODO: remove const_cast
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+{
+	auto &formulaMutable = const_cast<Formula &>(formula);
+	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 }
--- a/src/anthem/Completion.cpp
+++ b/src/anthem/Completion.cpp
@@ -35,7 +35,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c

 		auto &otherPredicate = implies.consequent.get<ast::Predicate>();

-		if (predicate.declaration != otherPredicate.declaration)
+		if (!ast::matches(predicate, otherPredicate))
 			continue;

 		assert(otherPredicate.arguments.size() == parameters.size());
@@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo

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

-ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
+ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
 	// Create new set of parameters for the completed definition for the predicate
 	ast::VariableDeclarationPointers parameters;
-	parameters.reserve(predicateDeclaration.arity());
+	parameters.reserve(predicateSignature.arity);

 	std::vector<ast::Term> arguments;
-	arguments.reserve(predicateDeclaration.arity());
+	arguments.reserve(predicateSignature.arity);

-	for (size_t i = 0; i < predicateDeclaration.arity(); i++)
+	for (size_t i = 0; i < predicateSignature.arity; i++)
 	{
 		parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
 		arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
 	}

-	ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
+	ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));

 	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
 	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@@ -161,27 +161,28 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 			throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
 	}

-	std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
+	std::vector<ast::PredicateSignature> predicateSignatures;
+
+	// Get a list of all predicates
+	for (const auto &scopedFormula : scopedFormulas)
+		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
+
+	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
 		[](const auto &lhs, const auto &rhs)
 		{
-			const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
+			const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str());

 			if (order != 0)
 				return (order < 0);

-			return lhs->arity() < rhs->arity();
+			return lhs.arity < rhs.arity;
 		});

 	std::vector<ast::Formula> completedFormulas;

 	// Complete predicates
-	for (auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-			continue;
-
-		completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
-	}
+	for (const auto &predicateSignature : predicateSignatures)
+		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));

 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)
@@ -201,7 +202,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 	}

 	// Eliminate all predicates that should not be visible in the output
-	eliminateHiddenPredicates(completedFormulas, context);
+	eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);

 	return completedFormulas;
 }
--- a/src/anthem/HiddenPredicateElimination.cpp
+++ b/src/anthem/HiddenPredicateElimination.cpp
@@ -78,7 +78,7 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
 {
 	static void accept(ast::Predicate &predicate, ast::Formula &formula, const PredicateReplacement &predicateReplacement)
 	{
-		if (predicate.declaration != predicateReplacement.predicate.declaration)
+		if (!ast::matches(predicate, predicateReplacement.predicate))
 			return;

 		auto formulaReplacement = ast::prepareCopy(predicateReplacement.replacement);
@@ -109,15 +109,15 @@ struct ReplacePredicateInFormulaVisitor : public ast::RecursiveFormulaVisitor<Re
 // Detect whether a formula contains a circular dependency on a given predicate
 struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<DetectCircularDependcyVisitor>
 {
-	static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
+	static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateSignature &predicateSignature, bool &hasCircularDependency)
 	{
-		if (predicate.declaration == &predicateDeclaration)
+		if (ast::matches(predicate, predicateSignature))
 			hasCircularDependency = true;
 	}

 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, bool &)
+	static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
 	{
 	}
 };
@@ -125,12 +125,12 @@ struct DetectCircularDependcyVisitor : public ast::RecursiveFormulaVisitor<Detec
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> q(X1, ..., Xn)”
-PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
+PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateDeclaration);
+	(void)(predicateSignature);

-	assert(predicate.declaration == &predicateDeclaration);
+	assert(ast::matches(predicate, predicateSignature));

 	// Replace with “#true”
 	return {predicate, ast::Formula::make<ast::Boolean>(true)};
@@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
-PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not &not_)
+PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not &not_)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateDeclaration);
+	(void)(predicateSignature);

 	assert(not_.argument.is<ast::Predicate>());
-	assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
+	assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));

 	// Replace with “#false”
 	return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
@@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
-PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
+PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateDeclaration);
+	(void)(predicateSignature);

 	assert(biconditional.left.is<ast::Predicate>());
-	assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
+	assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));

 	// TODO: avoid copy
 	return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
@@ -169,65 +169,77 @@ PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateD
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 // Finds a replacement for a predicate that should be hidden
-PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
+PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
 {
 	// TODO: refactor
 	if (completedPredicateDefinition.is<ast::ForAll>())
-		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
+		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
 	else if (completedPredicateDefinition.is<ast::Biconditional>())
-		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
+		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
 	else if (completedPredicateDefinition.is<ast::Predicate>())
-		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
+		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
 	else if (completedPredicateDefinition.is<ast::Not>())
-		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
+		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());

-	throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" +  std::to_string(predicateDeclaration.arity()) + "” for hiding predicates");
+	throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" +  std::to_string(predicateSignature.arity) + "” for hiding predicates");
 }

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

-void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
+void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
 {
-	if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
+	if (!context.visiblePredicateSignatures)
 	{
 		context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
 		return;
 	}

-	assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
-
-	// TODO: get rid of index-wise matching of completed formulas and predicate declarations
-	size_t i = -1;
+	auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();

 	// Replace all occurrences of hidden predicates
-	for (auto &predicateDeclaration : context.predicateDeclarations)
+	for (size_t i = 0; i < predicateSignatures.size(); i++)
 	{
-		// Check that the predicate is used and not declared #external
-		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-			continue;
+		auto &predicateSignature = predicateSignatures[i];

-		i++;
+		const auto matchesPredicateSignature =
+			[&](const auto &otherPredicateSignature)
+			{
+				return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+			};

-		const auto isPredicateVisible =
-			(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
-			|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
-				&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
+		const auto matchingVisiblePredicateSignature =
+			std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);

 		// If the predicate ought to be visible, don’t eliminate it
-		if (isPredicateVisible)
+		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
+		{
+			matchingVisiblePredicateSignature->used = true;
 			continue;
+		}

-		context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "”";
+		// Check that the predicate is not declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
+				continue;
+		}
+
+		context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";

 		const auto &completedPredicateDefinition = completedFormulas[i];
-		auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
+		auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);

 		bool hasCircularDependency = false;
-		replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
+		replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);

 		if (hasCircularDependency)
 		{
-			context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "” due to circular dependency";
+			context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
 			continue;
 		}

--- a/src/anthem/IntegerVariableDetection.cpp
+++ b/src/anthem/IntegerVariableDetection.cpp
@@ -1,655 +0,0 @@
-#include <anthem/IntegerVariableDetection.h>
-
-#include <anthem/ASTCopy.h>
-#include <anthem/ASTUtils.h>
-#include <anthem/ASTVisitors.h>
-#include <anthem/Exception.h>
-#include <anthem/Simplification.h>
-#include <anthem/output/AST.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// IntegerVariableDetection
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-{
-	if (variable.declaration->domain != ast::Domain::Unknown)
-		return variable.declaration->domain;
-
-	const auto match = variableDomainMap.find(variable.declaration);
-
-	if (match == variableDomainMap.end())
-		return ast::Domain::Unknown;
-
-	return match->second;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
-{
-	for (auto &variableDeclaration : variableDomainMap)
-		variableDeclaration.second = ast::Domain::Unknown;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class OperationResult
-{
-	Unchanged,
-	Changed,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class EvaluationResult
-{
-	True,
-	False,
-	Unknown,
-	Error,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct IsTermArithmeticVisitor
-{
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, VariableDomainMap &variableDomainMap)
-	{
-		const auto isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(binaryOperation.right, variableDomainMap);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Boolean &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Function &function, VariableDomainMap &)
-	{
-		switch (function.declaration->domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Integer &, VariableDomainMap &)
-	{
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Interval &interval, VariableDomainMap &variableDomainMap)
-	{
-		const auto isFromArithmetic = isArithmetic(interval.from, variableDomainMap);
-		const auto isToArithmetic = isArithmetic(interval.to, variableDomainMap);
-
-		if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::SpecialInteger &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::String &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, VariableDomainMap &variableDomainMap)
-	{
-		const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument, variableDomainMap);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-	{
-		switch (domain(variable, variableDomainMap))
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
-{
-	return term.accept(IsTermArithmeticVisitor(), variableDomainMap);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct EvaluateFormulaVisitor
-{
-	static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
-	{
-		bool someFalse = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : and_.arguments)
-		{
-			const auto result = evaluate(argument, variableDomainMap);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					break;
-				case EvaluationResult::False:
-					someFalse = true;
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someFalse)
-			return EvaluationResult::False;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
-	{
-		const auto leftResult = evaluate(biconditional.left, variableDomainMap);
-		const auto rightResult = evaluate(biconditional.right, variableDomainMap);
-
-		if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
-	{
-		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
-	{
-		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
-
-		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		if (isLeftArithmetic == isRightArithmetic)
-			return EvaluationResult::Unknown;
-
-		// Handle the case where one side is arithmetic but the other one isn’t
-		switch (comparison.operator_)
-		{
-			case ast::Comparison::Operator::Equal:
-				return EvaluationResult::False;
-			case ast::Comparison::Operator::NotEqual:
-				return EvaluationResult::True;
-			default:
-				// TODO: implement more cases
-				return EvaluationResult::Unknown;
-		}
-	}
-
-	static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
-	{
-		return evaluate(exists.argument, variableDomainMap);
-	}
-
-	static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
-	{
-		return evaluate(forAll.argument, variableDomainMap);
-	}
-
-	static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
-	{
-		const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
-		const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
-
-		if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (antecedentResult == EvaluationResult::False)
-			return EvaluationResult::True;
-
-		if (consequentResult == EvaluationResult::True)
-			return EvaluationResult::True;
-
-		if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
-			return EvaluationResult::False;
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
-	{
-		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
-		const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
-
-		if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		if (isElementArithmetic == isSetArithmetic)
-			return EvaluationResult::Unknown;
-
-		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Not &not_, VariableDomainMap &variableDomainMap)
-	{
-		const auto result = evaluate(not_.argument, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
-			return result;
-
-		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
-	}
-
-	static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
-	{
-		bool someTrue = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : or_.arguments)
-		{
-			const auto result = evaluate(argument, variableDomainMap);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					someTrue = true;
-					break;
-				case EvaluationResult::False:
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someTrue)
-			return EvaluationResult::True;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
-	{
-		assert(predicate.arguments.size() == predicate.declaration->arity());
-
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-		{
-			const auto &argument = predicate.arguments[i];
-			const auto &parameter = predicate.declaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
-
-			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
-				return isArgumentArithmetic;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
-{
-	return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DetectIntegerVariablesVisitor
-{
-	static OperationResult visit(ast::And &and_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		for (auto &argument : and_.arguments)
-			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
-				operationResult = OperationResult::Changed;
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		if (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::Boolean &, ast::Formula &, VariableDomainMap &)
-	{
-		return OperationResult::Unchanged;
-	}
-
-	static OperationResult visit(ast::Comparison &, ast::Formula &, VariableDomainMap &)
-	{
-		return OperationResult::Unchanged;
-	}
-
-	static OperationResult visit(ast::Exists &exists, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		for (auto &variableDeclaration : exists.variables)
-		{
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(exists.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(exists.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		for (auto &variableDeclaration : forAll.variables)
-		{
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(forAll.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(forAll.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::Implies &implies, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		if (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == OperationResult::Changed)
-			operationResult = OperationResult::Changed;
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::In &, ast::Formula &, VariableDomainMap &)
-	{
-		return OperationResult::Unchanged;
-	}
-
-	static OperationResult visit(ast::Not &not_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		return detectIntegerVariables(not_.argument, definition, variableDomainMap);
-	}
-
-	static OperationResult visit(ast::Or &or_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		for (auto &argument : or_.arguments)
-			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
-				operationResult = OperationResult::Changed;
-
-		return operationResult;
-	}
-
-	static OperationResult visit(ast::Predicate &predicate, ast::Formula &, VariableDomainMap &)
-	{
-		auto operationResult = OperationResult::Unchanged;
-
-		assert(predicate.arguments.size() == predicate.declaration->arity());
-
-		// Propagate integer domains from predicates to variables
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-		{
-			auto &variableArgument = predicate.arguments[i];
-			auto &parameter = predicate.declaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			if (!variableArgument.is<ast::Variable>())
-				continue;
-
-			auto &variable = variableArgument.get<ast::Variable>();
-
-			if (variable.declaration->domain == ast::Domain::Integer)
-				continue;
-
-			operationResult = OperationResult::Changed;
-			variable.declaration->domain = ast::Domain::Integer;
-		}
-
-		return operationResult;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-{
-	return formula.accept(DetectIntegerVariablesVisitor(), definition, variableDomainMap);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-// Assumes the completed formulas to be in translated but not simplified form.
-// That is, completed formulas are either variable-free or universally quantified
-void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
-{
-	VariableDomainMap variableDomainMap;
-	auto operationResult = OperationResult::Changed;
-
-	while (operationResult == OperationResult::Changed)
-	{
-		operationResult = OperationResult::Unchanged;
-
-		for (auto &completedFormula : completedFormulas)
-		{
-			if (detectIntegerVariables(completedFormula, completedFormula, variableDomainMap) == OperationResult::Changed)
-				operationResult = OperationResult::Changed;
-
-			if (!completedFormula.is<ast::ForAll>())
-				continue;
-
-			auto &forAll = completedFormula.get<ast::ForAll>();
-
-			if (!forAll.argument.is<ast::Biconditional>())
-				continue;
-
-			auto &biconditional = forAll.argument.get<ast::Biconditional>();
-
-			if (!biconditional.left.is<ast::Predicate>())
-				continue;
-
-			auto &predicate = biconditional.left.get<ast::Predicate>();
-			auto &definition = biconditional.right;
-
-			assert(predicate.arguments.size() == predicate.declaration->arity());
-
-			if (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
-				operationResult = OperationResult::Changed;
-
-			for (size_t i = 0; i < predicate.arguments.size(); i++)
-			{
-				auto &variableArgument = predicate.arguments[i];
-				auto &parameter = predicate.declaration->parameters[i];
-
-				assert(variableArgument.is<ast::Variable>());
-
-				auto &variable = variableArgument.get<ast::Variable>();
-
-				if (parameter.domain != ast::Domain::Unknown)
-					continue;
-
-				clearVariableDomainMap(variableDomainMap);
-
-				auto result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-					continue;
-
-				// As a hypothesis, make the parameter’s domain noninteger
-				variableDomainMap[variable.declaration] = ast::Domain::General;
-
-				result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-				{
-					// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-					operationResult = OperationResult::Changed;
-					variable.declaration->domain = ast::Domain::Integer;
-					parameter.domain = ast::Domain::Integer;
-				}
-			}
-		}
-	}
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -363,7 +363,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
 			std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
 			[&](const auto &argument)
 			{
-				return (ast::equal(predicateSide, argument) == Tristate::True);
+				return (ast::equal(predicateSide, argument) == ast::Tristate::True);
 			});

 		if (matchingPredicate == and_.arguments.cend())
@@ -466,52 +466,6 @@ struct SimplificationRuleImplicationFromDisjunction

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

-struct SimplificationRuleNegatedComparison
-{
-	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
-
-	static SimplificationResult apply(ast::Formula &formula)
-	{
-		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
-
-		auto &not_ = formula.get<ast::Not>();
-
-		if (!not_.argument.is<ast::Comparison>())
-			return SimplificationResult::Unchanged;
-
-		auto &comparison = not_.argument.get<ast::Comparison>();
-
-		switch (comparison.operator_)
-		{
-			case ast::Comparison::Operator::GreaterThan:
-				comparison.operator_ = ast::Comparison::Operator::LessEqual;
-				break;
-			case ast::Comparison::Operator::LessThan:
-				comparison.operator_ = ast::Comparison::Operator::GreaterEqual;
-				break;
-			case ast::Comparison::Operator::LessEqual:
-				comparison.operator_ = ast::Comparison::Operator::GreaterThan;
-				break;
-			case ast::Comparison::Operator::GreaterEqual:
-				comparison.operator_ = ast::Comparison::Operator::LessThan;
-				break;
-			case ast::Comparison::Operator::NotEqual:
-				comparison.operator_ = ast::Comparison::Operator::Equal;
-				break;
-			case ast::Comparison::Operator::Equal:
-				comparison.operator_ = ast::Comparison::Operator::NotEqual;
-				break;
-		}
-
-		formula = std::move(comparison);
-
-		return SimplificationResult::Simplified;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -525,8 +479,7 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleInWithPrimitiveArguments,
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
-		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleImplicationFromDisjunction
 	>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -8,7 +8,6 @@

 #include <anthem/Completion.h>
 #include <anthem/Context.h>
-#include <anthem/IntegerVariableDetection.h>
 #include <anthem/Simplification.h>
 #include <anthem/StatementVisitor.h>
 #include <anthem/output/AST.h>
@@ -68,10 +67,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 			for (auto &scopedFormula : scopedFormulas)
 				simplify(scopedFormula.formula);

-		if (context.showStatementsUsed)
+		if (context.visiblePredicateSignatures)
 			context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";

-		if (context.externalStatementsUsed)
+		if (context.externalPredicateSignatures)
 			context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";

 		for (const auto &scopedFormula : scopedFormulas)
@@ -86,33 +85,25 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	// Perform completion
 	auto completedFormulas = complete(std::move(scopedFormulas), context);

-	for (const auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		if (predicateDeclaration->isUsed)
-			continue;
+	// Check for #show statements with undeclared predicates
+	if (context.visiblePredicateSignatures)
+		for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
+			if (!predicateSignature.used)
+				context.logger.log(output::Priority::Warning)
+					<< "#show declaration of “"
+					<< predicateSignature.predicateSignature.name
+					<< "/" << predicateSignature.predicateSignature.arity
+					<< "” does not match any eligible predicate";

-		// Check for #show statements with undeclared predicates
-		if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
-			context.logger.log(output::Priority::Warning)
-				<< "#show declaration of “"
-				<< predicateDeclaration->name
-				<< "/"
-				<< predicateDeclaration->arity()
-				<< "” does not match any declared predicate";
-
-		// Check for #external statements with undeclared predicates
-		if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
-			context.logger.log(output::Priority::Warning)
-				<< "#external declaration of “"
-				<< predicateDeclaration->name
-				<< "/"
-				<< predicateDeclaration->arity()
-				<< "” does not match any declared predicate";
-	}
-
-	// Detect integer variables
-	if (context.performIntegerDetection)
-		detectIntegerVariables(completedFormulas);
+	// Check for #external statements with undeclared predicates
+	if (context.externalPredicateSignatures)
+		for (const auto &predicateSignature : context.externalPredicateSignatures.value())
+			if (!predicateSignature.used)
+				context.logger.log(output::Priority::Warning)
+					<< "#external declaration of “"
+					<< predicateSignature.predicateSignature.name
+					<< "/" << predicateSignature.predicateSignature.arity
+					<< "” does not match any eligible predicate";

 	// Simplify output if specified
 	if (context.performSimplification)
@@ -126,38 +117,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 		ast::print(context.logger.outputStream(), completedFormula, printContext);
 		context.logger.outputStream() << std::endl;
 	}
-
-	// Print specifiers for integer predicate parameters
-	for (auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		// Check that the predicate is used and not declared #external
-		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-			continue;
-
-		const auto isPredicateVisible =
-			(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
-			|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
-				&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
-
-		// If the predicate ought to be visible, don’t eliminate it
-		if (!isPredicateVisible)
-			continue;
-
-		for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
-		{
-			auto &parameter = predicateDeclaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			context.logger.outputStream()
-				<< output::Keyword("int")
-				<< "(" << predicateDeclaration->name
-				<< "/" << output::Number(predicateDeclaration->arity())
-				<< "@" << output::Number(i)
-				<< ")." << std::endl;
-		}
-	}
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -176,20 +176,4 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		CHECK(output.str() ==
 			"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
 	}
-
-	SECTION("negated comparisons")
-	{
-		input << ":- color(V, C1), color(V, C2), C1 != C2.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "forall V1, V2 not color(V1, V2)\nforall U1, U2, U3 (not color(U1, U2) or not color(U1, U3) or U2 = U3)\n");
-	}
-
-	SECTION("absolute value operation")
-	{
-		input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n");
-	}
 }
--- a/tests/TestTranslation.cpp
+++ b/tests/TestTranslation.cpp
@@ -296,12 +296,4 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")

 		CHECK(output.str() == "((V1 in U1 and V2 in U2 and exists X1, X2 (X1 in U3 and X2 in U4 and q(X1, X2))) -> p(V1, V2))\n");
 	}
-
-	SECTION("exponentiation operator")
-	{
-		input << "p(N, N ** N) :- N = 1..n.";
-		anthem::translate("input", input, context);
-
-		CHECK(output.str() == "((V1 in U1 and V2 in (U1 ** U1) and exists X1, X2 (X1 in U1 and X2 in 1..n and X1 = X2)) -> p(V1, V2))\n");
-	}
 }
Author	SHA1	Message	Date
Patrick Lühne	285fa08e5a	Version bump for release 0.1.8 RC 1	2018-04-10 00:19:55 +02:00
Patrick Lühne	dfffdcfce6	Add new simplification rule This adds the rule “(not F or G) === (F -> G)” to the simplification rule tableau.	2018-04-09 23:48:04 +02:00
Patrick Lühne	4967576b6c	Add new simplification rule This adds the rule “(not (F and G)) === (not F or not G)” to the simplification rule tableau.	2018-04-09 23:39:29 +02:00
Patrick Lühne	1c5851441d	Add new simplification rule This adds the rule “not not F === F” to the simplification rule tableau.	2018-04-09 23:36:16 +02:00
Patrick Lühne	b18ddcc575	Add new simplification rule This adds the rule “(F <-> (F and G)) === (F -> G)” to the simplification rule tableau.	2018-04-09 23:27:38 +02:00
Patrick Lühne	00ab975c2d	Iteratively apply simplification tableau rules With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached.	2018-04-08 22:24:14 +02:00
Patrick Lühne	e01b5dc561	Move simplification rule to tableau This moves the rule “[primitive A] in [primitive B] === A = B” to the simplification rule tableau.	2018-04-08 22:24:14 +02:00
Patrick Lühne	91529b84aa	Move simplification rule to tableau This moves the rule “exists () (F) === F” to the simplification rule tableau.	2018-04-08 22:24:14 +02:00
Patrick Lühne	1cbfd335a1	Move simplification rule to tableau This moves the rule “[conjunction of only F] === F” to the simplification rule tableau.	2018-04-08 22:24:14 +02:00
Patrick Lühne	a86e978a5a	Move simplification rule to tableau This moves the rule “exists ... ([#true/#false]) === [#true/#false]” to the simplification rule tableau along with “[empty conjunction] ===	2018-04-08 22:24:14 +02:00
Patrick Lühne	5eb3ed5681	Move simplification rule to tableau This moves the rule “exists X (X = t and F(X)) === exists () (F(t))” to the simplification rule tableau.	2018-04-08 22:24:14 +02:00
Patrick Lühne	3d0266136c	Implement simplification rule tableau This implements a tableau containing simplification rules that can be iteratively applied to input formulas until they remain unchanged. First, this moves the rule “exists X (X = Y) === #true” to the tableau as a reference implementation.	2018-04-08 22:24:10 +02:00