Version bump for release 0.1.9 RC 1

This adds suffixes to integer and general variables, where the domain is
explicitly known.

CHANGELOG.md

@@ -1,24 +1,11 @@
 # Change Log
 
-## (unreleased)
-
-## 0.1.9 (2018-05-04)
-
-### Changes
-
-* turns on completion and simplification by default, which can now be switched off with `--no-complete` and `--no-simplify`
+## 0.1.9 RC 1 (2018-04-20)
 
 ### Features
 
-* detection of integer variables and integer predicate parameters
-* command-line option `--no-detect-integers` to disable integer variable detection
-* new simplification rule applying to integer variables
-* support for declaring functions integer with the `#external` directive
-
-### Bug Fixes
-
-* fixes incorrect translation of unsupported choice rules with multiple elements by returning an error instead
-* fixes precedence of intervals by enclosing them in parentheses
+* optional detection of integer variables and integer predicate parameters
+* command-line option `--detect-integers` to enable integer variable detection
 
 ## 0.1.8 (2018-04-20)
 

README.md

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

app/main.cpp

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

examples/choice-rules.lp

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

examples/graph-coloring.lp

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

examples/letters.lp

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

examples/permutations.lp

@@ -1,4 +1,5 @@
 #show p/2.
+#external integer(n(0)).
 
 {p(1..n, 1..n)}.
 

examples/prime.lp

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

examples/schur-numbers.lp

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

examples/simple-external-show.lp

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

examples/simple-external.lp

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

include/anthem/AST.h

@@ -2,7 +2,8 @@
 #define __ANTHEM__AST_H
 
 #include <anthem/ASTForward.h>
-#include <anthem/Utils.h>
+#include <anthem/Domain.h>
+#include <anthem/Tristate.h>
 
 namespace anthem
 {
@@ -148,7 +149,7 @@ struct FunctionDeclaration
 
 	std::string name;
 	size_t arity;
-	Domain domain{Domain::Noninteger};
+	Domain domain{Domain::General};
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

include/anthem/ASTUtils.h

@@ -90,21 +90,6 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceV
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 }
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-// Accessing Variable Domains
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DefaultVariableDomainAccessor
-{
-	Domain operator()(const ast::Variable &variable)
-	{
-		return variable.declaration->domain;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 }
 
 #endif

include/anthem/Domain.h

@@ -0,0 +1,27 @@
+#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,7 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
-#include <anthem/Utils.h>
+#include <anthem/Tristate.h>
 
 namespace anthem
 {
@@ -268,8 +268,8 @@ struct TermEqualityVisitor
 			return Tristate::Unknown;
 		}
 
-		if (equal(binaryOperation.left, otherBinaryOperation.right) == Tristate::True
-		    && equal(binaryOperation.right, otherBinaryOperation.left) == Tristate::True)
+		if (equal(binaryOperation.left, binaryOperation.right) == Tristate::True
+		    && equal(binaryOperation.right, binaryOperation.left) == Tristate::True)
 		{
 			return Tristate::True;
 		}

include/anthem/Evaluation.h

@@ -1,244 +0,0 @@
-#ifndef __ANTHEM__EVALUATION_H
-#define __ANTHEM__EVALUATION_H
-
-#include <anthem/AST.h>
-#include <anthem/ASTUtils.h>
-#include <anthem/Utils.h>
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Evaluation
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor>
-struct EvaluateFormulaVisitor
-{
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::And &and_, Arguments &&... arguments)
-	{
-		bool someFalse = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : and_.arguments)
-		{
-			const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					break;
-				case EvaluationResult::False:
-					someFalse = true;
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someFalse)
-			return EvaluationResult::False;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Biconditional &biconditional, Arguments &&... arguments)
-	{
-		const auto leftResult = evaluate(biconditional.left, std::forward<Arguments>(arguments)...);
-		const auto rightResult = evaluate(biconditional.right, std::forward<Arguments>(arguments)...);
-
-		if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Boolean &boolean, Arguments &&...)
-	{
-		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Comparison &comparison, Arguments &&... arguments)
-	{
-		const auto leftType = type(comparison.left, std::forward<Arguments>(arguments)...);
-		const auto rightType = type(comparison.right, std::forward<Arguments>(arguments)...);
-
-		// Comparisons with empty sets always return false
-		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
-			return EvaluationResult::False;
-
-		// If either side has an unknown domain, the result is unknown
-		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
-			return EvaluationResult::Unknown;
-
-		// If both sides have the same domain, the result is unknown
-		if (leftType.domain == rightType.domain)
-			return EvaluationResult::Unknown;
-
-		// If one side is integer, but the other one isn’t, they are not equal
-		switch (comparison.operator_)
-		{
-			case ast::Comparison::Operator::Equal:
-				return EvaluationResult::False;
-			case ast::Comparison::Operator::NotEqual:
-				return EvaluationResult::True;
-			default:
-				// TODO: implement more cases
-				return EvaluationResult::Unknown;
-		}
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Exists &exists, Arguments &&... arguments)
-	{
-		return evaluate(exists.argument, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::ForAll &forAll, Arguments &&... arguments)
-	{
-		return evaluate(forAll.argument, std::forward<Arguments>(arguments)...);
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Implies &implies, Arguments &&... arguments)
-	{
-		const auto antecedentResult = evaluate(implies.antecedent, std::forward<Arguments>(arguments)...);
-		const auto consequentResult = evaluate(implies.consequent, std::forward<Arguments>(arguments)...);
-
-		if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (antecedentResult == EvaluationResult::False)
-			return EvaluationResult::True;
-
-		if (consequentResult == EvaluationResult::True)
-			return EvaluationResult::True;
-
-		if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
-			return EvaluationResult::False;
-
-		return EvaluationResult::Unknown;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::In &in, Arguments &&... arguments)
-	{
-		const auto elementType = type(in.element, std::forward<Arguments>(arguments)...);
-		const auto setType = type(in.set, std::forward<Arguments>(arguments)...);
-
-		// The element to test shouldn’t be empty or a proper set by itself
-		assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
-
-		// If the set is empty, no element can be selected
-		if (setType.setSize == SetSize::Empty)
-			return EvaluationResult::False;
-
-		// If one of the sides has an unknown type, the result is unknown
-		if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
-			return EvaluationResult::Unknown;
-
-		// If both sides have the same domain, the result is unknown
-		if (elementType.domain == setType.domain)
-			return EvaluationResult::Unknown;
-
-		// If one side is integer, but the other one isn’t, set inclusion is never satisfied
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Not &not_, Arguments &&... arguments)
-	{
-		const auto result = evaluate(not_.argument, std::forward<Arguments>(arguments)...);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
-			return result;
-
-		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Or &or_, Arguments &&... arguments)
-	{
-		bool someTrue = false;
-		bool someUnknown = false;
-
-		for (const auto &argument : or_.arguments)
-		{
-			const auto result = evaluate(argument, std::forward<Arguments>(arguments)...);
-
-			switch (result)
-			{
-				case EvaluationResult::Error:
-					return EvaluationResult::Error;
-				case EvaluationResult::True:
-					someTrue = true;
-					break;
-				case EvaluationResult::False:
-					break;
-				case EvaluationResult::Unknown:
-					someUnknown = true;
-					break;
-			}
-		}
-
-		if (someTrue)
-			return EvaluationResult::True;
-
-		if (someUnknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::False;
-	}
-
-	template <class... Arguments>
-	static EvaluationResult visit(const ast::Predicate &predicate, Arguments &&... arguments)
-	{
-		assert(predicate.arguments.size() == predicate.declaration->arity());
-
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-		{
-			const auto &argument = predicate.arguments[i];
-			const auto &parameter = predicate.declaration->parameters[i];
-
-			if (parameter.domain != Domain::Integer)
-				continue;
-
-			const auto argumentType = type(argument, std::forward<Arguments>(arguments)...);
-
-			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
-				return EvaluationResult::Error;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
-EvaluationResult evaluate(const ast::Formula &formula, Arguments &&... arguments)
-{
-	return formula.accept(EvaluateFormulaVisitor<VariableDomainAccessor>(), std::forward<Arguments>(arguments)...);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif

include/anthem/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,69 @@ 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(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

@@ -237,7 +237,7 @@ struct StatementVisitor
 				const size_t arity = aritySymbol.number();
 
 				auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
-				functionDeclaration->domain = Domain::Integer;
+				functionDeclaration->domain = ast::Domain::Integer;
 
 				return true;
 			};

include/anthem/Tristate.h

@@ -0,0 +1,24 @@
+#ifndef __ANTHEM__TRISTATE_H
+#define __ANTHEM__TRISTATE_H
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// Tristate
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+
+#endif

include/anthem/Type.h

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

include/anthem/Utils.h

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

include/anthem/output/AST.h

@@ -35,7 +35,6 @@ struct PrintContext
 	std::map<const VariableDeclaration *, size_t> userVariableIDs;
 	std::map<const VariableDeclaration *, size_t> headVariableIDs;
 	std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
-	std::map<const VariableDeclaration *, size_t> integerVariableIDs;
 
 	const Context &context;
 };
@@ -219,16 +218,16 @@ inline output::ColorStream &print(output::ColorStream &stream, const Integer &in
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool omitParentheses)
+inline output::ColorStream &print(output::ColorStream &stream, const Interval &interval, PrintContext &printContext, bool)
 {
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << "(";
 
 	print(stream, interval.from, printContext);
 	stream << "..";
 	print(stream, interval.to, printContext);
 
-	if (!omitParentheses || printContext.context.parenthesisStyle == ParenthesisStyle::Full)
+	if (printContext.context.parenthesisStyle == ParenthesisStyle::Full)
 		stream << ")";
 
 	return stream;
@@ -323,8 +322,24 @@ 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 =
-		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
+		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
 			auto matchingVariableID = variableIDs.find(&variableDeclaration);
 
@@ -335,14 +350,11 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 				matchingVariableID = emplaceResult.first;
 			}
 
-			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);
+			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
 
 			return (stream << output::Variable(variableName.c_str()));
 		};
 
-	if (variableDeclaration.domain == Domain::Integer)
-		return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
-
 	switch (variableDeclaration.type)
 	{
 		case VariableDeclaration::Type::UserDefined:

src/anthem/Completion.cpp

@@ -40,36 +40,8 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 
 		assert(otherPredicate.arguments.size() == parameters.size());
 
-		auto &freeVariables = scopedFormula.freeVariables;
-
 		// Each formula with the predicate as its consequent currently has its own copy of the predicate’s parameters
 		// These need to be linked to the new, unique set of parameters
-
-		// First, remove the free variables whose occurrences will be relinked, which is why they are no longer needed
-		const auto isFreeVariableUnneeded =
-			[&](const auto &freeVariable)
-			{
-				const auto matchesVariableToBeReplaced = std::find_if(otherPredicate.arguments.cbegin(), otherPredicate.arguments.cend(),
-					[&](const ast::Term &argument)
-					{
-						assert(argument.is<ast::Variable>());
-						const auto &otherVariable = argument.get<ast::Variable>();
-
-						return (freeVariable.get() == otherVariable.declaration);
-					});
-
-				return (matchesVariableToBeReplaced != otherPredicate.arguments.cend());
-			};
-
-		freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isFreeVariableUnneeded), freeVariables.end());
-
-		// Currently, only rules with singleton heads are supported
-		// Rules with multiple elements in the head are not yet handled correctly by the head variable detection mechanism
-		for (const auto &freeVariable : freeVariables)
-			if (freeVariable->type == ast::VariableDeclaration::Type::Head)
-				throw CompletionException("cannot perform completion, only singleton rule heads supported currently");
-
-		// Second, link all occurrences of the deleted free variable to the new, unique parameter
 		for (size_t i = 0; i < parameters.size(); i++)
 		{
 			assert(otherPredicate.arguments[i].is<ast::Variable>());
@@ -78,6 +50,16 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, c
 			scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
 		}
 
+		// Remove all the head variables, because they are not free variables after completion
+		const auto isHeadVariable =
+			[](const auto &variableDeclaration)
+			{
+				return variableDeclaration->type == ast::VariableDeclaration::Type::Head;
+			};
+
+		auto &freeVariables = scopedFormula.freeVariables;
+		freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end());
+
 		if (freeVariables.empty())
 			disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
 		else

src/anthem/IntegerVariableDetection.cpp

@@ -3,11 +3,8 @@
 #include <anthem/ASTCopy.h>
 #include <anthem/ASTUtils.h>
 #include <anthem/ASTVisitors.h>
-#include <anthem/Evaluation.h>
 #include <anthem/Exception.h>
 #include <anthem/Simplification.h>
-#include <anthem/Type.h>
-#include <anthem/Utils.h>
 #include <anthem/output/AST.h>
 
 namespace anthem
@@ -19,19 +16,19 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
+using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
 {
-	if (variable.declaration->domain != Domain::Unknown)
+	if (variable.declaration->domain != ast::Domain::Unknown)
 		return variable.declaration->domain;
 
 	const auto match = variableDomainMap.find(variable.declaration);
 
 	if (match == variableDomainMap.end())
-		return Domain::Unknown;
+		return ast::Domain::Unknown;
 
 	return match->second;
 }
@@ -41,234 +38,542 @@ Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMa
 void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
 {
 	for (auto &variableDeclaration : variableDomainMap)
-		variableDeclaration.second = Domain::Unknown;
+		variableDeclaration.second = ast::Domain::Unknown;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct VariableDomainMapAccessor
+enum class OperationResult
 {
-	Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class EvaluationResult
+{
+	True,
+	False,
+	Unknown,
+	Error,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct IsTermArithmeticVisitor
+{
+	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, VariableDomainMap &variableDomainMap)
 	{
-		return domain(variable, variableDomainMap);
+		const auto isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
+		const auto isRightArithmetic = isArithmetic(binaryOperation.right, variableDomainMap);
+
+		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
+			return EvaluationResult::Error;
+
+		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::True;
+	}
+
+	static EvaluationResult visit(const ast::Boolean &, VariableDomainMap &)
+	{
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::Function &function, VariableDomainMap &)
+	{
+		switch (function.declaration->domain)
+		{
+			case ast::Domain::General:
+				return EvaluationResult::False;
+			case ast::Domain::Integer:
+				return EvaluationResult::True;
+			case ast::Domain::Unknown:
+				return EvaluationResult::Unknown;
+		}
+
+		return EvaluationResult::Unknown;
+	}
+
+	static EvaluationResult visit(const ast::Integer &, VariableDomainMap &)
+	{
+		return EvaluationResult::True;
+	}
+
+	static EvaluationResult visit(const ast::Interval &interval, VariableDomainMap &variableDomainMap)
+	{
+		const auto isFromArithmetic = isArithmetic(interval.from, variableDomainMap);
+		const auto isToArithmetic = isArithmetic(interval.to, variableDomainMap);
+
+		if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
+			return EvaluationResult::Error;
+
+		if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::True;
+	}
+
+	static EvaluationResult visit(const ast::SpecialInteger &, VariableDomainMap &)
+	{
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::String &, VariableDomainMap &)
+	{
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, VariableDomainMap &variableDomainMap)
+	{
+		const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument, variableDomainMap);
+
+		switch (unaryOperation.operator_)
+		{
+			case ast::UnaryOperation::Operator::Absolute:
+				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
+		}
+
+		return EvaluationResult::Unknown;
+	}
+
+	static EvaluationResult visit(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+	{
+		switch (domain(variable, variableDomainMap))
+		{
+			case ast::Domain::General:
+				return EvaluationResult::False;
+			case ast::Domain::Integer:
+				return EvaluationResult::True;
+			case ast::Domain::Unknown:
+				return EvaluationResult::Unknown;
+		}
+
+		return EvaluationResult::Unknown;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
+EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return type<VariableDomainMapAccessor>(term, variableDomainMap);
+	return term.accept(IsTermArithmeticVisitor(), variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct EvaluateFormulaVisitor
+{
+	static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
+	{
+		bool someFalse = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : and_.arguments)
+		{
+			const auto result = evaluate(argument, variableDomainMap);
+
+			switch (result)
+			{
+				case EvaluationResult::Error:
+					return EvaluationResult::Error;
+				case EvaluationResult::True:
+					break;
+				case EvaluationResult::False:
+					someFalse = true;
+					break;
+				case EvaluationResult::Unknown:
+					someUnknown = true;
+					break;
+			}
+		}
+
+		if (someFalse)
+			return EvaluationResult::False;
+
+		if (someUnknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::True;
+	}
+
+	static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
+	{
+		const auto leftResult = evaluate(biconditional.left, variableDomainMap);
+		const auto rightResult = evaluate(biconditional.right, variableDomainMap);
+
+		if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
+	}
+
+	static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
+	{
+		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
+	}
+
+	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
+	{
+		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
+		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
+
+		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		if (isLeftArithmetic == isRightArithmetic)
+			return EvaluationResult::Unknown;
+
+		// Handle the case where one side is arithmetic but the other one isn’t
+		switch (comparison.operator_)
+		{
+			case ast::Comparison::Operator::Equal:
+				return EvaluationResult::False;
+			case ast::Comparison::Operator::NotEqual:
+				return EvaluationResult::True;
+			default:
+				// TODO: implement more cases
+				return EvaluationResult::Unknown;
+		}
+	}
+
+	static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
+	{
+		return evaluate(exists.argument, variableDomainMap);
+	}
+
+	static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
+	{
+		return evaluate(forAll.argument, variableDomainMap);
+	}
+
+	static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
+	{
+		const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
+		const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
+
+		if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (antecedentResult == EvaluationResult::False)
+			return EvaluationResult::True;
+
+		if (consequentResult == EvaluationResult::True)
+			return EvaluationResult::True;
+
+		if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
+			return EvaluationResult::False;
+
+		return EvaluationResult::Unknown;
+	}
+
+	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
+	{
+		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
+		const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
+
+		if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		if (isElementArithmetic == isSetArithmetic)
+			return EvaluationResult::Unknown;
+
+		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::Not &not_, VariableDomainMap &variableDomainMap)
+	{
+		const auto result = evaluate(not_.argument, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
+			return result;
+
+		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
+	}
+
+	static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
+	{
+		bool someTrue = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : or_.arguments)
+		{
+			const auto result = evaluate(argument, variableDomainMap);
+
+			switch (result)
+			{
+				case EvaluationResult::Error:
+					return EvaluationResult::Error;
+				case EvaluationResult::True:
+					someTrue = true;
+					break;
+				case EvaluationResult::False:
+					break;
+				case EvaluationResult::Unknown:
+					someUnknown = true;
+					break;
+			}
+		}
+
+		if (someTrue)
+			return EvaluationResult::True;
+
+		if (someUnknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
+	{
+		assert(predicate.arguments.size() == predicate.declaration->arity());
+
+		for (size_t i = 0; i < predicate.arguments.size(); i++)
+		{
+			const auto &argument = predicate.arguments[i];
+			const auto &parameter = predicate.declaration->parameters[i];
+
+			if (parameter.domain != ast::Domain::Integer)
+				continue;
+
+			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
+
+			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
+				return isArgumentArithmetic;
+		}
+
+		return EvaluationResult::Unknown;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
 {
-	return evaluate<VariableDomainMap>(formula, variableDomainMap);
+	return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-template <class Functor>
-struct ForEachVariableDeclarationVisitor
+OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct DetectIntegerVariablesVisitor
 {
-	template <class... Arguments>
-	static OperationResult visit(ast::And &and_, Arguments &&... arguments)
+	static OperationResult visit(ast::And &and_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
 		for (auto &argument : and_.arguments)
-			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
+	static OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
-		if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
-		if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Boolean &, Arguments &&...)
+	static OperationResult visit(ast::Boolean &, ast::Formula &, VariableDomainMap &)
 	{
 		return OperationResult::Unchanged;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Comparison &, Arguments &&...)
+	static OperationResult visit(ast::Comparison &, ast::Formula &, VariableDomainMap &)
 	{
 		return OperationResult::Unchanged;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
+	static OperationResult visit(ast::Exists &exists, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
-		if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
 		for (auto &variableDeclaration : exists.variables)
-			if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		{
+			if (variableDeclaration->domain != ast::Domain::Unknown)
+				continue;
+
+			clearVariableDomainMap(variableDomainMap);
+
+			auto argumentResult = evaluate(exists.argument, variableDomainMap);
+			auto definitionResult = evaluate(definition, variableDomainMap);
+
+			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
+			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
+			{
+				continue;
+			}
+
+			// As a hypothesis, make the parameter’s domain noninteger
+			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
+
+			argumentResult = evaluate(exists.argument, variableDomainMap);
+			definitionResult = evaluate(definition, variableDomainMap);
+
+			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
+			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
+			{
+				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
 				operationResult = OperationResult::Changed;
+				variableDeclaration->domain = ast::Domain::Integer;
+			}
+		}
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
+	static OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
-		if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
 		for (auto &variableDeclaration : forAll.variables)
-			if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		{
+			if (variableDeclaration->domain != ast::Domain::Unknown)
+				continue;
+
+			clearVariableDomainMap(variableDomainMap);
+
+			auto argumentResult = evaluate(forAll.argument, variableDomainMap);
+			auto definitionResult = evaluate(definition, variableDomainMap);
+
+			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
+			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
+			{
+				continue;
+			}
+
+			// As a hypothesis, make the parameter’s domain noninteger
+			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
+
+			argumentResult = evaluate(forAll.argument, variableDomainMap);
+			definitionResult = evaluate(definition, variableDomainMap);
+
+			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
+			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
+			{
+				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
 				operationResult = OperationResult::Changed;
+				variableDeclaration->domain = ast::Domain::Integer;
+			}
+		}
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
+	static OperationResult visit(ast::Implies &implies, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
-		if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
-		if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+		if (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::In &, Arguments &&...)
+	static OperationResult visit(ast::In &, ast::Formula &, VariableDomainMap &)
 	{
 		return OperationResult::Unchanged;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
+	static OperationResult visit(ast::Not &not_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
-		return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
+		return detectIntegerVariables(not_.argument, definition, variableDomainMap);
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
+	static OperationResult visit(ast::Or &or_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
 		auto operationResult = OperationResult::Unchanged;
 
 		for (auto &argument : or_.arguments)
-			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;
 
 		return operationResult;
 	}
 
-	template <class... Arguments>
-	static OperationResult visit(ast::Predicate &, Arguments &&...)
+	static OperationResult visit(ast::Predicate &predicate, ast::Formula &, VariableDomainMap &)
 	{
-		return OperationResult::Unchanged;
+		auto operationResult = OperationResult::Unchanged;
+
+		assert(predicate.arguments.size() == predicate.declaration->arity());
+
+		// Propagate integer domains from predicates to variables
+		for (size_t i = 0; i < predicate.arguments.size(); i++)
+		{
+			auto &variableArgument = predicate.arguments[i];
+			auto &parameter = predicate.declaration->parameters[i];
+
+			if (parameter.domain != ast::Domain::Integer)
+				continue;
+
+			if (!variableArgument.is<ast::Variable>())
+				continue;
+
+			auto &variable = variableArgument.get<ast::Variable>();
+
+			if (variable.declaration->domain == ast::Domain::Integer)
+				continue;
+
+			operationResult = OperationResult::Changed;
+			variable.declaration->domain = ast::Domain::Integer;
+		}
+
+		return operationResult;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct CheckIfDefinitionFalseFunctor
+OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 {
-	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
-		ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
-	{
-		if (variableDeclaration.domain != Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
-
-		const auto result = evaluate(definition, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-		{
-			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
-			return OperationResult::Changed;
-		}
-
-		return OperationResult::Unchanged;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct CheckIfQuantifiedFormulaFalseFunctor
-{
-	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
-		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
-	{
-		if (variableDeclaration.domain != Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
-
-		const auto result = evaluate(quantifiedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-		{
-			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
-			return OperationResult::Changed;
-		}
-
-		return OperationResult::Unchanged;
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct CheckIfCompletedFormulaTrueFunctor
-{
-	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
-		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
-	{
-		if (variableDeclaration.domain != Domain::Unknown)
-			return OperationResult::Unchanged;
-
-		clearVariableDomainMap(variableDomainMap);
-
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
-
-		const auto result = evaluate(completedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::True)
-		{
-			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
-			return OperationResult::Changed;
-		}
-
-		return OperationResult::Unchanged;
-	}
-};
+	return formula.accept(DetectIntegerVariablesVisitor(), definition, variableDomainMap);
+}
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
@@ -285,10 +590,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
 
 		for (auto &completedFormula : completedFormulas)
 		{
-			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
-				operationResult = OperationResult::Changed;
-
-			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
+			if (detectIntegerVariables(completedFormula, completedFormula, variableDomainMap) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;
 
 			if (!completedFormula.is<ast::ForAll>())
@@ -307,11 +609,11 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
 			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());
 
+			if (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
 			for (size_t i = 0; i < predicate.arguments.size(); i++)
 			{
 				auto &variableArgument = predicate.arguments[i];
@@ -321,7 +623,28 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
 
 				auto &variable = variableArgument.get<ast::Variable>();
 
-				parameter.domain = variable.declaration->domain;
+				if (parameter.domain != ast::Domain::Unknown)
+					continue;
+
+				clearVariableDomainMap(variableDomainMap);
+
+				auto result = evaluate(definition, variableDomainMap);
+
+				if (result == EvaluationResult::Error || result == EvaluationResult::False)
+					continue;
+
+				// As a hypothesis, make the parameter’s domain noninteger
+				variableDomainMap[variable.declaration] = ast::Domain::General;
+
+				result = evaluate(definition, variableDomainMap);
+
+				if (result == EvaluationResult::Error || result == EvaluationResult::False)
+				{
+					// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+					operationResult = OperationResult::Changed;
+					variable.declaration->domain = ast::Domain::Integer;
+					parameter.domain = ast::Domain::Integer;
+				}
 			}
 		}
 	}

src/anthem/Simplification.cpp

@@ -4,9 +4,8 @@
 
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
-#include <anthem/SimplificationVisitors.h>
-#include <anthem/Type.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);
@@ -368,13 +367,13 @@ struct SimplificationRuleSubsumptionInBiconditionals
 			});
 
 		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,35 +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 elementType = type(in.element);
-		const auto setType = type(in.set);
-
-		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
-		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
-		{
-			return OperationResult::Unchanged;
-		}
-
-		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
-
-		return OperationResult::Changed;
+		return SimplificationResult::Simplified;
 	}
 };
 
@@ -555,8 +526,7 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison,
-		SimplificationRuleIntegerSetInclusion
+		SimplificationRuleNegatedComparison
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -565,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);
 	}
@@ -575,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

@@ -147,15 +147,15 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 		{
 			auto &parameter = predicateDeclaration->parameters[i];
 
-			if (parameter.domain != Domain::Integer)
+			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;
+				<< "@" << output::Number(i)
+				<< ")." << std::endl;
 		}
 	}
 }

tests/TestCompletion.cpp

@@ -123,7 +123,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		anthem::translate("input", input, context);
 
 		CHECK(output.str() ==
-			"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in (1..5)))\n");
+			"forall V1 (f(V1) <-> (exists U1 (V1 = f(f(f(f(U1)))) and f(U1)) or V1 in 1..5))\n");
 	}
 
 	SECTION("useless implications")
@@ -152,8 +152,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 
 		CHECK(output.str() ==
 			"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
-			"forall V2, V3 (in(V2, V3) -> (V2 in (1..n) and V3 in (1..r)))\n"
-			"forall U2 (U2 in (1..n) -> covered(U2))\n"
+			"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
+			"forall U2 (U2 in 1..n -> covered(U2))\n"
 			"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}
 
@@ -190,6 +190,6 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		input << "adj(X, Y) :- X = 1..n, Y = 1..n, |X - Y| = 1.";
 		anthem::translate("input", input, context);
 
-		CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in (1..n) and V2 in (1..n) and |V1 - V2| = 1))\n");
+		CHECK(output.str() == "forall V1, V2 (adj(V1, V2) <-> (V1 in 1..n and V2 in 1..n and |V1 - V2| = 1))\n");
 	}
 }

tests/TestHiddenPredicateElimination.cpp

@@ -150,7 +150,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 
 		// TODO: simplify further
 		CHECK(output.str() ==
-			"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in (1..4)))\n");
+			"forall V1 (a(V1) <-> exists U1 (c(V1) = c(U1) and U1 in 1..4))\n");
 	}
 
 	SECTION("simple propositions are hidden correctly")

tests/TestIntegerDetection.cpp

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

tests/TestSimplification.cpp

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

tests/TestTranslation.cpp

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

tests/TestUnsupported.cpp

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