Version bump for release 0.1.9 RC 3

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

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

CHANGELOG.md

@@ -1,24 +1,13 @@
 # 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 3 (2018-04-22)
 
 ### 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
+* optional detection of integer variables and integer predicate parameters
+* command-line option `--detect-integers` to enable integer variable detection
 * support for declaring functions integer with the `#external` directive
-
-### 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
+* new simplification rule applying to integer variables
 
 ## 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.3" << 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/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/Equality.h

@@ -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/Type.h

@@ -1,8 +1,7 @@
-#ifndef __ANTHEM__TYPE_H
-#define __ANTHEM__TYPE_H
+#ifndef __ANTHEM__ARITHMETICS_H
+#define __ANTHEM__ARITHMETICS_H
 
 #include <anthem/AST.h>
-#include <anthem/ASTUtils.h>
 #include <anthem/Utils.h>
 
 namespace anthem
@@ -10,12 +9,22 @@ namespace anthem
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 //
-// Type
+// Arithmetics
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct DefaultVariableDomainAccessor
+{
+	Domain operator()(const ast::Variable &variable)
+	{
+		return variable.declaration->domain;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 template <class VariableDomainAccessor = DefaultVariableDomainAccessor, class... Arguments>
-Type type(const ast::Term &term, Arguments &&... arguments);
+Type type(const ast::Term &term, Arguments &&...);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

include/anthem/Utils.h

@@ -13,7 +13,6 @@ namespace anthem
 constexpr const auto HeadVariablePrefix = "V";
 constexpr const auto BodyVariablePrefix = "X";
 constexpr const auto UserVariablePrefix = "U";
-constexpr const auto IntegerVariablePrefix = "N";
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
@@ -26,14 +25,6 @@ enum class Tristate
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-enum class OperationResult
-{
-	Unchanged,
-	Changed,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 enum class EvaluationResult
 {
 	True,
@@ -44,6 +35,14 @@ enum class EvaluationResult
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class OperationResult
+{
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 enum class Domain
 {
 	Noninteger,

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::Noninteger:
+					return "n";
+				case Domain::Integer:
+					return "i";
+			}
+
+			return "";
+		};
+
 	const auto printVariableDeclaration =
-		[&stream, &variableDeclaration](const auto *prefix, auto &variableIDs) -> output::ColorStream &
+		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
 			auto matchingVariableID = variableIDs.find(&variableDeclaration);
 
@@ -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,7 +3,6 @@
 #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>
@@ -63,9 +62,218 @@ Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap);
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct EvaluateFormulaVisitor
+{
+	static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
+	{
+		bool someFalse = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : and_.arguments)
+		{
+			const auto result = evaluate(argument, variableDomainMap);
+
+			switch (result)
+			{
+				case EvaluationResult::Error:
+					return EvaluationResult::Error;
+				case EvaluationResult::True:
+					break;
+				case EvaluationResult::False:
+					someFalse = true;
+					break;
+				case EvaluationResult::Unknown:
+					someUnknown = true;
+					break;
+			}
+		}
+
+		if (someFalse)
+			return EvaluationResult::False;
+
+		if (someUnknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::True;
+	}
+
+	static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
+	{
+		const auto leftResult = evaluate(biconditional.left, variableDomainMap);
+		const auto rightResult = evaluate(biconditional.right, variableDomainMap);
+
+		if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
+			return EvaluationResult::Unknown;
+
+		return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
+	}
+
+	static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
+	{
+		return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
+	}
+
+	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
+	{
+		const auto leftType = type(comparison.left, variableDomainMap);
+		const auto rightType = type(comparison.right, variableDomainMap);
+
+		// Comparisons with empty sets always return false
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
+
+		// If either side has an unknown domain, the result is unknown
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
+			return EvaluationResult::Unknown;
+
+		// If both sides have the same domain, the result is unknown
+		if (leftType.domain == rightType.domain)
+			return EvaluationResult::Unknown;
+
+		// If one side is integer, but the other one isn’t, they are not equal
+		switch (comparison.operator_)
+		{
+			case ast::Comparison::Operator::Equal:
+				return EvaluationResult::False;
+			case ast::Comparison::Operator::NotEqual:
+				return EvaluationResult::True;
+			default:
+				// TODO: implement more cases
+				return EvaluationResult::Unknown;
+		}
+	}
+
+	static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
+	{
+		return evaluate(exists.argument, variableDomainMap);
+	}
+
+	static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
+	{
+		return evaluate(forAll.argument, variableDomainMap);
+	}
+
+	static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
+	{
+		const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
+		const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
+
+		if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
+			return EvaluationResult::Error;
+
+		if (antecedentResult == EvaluationResult::False)
+			return EvaluationResult::True;
+
+		if (consequentResult == EvaluationResult::True)
+			return EvaluationResult::True;
+
+		if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
+			return EvaluationResult::False;
+
+		return EvaluationResult::Unknown;
+	}
+
+	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
+	{
+		const auto elementType = type(in.element, variableDomainMap);
+		const auto setType = type(in.set, variableDomainMap);
+
+		// The element to test shouldn’t be empty or a proper set by itself
+		assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
+
+		// If the set is empty, no element can be selected
+		if (setType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
+
+		// If one of the sides has an unknown type, the result is unknown
+		if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown)
+			return EvaluationResult::Unknown;
+
+		// If both sides have the same domain, the result is unknown
+		if (elementType.domain == setType.domain)
+			return EvaluationResult::Unknown;
+
+		// If one side is integer, but the other one isn’t, set inclusion is never satisfied
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::Not &not_, VariableDomainMap &variableDomainMap)
+	{
+		const auto result = evaluate(not_.argument, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
+			return result;
+
+		return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
+	}
+
+	static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
+	{
+		bool someTrue = false;
+		bool someUnknown = false;
+
+		for (const auto &argument : or_.arguments)
+		{
+			const auto result = evaluate(argument, variableDomainMap);
+
+			switch (result)
+			{
+				case EvaluationResult::Error:
+					return EvaluationResult::Error;
+				case EvaluationResult::True:
+					someTrue = true;
+					break;
+				case EvaluationResult::False:
+					break;
+				case EvaluationResult::Unknown:
+					someUnknown = true;
+					break;
+			}
+		}
+
+		if (someTrue)
+			return EvaluationResult::True;
+
+		if (someUnknown)
+			return EvaluationResult::Unknown;
+
+		return EvaluationResult::False;
+	}
+
+	static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
+	{
+		assert(predicate.arguments.size() == predicate.declaration->arity());
+
+		for (size_t i = 0; i < predicate.arguments.size(); i++)
+		{
+			const auto &argument = predicate.arguments[i];
+			const auto &parameter = predicate.declaration->parameters[i];
+
+			if (parameter.domain != Domain::Integer)
+				continue;
+
+			const auto argumentType = type(argument, variableDomainMap);
+
+			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
+				return EvaluationResult::Error;
+		}
+
+		return EvaluationResult::Unknown;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
 {
-	return evaluate<VariableDomainMap>(formula, variableDomainMap);
+	return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

@@ -155,7 +155,7 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 				<< "(" << predicateDeclaration->name
 				<< "/" << output::Number(predicateDeclaration->arity())
 				<< "@" << output::Number(i + 1)
-				<< ")" << std::endl;
+				<< ")." << 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));
-	}
-}