Fixed incorrectly translated choice rules with multiple elements in the aggregate.

include/anthem/StatementVisitor.h

@@ -47,7 +47,7 @@ struct StatementVisitor
 			return {};
 		}
 
-		// Print auxiliary variables replacing the head atom’s arguments
+		// Generate auxiliary variables replacing the head atom’s arguments
 		for (auto i = context.headTerms.cbegin(); i != context.headTerms.cend(); i++)
 		{
 			const auto &headTerm = **i;
@@ -60,7 +60,7 @@ struct StatementVisitor
 			antecedent.arguments.emplace_back(std::move(in));
 		}
 
-		// Print translated body literals
+		// Translate body literals
 		for (auto i = rule.body.cbegin(); i != rule.body.cend(); i++)
 		{
 			const auto &bodyLiteral = *i;
@@ -76,17 +76,56 @@ struct StatementVisitor
 			antecedent.arguments.emplace_back(std::move(argument.value()));
 		}
 
-		// Handle choice rules
+		std::vector<ast::Formula> formulas;
-		if (context.isChoiceRule)
-			antecedent.arguments.emplace_back(ast::deepCopy(consequent.value()));
 
-		// Use “true” as the consequent in case it is empty
+		if (!context.isChoiceRule)
-		if (antecedent.arguments.empty())
+			formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value())));
-			return {ast::Formula::make<ast::Implies>(ast::Boolean(true), std::move(consequent.value()))};
+		else
-		else if (antecedent.arguments.size() == 1)
+		{
-			return {ast::Formula::make<ast::Implies>(std::move(antecedent.arguments[0]), std::move(consequent.value()))};
+			const auto createFormula =
+				[&](ast::Formula &argument, bool isLastOne)
+				{
+					auto consequent = std::move(argument);
 
-		return {ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()))};
+					if (!isLastOne)
+						formulas.emplace_back(ast::Formula::make<ast::Implies>(ast::deepCopy(antecedent), std::move(consequent)));
+					else
+						formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent)));
+
+					auto &implies = formulas.back().get<ast::Implies>();
+					auto &antecedent = implies.antecedent.get<ast::And>();
+					antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent));
+				};
+
+			if (consequent.value().is<ast::Or>())
+			{
+				auto &disjunction = consequent.value().get<ast::Or>();
+
+				for (auto &argument : disjunction.arguments)
+					createFormula(argument, &argument == &disjunction.arguments.back());
+			}
+			// TODO: check whether this is really correct for all possible consequent types
+			else
+				createFormula(consequent.value(), true);
+		}
+
+		for (auto &formula : formulas)
+		{
+			auto &implies = formula.get<ast::Implies>();
+			auto &antecedent = implies.antecedent.get<ast::And>();
+
+			// Use “true” as the consequent in case it is empty
+			if (antecedent.arguments.empty())
+				implies.antecedent = ast::Formula::make<ast::Boolean>(true);
+			else if (antecedent.arguments.size() == 1)
+			{
+				// TODO: remove workaround
+				auto tmp = std::move(antecedent.arguments[0]);
+				implies.antecedent = std::move(tmp);
+			}
+		}
+
+		return formulas;
 	}
 
 	std::vector<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)

src/anthem/Translation.cpp

@@ -41,29 +41,24 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 
 	bool isFirstStatement = true;
 
-	const auto printFormula =
-		[&context, &isFirstStatement](const ast::Formula &formula)
-		{
-			if (!isFirstStatement)
-				context.logger.outputStream() << std::endl;
-
-			context.logger.outputStream() << formula << std::endl;
-
-			isFirstStatement = false;
-		};
-
 	const auto translateStatement =
-		[&context, &printFormula](const Clingo::AST::Statement &statement)
+		[&context, &isFirstStatement](const Clingo::AST::Statement &statement)
 		{
 			auto formulas = statement.data.accept(StatementVisitor(), statement, context);
 
+			if (!isFirstStatement)
+				context.logger.outputStream() << std::endl;
+
 			for (auto &formula : formulas)
 			{
 				if (context.simplify)
 					simplify(formula);
 
-				printFormula(formula);
+				context.logger.outputStream() << formula << std::endl;
 			}
+
+			if (!formulas.empty())
+				isFirstStatement = false;
 		};
 
 	const auto logger =

tests/TestTranslation.cpp

@@ -226,7 +226,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p; q}.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "((p or q) -> (p or q))\n");
+		REQUIRE(output.str() == "(p -> p)\n(q -> q)\n");
 	}
 
 	SECTION("choice rule (n-ary elements)")
@@ -234,7 +234,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p(1..3, N); q(2..4)}.";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and (p(V1, V2) or q(V3))) -> (p(V1, V2) or q(V3)))\n");
+		REQUIRE(output.str() == "((V1 in 1..3 and V2 in N and V3 in 2..4 and p(V1, V2)) -> p(V1, V2))\n((V1 in 1..3 and V2 in N and V3 in 2..4 and q(V3)) -> q(V3))\n");
 	}
 
 	SECTION("choice rule with body")
@@ -242,7 +242,7 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{p(M, N); q(P)} :- s(M, N, P).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and (p(V1, V2) or q(V3))) -> (p(V1, V2) or q(V3)))\n");
+		REQUIRE(output.str() == "((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and p(V1, V2)) -> p(V1, V2))\n((V1 in M and V2 in N and V3 in P and exists X1, X2, X3 (X1 in M and X2 in N and X3 in P and s(X1, X2, X3)) and q(V3)) -> q(V3))\n");
 	}
 
 	SECTION("choice rule with negation")
@@ -258,6 +258,6 @@ TEST_CASE("[translation] Rules are translated correctly", "[translation]")
 		input << "{not p(X, 1); not s} :- not q(X, 2).";
 		anthem::translate("input", input, context);
 
-		REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and (not p(V1, V2) or not s)) -> (not p(V1, V2) or not s))\n");
+		REQUIRE(output.str() == "((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not p(V1, V2)) -> not p(V1, V2))\n((V1 in X and V2 in 1 and exists X1, X2 (X1 in X and X2 in 2 and not q(X1, X2)) and not s) -> not s)\n");
 	}
 }