Version bump for release 0.1.9 RC 2

CHANGELOG.md

@@ -1,6 +1,6 @@
 # Change Log
 
-## 0.1.9 RC 5 (2018-04-22)
+## 0.1.9 RC 2 (2018-04-21)
 
 ### Features
 

app/main.cpp

@@ -72,7 +72,7 @@ int main(int argc, char **argv)
 
 	if (version)
 	{
-		std::cout << "anthem version 0.1.9-rc.5" << std::endl;
+		std::cout << "anthem version 0.1.9-rc.2" << 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).
-
-#show prime/1.

examples/schur-numbers.lp

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

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

include/anthem/Arithmetics.h

@@ -0,0 +1,262 @@
+#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

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

@@ -1,166 +0,0 @@
-#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,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,7 +20,6 @@ namespace anthem
 constexpr const auto HeadVariablePrefix = "V";
 constexpr const auto BodyVariablePrefix = "X";
 constexpr const auto UserVariablePrefix = "U";
-constexpr const auto IntegerVariablePrefix = "N";
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
@@ -44,33 +50,6 @@ 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

@@ -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;
 };
@@ -323,6 +322,22 @@ inline output::ColorStream &print(output::ColorStream &stream, const Variable &v
 
 inline output::ColorStream &print(output::ColorStream &stream, const VariableDeclaration &variableDeclaration, PrintContext &printContext, bool)
 {
+	const auto domainSuffix =
+		[&variableDeclaration]()
+		{
+			switch (variableDeclaration.domain)
+			{
+				case Domain::Unknown:
+					return "";
+				case Domain::General:
+					return "g";
+				case Domain::Integer:
+					return "i";
+			}
+
+			return "";
+		};
+
 	const auto printVariableDeclaration =
 		[&](const auto *prefix, auto &variableIDs) -> output::ColorStream &
 		{
@@ -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/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 *, 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;
 }
@@ -40,14 +40,14 @@ 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
 {
-	Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
+	ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
 	{
 		return domain(variable, variableDomainMap);
 	}
@@ -55,9 +55,9 @@ struct VariableDomainMapAccessor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
+EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return type<VariableDomainMapAccessor>(term, variableDomainMap);
+	return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -122,22 +122,19 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
 	{
-		const auto leftType = type(comparison.left, variableDomainMap);
-		const auto rightType = type(comparison.right, variableDomainMap);
+		const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
+		const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
 
-		// Comparisons with empty sets always return false
-		if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty)
-			return EvaluationResult::False;
+		if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
 
-		// If either side has an unknown domain, the result is unknown
-		if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown)
+		if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
 			return EvaluationResult::Unknown;
 
-		// If both sides have the same domain, the result is unknown
-		if (leftType.domain == rightType.domain)
+		if (isLeftArithmetic == isRightArithmetic)
 			return EvaluationResult::Unknown;
 
-		// If one side is integer, but the other one isn’t, they are not equal
+		// Handle the case where one side is arithmetic but the other one isn’t
 		switch (comparison.operator_)
 		{
 			case ast::Comparison::Operator::Equal:
@@ -182,25 +179,19 @@ struct EvaluateFormulaVisitor
 
 	static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
 	{
-		const auto elementType = type(in.element, variableDomainMap);
-		const auto setType = type(in.set, variableDomainMap);
+		const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
+		const auto isSetArithmetic = isArithmetic(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 (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
+			return EvaluationResult::Error;
 
-		// 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)
+		if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
 			return EvaluationResult::Unknown;
 
-		// If both sides have the same domain, the result is unknown
-		if (elementType.domain == setType.domain)
+		if (isElementArithmetic == isSetArithmetic)
 			return EvaluationResult::Unknown;
 
-		// If one side is integer, but the other one isn’t, set inclusion is never satisfied
+		// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
 		return EvaluationResult::False;
 	}
 
@@ -256,13 +247,13 @@ struct EvaluateFormulaVisitor
 			const auto &argument = predicate.arguments[i];
 			const auto &parameter = predicate.declaration->parameters[i];
 
-			if (parameter.domain != Domain::Integer)
+			if (parameter.domain != ast::Domain::Integer)
 				continue;
 
-			const auto argumentType = type(argument, variableDomainMap);
+			const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
 
-			if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty)
-				return EvaluationResult::Error;
+			if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
+				return isArgumentArithmetic;
 		}
 
 		return EvaluationResult::Unknown;
@@ -401,20 +392,25 @@ struct CheckIfDefinitionFalseFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != Domain::Unknown)
+		if (variableDeclaration.domain != ast::Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+		auto result = evaluate(definition, variableDomainMap);
 
-		const auto result = evaluate(definition, variableDomainMap);
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(definition, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::False)
 		{
 			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
+			variableDeclaration.domain = ast::Domain::Integer;
 			return OperationResult::Changed;
 		}
 
@@ -429,20 +425,25 @@ struct CheckIfQuantifiedFormulaFalseFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != Domain::Unknown)
+		if (variableDeclaration.domain != ast::Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+		auto result = evaluate(quantifiedFormula, variableDomainMap);
 
-		const auto result = evaluate(quantifiedFormula, variableDomainMap);
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(quantifiedFormula, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::False)
 		{
 			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
+			variableDeclaration.domain = ast::Domain::Integer;
 			return OperationResult::Changed;
 		}
 
@@ -457,20 +458,25 @@ struct CheckIfCompletedFormulaTrueFunctor
 	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
 		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
 	{
-		if (variableDeclaration.domain != Domain::Unknown)
+		if (variableDeclaration.domain != ast::Domain::Unknown)
 			return OperationResult::Unchanged;
 
 		clearVariableDomainMap(variableDomainMap);
 
-		// As a hypothesis, make the parameter’s domain noninteger
-		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+		auto result = evaluate(completedFormula, variableDomainMap);
 
-		const auto result = evaluate(completedFormula, variableDomainMap);
+		if (result == EvaluationResult::Error || result == EvaluationResult::True)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(completedFormula, variableDomainMap);
 
 		if (result == EvaluationResult::Error || result == EvaluationResult::True)
 		{
 			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-			variableDeclaration.domain = Domain::Integer;
+			variableDeclaration.domain = ast::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,14 +524,11 @@ struct SimplificationRuleIntegerSetInclusion
 
 		auto &in = formula.get<ast::In>();
 
-		const auto elementType = type(in.element);
-		const auto setType = type(in.set);
+		const auto isElementInteger = isInteger(in.element);
+		const auto isSetInteger = isInteger(in.set);
 
-		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
-		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
-		{
+		if (isElementInteger != EvaluationResult::True || isSetInteger != EvaluationResult::True)
 			return OperationResult::Unchanged;
-		}
 
 		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
 

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 != Domain::Integer)
+			if (parameter.domain != ast::Domain::Integer)
 				continue;
 
 			context.logger.outputStream()
@@ -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;
 		}
 	}
 }