From 7ae0a1f2894d51fad099dd9f5e0ba31e436681c7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Mon, 5 Jun 2017 03:58:39 +0200
Subject: [PATCH] Removed unnecessary parentheses after simplification.

---
 CHANGELOG.md                  |  1 +
 src/anthem/Simplification.cpp | 11 ++++-------
 tests/TestCompletion.cpp      |  2 +-
 3 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1f58dd3..5d45bda 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,7 @@ Features:
 Bug Fixes:
 
 * adds missing error message when attempting to read inaccessible file
+* removes unnecessary parentheses after simplification
 
 ## 0.1.5 (2017-05-04)
 
diff --git a/src/anthem/Simplification.cpp b/src/anthem/Simplification.cpp
index f4df751..7a95734 100644
--- a/src/anthem/Simplification.cpp
+++ b/src/anthem/Simplification.cpp
@@ -170,19 +170,16 @@ void simplify(ast::Exists &exists, ast::Formula &formula)
 		i++;
 	}
 
+	// 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());
+
 	// If there are still remaining variables, simplification is over
 	if (!exists.variables.empty())
 		return;
 
 	assert(!arguments.empty());
 
-	// If the argument now is a conjunction with just one element, directly replace the input formula with the argument
-	if (arguments.size() == 1)
-	{
-		formula = std::move(arguments.front());
-		return;
-	}
-
 	// If there is more than one element in the conjunction, replace the input formula with the conjunction
 	formula = std::move(exists.argument);
 }
diff --git a/tests/TestCompletion.cpp b/tests/TestCompletion.cpp
index 1d301dc..14b59b1 100644
--- a/tests/TestCompletion.cpp
+++ b/tests/TestCompletion.cpp
@@ -140,7 +140,7 @@ TEST_CASE("[completion] Rules are completed", "[completion]")
 		anthem::translate("input", input, context);
 
 		CHECK(output.str() ==
-			"forall V1 (covered(V1) <-> exists U1 (in(V1, U1)))\n"
+			"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 and in(V2, V3)))\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");