Version bump for release 0.1.9 RC 2

Add integer simplifications to change log
Add integer simplification rule
2018-04-21 19:00:11 +02:00 · 2018-04-21 18:48:57 +02:00 · 2018-04-21 18:12:43 +02:00 · 2018-04-21 18:12:06 +02:00 · 2018-04-21 17:59:05 +02:00 · 2018-04-21 17:34:52 +02:00
12 changed files with 577 additions and 400 deletions
--- a/CHANGELOG.md
+++ b/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)

--- 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.8+git" << std::endl;
+		std::cout << "anthem version 0.1.9-rc.2" << std::endl;
 		return EXIT_SUCCESS;
 	}

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

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

 namespace anthem
 {
--- a/include/anthem/Arithmetics.h
+++ b/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
--- 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/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/Utils.h
+++ b/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
--- a/src/anthem/IntegerVariableDetection.cpp
+++ b/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,
-	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)
+	ast::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);
 	}
 };

@@ -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);
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-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 != 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 (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 +535,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
@@ -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)
-		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,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);
 }

 ////////////////////////////////////////////////////////////////////////////////////////////////////
--- a/src/anthem/Translation.cpp
+++ b/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;
 		}
 	}
Author	SHA1	Message	Date
Patrick Lühne	d6821dd4de	Version bump for release 0.1.9 RC 2	2018-04-21 19:00:11 +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