Version bump after release 0.1.9

By default, completion, simplification, and integer variable detection
are now turned on by default. This updates the readme accordingly.

.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

@@ -2,6 +2,38 @@
 
 ## (unreleased)
 
+## 0.1.9 (2018-05-04)
+
+### Changes
+
+* turns on completion and simplification by default, which can now be switched off with `--no-complete` and `--no-simplify`
+
+### Features
+
+* detection of integer variables and integer predicate parameters
+* command-line option `--no-detect-integers` to disable integer variable detection
+* new simplification rule applying to integer variables
+* support for declaring functions integer with the `#external` directive
+
+### Bug Fixes
+
+* fixes incorrect translation of unsupported choice rules with multiple elements by returning an error instead
+* fixes precedence of intervals by enclosing them in parentheses
+
+## 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)

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,12 @@
 ## Usage
 
 ```bash
-$ anthem [--simplify] file...
+$ anthem [--no-complete] [--no-simplify] [--no-detect-integers] file...
 ```
 
-With the option `--simplify`, output formulas are simplified by applying several basic transformation rules.
+By default, `anthem` performs Clark’s completion on the translated formulas, detects which variables are integer, and simplifies the output by applying several basic transformation rules.
+
+These processing steps can be turned off with the options `--no-complete`, `--no-simplify`, and `--no-detect-integers`.
 
 ## Building
 

app/main.cpp

@@ -16,8 +16,9 @@ int main(int argc, char **argv)
 		("h,help", "Display this help message")
 		("v,version", "Display version information")
 		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
-		("s,simplify", "Simplify the output")
+		("no-simplify", "Do not simplify the output")
-		("c,complete", "Perform completion")
+		("no-complete", "Do not perform completion")
+		("no-detect-integers", "Do not 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"));
@@ -48,8 +49,9 @@ int main(int argc, char **argv)
 		if (parseResult.count("input") > 0)
 			inputFiles = parseResult["input"].as<std::vector<std::string>>();
 
-		context.performSimplification = (parseResult.count("simplify") > 0);
+		context.performSimplification = (parseResult.count("no-simplify") == 0);
-		context.performCompletion = (parseResult.count("complete") > 0);
+		context.performCompletion = (parseResult.count("no-complete") == 0);
+		context.performIntegerDetection = (parseResult.count("no-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-git" << std::endl;
+		std::cout << "anthem version 0.1.9+git" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/choice-rules.lp

@@ -0,0 +1,2 @@
+p(a).
+{q(a)}.

examples/graph-coloring.lp

@@ -1,12 +1,18 @@
-colored(V, red) :- vertex(V), not colored(V, green), not colored(V, blue).
+% assign a set of colors to each vertex
-colored(V, green) :- vertex(V), not colored(V, red), not colored(V, blue).
+{color(V, C)} :- vertex(V), color(C).
-colored(V, blue) :- vertex(V), not colored(V, red), not colored(V, green).
 
-:- edge(V1, V2), colored(V1, C), colored(V2, C).
+% at most one color per vertex
+:- color(V, C1), color(V, C2), C1 != C2.
 
-vertex(a).
+% at least one color per vertex
-vertex(b).
+covered(V) :- color(V, _).
-vertex(c).
+:- vertex(V), not covered(V).
 
-edge(a, b).
+% adjacent vertices don’t share the same color
-edge(a, c).
+:- color(V1, C), color(V2, C), edge(V1, V2).
+
+#show color/2.
+
+#external vertex(1).
+#external edge(2).
+#external color(1).

examples/letters.lp

@@ -0,0 +1,11 @@
+letter(a).
+letter(b).
+letter(c).
+
+{p(1..3, Y)} :- letter(Y).
+:- p(X1, Y), p(X2, Y), X1 != X2.
+
+q(X) :- p(X, _).
+:- X = 1..3, not q(X).
+
+#show p/2.

examples/permutations.lp

@@ -0,0 +1,12 @@
+#show p/2.
+
+{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,4 @@
+#show prime/1.
+
+composite(I * J) :- I = 2..n, J = 2..n.
+prime(N) :- N = 2..n, not composite(N).

examples/schur-numbers.lp

@@ -1,3 +1,5 @@
+#show in/2.
+
 {in(1..n, 1..r)}.
 covered(I) :- in(I, S).
 

examples/simple-external-show.lp

@@ -0,0 +1,9 @@
+s(X) :- p(X).
+s(X) :- q(X).
+u(X) :- r(X), not s(X).
+
+#show u/1.
+
+#external p(1).
+#external q(1).
+#external r(1).

examples/simple-external.lp

@@ -0,0 +1,5 @@
+s(X) :- p(X).
+s(X) :- q(X).
+
+#external p(1).
+#external q(1).

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)
+	explicit Function(FunctionDeclaration *declaration)
-	:	name{std::move(name)}
+	:	declaration{declaration}
 	{
 	}
 
-	explicit Function(std::string &&name, std::vector<Term> &&arguments)
+	explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
-	:	name{std::move(name)},
+	:	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)
+	explicit Predicate(PredicateDeclaration *declaration)
-	:	name{std::move(name)}
+	:	declaration{declaration}
 	{
 	}
 
-	explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
+	explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
-	:	name{std::move(name)},
+	:	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
+	PredicateDeclaration *declaration{nullptr};
-	{
-		return arguments.size();
-	}
-
-	std::string name;
 	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// TODO: make more use of this class
+struct PredicateDeclaration
-struct PredicateSignature
 {
-	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;
+	PredicateDeclaration(const PredicateDeclaration &other) = delete;
-	PredicateSignature &operator=(const PredicateSignature &other) = delete;
+	PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
-	// TODO: make noexcept again
+	PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
-	// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
+	PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
-	PredicateSignature(PredicateSignature &&other) = default;
+
-	PredicateSignature &operator=(PredicateSignature &&other) = 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
@@ -95,6 +90,21 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 }
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Accessing Variable Domains
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct DefaultVariableDomainAccessor
+{
+	Domain operator()(const ast::Variable &variable)
+	{
+		return variable.declaration->domain;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif

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[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, 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,12 +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 performSimplification{false};
-	bool performCompletion = false;
+	bool performCompletion{false};
+	bool performIntegerDetection{false};
 
-	std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
+	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, otherBinaryOperation.right) == Tristate::True
+		    && equal(binaryOperation.right, otherBinaryOperation.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/Evaluation.h

@@ -0,0 +1,244 @@
+#ifndef __ANTHEM__EVALUATION_H
+#define __ANTHEM__EVALUATION_H
+
+#include <anthem/AST.h>
+#include <anthem/ASTUtils.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Evaluation
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
+struct EvaluateFormulaVisitor
+{
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::And &and_, Arguments &&... arguments)
+	{
+		bool someFalse = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : and_.arguments)
+		{
+			const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
+
+			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;
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Biconditional &biconditional, Arguments &&... arguments)
+	{
+		const auto leftResult = evaluate(biconditional.left, std::forward<Arguments>(arguments)...);
+		const auto rightResult = evaluate(biconditional.right, std::forward<Arguments>(arguments)...);
+
+		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);
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Boolean &boolean, Arguments &&...)
+	{
+		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Comparison &comparison, Arguments &&... arguments)
+	{
+		const auto leftType = type(comparison.left, std::forward<Arguments>(arguments)...);
+		const auto rightType = type(comparison.right, std::forward<Arguments>(arguments)...);
+
+		// 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;
+		}
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Exists &exists, Arguments &&... arguments)
+	{
+		return evaluate(exists.argument, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::ForAll &forAll, Arguments &&... arguments)
+	{
+		return evaluate(forAll.argument, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Implies &implies, Arguments &&... arguments)
+	{
+		const auto antecedentResult = evaluate(implies.antecedent, std::forward<Arguments>(arguments)...);
+		const auto consequentResult = evaluate(implies.consequent, std::forward<Arguments>(arguments)...);
+
+		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;
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::In &in, Arguments &&... arguments)
+	{
+		const auto elementType = type(in.element, std::forward<Arguments>(arguments)...);
+		const auto setType = type(in.set, std::forward<Arguments>(arguments)...);
+
+		// 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;
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Not &not_, Arguments &&... arguments)
+	{
+		const auto result = evaluate(not_.argument, std::forward<Arguments>(arguments)...);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
+			return result;
+
+		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Or &or_, Arguments &&... arguments)
+	{
+		bool someTrue = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : or_.arguments)
+		{
+			const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
+
+			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;
+	}
+
+	template <class... Arguments>
+	static EvaluationResult visit(const ast::Predicate &predicate, Arguments &&... arguments)
+	{
+		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, std::forward<Arguments>(arguments)...);
+
+			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
+				return EvaluationResult::Error;
+		}
+
+		return EvaluationResult::Unknown;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
+EvaluationResult evaluate(const ast::Formula &formula, Arguments &&... arguments)
+{
+	return formula.accept(EvaluateFormulaVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#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, Context &context, size_t &headVariableIndex)
-	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, size_t &headVariableIndex)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -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.showStatementsUsed = true;
-			context.visiblePredicateSignatures.emplace();
+		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 &)
@@ -184,6 +185,84 @@ struct StatementVisitor
 		throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently");
 	}
 
+	void visit(const Clingo::AST::External &external, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &context)
+	{
+		const auto fail =
+			[&]()
+			{
+				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())
+			fail();
+
+		if (!external.atom.data.is<Clingo::AST::Function>())
+			fail();
+
+		const auto &predicate = external.atom.data.get<Clingo::AST::Function>();
+
+		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>())
+			fail();
+
+		const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
+
+		if (aritySymbol.type() != Clingo::SymbolType::Number)
+			fail();
+
+		context.externalStatementsUsed = true;
+
+		const size_t arity = aritySymbol.number();
+
+		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
+		predicateDeclaration->isExternal = true;
+	}
+
 	template<class T>
 	void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
 	{

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:
+		case Clingo::AST::BinaryOperator::Power:
-			throw TranslationException(term.location, "“binary operation” terms currently unsupported");
+			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());
+				auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
-				// TODO: remove workaround
+
-				auto &functionRaw = function.get<ast::Function>();
+				auto function = ast::Function(functionDeclaration);
-				functionRaw.arguments.reserve(symbol.arguments().size());
+				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 &)
+	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
-	{
-		throw TranslationException(term.location, "“unary operation” terms currently unsupported");
-		return std::nullopt;
-	}
-
-	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
-		auto left = translate(binaryOperation.left, ruleContext, variableStack);
+		auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
-		auto right = translate(binaryOperation.right, ruleContext, 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);
+		const auto operator_ = translate(unaryOperation.unary_operator, term);
-		auto right = translate(interval.right, ruleContext, variableStack);
+		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,157 @@
+#ifndef __ANTHEM__TYPE_H
+#define __ANTHEM__TYPE_H
+
+#include <anthem/AST.h>
+#include <anthem/ASTUtils.h>
+#include <anthem/Utils.h>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Type
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
+Type type(const ast::Term &term, Arguments &&... 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
 {
 
@@ -20,6 +13,61 @@ namespace anthem
 constexpr const auto HeadVariablePrefix = "V";
 constexpr const auto BodyVariablePrefix = "X";
 constexpr const auto UserVariablePrefix = "U";
+constexpr const auto IntegerVariablePrefix = "N";
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class OperationResult
+{
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class EvaluationResult
+{
+	True,
+	False,
+	Unknown,
+	Error,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Domain
+{
+	Noninteger,
+	Integer,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class SetSize
+{
+	Empty,
+	Unit,
+	Multi,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Type
+{
+	Domain domain{Domain::Unknown};
+	SetSize setSize{SetSize::Unknown};
+};
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

include/anthem/output/AST.h

@@ -35,43 +35,46 @@ struct PrintContext
 	std::map<const VariableDeclaration *, size_t> userVariableIDs;
 	std::map<const VariableDeclaration *, size_t> headVariableIDs;
 	std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
+	std::map<const VariableDeclaration *, size_t> integerVariableIDs;
 
 	const Context &context;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-output::ColorStream &print(output::ColorStream &stream, const BinaryOperation::Operator operator_, 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);
+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);
+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);
+output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext);
+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);
+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);
+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);
+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);
+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);
+output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Variable &variable, PrintContext &printContext);
+output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext);
+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 And &and_, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Biconditional &biconditional, PrintContext &printContext);
+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);
+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);
+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);
+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);
+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);
+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 Formula &formula, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext);
+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 +88,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 +97,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 +126,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 +149,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 +168,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);
+	stream << function.declaration->name;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext)
-{
-	stream << function.name;
 
 	if (function.arguments.empty())
 		return stream;
@@ -183,7 +185,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 +195,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,23 +212,23 @@ 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 omitParentheses)
 {
-	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
 
 	print(stream, interval.from, printContext);
 	stream << "..";
 	print(stream, interval.to, printContext);
 
-	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << ")";
 
 	return stream;
@@ -234,9 +236,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 +260,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 +282,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,7 +321,7 @@ 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 printVariableDeclaration =
 		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
@@ -308,6 +340,9 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 			return (stream << output::Variable(variableName.c_str()));
 		};
 
+	if (variableDeclaration.domain == Domain::Integer)
+		return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
+
 	switch (variableDeclaration.type)
 	{
 		case VariableDeclaration::Type::UserDefined:
@@ -325,9 +360,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 +373,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 +424,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 +450,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 +483,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 +496,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 +510,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);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

lib/catch

@@ -1 +1 @@
-Subproject commit 0a34cc201ef28bf25c88b0062f331369596cb7b7
+Subproject commit d2d8455b571b6c66c4b7003500a77f9a93ecdc28

lib/clingo

@@ -1 +1 @@
-Subproject commit e2187b697f738f236828f7f780b5481c9a9284e6
+Subproject commit 969ce8f618c4cdf78d5c430ba827217075b88460

lib/cxxopts

@@ -1 +1 @@
-Subproject commit abe9ebd6b4084d576ceb79904c94ef8c9c0e6c56
+Subproject commit ca6e9f70eb6b5fab44504daf57d92a9412ab301c

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,13 +35,41 @@ 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());
 
+		auto &freeVariables = scopedFormula.freeVariables;
+
 		// Each formula with the predicate as its consequent currently has its own copy of the predicate’s parameters
 		// These need to be linked to the new, unique set of parameters
+
+		// First, remove the free variables whose occurrences will be relinked, which is why they are no longer needed
+		const auto isFreeVariableUnneeded =
+			[&](const auto &freeVariable)
+			{
+				const auto matchesVariableToBeReplaced = std::find_if(otherPredicate.arguments.cbegin(), otherPredicate.arguments.cend(),
+					[&](const ast::Term &argument)
+					{
+						assert(argument.is<ast::Variable>());
+						const auto &otherVariable = argument.get<ast::Variable>();
+
+						return (freeVariable.get() == otherVariable.declaration);
+					});
+
+				return (matchesVariableToBeReplaced != otherPredicate.arguments.cend());
+			};
+
+		freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isFreeVariableUnneeded), freeVariables.end());
+
+		// Currently, only rules with singleton heads are supported
+		// Rules with multiple elements in the head are not yet handled correctly by the head variable detection mechanism
+		for (const auto &freeVariable : freeVariables)
+			if (freeVariable->type == ast::VariableDeclaration::Type::Head)
+				throw CompletionException("cannot perform completion, only singleton rule heads supported currently");
+
+		// Second, link all occurrences of the deleted free variable to the new, unique parameter
 		for (size_t i = 0; i < parameters.size(); i++)
 		{
 			assert(otherPredicate.arguments[i].is<ast::Variable>());
@@ -50,16 +78,6 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 			scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
 		}
 
-		// Remove all the head variables, because they are not free variables after completion
-		const auto isHeadVariable =
-			[](const auto &variableDeclaration)
-			{
-				return variableDeclaration->type == ast::VariableDeclaration::Type::Head;
-			};
-
-		auto &freeVariables = scopedFormula.freeVariables;
-		freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end());
-
 		if (freeVariables.empty())
 			disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
 		else
@@ -100,22 +118,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,28 +179,27 @@ 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;
+	std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
-
-	// Get a list of all predicates
-	for (const auto &scopedFormula : scopedFormulas)
-		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
-
-	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
 		[](const auto &lhs, const auto &rhs)
 		{
-			const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str());
+			const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
 
 			if (order != 0)
 				return (order < 0);
 
-			return lhs.arity < rhs.arity;
+			return lhs->arity() < rhs->arity();
 		});
 
 	std::vector<ast::Formula> completedFormulas;
 
 	// Complete predicates
-	for (const auto &predicateSignature : predicateSignatures)
+	for (auto &predicateDeclaration : context.predicateDeclarations)
-		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
+	{
+		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
+			continue;
+
+		completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
+	}
 
 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)
@@ -202,7 +219,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,78 +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
+	// TODO: get rid of index-wise matching of completed formulas and predicate declarations
-	for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
+	size_t i = -1;
-	{
-		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 <<"”";
-	}
 
 	// Replace all occurrences of hidden predicates
-	for (size_t i = 0; i < predicateSignatures.size(); i++)
+	for (auto &predicateDeclaration : context.predicateDeclarations)
 	{
-		auto &predicateSignature = predicateSignatures[i];
+		// Check that the predicate is used and not declared #external
-
+		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-		const auto matchesVisiblePredicateSignature =
-			[&](const auto &visiblePredicateSignature)
-			{
-				return ast::matches(predicateSignature, visiblePredicateSignature);
-			};
-
-		const auto matchingPredicateSignature =
-			std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
-
-		// If the predicate ought to be visible, don’t eliminate it
-		if (matchingPredicateSignature != visiblePredicateSignatures.cend())
 			continue;
 
-		context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "”";
+		i++;
+
+		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;
+
+		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,332 @@
+#include <anthem/IntegerVariableDetection.h>
+
+#include <anthem/ASTCopy.h>
+#include <anthem/ASTUtils.h>
+#include <anthem/ASTVisitors.h>
+#include <anthem/Evaluation.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)
+{
+	return evaluate<VariableDomainMap>(formula, 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)”
+template<class SimplificationRule>
-// The exists statement has to be of the form “exists <variables> <conjunction>”
+OperationResult simplify(ast::Formula &formula)
-void simplify(ast::Exists &exists, ast::Formula &formula)
 {
-	// Simplify formulas like “exists X (X = Y)” to “#true”
+	return SimplificationRule::apply(formula);
-	// TODO: check that this covers all cases
+}
-	if (exists.argument.is<ast::Comparison>())
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+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())
+		if (matchingAssignment == exists.variables.cend())
-			formula = ast::Formula::make<ast::Boolean>(true);
+			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>();
+struct SimplificationRuleAssignmentInExists
-	auto &arguments = conjunction.arguments;
+{
+	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)”
+	static OperationResult apply(ast::Formula &formula)
-	for (auto i = exists.variables.begin(); i != exists.variables.end();)
 	{
-		const auto &variableDeclaration = **i;
+		if (!formula.is<ast::Exists>())
+			return OperationResult::Unchanged;
 
-		bool wasVariableReplaced = false;
+		auto &exists = formula.get<ast::Exists>();
 
-		// TODO: refactor
+		if (!exists.argument.is<ast::And>())
-		for (auto j = arguments.begin(); j != arguments.end(); j++)
+			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;
+			const auto &variableDeclaration = **i;
-			// Find term that is equivalent to the given variable
-			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
 
-			if (!assignedTerm)
+			bool wasVariableReplaced = false;
-				continue;
 
-			// Replace all occurrences of the variable with the equivalent term
+			// TODO: refactor
-			for (auto k = arguments.begin(); k != arguments.end(); k++)
+			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;
+				// Replace all occurrences of the variable with the equivalent term
-				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				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);
+			if (wasVariableReplaced)
-			wasVariableReplaced = true;
+			{
-			break;
+				i = exists.variables.erase(i);
+				continue;
+			}
+
+			i++;
 		}
 
-		if (wasVariableReplaced)
+		return simplificationResult;
-		{
-			i = exists.variables.erase(i);
-			continue;
-		}
-
-		i++;
 	}
+};
 
-	// 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
+struct SimplificationRuleOneElementConjunction
-	if (!exists.variables.empty())
+{
-		return;
+	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
+		auto &and_ = formula.get<ast::And>();
-	formula = std::move(exists.argument);
+
-}
+		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 OperationResult accept(ast::Formula &formula)
-	static void accept(T &, ast::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,9 +68,12 @@ 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.externalStatementsUsed)
+			context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
+
 		for (const auto &scopedFormula : scopedFormulas)
 		{
 			ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
@@ -82,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)
@@ -94,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

@@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		anthem::translate("input", input, context);
 
 		CHECK(output.str() ==
-			"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in 1..5))\n");
+			"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in (1..5)))\n");
 	}
 
 	SECTION("useless implications")
@@ -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 V2, V3 (in(V2, V3) -> (V2 in (1..n) and V3 in (1..r)))\n"
-			"forall U2 not (U2 in 1..n and not covered(U2))\n"
+			"forall U2 (U2 in (1..n) -> 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 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");
 	}
 
@@ -149,7 +150,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 
 		// TODO: simplify further
 		CHECK(output.str() ==
-			"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n");
+			"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in (1..4)))\n");
 	}
 
 	SECTION("simple propositions are hidden correctly")
@@ -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"
+			"(s -> not #false)\n"
-			"(t <-> (not #false and t))\n"
+			"(t -> not #false)\n"
-			"not (s and not t)\n"
+			"(s -> t)\n"
-			"not (not #false and not #false and #false)\n");
+			"(#false or #false or not #false)\n");
 	}
 
 	SECTION("predicate with more than one argument is hidden correctly")

tests/TestIntegerDetection.cpp

@@ -0,0 +1,117 @@
+#include <catch.hpp>
+
+#include <sstream>
+
+#include <anthem/AST.h>
+#include <anthem/Context.h>
+#include <anthem/Translation.h>
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+TEST_CASE("[integer detection] Integer variables are correctly detected", "[integer detection]")
+{
+	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;
+	context.performIntegerDetection = true;
+
+	SECTION("simple-to-detect integer parameter")
+	{
+		input << "p(X) :- X = 1..5.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in (1..5))\n"
+			"int(p/1@1)\n");
+	}
+
+	SECTION("simple noninteger parameter")
+	{
+		input <<
+			"p(X) :- X = 1..5.\n"
+			"p(X) :- X = error.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall V1 (p(V1) <-> (V1 in (1..5) or V1 = error))\n");
+	}
+	
+	SECTION("integer parameter with arithmetics")
+	{
+		input << "p(X) :- X = (2 + (1..5)) * 2.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in ((2 + (1..5)) * 2))\n"
+			"int(p/1@1)\n");
+	}
+	
+	SECTION("integer parameter with arithmetics depending on another integer parameter")
+	{
+		input
+			<< "p(X) :- X = 1..5."
+			<< "q(X) :- p(Y), X = (Y + 5) / 3.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in (1..5))\n"
+			"forall N2 (q(N2) <-> exists N3 (p(N3) and N2 in ((N3 + 5) / 3)))\n"
+			"int(p/1@1)\n"
+			"int(q/1@1)\n");
+	}
+
+	SECTION("multiple mixed parameters")
+	{
+		input
+			<< "p(X) :- X = 1..5."
+			<< "q(X) :- X = error."
+			<< "r(A, B, C) :- p(X), A = X ** 2, q(B), p(C).";
+		anthem::translate("input", input, context);
+		
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in (1..5))\n"
+			"forall V1 (q(V1) <-> V1 = error)\n"
+			"forall N2, V2, N3 (r(N2, V2, N3) <-> exists N4 (p(N4) and N2 = (N4 ** 2) and q(V2) and p(N3)))\n"
+			"int(p/1@1)\n"
+			"int(r/3@1)\n"
+			"int(r/3@3)\n");
+	}
+	
+	SECTION("integer parameter despite usage of constant symbol")
+	{
+		input
+			<< "p(X) :- X = 2..n.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in (2..n))\n"
+			"int(p/1@1)\n");
+	}
+	
+	SECTION("integer arithmetics are correctly simplified for operators other than division")
+	{
+		input
+			<< "p(X) :- X = 5 + 9 ** 2.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 = (5 + (9 ** 2)))\n"
+			"int(p/1@1)\n");
+	}
+	
+	SECTION("integer arithmetics are not simplified with the division operator")
+	{
+		input
+			<< "p(X) :- X = 5 + 9 / 0.";
+		anthem::translate("input", input, context);
+	
+		CHECK(output.str() ==
+			"forall N1 (p(N1) <-> N1 in (5 + (9 / 0)))\n"
+			"int(p/1@1)\n");
+	}
+}

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/TestSimplification.cpp

@@ -40,7 +40,7 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
 		input << ":- not covered(I), I = 1..n.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((not covered(U1) and U1 in 1..n) -> #false)\n");
+		CHECK(output.str() == "((not covered(U1) and U1 in (1..n)) -> #false)\n");
 	}
 
 	SECTION("comparisons")
@@ -50,4 +50,34 @@ TEST_CASE("[simplification] Rules are simplified correctly", "[simplification]")
 
 		CHECK(output.str() == "(U1 > U2 -> #false)\n");
 	}
+
+	SECTION("biconditionals are replaced with implifactions with choice rules")
+	{
+		context.performCompletion = true;
+
+		input << "{p(a)}.";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "forall V1 (p(V1) -> V1 = a)\n");
+	}
+
+	SECTION("biconditionals are replaced with implifactions with complicated choice rules")
+	{
+		context.performCompletion = true;
+
+		input << "{p(n + 5)}.";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "forall V1 (p(V1) -> V1 in (n + 5))\n");
+	}
+
+	SECTION("biconditionals are not replaced with implifactions with nonchoice rules")
+	{
+		context.performCompletion = true;
+
+		input << "p(a).";
+		anthem::translate("input", input, context);
+
+		CHECK(output.str() == "forall V1 (p(V1) <-> V1 = a)\n");
+	}
 }

tests/TestTranslation.cpp

@@ -24,7 +24,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(1..5).";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "(V1 in 1..5 -> p(V1))\n");
+		CHECK(output.str() == "(V1 in (1..5) -> p(V1))\n");
 	}
 
 	SECTION("simple example 2")
@@ -32,7 +32,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(N) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1))\n");
+		CHECK(output.str() == "((V1 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1))\n");
 	}
 
 	SECTION("simple example 3")
@@ -48,7 +48,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> p(V1, V2, V3))\n");
+		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> p(V1, V2, V3))\n");
 	}
 
 	SECTION("disjunctive head")
@@ -57,7 +57,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q(3, N); p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
+		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
 	}
 
 	SECTION("disjunctive head (alternative syntax)")
@@ -66,7 +66,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "q(3, N), p(N, 1, 2) :- N = 1..5.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in 1..5 and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
+		CHECK(output.str() == "((V1 in U1 and V2 in 1 and V3 in 2 and V4 in 3 and V5 in U1 and exists X1, X2 (X1 in U1 and X2 in (1..5) and X1 = X2)) -> (p(V1, V2, V3) or q(V4, V5)))\n");
 	}
 
 	SECTION("escaping conflicting variable names")
@@ -98,7 +98,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":- not p(I), I = 1..n.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in 1..n and X2 = X3)) -> #false)\n");
+		CHECK(output.str() == "((exists X1 (X1 in U1 and not p(X1)) and exists X2, X3 (X2 in U1 and X3 in (1..n) and X2 = X3)) -> #false)\n");
 	}
 
 	SECTION("disjunctive fact (no arguments)")
@@ -178,7 +178,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "p(X, 1..10) :- q(X, 6..12).";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((V1 in U1 and V2 in 1..10 and exists X1, X2 (X1 in U1 and X2 in 6..12 and q(X1, X2))) -> p(V1, V2))\n");
+		CHECK(output.str() == "((V1 in U1 and V2 in (1..10) and exists X1, X2 (X1 in U1 and X2 in (6..12) and q(X1, X2))) -> p(V1, V2))\n");
 	}
 
 	SECTION("intervals with variable")
@@ -186,7 +186,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":- q(N), 1 = 1..N.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in 1..U1 and X2 = X3)) -> #false)\n");
+		CHECK(output.str() == "((exists X1 (X1 in U1 and q(X1)) and exists X2, X3 (X2 in 1 and X3 in (1..U1) and X2 = X3)) -> #false)\n");
 	}
 
 	SECTION("intervals with two variables")
@@ -194,7 +194,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << ":- q(M, N), M = 1..N.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in 1..U2 and X3 = X4)) -> #false)\n");
+		CHECK(output.str() == "((exists X1, X2 (X1 in U1 and X2 in U2 and q(X1, X2)) and exists X3, X4 (X3 in U1 and X4 in (1..U2) and X3 = X4)) -> #false)\n");
 	}
 
 	SECTION("comparisons")
@@ -262,7 +262,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		anthem::translate("input", input, context);
 
 		// TODO: eliminate V5: not needed
-		CHECK(output.str() == "((V1 in 1..3 and V2 in U1 and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V4 in 1..3 and V5 in U2 and V6 in 2..4 and q(V6)) -> q(V6))\n");
+		CHECK(output.str() == "((V1 in (1..3) and V2 in U1 and V3 in (2..4) and p(V1, V2)) -> p(V1, V2))\n((V4 in (1..3) and V5 in U2 and V6 in (2..4) and q(V6)) -> q(V6))\n");
 	}
 
 	SECTION("choice rule with body")
@@ -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");
+	}
 }

tests/TestUnsupported.cpp

@@ -0,0 +1,73 @@
+#include <catch.hpp>
+
+#include <sstream>
+
+#include <anthem/AST.h>
+#include <anthem/Context.h>
+#include <anthem/Translation.h>
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+TEST_CASE("[unsupported] Errors are correctly issued when using unsupported features", "[unsupported]")
+{
+	std::stringstream input;
+	std::stringstream output;
+	std::stringstream errors;
+
+	anthem::output::Logger logger(output, errors);
+	anthem::Context context(std::move(logger));
+
+	SECTION("rules with disjunctive head are unsupported")
+	{
+		context.performCompletion = true;
+
+		input << "a; b.";
+
+		CHECK_THROWS(anthem::translate("input", input, context));
+	}
+
+	SECTION("rules with disjunctive head containing elements with arguments are unsupported")
+	{
+		context.performCompletion = true;
+
+		input << "p(a); p(b).";
+
+		CHECK_THROWS(anthem::translate("input", input, context));
+	}
+
+	SECTION("singleton choice rules are supported")
+	{
+		context.performCompletion = true;
+
+		input << "{a}.";
+
+		CHECK_NOTHROW(anthem::translate("input", input, context));
+	}
+
+	SECTION("singleton choice rules containing an element with arguments are supported")
+	{
+		context.performCompletion = true;
+
+		input << "{p(a)}.";
+
+		CHECK_NOTHROW(anthem::translate("input", input, context));
+	}
+
+	SECTION("choice rules with multiple simple elements are supported")
+	{
+		context.performCompletion = true;
+
+		input << "{a; b}.";
+
+		CHECK_NOTHROW(anthem::translate("input", input, context));
+	}
+
+	SECTION("choice rules with multiple elements with arguments are unsupported")
+	{
+		context.performCompletion = true;
+
+		input << "{p(a); p(b)}.";
+
+		CHECK_THROWS(anthem::translate("input", input, context));
+	}
+}