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,6 +1,6 @@
 # Change Log
 
-## 0.1.9 RC 2 (2018-04-21)
+## 0.1.9 RC 3 (2018-04-22)
 
 ### Features
 

app/main.cpp

@@ -72,7 +72,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.9-rc.2" << std::endl;
+		std::cout << "anthem version 0.1.9-rc.3" << std::endl;
 		return EXIT_SUCCESS;
 	}
 

examples/permutations.lp

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

examples/prime.lp

@@ -1,5 +1,5 @@
 #show prime/1.
-#external integer(n(0)).
+%#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,6 +1,6 @@
 #show in/2.
-#external integer(n(0)).
-#external integer(r(0)).
+%#external integer(n(0)).
+%#external integer(r(0)).
 
 {in(1..n, 1..r)}.
 covered(I) :- in(I, S).

include/anthem/AST.h

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

include/anthem/Arithmetics.h

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

include/anthem/Domain.h

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

include/anthem/StatementVisitor.h

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

include/anthem/Type.h

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

include/anthem/Utils.h

@@ -1,13 +1,6 @@
 #ifndef __ANTHEM__UTILS_H
 #define __ANTHEM__UTILS_H
 
-#include <iostream>
-
-#include <clingo.hh>
-
-#include <anthem/Context.h>
-#include <anthem/Location.h>
-
 namespace anthem
 {
 
@@ -50,6 +43,33 @@ enum class OperationResult
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class Domain
+{
+	Noninteger,
+	Integer,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class SetSize
+{
+	Empty,
+	Unit,
+	Multi,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Type
+{
+	Domain domain{Domain::Unknown};
+	SetSize setSize{SetSize::Unknown};
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif

include/anthem/output/AST.h

@@ -329,8 +329,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 			{
 				case Domain::Unknown:
 					return "";
-				case Domain::General:
-					return "g";
+				case Domain::Noninteger:
+					return "n";
 				case Domain::Integer:
 					return "i";
 			}

src/anthem/IntegerVariableDetection.cpp

@@ -1,11 +1,11 @@
 #include <anthem/IntegerVariableDetection.h>
 
-#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/ASTUtils.h>
 #include <anthem/ASTVisitors.h>
 #include <anthem/Exception.h>
 #include <anthem/Simplification.h>
+#include <anthem/Type.h>
 #include <anthem/Utils.h>
 #include <anthem/output/AST.h>
 
@@ -18,19 +18,19 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
+using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
 {
-	if (variable.declaration->domain != ast::Domain::Unknown)
+	if (variable.declaration->domain != Domain::Unknown)
 		return variable.declaration->domain;
 
 	const auto match = variableDomainMap.find(variable.declaration);
 
 	if (match == variableDomainMap.end())
-		return ast::Domain::Unknown;
+		return Domain::Unknown;
 
 	return match->second;
 }
@@ -40,14 +40,14 @@ ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDom
 void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
 {
 	for (auto &variableDeclaration : variableDomainMap)
-		variableDeclaration.second = ast::Domain::Unknown;
+		variableDeclaration.second = Domain::Unknown;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 struct VariableDomainMapAccessor
 {
-	ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+	Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
 	{
 		return domain(variable, variableDomainMap);
 	}
@@ -55,9 +55,9 @@ struct VariableDomainMapAccessor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
+Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
+	return type<VariableDomainMapAccessor>(term, variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -122,19 +122,22 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
 	{
-		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
+		const auto leftType = type(comparison.left, variableDomainMap);
+		const auto rightType = type(comparison.right, variableDomainMap);
 
-		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
+		// Comparisons with empty sets always return false
+		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
+			return EvaluationResult::False;
 
-		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
+		// If either side has an unknown domain, the result is unknown
+		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
 			return EvaluationResult::Unknown;
 
-		if (isLeftArithmetic == isRightArithmetic)
+		// If both sides have the same domain, the result is unknown
+		if (leftType.domain == rightType.domain)
 			return EvaluationResult::Unknown;
 
-		// Handle the case where one side is arithmetic but the other one isn’t
+		// If one side is integer, but the other one isn’t, they are not equal
 		switch (comparison.operator_)
 		{
 			case ast::Comparison::Operator::Equal:
@@ -179,19 +182,25 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
 	{
-		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
-		const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
+		const auto elementType = type(in.element, variableDomainMap);
+		const auto setType = type(in.set, variableDomainMap);
 
-		if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
+		// The element to test shouldn’t be empty or a proper set by itself
+		assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi);
 
-		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
+		// 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 (isElementArithmetic == isSetArithmetic)
+		// If both sides have the same domain, the result is unknown
+		if (elementType.domain == setType.domain)
 			return EvaluationResult::Unknown;
 
-		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
+		// If one side is integer, but the other one isn’t, set inclusion is never satisfied
 		return EvaluationResult::False;
 	}
 
@@ -247,13 +256,13 @@ struct EvaluateFormulaVisitor
 			const auto &argument = predicate.arguments[i];
 			const auto &parameter = predicate.declaration->parameters[i];
 
-			if (parameter.domain != ast::Domain::Integer)
+			if (parameter.domain != Domain::Integer)
 				continue;
 
-			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
+			const auto argumentType = type(argument, variableDomainMap);
 
-			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
-				return isArgumentArithmetic;
+			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
+				return EvaluationResult::Error;
 		}
 
 		return EvaluationResult::Unknown;
@@ -392,25 +401,20 @@ struct CheckIfDefinitionFalseFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != ast::Domain::Unknown)
+		if (variableDeclaration.domain != Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(definition, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(definition, variableDomainMap);
+		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 = ast::Domain::Integer;
+			variableDeclaration.domain = Domain::Integer;
 			return OperationResult::Changed;
 		}
 
@@ -425,25 +429,20 @@ struct CheckIfQuantifiedFormulaFalseFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != ast::Domain::Unknown)
+		if (variableDeclaration.domain != Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(quantifiedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::False)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(quantifiedFormula, variableDomainMap);
+		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 = ast::Domain::Integer;
+			variableDeclaration.domain = Domain::Integer;
 			return OperationResult::Changed;
 		}
 
@@ -458,25 +457,20 @@ struct CheckIfCompletedFormulaTrueFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != ast::Domain::Unknown)
+		if (variableDeclaration.domain != Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		auto result = evaluate(completedFormula, variableDomainMap);
-
-		if (result == EvaluationResult::Error || result == EvaluationResult::True)
-			return OperationResult::Unchanged;
-
 		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
 
-		result = evaluate(completedFormula, variableDomainMap);
+		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 = ast::Domain::Integer;
+			variableDeclaration.domain = Domain::Integer;
 			return OperationResult::Changed;
 		}
 

src/anthem/Simplification.cpp

@@ -2,10 +2,10 @@
 
 #include <optional>
 
-#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
 #include <anthem/SimplificationVisitors.h>
+#include <anthem/Type.h>
 #include <anthem/output/AST.h>
 
 namespace anthem
@@ -524,11 +524,14 @@ struct SimplificationRuleIntegerSetInclusion
 
 		auto &in = formula.get<ast::In>();
 
-		const auto isElementInteger = isInteger(in.element);
-		const auto isSetInteger = isInteger(in.set);
+		const auto elementType = type(in.element);
+		const auto setType = type(in.set);
 
-		if (isElementInteger != EvaluationResult::True || isSetInteger != EvaluationResult::True)
+		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));
 

src/anthem/Translation.cpp

@@ -147,7 +147,7 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 		{
 			auto &parameter = predicateDeclaration->parameters[i];
 
-			if (parameter.domain != ast::Domain::Integer)
+			if (parameter.domain != Domain::Integer)
 				continue;
 
 			context.logger.outputStream()