From c4c3156e77838bc7a311105d9b2db99ab6403977 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 25 Mar 2018 20:35:22 +0200
Subject: [PATCH] Move simplification rule to tableau
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This moves the rule “[primitive A] in [primitive B] === A = B” to the
simplification rule tableau.
---
 src/anthem/Simplification.cpp | 33 ++++++++++++++++++++++++++-------
 1 file changed, 26 insertions(+), 7 deletions(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index 29eeb5d..2f2ab52 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -317,6 +317,30 @@ struct SimplificationRuleTrivialExists
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleInWithPrimitiveArguments
+{
+	static constexpr const auto Description = "[primitive A] in [primitive B] === A = B";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::In>())
+			return SimplificationResult::Unchanged;
+
+		auto &in = formula.get<ast::In>();
+
+		assert(ast::isPrimitive(in.element));
+
+		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
+			return SimplificationResult::Unchanged;
+
+		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void simplify(ast::Exists &exists, ast::Formula &formula)
 {
 	SimplificationRuleTrivialAssignmentInExists::apply(formula);
@@ -341,14 +365,9 @@ struct SimplifyFormulaVisitor : public ast::RecursiveFormulaVisitor<SimplifyForm
 	}
 
 	// Simplify formulas of type “A in B” to “A = B” if A and B are primitive
-	static void accept(ast::In &in, ast::Formula &formula)
+	static void accept(ast::In &, ast::Formula &formula)
 	{
-		assert(ast::isPrimitive(in.element));
-
-		if (!ast::isPrimitive(in.element) || !ast::isPrimitive(in.set))
-			return;
-
-		formula = ast::Comparison(ast::Comparison::Operator::Equal, std::move(in.element), std::move(in.set));
+		SimplificationRuleInWithPrimitiveArguments::apply(formula);
 	}
 
 	// Do nothing for all other types of expressions