Version bump for release 0.1.9 RC 2

This adds the rule “(F in G) === (F = G) if F and G are integer
variables” to the simplification rule tableau

CHANGELOG.md

@@ -1,11 +1,13 @@
 # Change Log
 
-## (unreleased)
+## 0.1.9 RC 2 (2018-04-21)
 
 ### 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)
 

app/main.cpp

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

include/anthem/AST.h

@@ -3,7 +3,6 @@
 
 #include <anthem/ASTForward.h>
 #include <anthem/Domain.h>
-#include <anthem/Tristate.h>
 
 namespace anthem
 {

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/Equality.h

@@ -3,7 +3,7 @@
 
 #include <anthem/AST.h>
 #include <anthem/ASTUtils.h>
-#include <anthem/Tristate.h>
+#include <anthem/Utils.h>
 
 namespace anthem
 {

include/anthem/Simplification.h

@@ -12,14 +12,6 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-enum class SimplificationResult
-{
-	Simplified,
-	Unchanged,
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 void simplify(ast::Formula &formula);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

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)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-				return SimplificationResult::Simplified;
+				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)
+		if (biconditional.left.accept(*this, biconditional.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			return OperationResult::Changed;
 
-		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+		if (biconditional.right.accept(*this, biconditional.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+		if (exists.argument.accept(*this, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+		if (forAll.argument.accept(*this, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+		if (implies.antecedent.accept(*this, implies.antecedent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			return OperationResult::Changed;
 
-		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+		if (implies.consequent.accept(*this, implies.consequent, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+		if (not_.argument.accept(*this, not_.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-				return SimplificationResult::Simplified;
+				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)
+		if (binaryOperation.left.accept(*this, binaryOperation.left, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			return OperationResult::Changed;
 
-		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+		if (binaryOperation.right.accept(*this, binaryOperation.right, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)
+			if (argument.accept(*this, argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-				return SimplificationResult::Simplified;
+				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)
+		if (interval.from.accept(*this, interval.from, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			return OperationResult::Changed;
 
-		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == SimplificationResult::Simplified)
+		if (interval.to.accept(*this, interval.to, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			return SimplificationResult::Simplified;
+			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)...);
 	}

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

include/anthem/Utils.h

@@ -23,6 +23,33 @@ constexpr const auto UserVariablePrefix = "U";
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+enum class Tristate
+{
+	True,
+	False,
+	Unknown,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class EvaluationResult
+{
+	True,
+	False,
+	Unknown,
+	Error,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+enum class OperationResult
+{
+	Unchanged,
+	Changed,
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 }
 
 #endif

src/anthem/IntegerVariableDetection.cpp

@@ -1,10 +1,12 @@
 #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/Utils.h>
 #include <anthem/output/AST.h>
 
 namespace anthem
@@ -43,125 +45,11 @@ void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-enum class OperationResult
+struct VariableDomainMapAccessor
 {
-	Unchanged,
+	ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
-	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)
 	{
-		const auto isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
+		return domain(variable, 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;
 	}
 };
 
@@ -169,7 +57,7 @@ struct IsTermArithmeticVisitor
 
 EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
 {
-	return term.accept(IsTermArithmeticVisitor(), variableDomainMap);
+	return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -381,199 +269,220 @@ EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variab
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap);
+template <class Functor>
-
+struct ForEachVariableDeclarationVisitor
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-struct DetectIntegerVariablesVisitor
 {
-	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 (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(exists.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(exists.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
 				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}
 
 		return operationResult;
 	}
 
-	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 (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
-			if (variableDeclaration->domain != ast::Domain::Unknown)
-				continue;
-
-			clearVariableDomainMap(variableDomainMap);
-
-			auto argumentResult = evaluate(forAll.argument, variableDomainMap);
-			auto definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				continue;
-			}
-
-			// As a hypothesis, make the parameter’s domain noninteger
-			variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
-
-			argumentResult = evaluate(forAll.argument, variableDomainMap);
-			definitionResult = evaluate(definition, variableDomainMap);
-
-			if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
-			    || definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
-			{
-				// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
 				operationResult = OperationResult::Changed;
-				variableDeclaration->domain = ast::Domain::Integer;
-			}
-		}
 
 		return operationResult;
 	}
 
-	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;
+		return 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;
 	}
 };
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-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 != ast::Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		auto result = evaluate(definition, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(definition, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = ast::Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfQuantifiedFormulaFalseFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != ast::Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		auto result = evaluate(quantifiedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(quantifiedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::False)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = ast::Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct CheckIfCompletedFormulaTrueFunctor
+{
+	OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
+		ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
+	{
+		if (variableDeclaration.domain != ast::Domain::Unknown)
+			return OperationResult::Unchanged;
+
+		clearVariableDomainMap(variableDomainMap);
+
+		auto result = evaluate(completedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::True)
+			return OperationResult::Unchanged;
+
+		// As a hypothesis, make the parameter’s domain noninteger
+		variableDomainMap[&variableDeclaration] = ast::Domain::General;
+
+		result = evaluate(completedFormula, variableDomainMap);
+
+		if (result == EvaluationResult::Error || result == EvaluationResult::True)
+		{
+			// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
+			variableDeclaration.domain = ast::Domain::Integer;
+			return OperationResult::Changed;
+		}
+
+		return OperationResult::Unchanged;
+	}
+};
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
@@ -590,7 +499,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 +521,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 (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
-
-			if (detectIntegerVariables(definition, 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 +535,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
 
 				auto &variable = variableArgument.get<ast::Variable>();
 
-				if (parameter.domain != ast::Domain::Unknown)
+				parameter.domain = variable.declaration->domain;
-					continue;
-
-				clearVariableDomainMap(variableDomainMap);
-
-				auto result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-					continue;
-
-				// As a hypothesis, make the parameter’s domain noninteger
-				variableDomainMap[variable.declaration] = ast::Domain::General;
-
-				result = evaluate(definition, variableDomainMap);
-
-				if (result == EvaluationResult::Error || result == EvaluationResult::False)
-				{
-					// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
-					operationResult = OperationResult::Changed;
-					variable.declaration->domain = ast::Domain::Integer;
-					parameter.domain = ast::Domain::Integer;
-				}
 			}
 		}
 	}

src/anthem/Simplification.cpp

@@ -2,10 +2,11 @@
 
 #include <optional>
 
+#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
-#include <anthem/output/AST.h>
 #include <anthem/SimplificationVisitors.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)
+	if (simplify<FirstSimplificationRule>(formula) == OperationResult::Changed)
-		return SimplificationResult::Simplified;
+		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,32 @@ 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 isElementInteger = isInteger(in.element);
+		const auto isSetInteger = isInteger(in.set);
+
+		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));
+
+		return OperationResult::Changed;
 	}
 };
 
@@ -526,7 +552,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleNegatedComparison,
+		SimplificationRuleIntegerSetInclusion
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
@@ -535,7 +562,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 +572,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);
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

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