Add new simplification rule

This adds the rule “(not F or G) === (F -> G)” to the simplification
rule tableau.

src/anthem/Simplification.cpp

@@ -430,6 +430,42 @@ struct SimplificationRuleDeMorganForConjunctions
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+struct SimplificationRuleImplicationFromDisjunction
+{
+	static constexpr const auto Description = "(not F or G) === (F -> G)";
+
+	static SimplificationResult apply(ast::Formula &formula)
+	{
+		if (!formula.is<ast::Or>())
+			return SimplificationResult::Unchanged;
+
+		auto &or_ = formula.get<ast::Or>();
+
+		if (or_.arguments.size() != 2)
+			return SimplificationResult::Unchanged;
+
+		const auto leftIsNot = or_.arguments[0].is<ast::Not>();
+		const auto rightIsNot = or_.arguments[1].is<ast::Not>();
+
+		if (leftIsNot == rightIsNot)
+			return SimplificationResult::Unchanged;
+
+		auto &negativeSide = leftIsNot ? or_.arguments[0] : or_.arguments[1];
+		auto &positiveSide = leftIsNot ? or_.arguments[1] : or_.arguments[0];
+
+		assert(negativeSide.is<ast::Not>());
+		assert(!positiveSide.is<ast::Not>());
+
+		auto &negativeSideArgument = negativeSide.get<ast::Not>().argument;
+
+		formula = ast::Formula::make<ast::Implies>(std::move(negativeSideArgument), std::move(positiveSide));
+
+		return SimplificationResult::Simplified;
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 const auto simplifyWithDefaultRules =
 	simplify
 	<
@@ -442,7 +478,8 @@ const auto simplifyWithDefaultRules =
 		SimplificationRuleExistsWithoutQuantifiedVariables,
 		SimplificationRuleInWithPrimitiveArguments,
 		SimplificationRuleSubsumptionInBiconditionals,
-		SimplificationRuleDeMorganForConjunctions
+		SimplificationRuleDeMorganForConjunctions,
+		SimplificationRuleImplicationFromDisjunction
 	>;
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

@@ -153,7 +153,7 @@ 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 or covered(U2))\n"
+			"forall U2 (U2 in 1..n -> 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");
 	}
 

tests/TestHiddenPredicateElimination.cpp

@@ -168,7 +168,7 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 		CHECK(output.str() ==
 			"(s -> not #false)\n"
 			"(t -> not #false)\n"
-			"(not s or t)\n"
+			"(s -> t)\n"
 			"(#false or #false or not #false)\n");
 	}
 

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) or exists U2 color(U1, U2))\n"
+			"forall U1 (vertex(U1) -> 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");
 	}
 }