From 23624007eca85bfc9ed6bd8259e732774a5fed8b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 9 Apr 2018 23:35:02 +0200
Subject: [PATCH] Add new simplification rule
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This adds the rule “not not F === F” to the simplification rule tableau.
---
 src/anthem/Simplification.cpp            | 25 ++++++++++++++++++++++++
 tests/TestHiddenPredicateElimination.cpp |  3 ++-
 2 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index e4f69b4..7f6ffdb 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -379,9 +379,34 @@ struct SimplificationRuleSubsumptionInBiconditionals
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleDoubleNegation
+{
+	static constexpr const auto Description = "not not F === F";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &not_ = formula.get<ast::Not>();
+
+		if (!not_.argument.is<ast::Not>())
+			return SimplificationResult::Unchanged;
+
+		auto &notNot = not_.argument.get<ast::Not>();
+
+		formula = std::move(notNot.argument);
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto simplifyWithDefaultRules =
 	simplify
 	<
+		SimplificationRuleDoubleNegation,
 		SimplificationRuleTrivialAssignmentInExists,
 		SimplificationRuleAssignmentInExists,
 		SimplificationRuleEmptyConjunction,
diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp
index 04d0089..a6cfa0e 100644
--- a/tests/TestHiddenPredicateElimination.cpp
+++ b/tests/TestHiddenPredicateElimination.cpp
@@ -103,9 +103,10 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"#show a/1.";
 		anthem::translate("input", input, context);
 
+		// TODO: simplify further
 		CHECK(output.str() ==
 			"forall V1 (a(V1) <-> not d(V1))\n"
-			"forall V2 (d(V2) <-> not not d(V2))\n"
+			"forall V2 (d(V2) <-> d(V2))\n"
 			"forall V3 (e(V3) <-> e(V3))\n");
 	}