From 7e3fc007c86a2714cb39b8cad7ef7653a70b4cd8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 25 Mar 2018 19:14:04 +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 “exists X (X = t and F(X)) === exists () (F(t))” to
the simplification rule tableau.
---
 src/anthem/Simplification.cpp | 116 +++++++++++++++++++++-------------
 1 file changed, 71 insertions(+), 45 deletions(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index b17ed03..a7560fc 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -161,58 +161,84 @@ struct SimplificationRuleTrivialExists
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// Simplifies exists statements by using the equivalence “exists X (X = t and F(X))” == “F(t)”
-// The exists statement has to be of the form “exists <variables> <conjunction>”
+struct SimplificationRuleAssignmentInExists
+{
+	static constexpr const auto Description = "exists X (X = t and F(X)) === exists () (F(t))";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Exists>())
+			return SimplificationResult::Unchanged;
+
+		auto &exists = formula.get<ast::Exists>();
+
+		if (!exists.argument.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = exists.argument.get<ast::And>();
+		auto &arguments = and_.arguments;
+
+		auto simplificationResult = SimplificationResult::Unchanged;
+
+		for (auto i = exists.variables.begin(); i != exists.variables.end();)
+		{
+			const auto &variableDeclaration = **i;
+
+			bool wasVariableReplaced = false;
+
+			// TODO: refactor
+			for (auto j = arguments.begin(); j != arguments.end(); j++)
+			{
+				auto &argument = *j;
+				// Find term that is equivalent to the given variable
+				auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
+
+				if (!assignedTerm)
+					continue;
+
+				// Replace all occurrences of the variable with the equivalent term
+				for (auto k = arguments.begin(); k != arguments.end(); k++)
+				{
+					if (k == j)
+						continue;
+
+					auto &otherArgument = *k;
+					otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
+				}
+
+				arguments.erase(j);
+
+				wasVariableReplaced = true;
+				simplificationResult = SimplificationResult::Simplified;
+
+				break;
+			}
+
+			if (wasVariableReplaced)
+			{
+				i = exists.variables.erase(i);
+				continue;
+			}
+
+			i++;
+		}
+
+		return simplificationResult;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void simplify(ast::Exists &exists, ast::Formula &formula)
 {
 	SimplificationRuleTrivialExists::apply(formula);
+	SimplificationRuleAssignmentInExists::apply(formula);
 
 	if (!exists.argument.is<ast::And>())
 		return;
 
-	auto &conjunction = exists.argument.get<ast::And>();
-	auto &arguments = conjunction.arguments;
-
-	// Simplify formulas of type “exists X (X = t and F(X))” to “F(t)”
-	for (auto i = exists.variables.begin(); i != exists.variables.end();)
-	{
-		const auto &variableDeclaration = **i;
-
-		bool wasVariableReplaced = false;
-
-		// TODO: refactor
-		for (auto j = arguments.begin(); j != arguments.end(); j++)
-		{
-			auto &argument = *j;
-			// Find term that is equivalent to the given variable
-			auto assignedTerm = extractAssignedTerm(argument, variableDeclaration);
-
-			if (!assignedTerm)
-				continue;
-
-			// Replace all occurrences of the variable with the equivalent term
-			for (auto k = arguments.begin(); k != arguments.end(); k++)
-			{
-				if (k == j)
-					continue;
-
-				auto &otherArgument = *k;
-				otherArgument.accept(ReplaceVariableInFormulaVisitor(), otherArgument, variableDeclaration, assignedTerm.value());
-			}
-
-			arguments.erase(j);
-			wasVariableReplaced = true;
-			break;
-		}
-
-		if (wasVariableReplaced)
-		{
-			i = exists.variables.erase(i);
-			continue;
-		}
-
-		i++;
-	}
+	auto &and_ = exists.argument.get<ast::And>();
+	auto &arguments = and_.arguments;
 
 	// If there are no arguments left, we had a formula of the form “exists X1, ..., Xn (X1 = Y1 and ... and Xn = Yn)”
 	// Such exists statements are useless and can be safely replaced with “#true”