From a23e248e7b1cd30149d6b1aa66000922a1e9a9f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Sat, 8 Apr 2017 14:51:16 +0200
Subject: [PATCH] Omitting the universal quantifier for completion if predicate
 is 0-ary.

---
 src/anthem/Completion.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp
index 7165dc3..ffb0ee1 100644
--- a/src/anthem/Completion.cpp
+++ b/src/anthem/Completion.cpp
@@ -70,6 +70,15 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
 			i++;
 	}
 
+	// Build the biconditional within the completed formula
+	auto biconditional = ast::Formula::make<ast::Biconditional>(ast::deepCopy(predicate), std::move(or_));
+
+	if (predicate.arguments.empty())
+	{
+		formulas[formulasBegin] = std::move(biconditional);
+		return;
+	}
+
 	// Copy the predicate’s arguments for the completed formula
 	std::vector<ast::Variable> variables;
 	variables.reserve(predicate.arguments.size());
@@ -80,11 +89,8 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
 		variables.emplace_back(ast::deepCopy(argument.get<ast::Variable>()));
 	}
 
-	// Build the completed formula
-	auto biconditional = ast::Formula::make<ast::Biconditional>(ast::deepCopy(predicate), std::move(or_));
 	auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(biconditional));
 
-	// TODO: reduce formula, for instance, if there are no variables in the for-all expression
 	formulas[formulasBegin] = std::move(completedFormula);
 }