From 33f38b286ec09a3a61a0f36122cedda832de01f6 Mon Sep 17 00:00:00 2001
From: Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>
Date: Tue, 28 May 2024 18:31:18 +0200
Subject: [PATCH] Fix text output of minimize statements and aggregates.

* Use gringo-compatible syntax when printing minimize statements and
  sum/count aggregates.

* Fix output of empty projection and assumption directives.
---
 src/aspif_text.cpp  | 30 +++++++++++++++++-------------
 tests/test_text.cpp | 20 ++++++++++++++++----
 2 files changed, 33 insertions(+), 17 deletions(-)

diff --git a/src/aspif_text.cpp b/src/aspif_text.cpp
index ec90c1c..4c567ef 100644
--- a/src/aspif_text.cpp
+++ b/src/aspif_text.cpp
@@ -382,7 +382,7 @@ void AspifTextOutput::rule(Head_t ht, const AtomSpan& head, Weight_t bound, cons
 	}
 }
 void AspifTextOutput::minimize(Weight_t prio, const WeightLitSpan& lits) {
-	push(Directive_t::Minimize).push(lits).push(prio);
+	push(Directive_t::Minimize).push(prio).push(lits);
 }
 static bool isAtom(const StringSpan& s) {
 	std::size_t sz = size(s);
@@ -479,26 +479,29 @@ void AspifTextOutput::writeDirectives() {
 						break;
 					case Body_t::Count: // fall through
 					case Body_t::Sum:
-						os_ << sep << get<Weight_t>();
-						sep = "{";
-						for (uint32_t n = get<uint32_t>(); n--; sep = "; ") {
-							printName(os_ << sep, get<Lit_t>());
-							if (bt == Body_t::Sum) { os_ << "=" << get<Weight_t>(); }
+						os_ << sep << get<Weight_t>() << ' ';
+						sep = bt == Body_t::Count ? "#count{" : "#sum{";
+						for (uint32_t n = get<uint32_t>(), i = 1; n--; sep = "; ") {
+							os_ << sep;
+							Lit_t lit = get<Lit_t>();
+							if (bt == Body_t::Sum) { os_ << get<Weight_t>() << ','; }
+							printName(os_ << i++ << " : ", lit);
 						}
 						os_ << "}";
 						break;
 				}
 				break;
 			case Directive_t::Minimize:
-				sep = "#minimize{"; term = ".";
-				for (uint32_t n = get<uint32_t>(); n--; sep = "; ") {
-					printName(os_ << sep, get<Lit_t>());
-					os_ << "=" << get<Weight_t>();
+				term = "}.";
+				os_ << "#minimize{";
+				for (uint32_t prio = get<uint32_t>(), n = get<uint32_t>(), i = 1; n--; sep = "; ") {
+					Lit_t lit = get<Lit_t>();
+					printName(os_ << sep << get<Weight_t>() << '@' << static_cast<Weight_t>(prio) << ',' << i++ << " : ", lit);
 				}
-				os_ << "}@" << get<Weight_t>();
 				break;
 			case Directive_t::Project:
-				sep = "#project{"; term = "}.";
+				sep = ""; term = "}.";
+				os_ << "#project{";
 				for (uint32_t n = get<uint32_t>(); n--; sep = ", ") { printName(os_ << sep, get<Lit_t>()); }
 				break;
 			case Directive_t::Output:
@@ -519,7 +522,8 @@ void AspifTextOutput::writeDirectives() {
 				}
 				break;
 			case Directive_t::Assume:
-				sep = "#assume{"; term = "}.";
+				sep = ""; term = "}.";
+				os_ << "#assume{";
 				for (uint32_t n = get<uint32_t>(); n--; sep = ", ") { printName(os_ << sep, get<Lit_t>()); }
 				break;
 			case Directive_t::Heuristic:
diff --git a/tests/test_text.cpp b/tests/test_text.cpp
index 16dca4d..4201c9b 100644
--- a/tests/test_text.cpp
+++ b/tests/test_text.cpp
@@ -263,22 +263,24 @@ TEST_CASE("Text writer ", "[text]") {
 	SECTION("cardinality rule") {
 		input << "x1;x2 :- 1{not x3, x4}.\n#output foo : x1.\n#output bar : x3.";
 		read(prg, input);
-		REQUIRE(output.str() == "foo|x_2 :- 1{not bar; x_4}.\n");
+		REQUIRE(output.str() == "foo|x_2 :- 1 #count{1 : not bar; 2 : x_4}.\n");
 	}
 	SECTION("sum rule") {
 		input << "x1;x2 :- 3{not x3=2, x4, x5=1,x6=2}.\n#output foo : x1.\n#output bar : x3.";
 		read(prg, input);
-		REQUIRE(output.str() == "foo|x_2 :- 3{not bar=2; x_4=1; x_5=1; x_6=2}.\n");
+		REQUIRE(output.str() == "foo|x_2 :- 3 #sum{2,1 : not bar; 1,2 : x_4; 1,3 : x_5; 2,4 : x_6}.\n");
 	}
 	SECTION("convert sum rule to cardinality rule") {
 		input << "x1;x2 :- 3{not x3=2, x4=2, x5=2,x6=2}.\n#output foo : x1.\n#output bar : x3.";
 		read(prg, input);
-		REQUIRE(output.str() == "foo|x_2 :- 2{not bar; x_4; x_5; x_6}.\n");
+		REQUIRE(output.str() == "foo|x_2 :- 2 #count{1 : not bar; 2 : x_4; 3 : x_5; 4 : x_6}.\n");
 	}
 	SECTION("minimize rule") {
 		input << "#minimize{x1,x2=2,x3}.\n#minimize{not x1=3,not x2,not x3}@1.";
 		read(prg, input);
-		REQUIRE(output.str() == "#minimize{x_1=1; x_2=2; x_3=1}@0.\n#minimize{not x_1=3; not x_2=1; not x_3=1}@1.\n");
+		REQUIRE(output.str() ==
+		        "#minimize{1@0,1 : x_1; 2@0,2 : x_2; 1@0,3 : x_3}.\n#minimize{3@1,1 : not x_1; 1@1,2 : not "
+		        "x_2; 1@1,3 : not x_3}.\n");
 	}
 	SECTION("output statements") {
 		input << "{x1;x2}.\n#output foo.\n#output bar : x1.\n#output \"Hello World\" : x2, not x1.";
@@ -304,11 +306,21 @@ TEST_CASE("Text writer ", "[text]") {
 			REQUIRE(output.str() == "#external x_1. [true]\n#external x_2. [free]\n#external x_3. [release]\n");
 		}
 	}
+	SECTION("empty assumption directive") {
+		input << "#assume{}.";
+		read(prg, input);
+		REQUIRE(output.str() == "#assume{}.\n");
+	}
 	SECTION("assumption directive") {
 		input << "#assume{x1,not x2,x3}.";
 		read(prg, input);
 		REQUIRE(output.str() == "#assume{x_1, not x_2, x_3}.\n");
 	}
+	SECTION("empty projection directive") {
+		input << "#project{}.";
+		read(prg, input);
+		REQUIRE(output.str() == "#project{}.\n");
+	}
 	SECTION("projection directive") {
 		input << "#project{x1,x2,x3}.";
 		read(prg, input);