From 5f8c144628840a0233499089c508e3c60abbce90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Mon, 12 Jun 2017 18:27:39 +0200
Subject: [PATCH] Fixed regression in simplifying predicates with more than one
 argument.

---
 src/anthem/Simplification.cpp            |  8 ++++++++
 tests/TestCompletion.cpp                 | 10 ++++++++++
 tests/TestHiddenPredicateElimination.cpp | 13 +++++++++++++
 3 files changed, 31 insertions(+)

diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index 7a95734..b6a4250 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -170,6 +170,14 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 		i++;
 	}
 
+	// 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;
+	}
+
 	// 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());
diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp
index 764faa1..19419b4 100644
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -166,4 +166,14 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 			"forall V1, V2 (a(V1, V2) <-> b(c((V1 + V2)), d((1 + V2))))\n"
 			"forall V3, V4 not b(V3, V4)\n");
 	}
+
+	SECTION("predicate with more than one argument")
+	{
+		input << "p(X, Y, Z).";
+		anthem::translate("input", input, context);
+
+		// TODO: simplify further
+		CHECK(output.str() ==
+			"forall V1, V2, V3 (p(V1, V2, V3) <-> #true)\n");
+	}
 }
diff --git a/tests/TestHiddenPredicateElimination.cpp b/tests/TestHiddenPredicateElimination.cpp
index 624768b..792e24b 100644
--- a/tests/TestHiddenPredicateElimination.cpp
+++ b/tests/TestHiddenPredicateElimination.cpp
@@ -171,4 +171,17 @@ TEST_CASE("[hidden predicate elimination] Hidden predicates are correctly elimin
 			"not (s and not t)\n"
 			"not (not #false and not #false and #false)\n");
 	}
+
+	SECTION("predicate with more than one argument is hidden correctly")
+	{
+		input <<
+			"a(X, Y, Z) :- p(X, Y, Z).\n"
+			"p(X, Y, Z).\n"
+			"#show a/3.";
+		anthem::translate("input", input, context);
+
+		// TODO: simplify further
+		CHECK(output.str() ==
+			"forall V1, V2, V3 (a(V1, V2, V3) <-> #true)\n");
+	}
 }