Version bump for release 0.1.9 RC 3

Clingo treats operations that were assumed to be “invalid” not as
processing errors but as operations returning an empty set.

This changes how formulas have to be evaluated. This commit implements
an explicit function for retrieving the return type of an expression,
that is, both the domain of the result as well as whether it’s an empty,
unit, or general set with multiple values.

.ci/Dockerfile-ubuntu-18.04

@@ -3,7 +3,7 @@ FROM ubuntu:18.04
 ARG toolchain
 
 RUN apt-get update
-RUN apt-get install -y cmake git ninja-build re2c
+RUN apt-get install -y bison 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
 

CHANGELOG.md

@@ -1,14 +1,35 @@
 # Change Log
 
-## 0.1.7 (2018-04-05)
+## 0.1.9 RC 3 (2018-04-22)
 
-Features:
+### Features
+
+* optional detection of integer variables and integer predicate parameters
+* command-line option `--detect-integers` to enable integer variable detection
+* support for declaring functions integer with the `#external` directive
+* new simplification rule applying to integer variables
+
+## 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)
+
+## 0.1.7 (2018-04-08)
+
+### Features
 
 * support for declaring placeholders with the `#external` directive
 
+### Internal
+
+* drops Boost dependency in favor of the header-only command-line option library [cxxopts](https://github.com/jarro2783/cxxopts)
+
 ## 0.1.6 (2017-06-12)
 
-Features:
+### Features
 
 * unique IDs for all variables (user-defined variables are renamed)
 * support for hiding predicates from completed output by using `#show` statements
@@ -16,7 +37,7 @@ Features:
 * command-line option `--parentheses` to fully parenthesize the output
 * adds multiple example instances for experimenting
 
-Bug Fixes:
+### Bug Fixes
 
 * adds missing error message when attempting to read inaccessible file
 * removes unnecessary parentheses after simplification
@@ -24,52 +45,52 @@ Bug Fixes:
 
 ## 0.1.5 (2017-05-04)
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes lost signs with negated 0-ary predicates
 
 ## 0.1.4 (2017-04-12)
 
-Features:
+### Features
 
 * completion of input programs (optional)
 * command-line option `--complete` to turn on completion
 
 ## 0.1.3 (2017-03-30)
 
-Features:
+### Features
 
 * support for anonymous variables
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes incorrectly simplified rules with comparisons
 * fixes misleading error message concerning negated, unsupported body literals
 
 ## 0.1.2 (2017-03-23)
 
-Features:
+### Features
 
 * simplification of output formulas (optional)
 * command-line option `--simplify` to turn on simplification
 
-Bug Fixes:
+### Bug Fixes
 
 * fixes incorrectly translated choice rules with multiple elements in the head aggregate
 
-Internal:
+### Internal
 
 * explicit syntax tree representation for first-order formulas
 
 ## 0.1.1 (2017-03-06)
 
-Features:
+### Features
 
 * support for choice rules (without guards)
 
 ## 0.1.0 (2016-11-24)
 
-Features:
+### Features
 
 * initial support for translating rules in *Essential Gringo* (excluding aggregates) to first-order logic formulas
 * command-line option `--color` to autodetect, enable, or disable color output

LICENSE.md

@@ -1,6 +1,6 @@
 # The MIT License (MIT)
 
-Copyright © 2016–2017 Patrick Lühne
+Copyright © 2016–2018 Patrick Lühne
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -9,10 +9,11 @@
 ## Usage
 
 ```bash
-$ anthem [--simplify] file...
+$ anthem [--complete] [--simplify] file...
 ```
 
-With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
+`--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.
 
 ## Building
 

app/main.cpp

@@ -18,6 +18,7 @@ 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"));
@@ -50,6 +51,7 @@ 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>();
@@ -70,7 +72,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.7-rc.1" << std::endl;
+		std::cout << "anthem version 0.1.9-rc.3" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/graph-coloring.lp

@@ -1,12 +1,10 @@
-colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
-colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
-colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
+#external color(1).
+#external edge(2).
+#external vertex(1).
+#show color/2.
 
-:- edge(V1, V2), colored(V1, C), colored(V2, C).
-
-vertex(a).
-vertex(b).
-vertex(c).
-
-edge(a, b).
-edge(a, 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.

examples/permutations.lp

@@ -0,0 +1,13 @@
+#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.

examples/prime.lp

@@ -0,0 +1,5 @@
+#show prime/1.
+%#external integer(n(0)).
+
+composite(I * J) :- I = 2..n, J = 2..n.
+prime(N) :- N = 2..n, not composite(N).

examples/schur-numbers.lp

@@ -1,3 +1,7 @@
+#show in/2.
+%#external integer(n(0)).
+%#external integer(r(0)).
+
 {in(1..n, 1..r)}.
 covered(I) :- in(I, S).
 

include/anthem/AST.h

@@ -2,6 +2,7 @@
 #define __ANTHEM__AST_H
 
 #include <anthem/ASTForward.h>
+#include <anthem/Utils.h>
 
 namespace anthem
 {
@@ -32,7 +33,8 @@ struct BinaryOperation
 		Minus,
 		Multiplication,
 		Division,
-		Modulo
+		Modulo,
+		Power
 	};
 
 	explicit BinaryOperation(Operator operator_, Term &&left, Term &&right)
@@ -102,32 +104,15 @@ struct Comparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct Constant
-{
-	explicit Constant(std::string &&name)
-	:	name{std::move(name)}
-	{
-	}
-
-	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(FunctionDeclaration *declaration)
+	:	declaration{declaration}
 	{
 	}
 
-	explicit Function(std::string &&name, std::vector<Term> &&arguments)
-	:	name{std::move(name)},
+	explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
+	:	declaration{declaration},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -137,12 +122,37 @@ struct Function
 	Function(Function &&other) noexcept = default;
 	Function &operator=(Function &&other) noexcept = default;
 
-	std::string name;
+	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::Noninteger};
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 // TODO: refactor (limit element type to primitive terms)
 struct In
 {
@@ -203,13 +213,13 @@ struct Interval
 
 struct Predicate
 {
-	explicit Predicate(std::string &&name)
-	:	name{std::move(name)}
+	explicit Predicate(PredicateDeclaration *declaration)
+	:	declaration{declaration}
 	{
 	}
 
-	explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
-	:	name{std::move(name)},
+	explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
+	:	declaration{declaration},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -219,35 +229,47 @@ struct Predicate
 	Predicate(Predicate &&other) noexcept = default;
 	Predicate &operator=(Predicate &&other) noexcept = default;
 
-	std::size_t arity() const
-	{
-		return arguments.size();
-	}
-
-	std::string name;
+	PredicateDeclaration *declaration{nullptr};
 	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// TODO: make more use of this class
-struct PredicateSignature
+struct PredicateDeclaration
 {
-	explicit PredicateSignature(std::string &&name, size_t arity)
+	enum class Visibility
+	{
+		Default,
+		Visible,
+		Hidden
+	};
+
+	struct Parameter
+	{
+		Domain domain{Domain::Unknown};
+	};
+
+	explicit PredicateDeclaration(std::string &&name, size_t arity)
 	:	name{std::move(name)},
-		arity{arity}
+		parameters{std::vector<Parameter>(arity)}
 	{
 	}
 
-	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;
+	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();
+	}
 
 	std::string name;
-	size_t arity;
+	std::vector<Parameter> parameters;
+	bool isUsed{false};
+	bool isExternal{false};
+	Visibility visibility{Visibility::Default};
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -292,6 +314,30 @@ 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)
@@ -335,6 +381,7 @@ struct VariableDeclaration
 	VariableDeclaration &operator=(VariableDeclaration &&other) = default;
 
 	Type type;
+	Domain domain{Domain::Unknown};
 	std::string name;
 };
 

include/anthem/ASTCopy.h

@@ -22,7 +22,6 @@ 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);

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,8 +35,10 @@ 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>;
@@ -62,12 +64,12 @@ using Formula = Clingo::Variant<
 using Term = Clingo::Variant<
 	BinaryOperation,
 	Boolean,
-	Constant,
 	Function,
 	Integer,
 	Interval,
 	SpecialInteger,
 	String,
+	UnaryOperation,
 	Variable>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/ASTUtils.h

@@ -5,6 +5,7 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTVisitors.h>
+#include <anthem/Context.h>
 
 namespace anthem
 {
@@ -35,12 +36,6 @@ 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);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables

include/anthem/ASTVisitors.h

@@ -123,12 +123,6 @@ 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)
 	{
@@ -165,6 +159,14 @@ 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)
 	{

include/anthem/Body.h

@@ -43,19 +43,22 @@ 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, ast::VariableStack &variableStack)
+	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)
 	{
 		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 std::move(predicate);
+				return ast::Predicate(predicateDeclaration);
 			else if (literal.sign == Clingo::AST::Sign::Negation)
-				return ast::Formula::make<ast::Not>(std::move(predicate));
+				return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
 		}
 
 		// Create new body variable declarations
@@ -73,12 +76,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, variableStack)));
+			conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
 		}
 
 		variableStack.pop();
 
-		ast::Predicate predicate(std::string(function.name));
+		ast::Predicate predicate(predicateDeclaration);
 		predicate.arguments.reserve(function.arguments.size());
 
 		for (size_t i = 0; i < function.arguments.size(); i++)
@@ -93,7 +96,8 @@ struct BodyTermTranslateVisitor
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
+		const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
 	{
 		assert(!term.data.is<Clingo::AST::Function>());
 
@@ -106,18 +110,18 @@ struct BodyTermTranslateVisitor
 
 struct BodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, 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, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
 	{
-		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
+		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
 	}
 
 	// TODO: refactor
-	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, 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)
@@ -132,15 +136,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, 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::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::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 &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
 	{
 		throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
 		return std::nullopt;
@@ -151,16 +155,16 @@ struct BodyLiteralTranslateVisitor
 
 struct BodyBodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, 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, variableStack);
+		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
 	{
 		throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
 		return std::nullopt;

include/anthem/Context.h

@@ -16,6 +16,14 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct PredicateDeclarationMeta
+{
+	ast::PredicateDeclaration *declaration;
+	bool used{false};
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct Context
 {
 	Context() = default;
@@ -25,13 +33,59 @@ 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 performSimplification{false};
+	bool performCompletion{false};
+	bool performIntegerDetection{false};
 
-	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
-	std::optional<std::vector<ast::PredicateSignature>> externalPredicateSignatures;
+	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};
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

include/anthem/Equality.h

@@ -0,0 +1,409 @@
+#ifndef __ANTHEM__EQUALITY_H
+#define __ANTHEM__EQUALITY_H
+
+#include <anthem/AST.h>
+#include <anthem/ASTUtils.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Equality
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Formula &lhs, const Formula &rhs);
+Tristate equal(const Term &lhs, const Term &rhs);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct FormulaEqualityVisitor
+{
+	Tristate visit(const And &and_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<And>())
+			return Tristate::Unknown;
+
+		const auto &otherAnd = otherFormula.get<And>();
+
+		for (const auto &argument : and_.arguments)
+		{
+			const auto match = std::find_if(
+				otherAnd.arguments.cbegin(), otherAnd.arguments.cend(),
+				[&](const auto &otherArgument)
+				{
+					return equal(argument, otherArgument) == Tristate::True;
+				});
+
+			if (match == otherAnd.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		for (const auto &otherArgument : otherAnd.arguments)
+		{
+			const auto match = std::find_if(
+				and_.arguments.cbegin(), and_.arguments.cend(),
+				[&](const auto &argument)
+				{
+					return equal(otherArgument, argument) == Tristate::True;
+				});
+
+			if (match == and_.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Biconditional &biconditional, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Biconditional>())
+			return Tristate::Unknown;
+
+		const auto &otherBiconditional = otherFormula.get<Biconditional>();
+
+		if (equal(biconditional.left, otherBiconditional.left) == Tristate::True
+		    && equal(biconditional.right, otherBiconditional.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		if (equal(biconditional.left, otherBiconditional.right) == Tristate::True
+		    && equal(biconditional.right, otherBiconditional.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Boolean &boolean, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Boolean>())
+			return Tristate::Unknown;
+
+		const auto &otherBoolean = otherFormula.get<Boolean>();
+
+		return (boolean.value == otherBoolean.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Comparison &comparison, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Comparison>())
+			return Tristate::Unknown;
+
+		const auto &otherComparison = otherFormula.get<Comparison>();
+
+		if (comparison.operator_ != otherComparison.operator_)
+			return Tristate::Unknown;
+
+		if (equal(comparison.left, otherComparison.left) == Tristate::True
+		    && equal(comparison.right, otherComparison.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		// Only = and != are commutative operators, all others don’t need to be checked with exchanged arguments
+		if (comparison.operator_ != Comparison::Operator::Equal
+		    && comparison.operator_ != Comparison::Operator::NotEqual)
+		{
+			return Tristate::Unknown;
+		}
+
+		if (equal(comparison.left, otherComparison.right) == Tristate::True
+		    && equal(comparison.right, otherComparison.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Exists &, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Exists>())
+			return Tristate::Unknown;
+
+		// TODO: implement stronger check
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const ForAll &, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<ForAll>())
+			return Tristate::Unknown;
+
+		// TODO: implement stronger check
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Implies &implies, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Implies>())
+			return Tristate::Unknown;
+
+		const auto &otherImplies = otherFormula.get<Implies>();
+
+		if (equal(implies.antecedent, otherImplies.antecedent) == Tristate::True
+		    && equal(implies.consequent, otherImplies.consequent) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const In &in, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<In>())
+			return Tristate::Unknown;
+
+		const auto &otherIn = otherFormula.get<In>();
+
+		if (equal(in.element, otherIn.element) == Tristate::True
+		    && equal(in.set, otherIn.set) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Not &not_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Not>())
+			return Tristate::Unknown;
+
+		const auto &otherNot = otherFormula.get<Not>();
+
+		return equal(not_.argument, otherNot.argument);
+	}
+
+	Tristate visit(const Or &or_, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Or>())
+			return Tristate::Unknown;
+
+		const auto &otherOr = otherFormula.get<Or>();
+
+		for (const auto &argument : or_.arguments)
+		{
+			const auto match = std::find_if(
+				otherOr.arguments.cbegin(), otherOr.arguments.cend(),
+				[&](const auto &otherArgument)
+				{
+					return equal(argument, otherArgument) == Tristate::True;
+				});
+
+			if (match == otherOr.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		for (const auto &otherArgument : otherOr.arguments)
+		{
+			const auto match = std::find_if(
+				or_.arguments.cbegin(), or_.arguments.cend(),
+				[&](const auto &argument)
+				{
+					return equal(otherArgument, argument) == Tristate::True;
+				});
+
+			if (match == or_.arguments.cend())
+				return Tristate::Unknown;
+		}
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Predicate &predicate, const Formula &otherFormula)
+	{
+		if (!otherFormula.is<Predicate>())
+			return Tristate::Unknown;
+
+		const auto &otherPredicate = otherFormula.get<Predicate>();
+
+		if (predicate.declaration != otherPredicate.declaration)
+			return Tristate::False;
+
+		assert(predicate.arguments.size() == otherPredicate.arguments.size());
+
+		for (size_t i = 0; i < predicate.arguments.size(); i++)
+			if (equal(predicate.arguments[i], otherPredicate.arguments[i]) != Tristate::True)
+				return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct TermEqualityVisitor
+{
+	Tristate visit(const BinaryOperation &binaryOperation, const Term &otherTerm)
+	{
+		if (!otherTerm.is<BinaryOperation>())
+			return Tristate::Unknown;
+
+		const auto &otherBinaryOperation = otherTerm.get<BinaryOperation>();
+
+		if (binaryOperation.operator_ != otherBinaryOperation.operator_)
+			return Tristate::Unknown;
+
+		if (equal(binaryOperation.left, otherBinaryOperation.left) == Tristate::True
+		    && equal(binaryOperation.right, otherBinaryOperation.right) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		// Only + and * are commutative operators, all others don’t need to be checked with exchanged arguments
+		if (binaryOperation.operator_ != BinaryOperation::Operator::Plus
+		    && binaryOperation.operator_ != BinaryOperation::Operator::Multiplication)
+		{
+			return Tristate::Unknown;
+		}
+
+		if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
+		    && equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
+		{
+			return Tristate::True;
+		}
+
+		return Tristate::Unknown;
+	}
+
+	Tristate visit(const Boolean &boolean, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Boolean>())
+			return Tristate::Unknown;
+
+		const auto &otherBoolean = otherTerm.get<Boolean>();
+
+		return (boolean.value == otherBoolean.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Function &function, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Function>())
+			return Tristate::Unknown;
+
+		const auto &otherFunction = otherTerm.get<Function>();
+
+		if (function.declaration != otherFunction.declaration)
+			return Tristate::False;
+
+		if (function.arguments.size() != otherFunction.arguments.size())
+			return Tristate::False;
+
+		for (size_t i = 0; i < function.arguments.size(); i++)
+			if (equal(function.arguments[i], otherFunction.arguments[i]) != Tristate::True)
+				return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const Integer &integer, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Integer>())
+			return Tristate::Unknown;
+
+		const auto &otherInteger = otherTerm.get<Integer>();
+
+		return (integer.value == otherInteger.value)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const Interval &interval, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Interval>())
+			return Tristate::Unknown;
+
+		const auto &otherInterval = otherTerm.get<Interval>();
+
+		if (equal(interval.from, otherInterval.from) != Tristate::True)
+			return Tristate::Unknown;
+
+		if (equal(interval.to, otherInterval.to) != Tristate::True)
+			return Tristate::Unknown;
+
+		return Tristate::True;
+	}
+
+	Tristate visit(const SpecialInteger &specialInteger, const Term &otherTerm)
+	{
+		if (!otherTerm.is<SpecialInteger>())
+			return Tristate::Unknown;
+
+		const auto &otherSpecialInteger = otherTerm.get<SpecialInteger>();
+
+		return (specialInteger.type == otherSpecialInteger.type)
+			? Tristate::True
+			: Tristate::False;
+	}
+
+	Tristate visit(const String &string, const Term &otherTerm)
+	{
+		if (!otherTerm.is<String>())
+			return Tristate::Unknown;
+
+		const auto &otherString = otherTerm.get<String>();
+
+		return (string.text == otherString.text)
+			? Tristate::True
+			: 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>())
+			return Tristate::Unknown;
+
+		const auto &otherVariable = otherTerm.get<Variable>();
+
+		return (variable.declaration == otherVariable.declaration)
+			? Tristate::True
+			: Tristate::False;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Formula &lhs, const Formula &rhs)
+{
+	return lhs.accept(FormulaEqualityVisitor(), rhs);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Tristate equal(const Term &lhs, const Term &rhs)
+{
+	return lhs.accept(TermEqualityVisitor(), rhs);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif

include/anthem/Head.h

@@ -118,8 +118,7 @@ struct HeadLiteralCollectFunctionTermsVisitor
 
 struct FunctionTermTranslateVisitor
 {
-	// TODO: check correctness
-	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -130,11 +129,14 @@ struct FunctionTermTranslateVisitor
 		for (size_t i = 0; i < function.arguments.size(); i++)
 			arguments.emplace_back(ast::Variable(ruleContext.freeVariables[headVariableIndex++].get()));
 
-		return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
+		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
+		predicateDeclaration->isUsed = true;
+
+		return ast::Predicate(predicateDeclaration, std::move(arguments));
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, RuleContext &, Context &, size_t &)
 	{
 		throw TranslationException(term.location, "term currently unsupported in this context, function expected");
 		return std::nullopt;
@@ -145,18 +147,18 @@ struct FunctionTermTranslateVisitor
 
 struct LiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, 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, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
 	{
-		return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, headVariableIndex);
+		return term.data.accept(FunctionTermTranslateVisitor(), term, ruleContext, context, headVariableIndex);
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, size_t &)
 	{
 		throw TranslationException(literal.location, "only disjunctions of literals allowed as head literals");
 		return std::nullopt;
@@ -167,12 +169,12 @@ struct LiteralTranslateVisitor
 
 struct HeadLiteralTranslateToConsequentVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, RuleContext &ruleContext, Context &context, 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, headVariableIndex);
+		auto translatedLiteral = literal.data.accept(LiteralTranslateVisitor(), literal, ruleContext, context, headVariableIndex);
 
 		if (literal.sign == Clingo::AST::Sign::None)
 			return translatedLiteral;
@@ -183,7 +185,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, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
 	{
 		std::vector<ast::Formula> arguments;
 		arguments.reserve(disjunction.elements.size());
@@ -193,7 +195,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 			if (!conditionalLiteral.condition.empty())
 				throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
 
-			auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
+			auto argument = visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
 
 			if (!argument)
 				throw TranslationException(headLiteral.location, "could not parse argument");
@@ -204,7 +206,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, size_t &headVariableIndex)
+	std::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &ruleContext, Context &context, size_t &headVariableIndex)
 	{
 		if (aggregate.left_guard || aggregate.right_guard)
 			throw TranslationException(headLiteral.location, "aggregates with left or right guards currently unsupported");
@@ -215,7 +217,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 				if (!conditionalLiteral.condition.empty())
 					throw TranslationException(headLiteral.location, "conditional head literals currently unsupported");
 
-				return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, headVariableIndex);
+				return this->visit(conditionalLiteral.literal, headLiteral, ruleContext, context, headVariableIndex);
 			};
 
 		if (aggregate.elements.size() == 1)
@@ -238,7 +240,7 @@ struct HeadLiteralTranslateToConsequentVisitor
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, size_t &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, RuleContext &, Context &, size_t &)
 	{
 		throw TranslationException(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate");
 		return std::nullopt;

include/anthem/HiddenPredicateElimination.h

@@ -13,7 +13,7 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context);
+void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

include/anthem/IntegerVariableDetection.h

@@ -0,0 +1,22 @@
+#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

include/anthem/SimplificationVisitors.h

@@ -0,0 +1,193 @@
+#ifndef __ANTHEM__SIMPLIFICATION_VISITORS_H
+#define __ANTHEM__SIMPLIFICATION_VISITORS_H
+
+#include <anthem/AST.h>
+#include <anthem/Simplification.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Simplification Visitor
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class T>
+struct FormulaSimplificationVisitor
+{
+	template <class... Arguments>
+	OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
+	{
+		for (auto &argument : and_.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
+	{
+		if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
+	{
+		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
+	{
+		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
+	{
+		if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
+	{
+		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
+	{
+		for (auto &argument : or_.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;
+
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
+	{
+		return T::accept(formula, std::forward<Arguments>(arguments)...);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class T, class OperationResult = void>
+struct TermSimplificationVisitor
+{
+	template <class... Arguments>
+	OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
+	{
+		if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
+	{
+		for (auto &argument : function.arguments)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
+	{
+		if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;
+
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(String &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif

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, headVariableIndex);
+		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, 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, variableStack);
+			auto set = translate(headTerm, ruleContext, context, 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, variableStack);
+			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, 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");
 
-		if (!context.visiblePredicateSignatures)
-			context.visiblePredicateSignatures.emplace();
+		context.showStatementsUsed = true;
+		context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
 
 		if (std::strlen(signature.name()) == 0)
 		{
@@ -176,7 +176,8 @@ struct StatementVisitor
 
 		context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
 
-		context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity());
+		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
+		predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
 	}
 
 	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@@ -189,7 +190,7 @@ struct StatementVisitor
 		const auto fail =
 			[&]()
 			{
-				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” supported");
+				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” or “#external integer(<function name>(<arity>)).” supported");
 			};
 
 		if (!external.body.empty())
@@ -203,6 +204,47 @@ 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 = Domain::Integer;
+
+				return true;
+			};
+
+		if (handleIntegerDeclaration())
+			return;
+
 		const auto &arityArgument = predicate.arguments.front();
 
 		if (!arityArgument.data.is<Clingo::Symbol>())
@@ -213,12 +255,12 @@ struct StatementVisitor
 		if (aritySymbol.type() != Clingo::SymbolType::Number)
 			fail();
 
-		const auto &arity = arityArgument.data.get<Clingo::Symbol>().number();
+		context.externalStatementsUsed = true;
 
-		if (!context.externalPredicateSignatures)
-			context.externalPredicateSignatures.emplace();
+		const size_t arity = aritySymbol.number();
 
-		context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity);
+		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
+		predicateDeclaration->isExternal = true;
 	}
 
 	template<class T>

include/anthem/Term.h

@@ -23,6 +23,12 @@ 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:
@@ -33,22 +39,39 @@ ast::BinaryOperation::Operator translate(Clingo::AST::BinaryOperator binaryOpera
 			return ast::BinaryOperation::Operator::Division;
 		case Clingo::AST::BinaryOperator::Modulo:
 			return ast::BinaryOperation::Operator::Modulo;
-		default:
-			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
+		case Clingo::AST::BinaryOperator::Power:
+			return ast::BinaryOperation::Operator::Power;
 	}
 
-	return ast::BinaryOperation::Operator::Plus;
+	throw TranslationException(term.location, "unknown binary operation");
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack);
+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);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct TermTranslateVisitor
 {
-	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
 	{
 		switch (symbol.type())
 		{
@@ -62,19 +85,19 @@ struct TermTranslateVisitor
 				return ast::Term::make<ast::String>(std::string(symbol.string()));
 			case Clingo::SymbolType::Function:
 			{
-				auto function = ast::Term::make<ast::Function>(symbol.name());
-				// TODO: remove workaround
-				auto &functionRaw = function.get<ast::Function>();
-				functionRaw.arguments.reserve(symbol.arguments().size());
+				auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
+
+				auto function = ast::Function(functionDeclaration);
+				function.arguments.reserve(symbol.arguments().size());
 
 				for (const auto &argument : symbol.arguments())
 				{
-					auto translatedArgument = visit(argument, term, ruleContext, variableStack);
+					auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
 
 					if (!translatedArgument)
 						throw TranslationException(term.location, "could not translate argument");
 
-					functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
+					function.arguments.emplace_back(std::move(translatedArgument.value()));
 				}
 
 				return std::move(function);
@@ -84,7 +107,7 @@ struct TermTranslateVisitor
 		return std::nullopt;
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
 	{
 		const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
 		const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@@ -97,33 +120,36 @@ 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::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)
+	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
-		auto left = translate(binaryOperation.left, ruleContext, variableStack);
-		auto right = translate(binaryOperation.right, ruleContext, variableStack);
+		auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
+		auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
 
 		return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
 	{
-		auto left = translate(interval.left, ruleContext, variableStack);
-		auto right = translate(interval.right, ruleContext, 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);
 
 		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, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -132,12 +158,14 @@ struct TermTranslateVisitor
 		arguments.reserve(function.arguments.size());
 
 		for (const auto &argument : function.arguments)
-			arguments.emplace_back(translate(argument, ruleContext, variableStack));
+			arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
 
-		return ast::Term::make<ast::Function>(function.name, std::move(arguments));
+		auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
+
+		return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
+	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
 	{
 		throw TranslationException(term.location, "“pool” terms currently unsupported");
 		return std::nullopt;
@@ -146,9 +174,9 @@ struct TermTranslateVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
+ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
 {
-	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);
+	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
 
 	if (!translatedTerm)
 		throw TranslationException(term.location, "could not translate term");

include/anthem/Type.h

@@ -0,0 +1,166 @@
+#ifndef __ANTHEM__ARITHMETICS_H
+#define __ANTHEM__ARITHMETICS_H
+
+#include <anthem/AST.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Arithmetics
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct DefaultVariableDomainAccessor
+{
+	Domain operator()(const ast::Variable &variable)
+	{
+		return variable.declaration->domain;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
+Type type(const ast::Term &term, Arguments &&...);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
+struct TermTypeVisitor
+{
+	template <class... Arguments>
+	static Type visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
+	{
+		const auto leftType = type<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
+		const auto rightType = type<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
+
+		// Binary operations on empty sets return an empty set (also with division)
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Binary operations on nonintegers return an empty set (also with division)
+		if (leftType.domain == Domain::Noninteger || rightType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Binary operations on unknown types return an unknown set
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
+			return {Domain::Unknown, SetSize::Unknown};
+
+		// Divisions return an unknown set
+		if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
+			return {Domain::Integer, SetSize::Unknown};
+
+		// Binary operations on integer sets of unknown size return an integer set of unknown size
+		if (leftType.setSize == SetSize::Unknown || rightType.setSize == SetSize::Unknown)
+			return {Domain::Integer, SetSize::Unknown};
+
+		// Binary operations on integer sets with multiple elements return an integer set with multiple elements
+		if (leftType.setSize == SetSize::Multi || rightType.setSize == SetSize::Multi)
+			return {Domain::Integer, SetSize::Multi};
+
+		// Binary operations on plain integers return a plain integer
+		return {Domain::Integer, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Boolean &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Function &function, Arguments &&...)
+	{
+		// TODO: check that functions cannot return sets
+
+		return {function.declaration->domain, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Integer &, Arguments &&...)
+	{
+		return {Domain::Integer, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Interval &interval, Arguments &&... arguments)
+	{
+		const auto fromType = type<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
+		const auto toType = type<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
+
+		// Intervals with empty sets return an empty set
+		if (fromType.setSize == SetSize::Empty || toType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Intervals with nonintegers return an empty set
+		if (fromType.domain == Domain::Noninteger || toType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Intervals with unknown types return an unknown set
+		if (fromType.domain == Domain::Unknown || toType.domain == Domain::Unknown)
+			return {Domain::Unknown, SetSize::Unknown};
+
+		// Intervals with integers generally return integer sets
+		// TODO: handle 1-element intervals such as 1..1 and empty intervals such as 2..1
+		return {Domain::Integer, SetSize::Unknown};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::SpecialInteger &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::String &, Arguments &&...)
+	{
+		return {Domain::Noninteger, SetSize::Unit};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
+	{
+		assert(unaryOperation.operator_ == ast::UnaryOperation::Operator::Absolute);
+
+		const auto argumentType = type<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
+
+		// Absolute value of an empty set returns an empty set
+		if (argumentType.setSize == SetSize::Empty)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Absolute value of nonintegers returns an empty set
+		if (argumentType.domain == Domain::Noninteger)
+			return {Domain::Unknown, SetSize::Empty};
+
+		// Absolute value of integers returns the same type
+		if (argumentType.domain == Domain::Integer)
+			return argumentType;
+
+		return {Domain::Unknown, SetSize::Unknown};
+	}
+
+	template <class... Arguments>
+	static Type visit(const ast::Variable &variable, Arguments &&... arguments)
+	{
+		const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
+
+		return {domain, SetSize::Unit};
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor, class... Arguments>
+Type type(const ast::Term &term, Arguments &&... arguments)
+{
+	return term.accept(TermTypeVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#endif

include/anthem/Utils.h

@@ -1,13 +1,6 @@
 #ifndef __ANTHEM__UTILS_H
 #define __ANTHEM__UTILS_H
 
-#include <iostream>
-
-#include <clingo.hh>
-
-#include <anthem/Context.h>
-#include <anthem/Location.h>
-
 namespace anthem
 {
 
@@ -23,6 +16,60 @@ constexpr const auto UserVariablePrefix = "U";
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class EvaluationResult
+{
+	True,
+	False,
+	Unknown,
+	Error,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class OperationResult
+{
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Domain
+{
+	Noninteger,
+	Integer,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class SetSize
+{
+	Empty,
+	Unit,
+	Multi,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Type
+{
+	Domain domain{Domain::Unknown};
+	SetSize setSize{SetSize::Unknown};
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif

include/anthem/output/AST.h

@@ -41,37 +41,39 @@ struct PrintContext
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-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 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 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 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 Formula &formula, PrintContext &printContext);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, 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);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Primitives
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::Operator operator_, PrintContext &, bool)
 {
 	switch (operator_)
 	{
@@ -85,6 +87,8 @@ 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;
@@ -92,22 +96,26 @@ inline output::ColorStream &print(output::ColorStream &stream, BinaryOperation::
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &binaryOperation, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, binaryOperation.left, printContext);
 	stream << " ";
 	print(stream, binaryOperation.operator_, printContext);
 	stream << " ";
 	print(stream, binaryOperation.right, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &, bool)
 {
 	if (boolean.value)
 		return (stream << output::Boolean("#true"));
@@ -117,7 +125,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Boolean &bo
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &, bool)
 {
 	switch (operator_)
 	{
@@ -140,7 +148,7 @@ inline output::ColorStream &print(output::ColorStream &stream, Comparison::Opera
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -159,16 +167,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
 {
-	return (stream << constant.name);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
-{
-	stream << function.name;
+	stream << function.declaration->name;
 
 	if (function.arguments.empty())
 		return stream;
@@ -183,7 +184,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
 		print(stream, *i, printContext);
 	}
 
-	if (function.name.empty() && function.arguments.size() == 1)
+	if (function.declaration->name.empty() && function.arguments.size() == 1)
 		stream << ",";
 
 	stream << ")";
@@ -193,7 +194,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -210,14 +211,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const In &in, Pri
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &, bool)
 {
 	return (stream << output::Number<int>(integer.value));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -234,9 +235,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
 {
-	stream << predicate.name;
+	stream << predicate.declaration->name;
 
 	if (predicate.arguments.empty())
 		return stream;
@@ -258,7 +259,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &)
+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)
 {
 	switch (specialInteger.type)
 	{
@@ -273,14 +281,37 @@ inline output::ColorStream &print(output::ColorStream &stream, const SpecialInte
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &)
+inline output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &, bool)
 {
 	return (stream << output::String(string.text.c_str()));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext)
+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)
 {
 	assert(variable.declaration != nullptr);
 
@@ -289,10 +320,26 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
 {
+	const auto domainSuffix =
+		[&variableDeclaration]()
+		{
+			switch (variableDeclaration.domain)
+			{
+				case Domain::Unknown:
+					return "";
+				case Domain::Noninteger:
+					return "n";
+				case Domain::Integer:
+					return "i";
+			}
+
+			return "";
+		};
+
 	const auto printVariableDeclaration =
-		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
+		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
 			auto matchingVariableID = variableIDs.find(&variableDeclaration);
 
@@ -303,7 +350,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 				matchingVariableID = emplaceResult.first;
 			}
 
-			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);
+			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
 
 			return (stream << output::Variable(variableName.c_str()));
 		};
@@ -325,9 +372,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 // Expressions
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const And &and_, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
 
 	for (auto i = and_.arguments.cbegin(); i != and_.arguments.cend(); i++)
 	{
@@ -337,27 +385,32 @@ inline output::ColorStream &print(output::ColorStream &stream, const And &and_,
 		print(stream, *i, printContext);
 	}
 
-	stream << ")";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, biconditional.left, printContext);
 	stream << " <-> ";
 	print(stream, biconditional.right, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Exists &exists, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -383,7 +436,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Exists &exi
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const ForAll &forAll, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -409,20 +462,24 @@ inline output::ColorStream &print(output::ColorStream &stream, const ForAll &for
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Implies &implies, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
+
 	print(stream, implies.antecedent, printContext);
 	stream << " -> ";
 	print(stream, implies.consequent, printContext);
-	stream << ")";
+
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";
 
 	return stream;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Not &not_, PrintContext &printContext, bool)
 {
 	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
@@ -438,9 +495,10 @@ inline output::ColorStream &print(output::ColorStream &stream, const Not &not_,
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, PrintContext &printContext, bool omitParentheses)
 {
-	stream << "(";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << "(";
 
 	for (auto i = or_.arguments.cbegin(); i != or_.arguments.cend(); i++)
 	{
@@ -450,7 +508,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const Or &or_, Pr
 		print(stream, *i, printContext);
 	}
 
-	stream << ")";
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+		stream << ")";
 
 	return stream;
 }
@@ -463,24 +522,24 @@ template<class Variant>
 struct VariantPrintVisitor
 {
 	template<class T>
-	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext)
+	output::ColorStream &visit(const T &x, output::ColorStream &stream, PrintContext &printContext, bool omitParentheses)
 	{
-		return print(stream, x, printContext);
+		return print(stream, x, printContext, omitParentheses);
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext, bool omitParentheses)
 {
-	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
+	return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext, omitParentheses);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
+inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext, bool omitParentheses)
 {
-	return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
+	return term.accept(VariantPrintVisitor<Term>(), stream, printContext, omitParentheses);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/ASTCopy.cpp

@@ -103,16 +103,9 @@ Comparison prepareCopy(const Comparison &other)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-Constant prepareCopy(const Constant &other)
-{
-	return Constant(std::string(other.name));
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 Function prepareCopy(const Function &other)
 {
-	return Function(std::string(other.name), prepareCopy(other.arguments));
+	return Function(other.declaration, prepareCopy(other.arguments));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -140,7 +133,7 @@ Interval prepareCopy(const Interval &other)
 
 Predicate prepareCopy(const Predicate &other)
 {
-	return Predicate(std::string(other.name), prepareCopy(other.arguments));
+	return Predicate(other.declaration, prepareCopy(other.arguments));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -159,6 +152,13 @@ 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,11 +286,6 @@ struct FixDanglingVariablesInTermVisitor
 	{
 	}
 
-	template <class... Arguments>
-	void visit(Constant &, Arguments &&...)
-	{
-	}
-
 	template <class... Arguments>
 	void visit(Function &function, Arguments &&... arguments)
 	{
@@ -320,6 +315,12 @@ 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)
 	{

src/anthem/ASTUtils.cpp

@@ -59,7 +59,7 @@ bool VariableStack::contains(const VariableDeclaration &variableDeclaration) con
 		};
 
 	const auto layerContainsVariableDeclaration =
-		[&variableDeclaration, &variableDeclarationMatches](const auto &layer)
+		[&variableDeclarationMatches](const auto &layer)
 		{
 			return (std::find_if(layer->cbegin(), layer->cend(), variableDeclarationMatches) != layer->cend());
 		};
@@ -150,10 +150,6 @@ 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)
@@ -178,6 +174,11 @@ 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))
@@ -192,61 +193,5 @@ struct CollectFreeVariablesVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
-{
-	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
-	{
-		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
-		predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
-	}
-
-	// Ignore all other types of expressions
-	template<class T>
-	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
-	{
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-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)
-{
-	auto &formulaMutable = const_cast<Formula &>(formula);
-	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 }

src/anthem/Completion.cpp

@@ -35,7 +35,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 
 		auto &otherPredicate = implies.consequent.get<ast::Predicate>();
 
-		if (!ast::matches(predicate, otherPredicate))
+		if (predicate.declaration != otherPredicate.declaration)
 			continue;
 
 		assert(otherPredicate.arguments.size() == parameters.size());
@@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
+ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
 	// Create new set of parameters for the completed definition for the predicate
 	ast::VariableDeclarationPointers parameters;
-	parameters.reserve(predicateSignature.arity);
+	parameters.reserve(predicateDeclaration.arity());
 
 	std::vector<ast::Term> arguments;
-	arguments.reserve(predicateSignature.arity);
+	arguments.reserve(predicateDeclaration.arity());
 
-	for (size_t i = 0; i < predicateSignature.arity; i++)
+	for (size_t i = 0; i < predicateDeclaration.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(std::string(predicateSignature.name), std::move(arguments));
+	ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
 
 	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
 	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@@ -161,65 +161,26 @@ 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::vector<ast::PredicateSignature> predicateSignatures;
-
-	// Get a list of all predicates
-	for (const auto &scopedFormula : scopedFormulas)
-		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
-
-	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
+	std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.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;
 
-	// Warn about incorrect #external declarations
-	if (context.externalPredicateSignatures)
-		for (const auto &externalPredicateSignature : *context.externalPredicateSignatures)
-		{
-			// TODO: avoid code duplication
-			const auto matchesPredicateSignature =
-				[&](const auto &otherPredicateSignature)
-				{
-					return ast::matches(externalPredicateSignature, otherPredicateSignature);
-				};
-
-			const auto matchingPredicateSignature =
-				std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
-
-			if (matchingPredicateSignature == predicateSignatures.cend())
-				context.logger.log(output::Priority::Warning) << "#external declaration of “" << externalPredicateSignature.name << "/" << externalPredicateSignature.arity <<"” does not match any known predicate";
-		}
-
 	// Complete predicates
-	for (const auto &predicateSignature : predicateSignatures)
+	for (auto &predicateDeclaration : context.predicateDeclarations)
 	{
-		// Don’t complete predicates that are declared #external
-		if (context.externalPredicateSignatures)
-		{
-			const auto matchesPredicateSignature =
-				[&](const auto &otherPredicateSignature)
-				{
-					return ast::matches(predicateSignature, otherPredicateSignature);
-				};
+		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
+			continue;
 
-			const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
-
-			const auto matchingExternalPredicateSignature =
-				std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
-
-			if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
-				continue;
-		}
-
-		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
+		completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
 	}
 
 	// Complete integrity constraints
@@ -240,7 +201,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 	}
 
 	// Eliminate all predicates that should not be visible in the output
-	eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
+	eliminateHiddenPredicates(completedFormulas, context);
 
 	return completedFormulas;
 }

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 (!ast::matches(predicate, predicateReplacement.predicate))
+		if (predicate.declaration != predicateReplacement.predicate.declaration)
 			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::PredicateSignature &predicateSignature, bool &hasCircularDependency)
+	static void accept(ast::Predicate &predicate, ast::Formula &, const ast::PredicateDeclaration &predicateDeclaration, bool &hasCircularDependency)
 	{
-		if (ast::matches(predicate, predicateSignature))
+		if (predicate.declaration == &predicateDeclaration)
 			hasCircularDependency = true;
 	}
 
 	// Ignore all other types of expressions
 	template<class T>
-	static void accept(T &, ast::Formula &, const ast::PredicateSignature &, bool &)
+	static void accept(T &, ast::Formula &, const ast::PredicateDeclaration &, 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::PredicateSignature &predicateSignature, const ast::Predicate &predicate)
+PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Predicate &predicate)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateSignature);
+	(void)(predicateDeclaration);
 
-	assert(ast::matches(predicate, predicateSignature));
+	assert(predicate.declaration == &predicateDeclaration);
 
 	// Replace with “#true”
 	return {predicate, ast::Formula::make<ast::Boolean>(true)};
@@ -139,13 +139,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // Finds the replacement for predicates of the form “p(X1, ..., Xn) <-> not q(X1, ..., Xn)”
-PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Not &not_)
+PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Not &not_)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateSignature);
+	(void)(predicateDeclaration);
 
 	assert(not_.argument.is<ast::Predicate>());
-	assert(ast::matches(not_.argument.get<ast::Predicate>(), predicateSignature));
+	assert(not_.argument.get<ast::Predicate>().declaration == &predicateDeclaration);
 
 	// Replace with “#false”
 	return {not_.argument.get<ast::Predicate>(), ast::Formula::make<ast::Boolean>(false)};
@@ -154,13 +154,13 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // Finds the replacement for predicates of the form “forall X1, ..., Xn (p(X1, ..., Xn) <-> ...)”
-PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Biconditional &biconditional)
+PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Biconditional &biconditional)
 {
 	// Declare variable used, only used in debug mode
-	(void)(predicateSignature);
+	(void)(predicateDeclaration);
 
 	assert(biconditional.left.is<ast::Predicate>());
-	assert(ast::matches(biconditional.left.get<ast::Predicate>(), predicateSignature));
+	assert(biconditional.left.get<ast::Predicate>().declaration == &predicateDeclaration);
 
 	// TODO: avoid copy
 	return {biconditional.left.get<ast::Predicate>(), ast::prepareCopy(biconditional.right)};
@@ -169,90 +169,65 @@ PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSig
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // Finds a replacement for a predicate that should be hidden
-PredicateReplacement findReplacement(const ast::PredicateSignature &predicateSignature, const ast::Formula &completedPredicateDefinition)
+PredicateReplacement findReplacement(const ast::PredicateDeclaration &predicateDeclaration, const ast::Formula &completedPredicateDefinition)
 {
 	// TODO: refactor
 	if (completedPredicateDefinition.is<ast::ForAll>())
-		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::ForAll>().argument);
+		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::ForAll>().argument);
 	else if (completedPredicateDefinition.is<ast::Biconditional>())
-		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Biconditional>());
+		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Biconditional>());
 	else if (completedPredicateDefinition.is<ast::Predicate>())
-		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Predicate>());
+		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Predicate>());
 	else if (completedPredicateDefinition.is<ast::Not>())
-		return findReplacement(predicateSignature, completedPredicateDefinition.get<ast::Not>());
+		return findReplacement(predicateDeclaration, completedPredicateDefinition.get<ast::Not>());
 
-	throw CompletionException("unsupported completed definition for predicate “" + predicateSignature.name + "/" +  std::to_string(predicateSignature.arity) + "” for hiding predicates");
+	throw CompletionException("unsupported completed definition for predicate “" + predicateDeclaration.name + "/" +  std::to_string(predicateDeclaration.arity()) + "” for hiding predicates");
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predicateSignatures, std::vector<ast::Formula> &completedFormulas, Context &context)
+void eliminateHiddenPredicates(std::vector<ast::Formula> &completedFormulas, Context &context)
 {
-	if (!context.visiblePredicateSignatures)
+	if (context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible)
 	{
 		context.logger.log(output::Priority::Debug) << "no predicates to be eliminated";
 		return;
 	}
 
-	const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
+	assert(context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Hidden);
 
-	// Check for undeclared predicates that are requested to be shown
-	for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
-	{
-		const auto matchesPredicateSignature =
-			[&](const auto &predicateSignature)
-			{
-				return ast::matches(predicateSignature, visiblePredicateSignature);
-			};
-
-		const auto matchingPredicateSignature =
-			std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
-
-		if (matchingPredicateSignature == predicateSignatures.cend())
-			context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”";
-	}
+	// TODO: get rid of index-wise matching of completed formulas and predicate declarations
+	size_t i = -1;
 
 	// Replace all occurrences of hidden predicates
-	for (size_t i = 0; i < predicateSignatures.size(); i++)
+	for (auto &predicateDeclaration : context.predicateDeclarations)
 	{
-		auto &predicateSignature = predicateSignatures[i];
-
-		const auto matchesPredicateSignature =
-			[&](const auto &otherPredicateSignature)
-			{
-				return ast::matches(predicateSignature, otherPredicateSignature);
-			};
-
-		const auto matchingVisiblePredicateSignature =
-			std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesPredicateSignature);
-
-		// If the predicate ought to be visible, don’t eliminate it
-		if (matchingVisiblePredicateSignature != visiblePredicateSignatures.cend())
+		// Check that the predicate is used and not declared #external
+		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
 			continue;
 
-		// Check that the predicate is not declared #external
-		if (context.externalPredicateSignatures)
-		{
-			const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+		i++;
 
-			const auto matchingExternalPredicateSignature =
-				std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
+		const auto isPredicateVisible =
+			(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
+			|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
+				&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
 
-			if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
-				continue;
-		}
+		// If the predicate ought to be visible, don’t eliminate it
+		if (isPredicateVisible)
+			continue;
 
-		context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";
+		context.logger.log(output::Priority::Debug) << "eliminating “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "”";
 
 		const auto &completedPredicateDefinition = completedFormulas[i];
-		auto replacement = findReplacement(predicateSignature, completedPredicateDefinition);
+		auto replacement = findReplacement(*predicateDeclaration, completedPredicateDefinition);
 
 		bool hasCircularDependency = false;
-		replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, predicateSignature, hasCircularDependency);
+		replacement.replacement.accept(DetectCircularDependcyVisitor(), replacement.replacement, *predicateDeclaration, hasCircularDependency);
 
 		if (hasCircularDependency)
 		{
-			context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateSignature.name << "/" << predicateSignature.arity << "” due to circular dependency";
+			context.logger.log(output::Priority::Warning) << "cannot hide predicate “" << predicateDeclaration->name << "/" << predicateDeclaration->arity() << "” due to circular dependency";
 			continue;
 		}
 

src/anthem/IntegerVariableDetection.cpp

@@ -0,0 +1,540 @@
+#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/Type.h>
+#include <anthem/Utils.h>
+#include <anthem/output/AST.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// IntegerVariableDetection
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+{
+	if (variable.declaration->domain != Domain::Unknown)
+		return variable.declaration->domain;
+
+	const auto match = variableDomainMap.find(variable.declaration);
+
+	if (match == variableDomainMap.end())
+		return Domain::Unknown;
+
+	return match->second;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
+{
+	for (auto &variableDeclaration : variableDomainMap)
+		variableDeclaration.second = Domain::Unknown;
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct VariableDomainMapAccessor
+{
+	Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+	{
+		return domain(variable, variableDomainMap);
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
+{
+	return type<VariableDomainMapAccessor>(term, 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 leftType = type(comparison.left, variableDomainMap);
+		const auto rightType = type(comparison.right, variableDomainMap);
+
+		// Comparisons with empty sets always return false
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
+
+		// If either side has an unknown domain, the result is unknown
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
+			return EvaluationResult::Unknown;
+
+		// If both sides have the same domain, the result is unknown
+		if (leftType.domain == rightType.domain)
+			return EvaluationResult::Unknown;
+
+		// If one side is integer, but the other one isn’t, they are not equal
+		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 elementType = type(in.element, variableDomainMap);
+		const auto setType = type(in.set, variableDomainMap);
+
+		// The element to test shouldn’t be empty or a proper set by itself
+		assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
+
+		// If the set is empty, no element can be selected
+		if (setType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
+
+		// If one of the sides has an unknown type, the result is unknown
+		if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
+			return EvaluationResult::Unknown;
+
+		// If both sides have the same domain, the result is unknown
+		if (elementType.domain == setType.domain)
+			return EvaluationResult::Unknown;
+
+		// If one side is integer, 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 != Domain::Integer)
+				continue;
+
+			const auto argumentType = type(argument, variableDomainMap);
+
+			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
+				return EvaluationResult::Error;
+		}
+
+		return EvaluationResult::Unknown;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
+{
+	return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class Functor>
+struct ForEachVariableDeclarationVisitor
+{
+	template <class... Arguments>
+	static OperationResult visit(ast::And &and_, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		for (auto &argument : and_.arguments)
+			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Boolean &, Arguments &&...)
+	{
+		return OperationResult::Unchanged;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Comparison &, Arguments &&...)
+	{
+		return OperationResult::Unchanged;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		for (auto &variableDeclaration : exists.variables)
+			if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		for (auto &variableDeclaration : forAll.variables)
+			if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::In &, Arguments &&...)
+	{
+		return OperationResult::Unchanged;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
+	{
+		return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
+	{
+		auto operationResult = OperationResult::Unchanged;
+
+		for (auto &argument : or_.arguments)
+			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+		return operationResult;
+	}
+
+	template <class... Arguments>
+	static OperationResult visit(ast::Predicate &, Arguments &&...)
+	{
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfDefinitionFalseFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto 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
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfQuantifiedFormulaFalseFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto result = evaluate(quantifiedFormula, 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
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfCompletedFormulaTrueFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto result = evaluate(completedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::True)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// 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 (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), 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;
+
+			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+			assert(predicate.arguments.size() == predicate.declaration->arity());
+
+			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>();
+
+				parameter.domain = variable.declaration->domain;
+			}
+		}
+	}
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}

src/anthem/Simplification.cpp

@@ -3,7 +3,10 @@
 #include <optional>
 
 #include <anthem/ASTCopy.h>
-#include <anthem/ASTVisitors.h>
+#include <anthem/Equality.h>
+#include <anthem/SimplificationVisitors.h>
+#include <anthem/Type.h>
+#include <anthem/output/AST.h>
 
 namespace anthem
 {
@@ -97,18 +100,65 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
-// The exists statement has to be of the form “exists <variables> <conjunction>”
-void simplify(ast::Exists &exists, ast::Formula &formula)
+template<class SimplificationRule>
+OperationResult simplify(ast::Formula &formula)
 {
-	// Simplify formulas like “exists X (X = Y)” to “#true”
-	// TODO: check that this covers all cases
-	if (exists.argument.is<ast::Comparison>())
+	return SimplificationRule::apply(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
+OperationResult simplify(ast::Formula &formula)
+{
+	if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
+		return OperationResult::Changed;
+
+	return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleExistsWithoutQuantifiedVariables
+{
+	static constexpr const auto Description = "exists () (F) === F";
+
+	static OperationResult apply(ast::Formula &formula)
 	{
+		if (!formula.is<ast::Exists>())
+			return OperationResult::Unchanged;
+
+		auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.variables.empty())
+			return OperationResult::Unchanged;
+
+		formula = std::move(exists.argument);
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleTrivialAssignmentInExists
+{
+	static constexpr const auto Description = "exists X (X = Y) === #true";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Exists>())
+			return OperationResult::Unchanged;
+
+		const auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.argument.is<ast::Comparison>())
+			return OperationResult::Unchanged;
+
 		const auto &comparison = exists.argument.get<ast::Comparison>();
 
 		if (comparison.operator_ != ast::Comparison::Operator::Equal)
-			return;
+			return OperationResult::Unchanged;
 
 		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
 			[&](const auto &variableDeclaration)
@@ -117,107 +167,407 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 					|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
 			});
 
-		if (matchingAssignment != exists.variables.cend())
-			formula = ast::Formula::make<ast::Boolean>(true);
+		if (matchingAssignment == exists.variables.cend())
+			return OperationResult::Unchanged;
 
-		return;
+		formula = ast::Formula::make<ast::Boolean>(true);
+
+		return OperationResult::Changed;
 	}
+};
 
-	if (!exists.argument.is<ast::And>())
-		return;
+////////////////////////////////////////////////////////////////////////////////////////////////////
 
-	auto &conjunction = exists.argument.get<ast::And>();
-	auto &arguments = conjunction.arguments;
+struct SimplificationRuleAssignmentInExists
+{
+	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
 
-	// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
-	for (auto i = exists.variables.begin(); i != exists.variables.end();)
+	static OperationResult apply(ast::Formula &formula)
 	{
-		const auto &variableDeclaration = **i;
+		if (!formula.is<ast::Exists>())
+			return OperationResult::Unchanged;
 
-		bool wasVariableReplaced = false;
+		auto &exists = formula.get<ast::Exists>();
 
-		// TODO: refactor
-		for (auto j = arguments.begin(); j != arguments.end(); j++)
+		if (!exists.argument.is<ast::And>())
+			return OperationResult::Unchanged;
+
+		auto &and_ = exists.argument.get<ast::And>();
+		auto &arguments = and_.arguments;
+
+		auto simplificationResult = OperationResult::Unchanged;
+
+		for (auto i = exists.variables.begin(); i != exists.variables.end();)
 		{
-			auto &argument = *j;
-			// Find term that is equivalent to the given variable
-			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
+			const auto &variableDeclaration = **i;
 
-			if (!assignedTerm)
-				continue;
+			bool wasVariableReplaced = false;
 
-			// Replace all occurrences of the variable with the equivalent term
-			for (auto k = arguments.begin(); k != arguments.end(); k++)
+			// TODO: refactor
+			for (auto j = arguments.begin(); j != arguments.end(); j++)
 			{
-				if (k == j)
+				auto &argument = *j;
+				// Find term that is equivalent to the given variable
+				auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
+
+				if (!assignedTerm)
 					continue;
 
-				auto &otherArgument = *k;
-				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				// Replace all occurrences of the variable with the equivalent term
+				for (auto k = arguments.begin(); k != arguments.end(); k++)
+				{
+					if (k == j)
+						continue;
+
+					auto &otherArgument = *k;
+					otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				}
+
+				arguments.erase(j);
+
+				wasVariableReplaced = true;
+				simplificationResult = OperationResult::Changed;
+
+				break;
 			}
 
-			arguments.erase(j);
-			wasVariableReplaced = true;
-			break;
+			if (wasVariableReplaced)
+			{
+				i = exists.variables.erase(i);
+				continue;
+			}
+
+			i++;
 		}
 
-		if (wasVariableReplaced)
-		{
-			i = exists.variables.erase(i);
-			continue;
-		}
-
-		i++;
+		return simplificationResult;
 	}
+};
 
-	// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
-	// Such exists statements are useless and can be safely replaced with “#true”
-	if (arguments.empty())
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleEmptyConjunction
+{
+	static constexpr const auto Description = "[empty conjunction] === #true";
+
+	static OperationResult apply(ast::Formula &formula)
 	{
+		if (!formula.is<ast::And>())
+			return OperationResult::Unchanged;
+
+		auto &and_ = formula.get<ast::And>();
+
+		if (!and_.arguments.empty())
+			return OperationResult::Unchanged;
+
 		formula = ast::Formula::make<ast::Boolean>(true);
-		return;
+
+		return OperationResult::Changed;
 	}
+};
 
-	// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
-	if (arguments.size() == 1)
-		exists.argument = std::move(arguments.front());
+////////////////////////////////////////////////////////////////////////////////////////////////////
 
-	// If there are still remaining variables, simplification is over
-	if (!exists.variables.empty())
-		return;
+struct SimplificationRuleOneElementConjunction
+{
+	static constexpr const auto Description = "[conjunction of only F] === F";
 
-	assert(!arguments.empty());
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::And>())
+			return OperationResult::Unchanged;
 
-	// If there is more than one element in the conjunction, replace the input formula with the conjunction
-	formula = std::move(exists.argument);
-}
+		auto &and_ = formula.get<ast::And>();
+
+		if (and_.arguments.size() != 1)
+			return OperationResult::Unchanged;
+
+		formula = std::move(and_.arguments.front());
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleTrivialExists
+{
+	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Exists>())
+			return OperationResult::Unchanged;
+
+		auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.argument.is<ast::Boolean>())
+			return OperationResult::Unchanged;
+
+		formula = std::move(exists.argument);
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleInWithPrimitiveArguments
+{
+	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::In>())
+			return OperationResult::Unchanged;
+
+		auto &in = formula.get<ast::In>();
+
+		assert(ast::isPrimitive(in.element));
+
+		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
+			return OperationResult::Unchanged;
+
+		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleSubsumptionInBiconditionals
+{
+	static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Biconditional>())
+			return OperationResult::Unchanged;
+
+		auto &biconditional = formula.get<ast::Biconditional>();
+
+		const auto leftIsPredicate = biconditional.left.is<ast::Predicate>();
+		const auto rightIsPredicate = biconditional.right.is<ast::Predicate>();
+
+		const auto leftIsAnd = biconditional.left.is<ast::And>();
+		const auto rightIsAnd = biconditional.right.is<ast::And>();
+
+		if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
+			return OperationResult::Unchanged;
+
+		auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
+		auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
+		auto &and_ = andSide.get<ast::And>();
+
+		const auto matchingPredicate =
+			std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
+			[&](const auto &argument)
+			{
+				return (ast::equal(predicateSide, argument) == Tristate::True);
+			});
+
+		if (matchingPredicate == and_.arguments.cend())
+			return OperationResult::Unchanged;
+
+		and_.arguments.erase(matchingPredicate);
+
+		formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleDoubleNegation
+{
+	static constexpr const auto Description = "not not F === F";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return OperationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::Not>())
+			return OperationResult::Unchanged;
+
+		auto &notNot = not_.argument.get<ast::Not>();
+
+		formula = std::move(notNot.argument);
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleDeMorganForConjunctions
+{
+	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return OperationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::And>())
+			return OperationResult::Unchanged;
+
+		auto &and_ = not_.argument.get<ast::And>();
+
+		for (auto &argument : and_.arguments)
+			argument = ast::Formula::make<ast::Not>(std::move(argument));
+
+		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleImplicationFromDisjunction
+{
+	static constexpr const auto Description = "(not F or G) === (F -> G)";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Or>())
+			return OperationResult::Unchanged;
+
+		auto &or_ = formula.get<ast::Or>();
+
+		if (or_.arguments.size() != 2)
+			return OperationResult::Unchanged;
+
+		const auto leftIsNot = or_.arguments[0].is<ast::Not>();
+		const auto rightIsNot = or_.arguments[1].is<ast::Not>();
+
+		if (leftIsNot == rightIsNot)
+			return OperationResult::Unchanged;
+
+		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
+		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
+
+		assert(negativeSide.is<ast::Not>());
+		assert(!positiveSide.is<ast::Not>());
+
+		auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
+
+		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleNegatedComparison
+{
+	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return OperationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::Comparison>())
+			return OperationResult::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 OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleIntegerSetInclusion
+{
+	static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::In>())
+			return OperationResult::Unchanged;
+
+		auto &in = formula.get<ast::In>();
+
+		const auto elementType = type(in.element);
+		const auto setType = type(in.set);
+
+		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
+		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
+		{
+			return OperationResult::Unchanged;
+		}
+
+		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+const auto simplifyWithDefaultRules =
+	simplify
+	<
+		SimplificationRuleDoubleNegation,
+		SimplificationRuleTrivialAssignmentInExists,
+		SimplificationRuleAssignmentInExists,
+		SimplificationRuleEmptyConjunction,
+		SimplificationRuleTrivialExists,
+		SimplificationRuleOneElementConjunction,
+		SimplificationRuleExistsWithoutQuantifiedVariables,
+		SimplificationRuleInWithPrimitiveArguments,
+		SimplificationRuleSubsumptionInBiconditionals,
+		SimplificationRuleDeMorganForConjunctions,
+		SimplificationRuleImplicationFromDisjunction,
+		SimplificationRuleNegatedComparison,
+		SimplificationRuleIntegerSetInclusion
+	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 // Performs the different simplification techniques
-struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyFormulaVisitor>
+struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
 {
-	// Forward exists statements to the dedicated simplification function
-	static void accept(ast::Exists &exists, ast::Formula &formula)
-	{
-		simplify(exists, formula);
-	}
-
-	// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
-	static void accept(ast::In &in, ast::Formula &formula)
-	{
-		assert(ast::isPrimitive(in.element));
-
-		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return;
-
-		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
-	}
-
 	// Do nothing for all other types of expressions
-	template<class T>
-	static void accept(T &, ast::Formula &)
+	static OperationResult accept(ast::Formula &formula)
 	{
+		return simplifyWithDefaultRules(formula);
 	}
 };
 
@@ -225,7 +575,7 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
 
 void simplify(ast::Formula &formula)
 {
-	formula.accept(SimplifyFormulaVisitor(), formula);
+	while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

@@ -8,6 +8,7 @@
 
 #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>
@@ -67,10 +68,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 			for (auto &scopedFormula : scopedFormulas)
 				simplify(scopedFormula.formula);
 
-		if (context.visiblePredicateSignatures)
+		if (context.showStatementsUsed)
 			context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
 
-		if (context.externalPredicateSignatures)
+		if (context.externalStatementsUsed)
 			context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
 
 		for (const auto &scopedFormula : scopedFormulas)
@@ -85,6 +86,34 @@ 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 (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);
+
 	// Simplify output if specified
 	if (context.performSimplification)
 		for (auto &completedFormula : completedFormulas)
@@ -97,6 +126,38 @@ 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 != Domain::Integer)
+				continue;
+
+			context.logger.outputStream()
+				<< output::Keyword("int")
+				<< "(" << predicateDeclaration->name
+				<< "/" << output::Number(predicateDeclaration->arity())
+				<< "@" << output::Number(i + 1)
+				<< ")." << std::endl;
+		}
+	}
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

@@ -152,9 +152,9 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 
 		CHECK(output.str() ==
 			"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
-			"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
-			"forall U2 not (U2 in 1..n and not covered(U2))\n"
-			"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
+			"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
+			"forall U2 (U2 in 1..n -> covered(U2))\n"
+			"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}
 
 	SECTION("binary operations with multiple variables")
@@ -176,4 +176,20 @@ 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");
+	}
 }

tests/TestHiddenPredicateElimination.cpp

@@ -103,9 +103,10 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show a/1.";
 		anthem::translate("input", input, context);
 
+		// TODO: simplify further
 		CHECK(output.str() ==
 			"forall V1 (a(V1) <-> not d(V1))\n"
-			"forall V2 (d(V2) <-> not not d(V2))\n"
+			"forall V2 (d(V2) <-> d(V2))\n"
 			"forall V3 (e(V3) <-> e(V3))\n");
 	}
 
@@ -164,12 +165,11 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show t/0.";
 		anthem::translate("input", input, context);
 
-		// TODO: simplify further
 		CHECK(output.str() ==
-			"(s <-> (not #false and s))\n"
-			"(t <-> (not #false and t))\n"
-			"not (s and not t)\n"
-			"not (not #false and not #false and #false)\n");
+			"(s -> not #false)\n"
+			"(t -> not #false)\n"
+			"(s -> t)\n"
+			"(#false or #false or not #false)\n");
 	}
 
 	SECTION("predicate with more than one argument is hidden correctly")

tests/TestPlaceholders.cpp

@@ -0,0 +1,62 @@
+#include <catch.hpp>
+
+#include <sstream>
+
+#include <anthem/AST.h>
+#include <anthem/Context.h>
+#include <anthem/Translation.h>
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "[placeholders]")
+{
+	std::stringstream input;
+	std::stringstream output;
+	std::stringstream errors;
+
+	anthem::output::Logger logger(output, errors);
+	anthem::Context context(std::move(logger));
+	context.performSimplification = true;
+	context.performCompletion = true;
+
+	SECTION("no placeholders")
+	{
+		input <<
+			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n"
+			"forall V3 not vertex(V3)\n");
+	}
+
+	SECTION("single placeholder")
+	{
+		input <<
+			"#external vertex(1).\n"
+			"colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (colored(V1, V2) <-> (V2 = red and vertex(V1) and not colored(V1, green) and not colored(V1, blue)))\n");
+	}
+
+	SECTION("complex example: graph coloring")
+	{
+		input <<
+			"#external color(1).\n"
+			"#external edge(2).\n"
+			"#external vertex(1).\n"
+			"#show color/2.\n"
+			"{color(V, C)} :- vertex(V), color(C).\n"
+			"covered(V) :- color(V, _).\n"
+			":- vertex(V), not covered(V).\n"
+			":- color(V1, C), color(V2, C), edge(V1, V2).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() ==
+			"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
+			"forall U1 (vertex(U1) -> exists U2 color(U1, U2))\n"
+			"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
+	}
+}

tests/TestTranslation.cpp

@@ -296,4 +296,12 @@ 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");
+	}
 }