From 6f7b021712eff0aa08fcf70c33720e9ed187c9a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 9 Apr 2018 23:38:58 +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 (F and G)) === (not F or not G)” to the
simplification rule tableau.
---
 src/anthem/Simplification.cpp            | 30 +++++++++++++++++++++++-
 tests/TestCompletion.cpp                 |  4 ++--
 tests/TestHiddenPredicateElimination.cpp |  4 ++--
 tests/TestPlaceholders.cpp               |  4 ++--
 4 files changed, 35 insertions(+), 7 deletions(-)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index 7f6ffdb..abb2bc6 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -403,6 +403,33 @@ struct SimplificationRuleDoubleNegation
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleDeMorganForConjunctions
+{
+	static constexpr const auto Description = "(not (F and G)) === (not F or not G)";
+
+	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::And>())
+			return SimplificationResult::Unchanged;
+
+		auto &and_ = not_.argument.get<ast::And>();
+
+		for (auto &argument : and_.arguments)
+			argument = ast::Formula::make<ast::Not>(std::move(argument));
+
+		formula = ast::Formula::make<ast::Or>(std::move(and_.arguments));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -414,7 +441,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleOneElementConjunction,
 		SimplificationRuleExistsWithoutQuantifiedVariables,
 		SimplificationRuleInWithPrimitiveArguments,
-		SimplificationRuleSubsumptionInBiconditionals
+		SimplificationRuleSubsumptionInBiconditionals,
+		SimplificationRuleDeMorganForConjunctions
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp
index 27ac73a..a5bad75 100644
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -153,8 +153,8 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		CHECK(output.str() ==
 			"forall V1 (covered(V1) <-> exists U1 in(V1, U1))\n"
 			"forall V2, V3 (in(V2, V3) -> (V2 in 1..n and V3 in 1..r))\n"
-			"forall U2 not (U2 in 1..n and not covered(U2))\n"
-			"forall U3, U4, U5 not (in(U3, U4) and in(U5, U4) and exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
+			"forall U2 (not U2 in 1..n or covered(U2))\n"
+			"forall U3, U4, U5 (not in(U3, U4) or not in(U5, U4) or not exists X1 (X1 in (U3 + U5) and in(X1, U4)))\n");
 	}
 
 	SECTION("binary operations with multiple variables")
diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp
index a6cfa0e..3b4fcf1 100644
--- a/tests/TestHiddenPredicateElimination.cpp
+++ b/tests/TestHiddenPredicateElimination.cpp
@@ -168,8 +168,8 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 		CHECK(output.str() ==
 			"(s -> not #false)\n"
 			"(t -> not #false)\n"
-			"not (s and not t)\n"
-			"not (not #false and not #false and #false)\n");
+			"(not s or t)\n"
+			"(#false or #false or not #false)\n");
 	}
 
 	SECTION("predicate with more than one argument is hidden correctly")
diff --git a/tests/TestPlaceholders.cpp b/tests/TestPlaceholders.cpp
index 810d3b9..3ce361f 100644
--- a/tests/TestPlaceholders.cpp
+++ b/tests/TestPlaceholders.cpp
@@ -56,7 +56,7 @@ TEST_CASE("[placeholders] Programs with placeholders are correctly completed", "
 
 		CHECK(output.str() ==
 			"forall V1, V2 (color(V1, V2) -> (vertex(V1) and color(V2)))\n"
-			"forall U1 not (vertex(U1) and not exists U2 color(U1, U2))\n"
-			"forall U3, U4, U5 not (color(U3, U4) and color(U5, U4) and edge(U3, U5))\n");
+			"forall U1 (not vertex(U1) or exists U2 color(U1, U2))\n"
+			"forall U3, U4, U5 (not color(U3, U4) or not color(U5, U4) or not edge(U3, U5))\n");
 	}
 }