From 827d6e40fecf178861f15afd827226b866556ffe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Sun, 25 Mar 2018 19:33:07 +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 “[conjunction of only F] === F” to the
simplification rule tableau.
---
 src/anthem/Simplification.cpp | 35 +++++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 12 deletions(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index d7e8bd8..e85a369 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -251,6 +251,28 @@ struct SimplificationRuleEmptyConjunction
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleOneElementConjunction
+{
+	static constexpr const auto Description = "[conjunction of only F] === F";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = formula.get<ast::And>();
+
+		if (and_.arguments.size() != 1)
+			return SimplificationResult::Unchanged;
+
+		formula = std::move(and_.arguments.front());
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 struct SimplificationRuleTrivialExists
 {
 	static constexpr const auto Description = "exists ... ([#true/#false]) === [#true/#false]";
@@ -278,25 +300,14 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 	SimplificationRuleTrivialAssignmentInExists::apply(formula);
 	SimplificationRuleAssignmentInExists::apply(formula);
 
-	if (!exists.argument.is<ast::And>())
-		return;
-
-	auto &and_ = exists.argument.get<ast::And>();
-	auto &arguments = and_.arguments;
-
 	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)
-		exists.argument = std::move(arguments.front());
+	SimplificationRuleOneElementConjunction::apply(exists.argument);
 
 	// If there are still remaining variables, simplification is over
 	if (!exists.variables.empty())
 		return;
 
-	assert(!arguments.empty());
-
 	// If there is more than one element in the conjunction, replace the input formula with the conjunction
 	formula = std::move(exists.argument);
 }