Version bump for release 0.1.9 RC 4

Prefix integer variables with “N”
Instead of suffixing integer variables with “i,” this prefixes them with “N” instead to make it consistent with common mathematical notations.
2018-04-22 21:12:55 +02:00 · 2018-04-22 21:10:20 +02:00 · 2018-04-22 17:04:15 +02:00 · 2018-04-22 14:57:16 +02:00 · 2018-04-22 14:56:58 +02:00 · 2018-04-21 18:48:57 +02:00
18 changed files with 543 additions and 483 deletions
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,11 +1,13 @@
 # Change Log

-## 0.1.9 RC 1 (2018-04-20)
+## 0.1.9 RC 4 (2018-04-22)

 ### Features

 * optional detection of integer variables and integer predicate parameters
 * command-line option `--detect-integers` to enable integer variable detection
+* support for declaring functions integer with the `#external` directive
+* new simplification rule applying to integer variables

 ## 0.1.8 (2018-04-20)

--- a/app/main.cpp
+++ b/app/main.cpp
@@ -72,7 +72,7 @@ int main(int argc, char **argv)

 	if (version)
 	{
-		std::cout << "anthem version 0.1.9-rc.1" << std::endl;
+		std::cout << "anthem version 0.1.8-rc.4" << std::endl;
 		return EXIT_SUCCESS;
 	}

--- a/examples/permutations.lp
+++ b/examples/permutations.lp
@@ -1,5 +1,5 @@
 #show p/2.
-#external integer(n(0)).
+%#external integer(n(0)).

 {p(1..n, 1..n)}.

--- a/examples/prime.lp
+++ b/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).
--- a/examples/schur-numbers.lp
+++ b/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).
--- a/include/anthem/AST.h
+++ b/include/anthem/AST.h
@@ -2,8 +2,7 @@
 #define __ANTHEM__AST_H

 #include <anthem/ASTForward.h>
-#include <anthem/Domain.h>
-#include <anthem/Tristate.h>
+#include <anthem/Utils.h>

 namespace anthem
 {
@@ -149,7 +148,7 @@ struct FunctionDeclaration

 	std::string name;
 	size_t arity;
-	Domain domain{Domain::General};
+	Domain domain{Domain::Noninteger};
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/Domain.h
+++ b/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
--- a/include/anthem/Equality.h
+++ b/include/anthem/Equality.h
@@ -3,7 +3,7 @@

 #include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
-#include <anthem/Tristate.h>
+#include <anthem/Utils.h>

 namespace anthem
 {
--- a/include/anthem/Simplification.h
+++ b/include/anthem/Simplification.h
@@ -12,14 +12,6 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////

-enum class SimplificationResult
-{
-	Simplified,
-	Unchanged,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 void simplify(ast::Formula &formula);

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/include/anthem/SimplificationVisitors.h
+++ b/include/anthem/SimplificationVisitors.h
@@ -3,6 +3,7 @@

 #include <anthem/AST.h>
 #include <anthem/Simplification.h>
+#include <anthem/Utils.h>

 namespace anthem
 {
@@ -19,96 +20,96 @@ template<class T>
 struct FormulaSimplificationVisitor
 {
 	template <class... Arguments>
-	SimplificationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(And &and_, Formula &formula, Arguments &&... arguments)
 	{
 		for (auto &argument : and_.arguments)
-			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-				return SimplificationResult::Simplified;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Biconditional &biconditional, Formula &formula, Arguments &&... arguments)
 	{
-		if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

-		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Boolean &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Comparison &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Exists &exists, Formula &formula, Arguments &&... arguments)
 	{
-		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(ForAll &forAll, Formula &formula, Arguments &&... arguments)
 	{
-		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Implies &implies, Formula &formula, Arguments &&... arguments)
 	{
-		if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

-		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(In &, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(In &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Not &not_, Formula &formula, Arguments &&... arguments)
 	{
-		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Or &or_, Formula &formula, Arguments &&... arguments)
 	{
 		for (auto &argument : or_.arguments)
-			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-				return SimplificationResult::Simplified;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;

 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
+	OperationResult visit(Predicate &, Formula &formula, Arguments &&... arguments)
 	{
 		return T::accept(formula, std::forward<Arguments>(arguments)...);
 	}
@@ -116,69 +117,69 @@ struct FormulaSimplificationVisitor

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-template<class T, class SimplificationResult = void>
+template<class T, class OperationResult = void>
 struct TermSimplificationVisitor
 {
 	template <class... Arguments>
-	SimplificationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
+	OperationResult visit(BinaryOperation &binaryOperation, Term &term, Arguments &&... arguments)
 	{
-		if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

-		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Boolean &, Term &term, Arguments &&... arguments)
+	OperationResult visit(Boolean &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Function &function, Term &term, Arguments &&... arguments)
+	OperationResult visit(Function &function, Term &term, Arguments &&... arguments)
 	{
 		for (auto &argument : function.arguments)
-			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-				return SimplificationResult::Simplified;
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+				return OperationResult::Changed;

 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Integer &, Term &term, Arguments &&... arguments)
+	OperationResult visit(Integer &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
+	OperationResult visit(Interval &interval, Term &term, Arguments &&... arguments)
 	{
-		if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

-		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
-			return SimplificationResult::Simplified;
+		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
+			return OperationResult::Changed;

 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
+	OperationResult visit(SpecialInteger &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(String &, Term &term, Arguments &&... arguments)
+	OperationResult visit(String &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}

 	template <class... Arguments>
-	SimplificationResult visit(Variable &, Term &term, Arguments &&... arguments)
+	OperationResult visit(Variable &, Term &term, Arguments &&... arguments)
 	{
 		return T::accept(term, std::forward<Arguments>(arguments)...);
 	}
--- a/include/anthem/StatementVisitor.h
+++ b/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;
 			};
--- a/include/anthem/Tristate.h
+++ b/include/anthem/Tristate.h
@@ -1,24 +0,0 @@
-#ifndef __ANTHEM__TRISTATE_H
-#define __ANTHEM__TRISTATE_H
-
-namespace anthem
-{
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-//
-// Tristate
-//
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class Tristate
-{
-	True,
-	False,
-	Unknown,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-}
-
-#endif
--- a/include/anthem/Type.h
+++ b/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
--- a/include/anthem/Utils.h
+++ b/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
 {

@@ -20,6 +13,61 @@ namespace anthem
 constexpr const auto HeadVariablePrefix = "V";
 constexpr const auto BodyVariablePrefix = "X";
 constexpr const auto UserVariablePrefix = "U";
+constexpr const auto IntegerVariablePrefix = "N";
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class EvaluationResult
+{
+	True,
+	False,
+	Unknown,
+	Error,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class OperationResult
+{
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class Domain
+{
+	Noninteger,
+	Integer,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class SetSize
+{
+	Empty,
+	Unit,
+	Multi,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Type
+{
+	Domain domain{Domain::Unknown};
+	SetSize setSize{SetSize::Unknown};
+};

 ////////////////////////////////////////////////////////////////////////////////////////////////////

--- a/include/anthem/output/AST.h
+++ b/include/anthem/output/AST.h
@@ -35,6 +35,7 @@ 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;
 };
@@ -322,22 +323,6 @@ 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 &
 		{
@@ -350,11 +335,14 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec
 				matchingVariableID = emplaceResult.first;
 			}

-			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second) + domainSuffix();
+			const auto variableName = std::string(prefix) + std::to_string(matchingVariableID->second);

 			return (stream << output::Variable(variableName.c_str()));
 		};

+	if (variableDeclaration.domain == Domain::Integer)
+		return printVariableDeclaration(IntegerVariablePrefix, printContext.integerVariableIDs);
+
 	switch (variableDeclaration.type)
 	{
 		case VariableDeclaration::Type::UserDefined:
--- a/src/anthem/IntegerVariableDetection.cpp
+++ b/src/anthem/IntegerVariableDetection.cpp
@@ -5,6 +5,8 @@
 #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>

 namespace anthem
@@ -16,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;
 }
@@ -38,138 +40,24 @@ 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;
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-enum class OperationResult
+struct VariableDomainMapAccessor
 {
-	Unchanged,
-	Changed,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-enum class EvaluationResult
-{
-	True,
-	False,
-	Unknown,
-	Error,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct IsTermArithmeticVisitor
-{
-	static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, VariableDomainMap &variableDomainMap)
+	Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
 	{
-		const auto isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
-		const auto isRightArithmetic = isArithmetic(binaryOperation.right, variableDomainMap);
-
-		if (isLeftArithemtic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Boolean &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::Function &function, VariableDomainMap &)
-	{
-		switch (function.declaration->domain)
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Integer &, VariableDomainMap &)
-	{
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::Interval &interval, VariableDomainMap &variableDomainMap)
-	{
-		const auto isFromArithmetic = isArithmetic(interval.from, variableDomainMap);
-		const auto isToArithmetic = isArithmetic(interval.to, variableDomainMap);
-
-		if (isFromArithmetic == EvaluationResult::Error || isToArithmetic == EvaluationResult::Error)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
-			return EvaluationResult::Error;
-
-		if (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
-			return EvaluationResult::Unknown;
-
-		return EvaluationResult::True;
-	}
-
-	static EvaluationResult visit(const ast::SpecialInteger &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::String &, VariableDomainMap &)
-	{
-		return EvaluationResult::False;
-	}
-
-	static EvaluationResult visit(const ast::UnaryOperation &unaryOperation, VariableDomainMap &variableDomainMap)
-	{
-		const auto isArgumentArithmetic = isArithmetic(unaryOperation.argument, variableDomainMap);
-
-		switch (unaryOperation.operator_)
-		{
-			case ast::UnaryOperation::Operator::Absolute:
-				return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
-		}
-
-		return EvaluationResult::Unknown;
-	}
-
-	static EvaluationResult visit(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-	{
-		switch (domain(variable, variableDomainMap))
-		{
-			case ast::Domain::General:
-				return EvaluationResult::False;
-			case ast::Domain::Integer:
-				return EvaluationResult::True;
-			case ast::Domain::Unknown:
-				return EvaluationResult::Unknown;
-		}
-
-		return EvaluationResult::Unknown;
+		return domain(variable, variableDomainMap);
 	}
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
+Type type(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return term.accept(IsTermArithmeticVisitor(), variableDomainMap);
+	return type<VariableDomainMapAccessor>(term, variableDomainMap);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -234,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:
@@ -291,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;
 	}

@@ -359,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;
@@ -381,199 +278,205 @@ EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variab

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DetectIntegerVariablesVisitor
+template <class Functor>
+struct ForEachVariableDeclarationVisitor
 {
-	static OperationResult visit(ast::And &and_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::And &and_, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

 		for (auto &argument : and_.arguments)
-			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
+			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;

 		return operationResult;
 	}

-	static OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

-		if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == OperationResult::Changed)
+		if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

-		if (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == OperationResult::Changed)
+		if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

 		return operationResult;
 	}

-	static OperationResult visit(ast::Boolean &, ast::Formula &, VariableDomainMap &)
+	template <class... Arguments>
+	static OperationResult visit(ast::Boolean &, Arguments &&...)
 	{
 		return OperationResult::Unchanged;
 	}

-	static OperationResult visit(ast::Comparison &, ast::Formula &, VariableDomainMap &)
+	template <class... Arguments>
+	static OperationResult visit(ast::Comparison &, Arguments &&...)
 	{
 		return OperationResult::Unchanged;
 	}

-	static OperationResult visit(ast::Exists &exists, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

-		if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == OperationResult::Changed)
+		if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

 		for (auto &variableDeclaration : exists.variables)
-		{
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(exists.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(exists.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}

 		return operationResult;
 	}

-	static OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

-		if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == OperationResult::Changed)
+		if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

 		for (auto &variableDeclaration : forAll.variables)
-		{
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(forAll.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(forAll.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}

 		return operationResult;
 	}

-	static OperationResult visit(ast::Implies &implies, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

-		if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == OperationResult::Changed)
+		if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

-		if (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == OperationResult::Changed)
+		if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 			operationResult = OperationResult::Changed;

 		return operationResult;
 	}

-	static OperationResult visit(ast::In &, ast::Formula &, VariableDomainMap &)
+	template <class... Arguments>
+	static OperationResult visit(ast::In &, Arguments &&...)
 	{
 		return OperationResult::Unchanged;
 	}

-	static OperationResult visit(ast::Not &not_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
 	{
-		return detectIntegerVariables(not_.argument, definition, variableDomainMap);
+		return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
 	}

-	static OperationResult visit(ast::Or &or_, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	template <class... Arguments>
+	static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
 	{
 		auto operationResult = OperationResult::Unchanged;

 		for (auto &argument : or_.arguments)
-			if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed)
+			if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;

 		return operationResult;
 	}

-	static OperationResult visit(ast::Predicate &predicate, ast::Formula &, VariableDomainMap &)
+	template <class... Arguments>
+	static OperationResult visit(ast::Predicate &, Arguments &&...)
 	{
-		auto operationResult = OperationResult::Unchanged;
-
-		assert(predicate.arguments.size() == predicate.declaration->arity());
-
-		// Propagate integer domains from predicates to variables
-		for (size_t i = 0; i < predicate.arguments.size(); i++)
-		{
-			auto &variableArgument = predicate.arguments[i];
-			auto &parameter = predicate.declaration->parameters[i];
-
-			if (parameter.domain != ast::Domain::Integer)
-				continue;
-
-			if (!variableArgument.is<ast::Variable>())
-				continue;
-
-			auto &variable = variableArgument.get<ast::Variable>();
-
-			if (variable.declaration->domain == ast::Domain::Integer)
-				continue;
-
-			operationResult = OperationResult::Changed;
-			variable.declaration->domain = ast::Domain::Integer;
-		}
-
-		return operationResult;
+		return OperationResult::Unchanged;
 	}
 };

 ////////////////////////////////////////////////////////////////////////////////////////////////////

-OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+struct CheckIfDefinitionFalseFunctor
 {
-	return formula.accept(DetectIntegerVariablesVisitor(), definition, variableDomainMap);
-}
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto result = evaluate(definition, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfQuantifiedFormulaFalseFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto result = evaluate(quantifiedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfCompletedFormulaTrueFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = Domain::Noninteger;
+
+		const auto result = evaluate(completedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::True)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};

 ////////////////////////////////////////////////////////////////////////////////////////////////////

@@ -590,7 +493,10 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)

 		for (auto &completedFormula : completedFormulas)
 		{
-			if (detectIntegerVariables(completedFormula, completedFormula, variableDomainMap) == OperationResult::Changed)
+			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
+				operationResult = OperationResult::Changed;
+
+			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;

 			if (!completedFormula.is<ast::ForAll>())
@@ -609,11 +515,11 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
 			auto &predicate = biconditional.left.get<ast::Predicate>();
 			auto &definition = biconditional.right;

-			assert(predicate.arguments.size() == predicate.declaration->arity());
-
-			if (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
+			if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
 				operationResult = OperationResult::Changed;

+			assert(predicate.arguments.size() == predicate.declaration->arity());
+
 			for (size_t i = 0; i < predicate.arguments.size(); i++)
 			{
 				auto &variableArgument = predicate.arguments[i];
@@ -623,28 +529,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)

 				auto &variable = variableArgument.get<ast::Variable>();

-				if (parameter.domain != ast::Domain::Unknown)
-					continue;
-
-				clearVariableDomainMap(variableDomainMap);
-
-				auto result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-					continue;
-
-				// As a hypothesis, make the parameter’s domain noninteger
-				variableDomainMap[variable.declaration] = ast::Domain::General;
-
-				result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-				{
-					// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-					operationResult = OperationResult::Changed;
-					variable.declaration->domain = ast::Domain::Integer;
-					parameter.domain = ast::Domain::Integer;
-				}
+				parameter.domain = variable.declaration->domain;
 			}
 		}
 	}
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -4,8 +4,9 @@

 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
-#include <anthem/output/AST.h>
 #include <anthem/SimplificationVisitors.h>
+#include <anthem/Type.h>
+#include <anthem/output/AST.h>

 namespace anthem
 {
@@ -100,7 +101,7 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 template<class SimplificationRule>
-SimplificationResult simplify(ast::Formula &formula)
+OperationResult simplify(ast::Formula &formula)
 {
 	return SimplificationRule::apply(formula);
 }
@@ -108,10 +109,10 @@ SimplificationResult simplify(ast::Formula &formula)
 ////////////////////////////////////////////////////////////////////////////////////////////////////

 template<class FirstSimplificationRule, class SecondSimplificationRule, class... OtherSimplificationRules>
-SimplificationResult simplify(ast::Formula &formula)
+OperationResult simplify(ast::Formula &formula)
 {
-	if (simplify<FirstSimplificationRule>(formula) == SimplificationResult::Simplified)
-		return SimplificationResult::Simplified;
+	if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
+		return OperationResult::Changed;

 	return simplify<SecondSimplificationRule, OtherSimplificationRules...>(formula);
 }
@@ -122,19 +123,19 @@ struct SimplificationRuleExistsWithoutQuantifiedVariables
 {
 	static constexpr const auto Description = "exists () (F) === F";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &exists = formula.get<ast::Exists>();

 		if (!exists.variables.empty())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = std::move(exists.argument);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -144,20 +145,20 @@ struct SimplificationRuleTrivialAssignmentInExists
 {
 	static constexpr const auto Description = "exists X (X = Y) === #true";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		const auto &exists = formula.get<ast::Exists>();

 		if (!exists.argument.is<ast::Comparison>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		const auto &comparison = exists.argument.get<ast::Comparison>();

 		if (comparison.operator_ != ast::Comparison::Operator::Equal)
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
 			[&](const auto &variableDeclaration)
@@ -167,11 +168,11 @@ struct SimplificationRuleTrivialAssignmentInExists
 			});

 		if (matchingAssignment == exists.variables.cend())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = ast::Formula::make<ast::Boolean>(true);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -181,20 +182,20 @@ struct SimplificationRuleAssignmentInExists
 {
 	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &exists = formula.get<ast::Exists>();

 		if (!exists.argument.is<ast::And>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &and_ = exists.argument.get<ast::And>();
 		auto &arguments = and_.arguments;

-		auto simplificationResult = SimplificationResult::Unchanged;
+		auto simplificationResult = OperationResult::Unchanged;

 		for (auto i = exists.variables.begin(); i != exists.variables.end();)
 		{
@@ -225,7 +226,7 @@ struct SimplificationRuleAssignmentInExists
 				arguments.erase(j);

 				wasVariableReplaced = true;
-				simplificationResult = SimplificationResult::Simplified;
+				simplificationResult = OperationResult::Changed;

 				break;
 			}
@@ -249,19 +250,19 @@ struct SimplificationRuleEmptyConjunction
 {
 	static constexpr const auto Description = "[empty conjunction] === #true";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::And>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &and_ = formula.get<ast::And>();

 		if (!and_.arguments.empty())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = ast::Formula::make<ast::Boolean>(true);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -271,19 +272,19 @@ struct SimplificationRuleOneElementConjunction
 {
 	static constexpr const auto Description = "[conjunction of only F] === F";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::And>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &and_ = formula.get<ast::And>();

 		if (and_.arguments.size() != 1)
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = std::move(and_.arguments.front());

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -293,19 +294,19 @@ struct SimplificationRuleTrivialExists
 {
 	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Exists>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &exists = formula.get<ast::Exists>();

 		if (!exists.argument.is<ast::Boolean>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = std::move(exists.argument);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -315,21 +316,21 @@ struct SimplificationRuleInWithPrimitiveArguments
 {
 	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::In>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &in = formula.get<ast::In>();

 		assert(ast::isPrimitive(in.element));

 		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -339,10 +340,10 @@ struct SimplificationRuleSubsumptionInBiconditionals
 {
 	static constexpr const auto Description = "(F <-> (F and G)) === (F -> G)";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Biconditional>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &biconditional = formula.get<ast::Biconditional>();

@@ -353,7 +354,7 @@ struct SimplificationRuleSubsumptionInBiconditionals
 		const auto rightIsAnd = biconditional.right.is<ast::And>();

 		if (!(leftIsPredicate && rightIsAnd) && !(rightIsPredicate && leftIsAnd))
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &predicateSide = (leftIsPredicate ? biconditional.left : biconditional.right);
 		auto &andSide = (leftIsPredicate ? biconditional.right : biconditional.left);
@@ -367,13 +368,13 @@ struct SimplificationRuleSubsumptionInBiconditionals
 			});

 		if (matchingPredicate == and_.arguments.cend())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		and_.arguments.erase(matchingPredicate);

 		formula = ast::Formula::make<ast::Implies>(std::move(predicateSide), std::move(andSide));

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -383,21 +384,21 @@ struct SimplificationRuleDoubleNegation
 {
 	static constexpr const auto Description = "not not F === F";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &not_ = formula.get<ast::Not>();

 		if (!not_.argument.is<ast::Not>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &notNot = not_.argument.get<ast::Not>();

 		formula = std::move(notNot.argument);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -407,15 +408,15 @@ struct SimplificationRuleDeMorganForConjunctions
 {
 	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &not_ = formula.get<ast::Not>();

 		if (!not_.argument.is<ast::And>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &and_ = not_.argument.get<ast::And>();

@@ -424,7 +425,7 @@ struct SimplificationRuleDeMorganForConjunctions

 		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -434,21 +435,21 @@ struct SimplificationRuleImplicationFromDisjunction
 {
 	static constexpr const auto Description = "(not F or G) === (F -> G)";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Or>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &or_ = formula.get<ast::Or>();

 		if (or_.arguments.size() != 2)
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		const auto leftIsNot = or_.arguments[0].is<ast::Not>();
 		const auto rightIsNot = or_.arguments[1].is<ast::Not>();

 		if (leftIsNot == rightIsNot)
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
 		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
@@ -460,7 +461,7 @@ struct SimplificationRuleImplicationFromDisjunction

 		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
 	}
 };

@@ -470,15 +471,15 @@ struct SimplificationRuleNegatedComparison
 {
 	static constexpr const auto Description = "(not F [comparison] G) === (F [negated comparison] G)";

-	static SimplificationResult apply(ast::Formula &formula)
+	static OperationResult apply(ast::Formula &formula)
 	{
 		if (!formula.is<ast::Not>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &not_ = formula.get<ast::Not>();

 		if (!not_.argument.is<ast::Comparison>())
-			return SimplificationResult::Unchanged;
+			return OperationResult::Unchanged;

 		auto &comparison = not_.argument.get<ast::Comparison>();

@@ -506,7 +507,35 @@ struct SimplificationRuleNegatedComparison

 		formula = std::move(comparison);

-		return SimplificationResult::Simplified;
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleIntegerSetInclusion
+{
+	static constexpr const auto Description = "(F in G) === (F = G) if F and G are integer variables";
+
+	static OperationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::In>())
+			return OperationResult::Unchanged;
+
+		auto &in = formula.get<ast::In>();
+
+		const auto elementType = type(in.element);
+		const auto setType = type(in.set);
+
+		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
+		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
+		{
+			return OperationResult::Unchanged;
+		}
+
+		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return OperationResult::Changed;
 	}
 };

@@ -526,7 +555,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleNegatedComparison,
+		SimplificationRuleIntegerSetInclusion
 	>;

 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -535,7 +565,7 @@ const auto simplifyWithDefaultRules =
 struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<SimplifyFormulaVisitor>
 {
 	// Do nothing for all other types of expressions
-	static SimplificationResult accept(ast::Formula &formula)
+	static OperationResult accept(ast::Formula &formula)
 	{
 		return simplifyWithDefaultRules(formula);
 	}
@@ -545,7 +575,7 @@ struct SimplifyFormulaVisitor : public ast::FormulaSimplificationVisitor<Simplif

 void simplify(ast::Formula &formula)
 {
-	while (formula.accept(SimplifyFormulaVisitor(), formula) == SimplificationResult::Simplified);
+	while (formula.accept(SimplifyFormulaVisitor(), formula) == OperationResult::Changed);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/src/anthem/Translation.cpp
+++ b/src/anthem/Translation.cpp
@@ -147,14 +147,14 @@ 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()
 				<< output::Keyword("int")
 				<< "(" << predicateDeclaration->name
 				<< "/" << output::Number(predicateDeclaration->arity())
-				<< "@" << output::Number(i)
+				<< "@" << output::Number(i + 1)
 				<< ")." << std::endl;
 		}
 	}
Author	SHA1	Message	Date
Patrick Lühne	934dceac6e	Version bump for release 0.1.9 RC 4	2018-04-22 21:12:55 +02:00
Patrick Lühne	4a57a9e502	Prefix integer variables with “N” Instead of suffixing integer variables with “i,” this prefixes them with “N” instead to make it consistent with common mathematical notations.	2018-04-22 21:10:20 +02:00
Patrick Lühne	ea885f5fdb	Fix integer detection 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.	2018-04-22 17:04:15 +02:00
Patrick Lühne	92cd114cf8	Rename “general” domain to “noninteger” The “general” domain wasn’t really about general variables, but meant as a distinction from integer variables. For this reason, this commit renames the “general” domain to “noninteger.”	2018-04-22 14:57:16 +02:00
Patrick Lühne	2b62c6227d	Move Domain class to Utils header	2018-04-22 14:56:58 +02:00
Patrick Lühne	529aec15af	Add integer simplifications to change log	2018-04-21 18:48:57 +02:00
Patrick Lühne	d950b8ec1a	Add integer simplification rule This adds the rule “(F in G) === (F = G) if F and G are integer variables” to the simplification rule tableau	2018-04-21 18:12:43 +02:00
Patrick Lühne	97190ace71	Add integer check This adds a function to check whether a term evaluates to a singular integer.	2018-04-21 18:12:06 +02:00
Patrick Lühne	d6a811e363	Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.	2018-04-21 17:59:05 +02:00
Patrick Lühne	b1ca027de5	Consolidate commonly used enum classes This moves the commonly enum classes EvaluationResult, OperationResult, and Tristate to the Utils header file to avoid code duplication. Additionally, the SimplificationResult class is replaced by the semantically similar OperationResult.	2018-04-21 17:34:52 +02:00
Patrick Lühne	f190c28ea5	Add integer function declarations to change log	2018-04-21 17:26:15 +02:00
Patrick Lühne	28dbd407e2	Extend integer variable detection If making a variable noninteger turns the entire formula obtained from completion true, we can drop that statement and conclude that the variable is integer.	2018-04-21 17:26:15 +02:00
Patrick Lühne	9c792ff079	Fix incorrect index in output The indices printed in the output are meant to be indexed starting with 1 and not 0.	2018-04-21 17:09:45 +02:00
Patrick Lühne	f65d4dbbd8	Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.	2018-04-21 17:02:42 +02:00
Patrick Lühne	8f3ff23f38	Add to-do	2018-04-21 16:58:42 +02:00
Patrick Lühne	03c22d00f5	Remove unwanted detection rule This piece of code was responsible for propagating the domain of predicate parameters to argument variables. However, this approach doesn’t seem to be correct, which is why this commit removes it.	2018-04-21 16:58:42 +02:00