From 4fd143ef643ce7452bbefc45013adf148b5605bd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Mon, 5 Jun 2017 02:41:17 +0200
Subject: [PATCH] =?UTF-8?q?Added=20simplification=20rule=20=E2=80=9Cexists?=
 =?UTF-8?q?=20X=20(X=20=3D=20Y)=E2=80=9D=20=E2=86=92=20=E2=80=9C#true.?=
 =?UTF-8?q?=E2=80=9D?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/anthem/Simplification.cpp | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index 18dc3e3..58da9b3 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -101,6 +101,28 @@ struct ReplaceVariableInFormulaVisitor : public ast::RecursiveFormulaVisitor<Rep
 // The exists statement has to be of the form “exists <variables> <conjunction>”
 void simplify(ast::Exists &exists, ast::Formula &formula)
 {
+	// Simplify formulas like “exists X (X = Y)” to “#true”
+	// TODO: check that this covers all cases
+	if (exists.argument.is<ast::Comparison>())
+	{
+		const auto &comparison = exists.argument.get<ast::Comparison>();
+
+		if (comparison.operator_ != ast::Comparison::Operator::Equal)
+			return;
+
+		const auto matchingAssignment = std::find_if(exists.variables.cbegin(), exists.variables.cend(),
+			[&](const auto &variableDeclaration)
+			{
+				return matchesVariableDeclaration(comparison.left, *variableDeclaration)
+					|| matchesVariableDeclaration(comparison.right, *variableDeclaration);
+			});
+
+		if (matchingAssignment != exists.variables.cend())
+			formula = ast::Formula::make<ast::Boolean>(true);
+
+		return;
+	}
+
 	if (!exists.argument.is<ast::And>())
 		return;