From 69688d1d39eeef316418d93f383d1e56d7c64387 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 | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index aa9129b..33303fc 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -5,6 +5,7 @@
 #include <anthem/ASTCopy.h>
 #include <anthem/Equality.h>
 #include <anthem/SimplificationVisitors.h>
+#include <anthem/Type.h>
 #include <anthem/output/AST.h>
 
 namespace anthem
@@ -512,6 +513,34 @@ 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 elementType = type(in.element);
+		const auto setType = type(in.set);
+
+		if (elementType.domain != Domain::Integer || setType.domain != Domain::Integer
+		    || elementType.setSize != SetSize::Unit || setType.setSize != SetSize::Unit)
+		{
+			return OperationResult::Unchanged;
+		}
+
+		formula = ast::Formula::make<ast::Comparison>(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return OperationResult::Changed;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -526,7 +555,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleSubsumptionInBiconditionals,
 		SimplificationRuleDeMorganForConjunctions,
 		SimplificationRuleImplicationFromDisjunction,
-		SimplificationRuleNegatedComparison
+		SimplificationRuleNegatedComparison,
+		SimplificationRuleIntegerSetInclusion
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////