From d950b8ec1a1f70b7b82b31b223de76471b0f4e8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sat, 21 Apr 2018 18:12:43 +0200
Subject: [PATCH] Add integer simplification rule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds the rule “(F in G) === (F = G) if F and G are integer
variables” to the simplification rule tableau
---
 src/anthem/Simplification.cpp | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index aa9129b..3d00eaf 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -2,6 +2,7 @@
 
 #include <optional>
 
+#include <anthem/Arithmetics.h>
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
 #include <anthem/SimplificationVisitors.h>
@@ -512,6 +513,31 @@ struct SimplificationRuleNegatedComparison
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+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;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -526,7 +552,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleNegatedComparison,
+		SimplificationRuleIntegerSetInclusion
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////