Version bump for release 0.1.8 RC 3

CHANGELOG.md

@@ -1,15 +1,6 @@
 # Change Log
 
-## 0.1.9 RC 2 (2018-04-21)
-
-### Features
-
-* optional detection of integer variables and integer predicate parameters
-* command-line option `--detect-integers` to enable integer variable detection
-* support for declaring functions integer with the `#external` directive
-* new simplification rule applying to integer variables
-
-## 0.1.8 (2018-04-20)
+## 0.1.8 RC 3 (2018-04-12)
 
 ### Features
 

app/main.cpp

@@ -18,7 +18,6 @@ int main(int argc, char **argv)
 		("i,input", "Input files", cxxopts::value<std::vector<std::string>>())
 		("s,simplify", "Simplify the output")
 		("c,complete", "Perform completion")
-		("d,detect-integers", "Detect integer variables")
 		("color", "Colorize output (always, never, auto)", cxxopts::value<std::string>()->default_value("auto"))
 		("parentheses", "Parenthesis style (normal, full)", cxxopts::value<std::string>()->default_value("normal"))
 		("p,log-priority", "Log messages starting from this priority (debug, info, warning, error)", cxxopts::value<std::string>()->default_value("info"));
@@ -51,7 +50,6 @@ int main(int argc, char **argv)
 
 		context.performSimplification = (parseResult.count("simplify") > 0);
 		context.performCompletion = (parseResult.count("complete") > 0);
-		context.performIntegerDetection = (parseResult.count("detect-integers") > 0);
 		colorPolicyString = parseResult["color"].as<std::string>();
 		parenthesisStyleString = parseResult["parentheses"].as<std::string>();
 		logPriorityString = parseResult["log-priority"].as<std::string>();
@@ -72,7 +70,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.9-rc.2" << std::endl;
+		std::cout << "anthem version 0.1.8-rc.3" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/permutations.lp

@@ -1,6 +1,3 @@
-#show p/2.
-#external integer(n(0)).
-
 {p(1..n, 1..n)}.
 
 :- p(X, Y1), p(X, Y2), Y1 != Y2.
@@ -11,3 +8,5 @@ q2(Y) :- p(_, Y).
 
 :- not q1(X), X = 1..n.
 :- not q2(Y), Y = 1..n.
+
+#show p/2.

examples/prime.lp

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

examples/schur-numbers.lp

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

include/anthem/AST.h

@@ -2,7 +2,6 @@
 #define __ANTHEM__AST_H
 
 #include <anthem/ASTForward.h>
-#include <anthem/Domain.h>
 
 namespace anthem
 {
@@ -104,15 +103,32 @@ struct Comparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct Function
+struct Constant
 {
-	explicit Function(FunctionDeclaration *declaration)
-	:	declaration{declaration}
+	explicit Constant(std::string &&name)
+	:	name{std::move(name)}
 	{
 	}
 
-	explicit Function(FunctionDeclaration *declaration, std::vector<Term> &&arguments)
-	:	declaration{declaration},
+	Constant(const Constant &other) = delete;
+	Constant &operator=(const Constant &other) = delete;
+	Constant(Constant &&other) = default;
+	Constant &operator=(Constant &&other) = default;
+
+	std::string name;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Function
+{
+	explicit Function(std::string &&name)
+	:	name{std::move(name)}
+	{
+	}
+
+	explicit Function(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -122,33 +138,8 @@ struct Function
 	Function(Function &&other) noexcept = default;
 	Function &operator=(Function &&other) noexcept = default;
 
-	FunctionDeclaration *declaration;
-	std::vector<Term> arguments;
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct FunctionDeclaration
-{
-	explicit FunctionDeclaration(std::string &&name)
-	:	name{std::move(name)}
-	{
-	}
-
-	explicit FunctionDeclaration(std::string &&name, size_t arity)
-	:	name{std::move(name)},
-		arity{arity}
-	{
-	}
-
-	FunctionDeclaration(const FunctionDeclaration &other) = delete;
-	FunctionDeclaration &operator=(const FunctionDeclaration &other) = delete;
-	FunctionDeclaration(FunctionDeclaration &&other) noexcept = default;
-	FunctionDeclaration &operator=(FunctionDeclaration &&other) noexcept = default;
-
 	std::string name;
-	size_t arity;
-	Domain domain{Domain::General};
+	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -213,13 +204,13 @@ struct Interval
 
 struct Predicate
 {
-	explicit Predicate(PredicateDeclaration *declaration)
-	:	declaration{declaration}
+	explicit Predicate(std::string &&name)
+	:	name{std::move(name)}
 	{
 	}
 
-	explicit Predicate(PredicateDeclaration *declaration, std::vector<Term> &&arguments)
-	:	declaration{declaration},
+	explicit Predicate(std::string &&name, std::vector<Term> &&arguments)
+	:	name{std::move(name)},
 		arguments{std::move(arguments)}
 	{
 	}
@@ -229,47 +220,35 @@ struct Predicate
 	Predicate(Predicate &&other) noexcept = default;
 	Predicate &operator=(Predicate &&other) noexcept = default;
 
-	PredicateDeclaration *declaration{nullptr};
+	std::size_t arity() const
+	{
+		return arguments.size();
+	}
+
+	std::string name;
 	std::vector<Term> arguments;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct PredicateDeclaration
+// TODO: make more use of this class
+struct PredicateSignature
 {
-	enum class Visibility
-	{
-		Default,
-		Visible,
-		Hidden
-	};
-
-	struct Parameter
-	{
-		Domain domain{Domain::Unknown};
-	};
-
-	explicit PredicateDeclaration(std::string &&name, size_t arity)
+	explicit PredicateSignature(std::string &&name, size_t arity)
 	:	name{std::move(name)},
-		parameters{std::vector<Parameter>(arity)}
+		arity{arity}
 	{
 	}
 
-	PredicateDeclaration(const PredicateDeclaration &other) = delete;
-	PredicateDeclaration &operator=(const PredicateDeclaration &other) = delete;
-	PredicateDeclaration(PredicateDeclaration &&other) noexcept = default;
-	PredicateDeclaration &operator=(PredicateDeclaration &&other) noexcept = default;
-
-	size_t arity() const noexcept
-	{
-		return parameters.size();
-	}
+	PredicateSignature(const PredicateSignature &other) = delete;
+	PredicateSignature &operator=(const PredicateSignature &other) = delete;
+	// TODO: make noexcept again
+	// GCC versions before 7 don’t declare moving std::string noexcept and would complain here
+	PredicateSignature(PredicateSignature &&other) = default;
+	PredicateSignature &operator=(PredicateSignature &&other) = default;
 
 	std::string name;
-	std::vector<Parameter> parameters;
-	bool isUsed{false};
-	bool isExternal{false};
-	Visibility visibility{Visibility::Default};
+	size_t arity;
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -381,7 +360,6 @@ struct VariableDeclaration
 	VariableDeclaration &operator=(VariableDeclaration &&other) = default;
 
 	Type type;
-	Domain domain{Domain::Unknown};
 	std::string name;
 };
 

include/anthem/ASTCopy.h

@@ -22,6 +22,7 @@ namespace ast
 BinaryOperation prepareCopy(const BinaryOperation &other);
 Boolean prepareCopy(const Boolean &other);
 Comparison prepareCopy(const Comparison &other);
+Constant prepareCopy(const Constant &other);
 Function prepareCopy(const Function &other);
 In prepareCopy(const In &other);
 Integer prepareCopy(const Integer &other);

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,7 +35,6 @@ struct Interval;
 struct Not;
 struct Or;
 struct Predicate;
-struct PredicateDeclaration;
 struct SpecialInteger;
 struct String;
 struct UnaryOperation;
@@ -64,6 +63,7 @@ using Formula = Clingo::Variant<
 using Term = Clingo::Variant<
 	BinaryOperation,
 	Boolean,
+	Constant,
 	Function,
 	Integer,
 	Interval,

include/anthem/ASTUtils.h

@@ -36,6 +36,12 @@ class VariableStack
 		std::vector<Layer> m_layers;
 };
 
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &lhs, const Predicate &rhs);
+bool matches(const Predicate &predicate, const PredicateSignature &signature);
+bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Replacing Variables

include/anthem/ASTVisitors.h

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

include/anthem/Arithmetics.h

@@ -1,262 +0,0 @@
-#ifndef __ANTHEM__ARITHMETICS_H
-#define __ANTHEM__ARITHMETICS_H
-
-#include <anthem/Utils.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Arithmetics
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DefaultVariableDomainAccessor
-{
-	ast::Domain operator()(const ast::Variable &variable)
-	{
-		return variable.declaration->domain;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
-EvaluationResult isArithmetic(const ast::Term &term, Arguments &&...);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
-struct IsTermArithmeticVisitor
-{
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, Arguments &&... arguments)
-	{
-		const auto isLeftArithemtic = isArithmetic<VariableDomainAccessor>(binaryOperation.left, std::forward<Arguments>(arguments)...);
-		const auto isRightArithmetic = isArithmetic<VariableDomainAccessor>(binaryOperation.right, std::forward<Arguments>(arguments)...);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Boolean &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Function &function, Arguments &&...)
-	{
-		switch (function.declaration->domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Integer &, Arguments &&...)
-	{
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Interval &interval, Arguments &&... arguments)
-	{
-		const auto isFromArithmetic = isArithmetic<VariableDomainAccessor>(interval.from, std::forward<Arguments>(arguments)...);
-		const auto isToArithmetic = isArithmetic<VariableDomainAccessor>(interval.to, std::forward<Arguments>(arguments)...);
-
-		if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::SpecialInteger &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::String &, Arguments &&...)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, Arguments &&... arguments)
-	{
-		const auto isArgumentArithmetic = isArithmetic<VariableDomainAccessor>(unaryOperation.argument, std::forward<Arguments>(arguments)...);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Variable &variable, Arguments &&... arguments)
-	{
-		const auto domain = VariableDomainAccessor()(variable, std::forward<Arguments>(arguments)...);
-
-		switch (domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor, class... Arguments>
-EvaluationResult isArithmetic(const ast::Term &term, Arguments &&... arguments)
-{
-	return term.accept(IsTermArithmeticVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isInteger(const ast::Term &term);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct IsTermIntegerVisitor
-{
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation)
-	{
-		const auto isLeftArithemtic = isArithmetic(binaryOperation.left);
-		const auto isRightArithmetic = isArithmetic(binaryOperation.right);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (binaryOperation.operator_ == ast::BinaryOperation::Operator::Division)
-			return EvaluationResult::False;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Boolean &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Function &function)
-	{
-		switch (function.declaration->domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Integer &)
-	{
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Interval &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::SpecialInteger &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::String &)
-	{
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation)
-	{
-		const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Variable &variable)
-	{
-		switch (variable.declaration->domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-inline EvaluationResult isInteger(const ast::Term &term)
-{
-	return term.accept(IsTermIntegerVisitor());
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif

include/anthem/Body.h

@@ -43,22 +43,19 @@ ast::Comparison::Operator translate(Clingo::AST::ComparisonOperator comparisonOp
 struct BodyTermTranslateVisitor
 {
 	// TODO: refactor
-	std::optional<ast::Formula> visit(const Clingo::AST::Function &function,
-		const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext,
-		Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (literal.sign == Clingo::AST::Sign::DoubleNegation)
 			throw TranslationException(literal.location, "double-negated literals currently unsupported");
 
-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(function.name, function.arguments.size());
-		predicateDeclaration->isUsed = true;
-
 		if (function.arguments.empty())
 		{
+			auto predicate = ast::Formula::make<ast::Predicate>(std::string(function.name));
+
 			if (literal.sign == Clingo::AST::Sign::None)
-				return ast::Predicate(predicateDeclaration);
+				return std::move(predicate);
 			else if (literal.sign == Clingo::AST::Sign::Negation)
-				return ast::Formula::make<ast::Not>(ast::Predicate(predicateDeclaration));
+				return ast::Formula::make<ast::Not>(std::move(predicate));
 		}
 
 		// Create new body variable declarations
@@ -76,12 +73,12 @@ struct BodyTermTranslateVisitor
 		for (size_t i = 0; i < function.arguments.size(); i++)
 		{
 			auto &argument = function.arguments[i];
-			conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, context, variableStack)));
+			conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[i].get()), translate(argument, ruleContext, variableStack)));
 		}
 
 		variableStack.pop();
 
-		ast::Predicate predicate(predicateDeclaration);
+		ast::Predicate predicate(std::string(function.name));
 		predicate.arguments.reserve(function.arguments.size());
 
 		for (size_t i = 0; i < function.arguments.size(); i++)
@@ -96,8 +93,7 @@ struct BodyTermTranslateVisitor
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &,
-		const Clingo::AST::Term &term, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, RuleContext &, ast::VariableStack &)
 	{
 		assert(!term.data.is<Clingo::AST::Function>());
 
@@ -110,18 +106,18 @@ struct BodyTermTranslateVisitor
 
 struct BodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, RuleContext &, ast::VariableStack &)
 	{
 		return ast::Formula::make<ast::Boolean>(boolean.value);
 	}
 
-	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
-		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, context, variableStack);
+		return term.data.accept(BodyTermTranslateVisitor(), literal, term, ruleContext, variableStack);
 	}
 
 	// TODO: refactor
-	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
 		if (literal.sign != Clingo::AST::Sign::None)
@@ -136,15 +132,15 @@ struct BodyLiteralTranslateVisitor
 
 		ast::And conjunction;
 		conjunction.arguments.reserve(3);
-		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, context, variableStack)));
-		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, context, variableStack)));
+		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[0].get()), translate(comparison.left, ruleContext, variableStack)));
+		conjunction.arguments.emplace_back(ast::Formula::make<ast::In>(ast::Variable(parameters[1].get()), translate(comparison.right, ruleContext, variableStack)));
 		conjunction.arguments.emplace_back(ast::Formula::make<ast::Comparison>(operator_, ast::Variable(parameters[0].get()), ast::Variable(parameters[1].get())));
 
 		return ast::Formula::make<ast::Exists>(std::move(parameters), std::move(conjunction));
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(literal.location, "literal currently unsupported in this context, expected function or term");
 		return std::nullopt;
@@ -155,16 +151,16 @@ struct BodyLiteralTranslateVisitor
 
 struct BodyBodyLiteralTranslateVisitor
 {
-	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, Context &context, ast::VariableStack &variableStack)
+	std::optional<ast::Formula> visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &ruleContext, ast::VariableStack &variableStack)
 	{
 		if (bodyLiteral.sign != Clingo::AST::Sign::None)
 			throw TranslationException(bodyLiteral.location, "only positive body literals supported currently");
 
-		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, context, variableStack);
+		return literal.data.accept(BodyLiteralTranslateVisitor(), literal, ruleContext, variableStack);
 	}
 
 	template<class T>
-	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, Context &, ast::VariableStack &)
+	std::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, RuleContext &, ast::VariableStack &)
 	{
 		throw TranslationException(bodyLiteral.location, "body literal currently unsupported in this context, expected literal");
 		return std::nullopt;

include/anthem/Context.h

@@ -16,9 +16,9 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct PredicateDeclarationMeta
+struct PredicateSignatureMeta
 {
-	ast::PredicateDeclaration *declaration;
+	ast::PredicateSignature predicateSignature;
 	bool used{false};
 };
 
@@ -33,59 +33,13 @@ struct Context
 	{
 	}
 
-	ast::PredicateDeclaration *findOrCreatePredicateDeclaration(const char *name, size_t arity)
-	{
-		const auto matchesExistingPredicateDeclaration =
-			[&](const auto &predicateDeclaration)
-			{
-				return (predicateDeclaration->arity() == arity
-					&& strcmp(predicateDeclaration->name.c_str(), name) == 0);
-			};
-
-		auto matchingPredicateDeclaration = std::find_if(predicateDeclarations.begin(),
-			predicateDeclarations.end(), matchesExistingPredicateDeclaration);
-
-		if (matchingPredicateDeclaration != predicateDeclarations.end())
-			return matchingPredicateDeclaration->get();
-
-		predicateDeclarations.emplace_back(std::make_unique<ast::PredicateDeclaration>(name, arity));
-
-		return predicateDeclarations.back().get();
-	}
-
-	ast::FunctionDeclaration *findOrCreateFunctionDeclaration(const char *name, size_t arity)
-	{
-		const auto matchesExistingFunctionDeclaration =
-			[&](const auto &functionDeclarations)
-			{
-				return (functionDeclarations->arity == arity
-					&& strcmp(functionDeclarations->name.c_str(), name) == 0);
-			};
-
-		auto matchingFunctionDeclaration = std::find_if(functionDeclarations.begin(),
-			functionDeclarations.end(), matchesExistingFunctionDeclaration);
-
-		if (matchingFunctionDeclaration != functionDeclarations.end())
-			return matchingFunctionDeclaration->get();
-
-		functionDeclarations.emplace_back(std::make_unique<ast::FunctionDeclaration>(name, arity));
-
-		return functionDeclarations.back().get();
-	}
-
 	output::Logger logger;
 
-	bool performSimplification{false};
-	bool performCompletion{false};
-	bool performIntegerDetection{false};
+	bool performSimplification = false;
+	bool performCompletion = false;
 
-	std::vector<std::unique_ptr<ast::PredicateDeclaration>> predicateDeclarations;
-	ast::PredicateDeclaration::Visibility defaultPredicateVisibility{ast::PredicateDeclaration::Visibility::Visible};
-
-	std::vector<std::unique_ptr<ast::FunctionDeclaration>> functionDeclarations;
-
-	bool externalStatementsUsed{false};
-	bool showStatementsUsed{false};
+	std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
+	std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
 
 	ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
 };

include/anthem/Domain.h

@@ -1,27 +0,0 @@
-#ifndef __ANTHEM__DOMAIN_H
-#define __ANTHEM__DOMAIN_H
-
-namespace anthem
-{
-namespace ast
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Domain
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class Domain
-{
-	General,
-	Integer,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-}
-
-#endif

include/anthem/Equality.h

@@ -3,7 +3,6 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
-#include <anthem/Utils.h>
 
 namespace anthem
 {
@@ -16,6 +15,16 @@ namespace ast
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+// TODO: move to separate class
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 Tristate equal(const Formula &lhs, const Formula &rhs);
 Tristate equal(const Term &lhs, const Term &rhs);
 
@@ -228,7 +237,7 @@ struct FormulaEqualityVisitor
 
 		const auto &otherPredicate = otherFormula.get<Predicate>();
 
-		if (predicate.declaration != otherPredicate.declaration)
+		if (!matches(predicate, otherPredicate))
 			return Tristate::False;
 
 		assert(predicate.arguments.size() == otherPredicate.arguments.size());
@@ -289,6 +298,18 @@ struct TermEqualityVisitor
 			: Tristate::False;
 	}
 
+	Tristate visit(const Constant &constant, const Term &otherTerm)
+	{
+		if (!otherTerm.is<Constant>())
+			return Tristate::Unknown;
+
+		const auto &otherConstant = otherTerm.get<Constant>();
+
+		return (constant.name == otherConstant.name)
+			? Tristate::True
+			: Tristate::False;
+	}
+
 	Tristate visit(const Function &function, const Term &otherTerm)
 	{
 		if (!otherTerm.is<Function>())
@@ -296,7 +317,7 @@ struct TermEqualityVisitor
 
 		const auto &otherFunction = otherTerm.get<Function>();
 
-		if (function.declaration != otherFunction.declaration)
+		if (function.name != otherFunction.name)
 			return Tristate::False;
 
 		if (function.arguments.size() != otherFunction.arguments.size())

include/anthem/Head.h

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

include/anthem/HiddenPredicateElimination.h

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

include/anthem/IntegerVariableDetection.h

@@ -1,22 +0,0 @@
-#ifndef __ANTHEM__INTEGER_VARIABLE_DETECTION_H
-#define __ANTHEM__INTEGER_VARIABLE_DETECTION_H
-
-#include <anthem/AST.h>
-#include <anthem/Context.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// IntegerVariableDetection
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif

include/anthem/Simplification.h

@@ -12,6 +12,14 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class SimplificationResult
+{
+	Simplified,
+	Unchanged,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void simplify(ast::Formula &formula);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/SimplificationVisitors.h

@@ -3,7 +3,6 @@
 
 #include <anthem/AST.h>
 #include <anthem/Simplification.h>
-#include <anthem/Utils.h>
 
 namespace anthem
 {
@@ -20,96 +19,96 @@ template<class T>
 struct FormulaSimplificationVisitor
 {
 	template <class... Arguments>
-	OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
-		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
+	SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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)
+	SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
 	{
-		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
+	SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
 	{
-		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
-		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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)
+	SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
 	{
-		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
+	SimplificationResult 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;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
 
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
+	SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
@@ -117,69 +116,75 @@ struct FormulaSimplificationVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template<class T, class OperationResult = void>
+template<class T, class SimplificationResult = void>
 struct TermSimplificationVisitor
 {
 	template <class... Arguments>
-	OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
+	SimplificationResult 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.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
-		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
+	SimplificationResult 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)
+	SimplificationResult visit(Constant &, Term &term, Arguments &&... arguments)
+	{
+		return T::accept(term, std::forward<Arguments>(arguments)...);
+	}
+
+	template <class... Arguments>
+	SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
 	{
 		for (auto &argument : function.arguments)
-			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-				return OperationResult::Changed;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+				return SimplificationResult::Simplified;
 
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
+	SimplificationResult 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)
+	SimplificationResult 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.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
-		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return OperationResult::Changed;
+		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+			return SimplificationResult::Simplified;
 
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
+	SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(String &, Term &term, Arguments &&... arguments)
+	SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
 
 	template <class... Arguments>
-	OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
+	SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

include/anthem/StatementVisitor.h

@@ -73,7 +73,7 @@ struct StatementVisitor
 
 		// Compute consequent
 		auto headVariableIndex = ruleContext.headVariablesStartIndex;
-		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, context, headVariableIndex);
+		auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
 
 		assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
 
@@ -87,7 +87,7 @@ struct StatementVisitor
 
 			const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
 			auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
-			auto set = translate(headTerm, ruleContext, context, variableStack);
+			auto set = translate(headTerm, ruleContext, variableStack);
 			auto in = ast::In(std::move(element), std::move(set));
 
 			antecedent.arguments.emplace_back(std::move(in));
@@ -98,7 +98,7 @@ struct StatementVisitor
 		{
 			const auto &bodyLiteral = *i;
 
-			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, context, variableStack);
+			auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
 
 			if (!argument)
 				throw TranslationException(bodyLiteral.location, "could not translate body literal");
@@ -165,8 +165,8 @@ struct StatementVisitor
 		if (signature.negative())
 			throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
 
-		context.showStatementsUsed = true;
-		context.defaultPredicateVisibility = ast::PredicateDeclaration::Visibility::Hidden;
+		if (!context.visiblePredicateSignatures)
+			context.visiblePredicateSignatures.emplace();
 
 		if (std::strlen(signature.name()) == 0)
 		{
@@ -176,8 +176,8 @@ struct StatementVisitor
 
 		context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
 
-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(signature.name(), signature.arity());
-		predicateDeclaration->visibility = ast::PredicateDeclaration::Visibility::Visible;
+		auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
+		context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}
 
 	void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
@@ -190,7 +190,7 @@ struct StatementVisitor
 		const auto fail =
 			[&]()
 			{
-				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” or “#external integer(<function name>(<arity>)).” supported");
+				throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>).” supported");
 			};
 
 		if (!external.body.empty())
@@ -204,47 +204,6 @@ struct StatementVisitor
 		if (predicate.arguments.size() != 1)
 			fail();
 
-		const auto handleIntegerDeclaration =
-			[&]()
-			{
-				// Integer function declarations are treated separately if applicable
-				if (strcmp(predicate.name, "integer") != 0)
-					return false;
-
-				if (predicate.arguments.size() != 1)
-					return false;
-
-				const auto &functionArgument = predicate.arguments.front();
-
-				if (!functionArgument.data.is<Clingo::AST::Function>())
-					return false;
-
-				const auto &function = functionArgument.data.get<Clingo::AST::Function>();
-
-				if (function.arguments.size() != 1)
-					return false;
-
-				const auto &arityArgument = function.arguments.front();
-
-				if (!arityArgument.data.is<Clingo::Symbol>())
-					return false;
-
-				const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
-
-				if (aritySymbol.type() != Clingo::SymbolType::Number)
-					return false;
-
-				const size_t arity = aritySymbol.number();
-
-				auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
-				functionDeclaration->domain = ast::Domain::Integer;
-
-				return true;
-			};
-
-		if (handleIntegerDeclaration())
-			return;
-
 		const auto &arityArgument = predicate.arguments.front();
 
 		if (!arityArgument.data.is<Clingo::Symbol>())
@@ -255,12 +214,13 @@ struct StatementVisitor
 		if (aritySymbol.type() != Clingo::SymbolType::Number)
 			fail();
 
-		context.externalStatementsUsed = true;
+		const size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
 
-		const size_t arity = aritySymbol.number();
+		if (!context.externalPredicateSignatures)
+			context.externalPredicateSignatures.emplace();
 
-		auto predicateDeclaration = context.findOrCreatePredicateDeclaration(predicate.name, arity);
-		predicateDeclaration->isExternal = true;
+		auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
+		context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
 	}
 
 	template<class T>

include/anthem/Term.h

@@ -65,13 +65,13 @@ ast::UnaryOperation::Operator translate(Clingo::AST::UnaryOperator unaryOperator
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack);
+ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct TermTranslateVisitor
 {
-	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		switch (symbol.type())
 		{
@@ -85,19 +85,19 @@ struct TermTranslateVisitor
 				return ast::Term::make<ast::String>(std::string(symbol.string()));
 			case Clingo::SymbolType::Function:
 			{
-				auto functionDeclaration = context.findOrCreateFunctionDeclaration(symbol.name(), symbol.arguments().size());
-
-				auto function = ast::Function(functionDeclaration);
-				function.arguments.reserve(symbol.arguments().size());
+				auto function = ast::Term::make<ast::Function>(symbol.name());
+				// TODO: remove workaround
+				auto &functionRaw = function.get<ast::Function>();
+				functionRaw.arguments.reserve(symbol.arguments().size());
 
 				for (const auto &argument : symbol.arguments())
 				{
-					auto translatedArgument = visit(argument, term, ruleContext, context, variableStack);
+					auto translatedArgument = visit(argument, term, ruleContext, variableStack);
 
 					if (!translatedArgument)
 						throw TranslationException(term.location, "could not translate argument");
 
-					function.arguments.emplace_back(std::move(translatedArgument.value()));
+					functionRaw.arguments.emplace_back(std::move(translatedArgument.value()));
 				}
 
 				return std::move(function);
@@ -107,7 +107,7 @@ struct TermTranslateVisitor
 		return std::nullopt;
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, Context &, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Variable &variable, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto matchingVariableDeclaration = variableStack.findUserVariableDeclaration(variable.name);
 		const auto isAnonymousVariable = (strcmp(variable.name, "_") == 0);
@@ -120,36 +120,35 @@ struct TermTranslateVisitor
 		auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::UserDefined, std::string(variable.name));
 		ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
 
-		// TODO: ast::Term::make is unnecessary and can be removed
 		return ast::Term::make<ast::Variable>(ruleContext.freeVariables.back().get());
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::BinaryOperation &binaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(binaryOperation.binary_operator, term);
-		auto left = translate(binaryOperation.left, ruleContext, context, variableStack);
-		auto right = translate(binaryOperation.right, ruleContext, context, variableStack);
+		auto left = translate(binaryOperation.left, ruleContext, variableStack);
+		auto right = translate(binaryOperation.right, ruleContext, variableStack);
 
 		return ast::Term::make<ast::BinaryOperation>(operator_, std::move(left), std::move(right));
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::UnaryOperation &unaryOperation, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		const auto operator_ = translate(unaryOperation.unary_operator, term);
-		auto argument = translate(unaryOperation.argument, ruleContext, context, variableStack);
+		auto argument = translate(unaryOperation.argument, ruleContext, 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)
+	std::optional<ast::Term> visit(const Clingo::AST::Interval &interval, const Clingo::AST::Term &, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
-		auto left = translate(interval.left, ruleContext, context, variableStack);
-		auto right = translate(interval.right, ruleContext, context, variableStack);
+		auto left = translate(interval.left, ruleContext, variableStack);
+		auto right = translate(interval.right, ruleContext, variableStack);
 
 		return ast::Term::make<ast::Interval>(std::move(left), std::move(right));
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+	std::optional<ast::Term> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 	{
 		if (function.external)
 			throw TranslationException(term.location, "external functions currently unsupported");
@@ -158,14 +157,12 @@ struct TermTranslateVisitor
 		arguments.reserve(function.arguments.size());
 
 		for (const auto &argument : function.arguments)
-			arguments.emplace_back(translate(argument, ruleContext, context, variableStack));
+			arguments.emplace_back(translate(argument, ruleContext, variableStack));
 
-		auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, function.arguments.size());
-
-		return ast::Term::make<ast::Function>(functionDeclaration, std::move(arguments));
+		return ast::Term::make<ast::Function>(function.name, std::move(arguments));
 	}
 
-	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, Context &, const ast::VariableStack &)
+	std::optional<ast::Term> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, RuleContext &, const ast::VariableStack &)
 	{
 		throw TranslationException(term.location, "“pool” terms currently unsupported");
 		return std::nullopt;
@@ -174,9 +171,9 @@ struct TermTranslateVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, Context &context, const ast::VariableStack &variableStack)
+ast::Term translate(const Clingo::AST::Term &term, RuleContext &ruleContext, const ast::VariableStack &variableStack)
 {
-	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, context, variableStack);
+	auto translatedTerm = term.data.accept(TermTranslateVisitor(), term, ruleContext, variableStack);
 
 	if (!translatedTerm)
 		throw TranslationException(term.location, "could not translate term");

include/anthem/Utils.h

@@ -23,33 +23,6 @@ constexpr const auto UserVariablePrefix = "U";
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-enum class Tristate
-{
-	True,
-	False,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class EvaluationResult
-{
-	True,
-	False,
-	Unknown,
-	Error,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class OperationResult
-{
-	Unchanged,
-	Changed,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 
 #endif

include/anthem/output/AST.h

@@ -46,12 +46,12 @@ output::ColorStream &print(output::ColorStream &stream, const BinaryOperation &b
 output::ColorStream &print(output::ColorStream &stream, const Boolean &boolean, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const Comparison &comparison, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, Comparison::Operator operator_, PrintContext &printContext, bool omitParentheses = false);
+output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const In &in, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const Integer &integer, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool omitParentheses = false);
-output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const String &string, PrintContext &printContext, bool omitParentheses = false);
 output::ColorStream &print(output::ColorStream &stream, const UnaryOperation &unaryOperation, PrintContext &printContext, bool omitParentheses = false);
@@ -167,9 +167,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Comparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+inline output::ColorStream &print(output::ColorStream &stream, const Constant &constant, PrintContext &, bool)
+{
+	return (stream << constant.name);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 inline output::ColorStream &print(output::ColorStream &stream, const Function &function, PrintContext &printContext, bool)
 {
-	stream << function.declaration->name;
+	stream << function.name;
 
 	if (function.arguments.empty())
 		return stream;
@@ -184,7 +191,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Function &f
 		print(stream, *i, printContext);
 	}
 
-	if (function.declaration->name.empty() && function.arguments.size() == 1)
+	if (function.name.empty() && function.arguments.size() == 1)
 		stream << ",";
 
 	stream << ")";
@@ -237,7 +244,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const Interval &i
 
 inline output::ColorStream &print(output::ColorStream &stream, const Predicate &predicate, PrintContext &printContext, bool)
 {
-	stream << predicate.declaration->name;
+	stream << predicate.name;
 
 	if (predicate.arguments.empty())
 		return stream;
@@ -259,13 +266,6 @@ inline output::ColorStream &print(output::ColorStream &stream, const Predicate &
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const PredicateDeclaration &predicateDeclaration, PrintContext &, bool)
-{
-	return (stream << predicateDeclaration.name << "/" << predicateDeclaration.arity());
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 inline output::ColorStream &print(output::ColorStream &stream, const SpecialInteger &specialInteger, PrintContext &, bool)
 {
 	switch (specialInteger.type)
@@ -322,24 +322,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
 
 inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
 {
-	const auto domainSuffix =
-		[&variableDeclaration]()
-		{
-			switch (variableDeclaration.domain)
-			{
-				case Domain::Unknown:
-					return "";
-				case Domain::General:
-					return "g";
-				case Domain::Integer:
-					return "i";
-			}
-
-			return "";
-		};
-
 	const auto printVariableDeclaration =
-		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
+		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
 			auto matchingVariableID = variableIDs.find(&variableDeclaration);
 
@@ -350,7 +334,7 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 				matchingVariableID = emplaceResult.first;
 			}
 
-			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
+			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);
 
 			return (stream << output::Variable(variableName.c_str()));
 		};

src/anthem/ASTCopy.cpp

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

src/anthem/ASTUtils.cpp

@@ -150,6 +150,10 @@ struct CollectFreeVariablesVisitor
 		binaryOperation.right.accept(*this, variableStack, freeVariables);
 	}
 
+	void visit(Constant &, VariableStack &, std::vector<VariableDeclaration *> &)
+	{
+	}
+
 	void visit(Function &function, VariableStack &variableStack, std::vector<VariableDeclaration *> &freeVariables)
 	{
 		for (auto &argument : function.arguments)
@@ -193,5 +197,84 @@ struct CollectFreeVariablesVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
+{
+	static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+	{
+		const auto predicateSignatureMatches =
+			[&predicate](const auto &predicateSignature)
+			{
+				return matches(predicate, predicateSignature);
+			};
+
+		if (std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), predicateSignatureMatches) != predicateSignatures.cend())
+			return;
+
+		// TODO: avoid copies
+		auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
+
+		// Ignore predicates that are declared #external
+		if (context.externalPredicateSignatures)
+		{
+			const auto matchesPredicateSignature =
+				[&](const auto &otherPredicateSignature)
+				{
+					return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
+				};
+
+			auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
+
+			const auto matchingExternalPredicateSignature =
+				std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
+
+			if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
+			{
+				matchingExternalPredicateSignature->used = true;
+				return;
+			}
+		}
+
+		predicateSignatures.emplace_back(std::move(predicateSignature));
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
+	{
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &lhs, const Predicate &rhs)
+{
+	return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const Predicate &predicate, const PredicateSignature &signature)
+{
+	return (predicate.name == signature.name && predicate.arity() == signature.arity);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
+{
+	return (lhs.name == rhs.name && lhs.arity == rhs.arity);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// TODO: remove const_cast
+void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
+{
+	auto &formulaMutable = const_cast<Formula &>(formula);
+	formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 }

src/anthem/Completion.cpp

@@ -35,7 +35,7 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 
 		auto &otherPredicate = implies.consequent.get<ast::Predicate>();
 
-		if (predicate.declaration != otherPredicate.declaration)
+		if (!ast::matches(predicate, otherPredicate))
 			continue;
 
 		assert(otherPredicate.arguments.size() == parameters.size());
@@ -100,22 +100,22 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Formula completePredicate(ast::PredicateDeclaration &predicateDeclaration, std::vector<ast::ScopedFormula> &scopedFormulas)
+ast::Formula completePredicate(const ast::PredicateSignature &predicateSignature, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
 	// Create new set of parameters for the completed definition for the predicate
 	ast::VariableDeclarationPointers parameters;
-	parameters.reserve(predicateDeclaration.arity());
+	parameters.reserve(predicateSignature.arity);
 
 	std::vector<ast::Term> arguments;
-	arguments.reserve(predicateDeclaration.arity());
+	arguments.reserve(predicateSignature.arity);
 
-	for (size_t i = 0; i < predicateDeclaration.arity(); i++)
+	for (size_t i = 0; i < predicateSignature.arity; i++)
 	{
 		parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
 		arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
 	}
 
-	ast::Predicate predicateCopy(&predicateDeclaration, std::move(arguments));
+	ast::Predicate predicateCopy(std::string(predicateSignature.name), std::move(arguments));
 
 	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
 	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
@@ -161,27 +161,28 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 			throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
 	}
 
-	std::sort(context.predicateDeclarations.begin(), context.predicateDeclarations.end(),
+	std::vector<ast::PredicateSignature> predicateSignatures;
+
+	// Get a list of all predicates
+	for (const auto &scopedFormula : scopedFormulas)
+		ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
+
+	std::sort(predicateSignatures.begin(), predicateSignatures.end(),
 		[](const auto &lhs, const auto &rhs)
 		{
-			const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
+			const auto order = std::strcmp(lhs.name.c_str(), rhs.name.c_str());
 
 			if (order != 0)
 				return (order < 0);
 
-			return lhs->arity() < rhs->arity();
+			return lhs.arity < rhs.arity;
 		});
 
 	std::vector<ast::Formula> completedFormulas;
 
 	// Complete predicates
-	for (auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-			continue;
-
-		completedFormulas.emplace_back(completePredicate(*predicateDeclaration, scopedFormulas));
-	}
+	for (const auto &predicateSignature : predicateSignatures)
+		completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
 
 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)
@@ -201,7 +202,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
 	}
 
 	// Eliminate all predicates that should not be visible in the output
-	eliminateHiddenPredicates(completedFormulas, context);
+	eliminateHiddenPredicates(predicateSignatures, completedFormulas, context);
 
 	return completedFormulas;
 }

src/anthem/HiddenPredicateElimination.cpp

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

src/anthem/IntegerVariableDetection.cpp

@@ -1,546 +0,0 @@
-#include <anthem/IntegerVariableDetection.h>
-
-#include <anthem/Arithmetics.h>
-#include <anthem/ASTCopy.h>
-#include <anthem/ASTUtils.h>
-#include <anthem/ASTVisitors.h>
-#include <anthem/Exception.h>
-#include <anthem/Simplification.h>
-#include <anthem/Utils.h>
-#include <anthem/output/AST.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// IntegerVariableDetection
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-{
-	if (variable.declaration->domain != ast::Domain::Unknown)
-		return variable.declaration->domain;
-
-	const auto match = variableDomainMap.find(variable.declaration);
-
-	if (match == variableDomainMap.end())
-		return ast::Domain::Unknown;
-
-	return match->second;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
-{
-	for (auto &variableDeclaration : variableDomainMap)
-		variableDeclaration.second = ast::Domain::Unknown;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct VariableDomainMapAccessor
-{
-	ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-	{
-		return domain(variable, variableDomainMap);
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
-{
-	return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct EvaluateFormulaVisitor
-{
-	static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
-	{
-		bool someFalse = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : and_.arguments)
-		{
-			const auto result = evaluate(argument, variableDomainMap);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					break;
-				case EvaluationResult::False:
-					someFalse = true;
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someFalse)
-			return EvaluationResult::False;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
-	{
-		const auto leftResult = evaluate(biconditional.left, variableDomainMap);
-		const auto rightResult = evaluate(biconditional.right, variableDomainMap);
-
-		if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
-	{
-		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
-	{
-		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
-
-		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		if (isLeftArithmetic == isRightArithmetic)
-			return EvaluationResult::Unknown;
-
-		// Handle the case where one side is arithmetic but the other one isn’t
-		switch (comparison.operator_)
-		{
-			case ast::Comparison::Operator::Equal:
-				return EvaluationResult::False;
-			case ast::Comparison::Operator::NotEqual:
-				return EvaluationResult::True;
-			default:
-				// TODO: implement more cases
-				return EvaluationResult::Unknown;
-		}
-	}
-
-	static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
-	{
-		return evaluate(exists.argument, variableDomainMap);
-	}
-
-	static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
-	{
-		return evaluate(forAll.argument, variableDomainMap);
-	}
-
-	static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
-	{
-		const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
-		const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
-
-		if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (antecedentResult == EvaluationResult::False)
-			return EvaluationResult::True;
-
-		if (consequentResult == EvaluationResult::True)
-			return EvaluationResult::True;
-
-		if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
-			return EvaluationResult::False;
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
-	{
-		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
-		const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
-
-		if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		if (isElementArithmetic == isSetArithmetic)
-			return EvaluationResult::Unknown;
-
-		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Not &not_, VariableDomainMap &variableDomainMap)
-	{
-		const auto result = evaluate(not_.argument, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
-			return result;
-
-		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
-	}
-
-	static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
-	{
-		bool someTrue = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : or_.arguments)
-		{
-			const auto result = evaluate(argument, variableDomainMap);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					someTrue = true;
-					break;
-				case EvaluationResult::False:
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someTrue)
-			return EvaluationResult::True;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
-	{
-		assert(predicate.arguments.size() == predicate.declaration->arity());
-
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-		{
-			const auto &argument = predicate.arguments[i];
-			const auto &parameter = predicate.declaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
-
-			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
-				return isArgumentArithmetic;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
-{
-	return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-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 != ast::Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		auto result = evaluate(definition, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
-
-		result = evaluate(definition, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-		{
-			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = ast::Domain::Integer;
-			return OperationResult::Changed;
-		}
-
-		return OperationResult::Unchanged;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct CheckIfQuantifiedFormulaFalseFunctor
-{
-	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
-		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
-	{
-		if (variableDeclaration.domain != ast::Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		auto result = evaluate(quantifiedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
-
-		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 = ast::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 != ast::Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		auto result = evaluate(completedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::True)
-			return OperationResult::Unchanged;
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
-
-		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 = ast::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

@@ -2,11 +2,10 @@
 
 #include <optional>
 
-#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
-#include <anthem/SimplificationVisitors.h>
 #include <anthem/output/AST.h>
+#include <anthem/SimplificationVisitors.h>
 
 namespace anthem
 {
@@ -101,7 +100,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class SimplificationRule>
-OperationResult simplify(ast::Formula &formula)
+SimplificationResult simplify(ast::Formula &formula)
 {
 	return SimplificationRule::apply(formula);
 }
@@ -109,10 +108,10 @@ OperationResult simplify(ast::Formula &formula)
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
-OperationResult simplify(ast::Formula &formula)
+SimplificationResult simplify(ast::Formula &formula)
 {
-	if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
-		return OperationResult::Changed;
+	if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
+		return SimplificationResult::Simplified;
 
 	return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
 }
@@ -123,19 +122,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
 {
 	static constexpr const auto Description = "exists () (F) === F";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &exists = formula.get<ast::Exists>();
 
 		if (!exists.variables.empty())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = std::move(exists.argument);
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -145,20 +144,20 @@ struct SimplificationRuleTrivialAssignmentInExists
 {
 	static constexpr const auto Description = "exists X (X = Y) === #true";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		const auto &exists = formula.get<ast::Exists>();
 
 		if (!exists.argument.is<ast::Comparison>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		const auto &comparison = exists.argument.get<ast::Comparison>();
 
 		if (comparison.operator_ != ast::Comparison::Operator::Equal)
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
 			[&](const auto &variableDeclaration)
@@ -168,11 +167,11 @@ struct SimplificationRuleTrivialAssignmentInExists
 			});
 
 		if (matchingAssignment == exists.variables.cend())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = ast::Formula::make<ast::Boolean>(true);
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -182,20 +181,20 @@ struct SimplificationRuleAssignmentInExists
 {
 	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &exists = formula.get<ast::Exists>();
 
 		if (!exists.argument.is<ast::And>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &and_ = exists.argument.get<ast::And>();
 		auto &arguments = and_.arguments;
 
-		auto simplificationResult = OperationResult::Unchanged;
+		auto simplificationResult = SimplificationResult::Unchanged;
 
 		for (auto i = exists.variables.begin(); i != exists.variables.end();)
 		{
@@ -226,7 +225,7 @@ struct SimplificationRuleAssignmentInExists
 				arguments.erase(j);
 
 				wasVariableReplaced = true;
-				simplificationResult = OperationResult::Changed;
+				simplificationResult = SimplificationResult::Simplified;
 
 				break;
 			}
@@ -250,19 +249,19 @@ struct SimplificationRuleEmptyConjunction
 {
 	static constexpr const auto Description = "[empty conjunction] === #true";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::And>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &and_ = formula.get<ast::And>();
 
 		if (!and_.arguments.empty())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = ast::Formula::make<ast::Boolean>(true);
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -272,19 +271,19 @@ struct SimplificationRuleOneElementConjunction
 {
 	static constexpr const auto Description = "[conjunction of only F] === F";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::And>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &and_ = formula.get<ast::And>();
 
 		if (and_.arguments.size() != 1)
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = std::move(and_.arguments.front());
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -294,19 +293,19 @@ struct SimplificationRuleTrivialExists
 {
 	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &exists = formula.get<ast::Exists>();
 
 		if (!exists.argument.is<ast::Boolean>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = std::move(exists.argument);
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -316,21 +315,21 @@ struct SimplificationRuleInWithPrimitiveArguments
 {
 	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::In>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &in = formula.get<ast::In>();
 
 		assert(ast::isPrimitive(in.element));
 
 		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -340,10 +339,10 @@ struct SimplificationRuleSubsumptionInBiconditionals
 {
 	static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Biconditional>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &biconditional = formula.get<ast::Biconditional>();
 
@@ -354,7 +353,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
 		const auto rightIsAnd = biconditional.right.is<ast::And>();
 
 		if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
 		auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
@@ -364,17 +363,17 @@ struct SimplificationRuleSubsumptionInBiconditionals
 			std::find_if(and_.arguments.cbegin(), and_.arguments.cend(),
 			[&](const auto &argument)
 			{
-				return (ast::equal(predicateSide, argument) == Tristate::True);
+				return (ast::equal(predicateSide, argument) == ast::Tristate::True);
 			});
 
 		if (matchingPredicate == and_.arguments.cend())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		and_.arguments.erase(matchingPredicate);
 
 		formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -384,21 +383,21 @@ struct SimplificationRuleDoubleNegation
 {
 	static constexpr const auto Description = "not not F === F";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &not_ = formula.get<ast::Not>();
 
 		if (!not_.argument.is<ast::Not>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &notNot = not_.argument.get<ast::Not>();
 
 		formula = std::move(notNot.argument);
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -408,15 +407,15 @@ struct SimplificationRuleDeMorganForConjunctions
 {
 	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &not_ = formula.get<ast::Not>();
 
 		if (!not_.argument.is<ast::And>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &and_ = not_.argument.get<ast::And>();
 
@@ -425,7 +424,7 @@ struct SimplificationRuleDeMorganForConjunctions
 
 		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -435,21 +434,21 @@ struct SimplificationRuleImplicationFromDisjunction
 {
 	static constexpr const auto Description = "(not F or G) === (F -> G)";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Or>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &or_ = formula.get<ast::Or>();
 
 		if (or_.arguments.size() != 2)
-			return OperationResult::Unchanged;
+			return SimplificationResult::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;
+			return SimplificationResult::Unchanged;
 
 		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
 		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
@@ -461,7 +460,7 @@ struct SimplificationRuleImplicationFromDisjunction
 
 		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
 
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -471,15 +470,15 @@ struct SimplificationRuleNegatedComparison
 {
 	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";
 
-	static OperationResult apply(ast::Formula &formula)
+	static SimplificationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &not_ = formula.get<ast::Not>();
 
 		if (!not_.argument.is<ast::Comparison>())
-			return OperationResult::Unchanged;
+			return SimplificationResult::Unchanged;
 
 		auto &comparison = not_.argument.get<ast::Comparison>();
 
@@ -507,32 +506,7 @@ struct SimplificationRuleNegatedComparison
 
 		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 isElementInteger = isInteger(in.element);
-		const auto isSetInteger = isInteger(in.set);
-
-		if (isElementInteger != EvaluationResult::True || isSetInteger != EvaluationResult::True)
-			return OperationResult::Unchanged;
-
-		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
-
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -552,8 +526,7 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison,
-		SimplificationRuleIntegerSetInclusion
+		SimplificationRuleNegatedComparison
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -562,7 +535,7 @@ const auto simplifyWithDefaultRules =
 struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
 {
 	// Do nothing for all other types of expressions
-	static OperationResult accept(ast::Formula &formula)
+	static SimplificationResult accept(ast::Formula &formula)
 	{
 		return simplifyWithDefaultRules(formula);
 	}
@@ -572,7 +545,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif
 
 void simplify(ast::Formula &formula)
 {
-	while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
+	while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

@@ -8,7 +8,6 @@
 
 #include <anthem/Completion.h>
 #include <anthem/Context.h>
-#include <anthem/IntegerVariableDetection.h>
 #include <anthem/Simplification.h>
 #include <anthem/StatementVisitor.h>
 #include <anthem/output/AST.h>
@@ -68,10 +67,10 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 			for (auto &scopedFormula : scopedFormulas)
 				simplify(scopedFormula.formula);
 
-		if (context.showStatementsUsed)
+		if (context.visiblePredicateSignatures)
 			context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
 
-		if (context.externalStatementsUsed)
+		if (context.externalPredicateSignatures)
 			context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
 
 		for (const auto &scopedFormula : scopedFormulas)
@@ -86,33 +85,25 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 	// Perform completion
 	auto completedFormulas = complete(std::move(scopedFormulas), context);
 
-	for (const auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		if (predicateDeclaration->isUsed)
-			continue;
+	// Check for #show statements with undeclared predicates
+	if (context.visiblePredicateSignatures)
+		for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
+			if (!predicateSignature.used)
+				context.logger.log(output::Priority::Warning)
+					<< "#show declaration of “"
+					<< predicateSignature.predicateSignature.name
+					<< "/" << predicateSignature.predicateSignature.arity
+					<< "” does not match any eligible predicate";
 
-		// Check for #show statements with undeclared predicates
-		if (predicateDeclaration->visibility != ast::PredicateDeclaration::Visibility::Default)
-			context.logger.log(output::Priority::Warning)
-				<< "#show declaration of “"
-				<< predicateDeclaration->name
-				<< "/"
-				<< predicateDeclaration->arity()
-				<< "” does not match any declared predicate";
-
-		// Check for #external statements with undeclared predicates
-		if (predicateDeclaration->isExternal && !predicateDeclaration->isUsed)
-			context.logger.log(output::Priority::Warning)
-				<< "#external declaration of “"
-				<< predicateDeclaration->name
-				<< "/"
-				<< predicateDeclaration->arity()
-				<< "” does not match any declared predicate";
-	}
-
-	// Detect integer variables
-	if (context.performIntegerDetection)
-		detectIntegerVariables(completedFormulas);
+	// Check for #external statements with undeclared predicates
+	if (context.externalPredicateSignatures)
+		for (const auto &predicateSignature : context.externalPredicateSignatures.value())
+			if (!predicateSignature.used)
+				context.logger.log(output::Priority::Warning)
+					<< "#external declaration of “"
+					<< predicateSignature.predicateSignature.name
+					<< "/" << predicateSignature.predicateSignature.arity
+					<< "” does not match any eligible predicate";
 
 	// Simplify output if specified
 	if (context.performSimplification)
@@ -126,38 +117,6 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 		ast::print(context.logger.outputStream(), completedFormula, printContext);
 		context.logger.outputStream() << std::endl;
 	}
-
-	// Print specifiers for integer predicate parameters
-	for (auto &predicateDeclaration : context.predicateDeclarations)
-	{
-		// Check that the predicate is used and not declared #external
-		if (!predicateDeclaration->isUsed || predicateDeclaration->isExternal)
-			continue;
-
-		const auto isPredicateVisible =
-			(predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Visible)
-			|| (predicateDeclaration->visibility == ast::PredicateDeclaration::Visibility::Default
-				&& context.defaultPredicateVisibility == ast::PredicateDeclaration::Visibility::Visible);
-
-		// If the predicate ought to be visible, don’t eliminate it
-		if (!isPredicateVisible)
-			continue;
-
-		for (size_t i = 0; i < predicateDeclaration->parameters.size(); i++)
-		{
-			auto &parameter = predicateDeclaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			context.logger.outputStream()
-				<< output::Keyword("int")
-				<< "(" << predicateDeclaration->name
-				<< "/" << output::Number(predicateDeclaration->arity())
-				<< "@" << output::Number(i + 1)
-				<< ")." << std::endl;
-		}
-	}
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////