From 4a85fc4b23e4d311cfaead8146d2586f9b7364bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 25 Mar 2018 19:29:46 +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 ... ([#true/#false]) === [#true/#false]” to
the simplification rule tableau along with “[empty conjunction] ===
---
 src/anthem/Simplification.cpp | 57 +++++++++++++++++++++++++++++------
 1 file changed, 48 insertions(+), 9 deletions(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index a7560fc..d7e8bd8 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -124,7 +124,7 @@ SimplificationResult simplify(ast::Formula &formula)
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-struct SimplificationRuleTrivialExists
+struct SimplificationRuleTrivialAssignmentInExists
 {
 	static constexpr const auto Description = "exists X (X = Y) === #true";
 
@@ -229,9 +229,53 @@ struct SimplificationRuleAssignmentInExists
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleEmptyConjunction
+{
+	static constexpr const auto Description = "[empty conjunction] === #true";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = formula.get<ast::And>();
+
+		if (!and_.arguments.empty())
+			return SimplificationResult::Unchanged;
+
+		formula = ast::Formula::make<ast::Boolean>(true);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct SimplificationRuleTrivialExists
+{
+	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
+
+	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::Boolean>())
+			return SimplificationResult::Unchanged;
+
+		formula = std::move(exists.argument);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void simplify(ast::Exists &exists, ast::Formula &formula)
 {
-	SimplificationRuleTrivialExists::apply(formula);
+	SimplificationRuleTrivialAssignmentInExists::apply(formula);
 	SimplificationRuleAssignmentInExists::apply(formula);
 
 	if (!exists.argument.is<ast::And>())
@@ -240,13 +284,8 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 	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”
-	if (arguments.empty())
-	{
-		formula = ast::Formula::make<ast::Boolean>(true);
-		return;
-	}
+	SimplificationRuleEmptyConjunction::apply(exists.argument);
+	SimplificationRuleTrivialExists::apply(formula);
 
 	// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
 	if (arguments.size() == 1)