Added back completion support.

include/anthem/ASTUtils.h

@@ -4,6 +4,7 @@
 #include <experimental/optional>
 
 #include <anthem/AST.h>
+#include <anthem/ASTVisitors.h>
 
 namespace anthem
 {
@@ -36,12 +37,59 @@ class VariableStack
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula);
-std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula, VariableStack &variableStack);
-
 bool matches(const Predicate &lhs, const Predicate &rhs);
 void collectPredicates(const Formula &formula, std::vector<const Predicate *> &predicates);
 
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Replacing Variables
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Replaces all occurrences of a variable in a given term with another term
+struct ReplaceVariableInTermVisitor : public RecursiveTermVisitor<ReplaceVariableInTermVisitor>
+{
+	static void accept(Variable &variable, Term &, const VariableDeclaration *original, VariableDeclaration *replacement)
+	{
+		if (variable.declaration == original)
+			variable.declaration = replacement;
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(T &, Term &, const VariableDeclaration *, VariableDeclaration *)
+	{
+	}
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+// Replaces all occurrences of a variable in a given formula with a term
+struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
+{
+	static void accept(Comparison &comparison, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
+	{
+		comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement);
+		comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement);
+	}
+
+	static void accept(In &in, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
+	{
+		in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement);
+		in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement);
+	}
+
+	static void accept(Predicate &predicate, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
+	{
+		for (auto &argument : predicate.arguments)
+			argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement);
+	}
+
+	// Ignore all other types of expressions
+	template<class T>
+	static void accept(T &, Formula &, const VariableDeclaration *, VariableDeclaration *)
+	{
+	}
+};
+
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
 }

include/anthem/Completion.h

@@ -12,7 +12,7 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void complete(std::vector<ast::ScopedFormula> &scopedFormulas);
+std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas);
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 

src/anthem/ASTCopy.cpp

@@ -16,56 +16,6 @@ namespace ast
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-////////////////////////////////////////////////////////////////////////////////////////////////////
-// Replacing Variables
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-// Replaces all occurrences of a variable in a given term with another term
-struct ReplaceVariableInTermVisitor : public RecursiveTermVisitor<ReplaceVariableInTermVisitor>
-{
-	static void accept(Variable &variable, Term &, const VariableDeclaration *original, VariableDeclaration *replacement)
-	{
-		if (variable.declaration == original)
-			variable.declaration = replacement;
-	}
-
-	// Ignore all other types of expressions
-	template<class T>
-	static void accept(T &, Term &, const VariableDeclaration *, VariableDeclaration *)
-	{
-	}
-};
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-// Replaces all occurrences of a variable in a given formula with a term
-struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitor<ReplaceVariableInFormulaVisitor>
-{
-	static void accept(Comparison &comparison, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
-	{
-		comparison.left.accept(ReplaceVariableInTermVisitor(), comparison.left, original, replacement);
-		comparison.right.accept(ReplaceVariableInTermVisitor(), comparison.right, original, replacement);
-	}
-
-	static void accept(In &in, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
-	{
-		in.element.accept(ReplaceVariableInTermVisitor(), in.element, original, replacement);
-		in.set.accept(ReplaceVariableInTermVisitor(), in.set, original, replacement);
-	}
-
-	static void accept(Predicate &predicate, Formula &, const VariableDeclaration *original, VariableDeclaration *replacement)
-	{
-		for (auto &argument : predicate.arguments)
-			argument.accept(ReplaceVariableInTermVisitor(), argument, original, replacement);
-	}
-
-	// Ignore all other types of expressions
-	template<class T>
-	static void accept(T &, Formula &, const VariableDeclaration *, VariableDeclaration *)
-	{
-	}
-};
-
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Preparing Copying
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/ASTUtils.cpp

@@ -192,25 +192,6 @@ struct CollectFreeVariablesVisitor
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula)
-{
-	VariableStack variableStack;
-	return collectFreeVariables(formula, variableStack);
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
-std::vector<VariableDeclaration *> collectFreeVariables(Formula &formula, VariableStack &variableStack)
-{
-	std::vector<VariableDeclaration *> freeVariables;
-
-	formula.accept(CollectFreeVariablesVisitor(), variableStack, freeVariables);
-
-	return freeVariables;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicatesVisitor>
 {
 	static void accept(const Predicate &predicate, const Formula &, std::vector<const Predicate *> &predicates)

src/anthem/Completion.cpp

@@ -1,8 +1,10 @@
 	#include <anthem/Completion.h>
 
 #include <anthem/AST.h>
+#include <anthem/ASTCopy.h>
 #include <anthem/ASTUtils.h>
 #include <anthem/ASTVisitors.h>
+#include <anthem/Exception.h>
 #include <anthem/Utils.h>
 
 namespace anthem
@@ -14,33 +16,14 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-// Copies the parameters of a predicate
-std::vector<std::unique_ptr<ast::VariableDeclaration>> copyParameters(const ast::Predicate &predicate)
-{
-	std::vector<std::unique_ptr<ast::VariableDeclaration>> parameters;
-	/*parameters.reserve(predicate.arity());
-
-	for (const auto &argument : predicate.arguments)
-	{
-		assert(argument.is<ast::Variable>());
-		// TODO: reimplement
-		//parameters.emplace_back(ast::deepCopy(parameter.get<ast::VariableDeclaration>()));
-	}*/
-
-	return parameters;
-}
-
-////////////////////////////////////////////////////////////////////////////////////////////////////
-
 // Builds the conjunction within the completed formula for a given predicate
-ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, std::vector<std::unique_ptr<ast::VariableDeclaration>> &parameters, std::vector<ast::ScopedFormula> &scopedFormulas)
+ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const ast::VariableDeclarationPointers &parameters, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
 	auto disjunction = ast::Formula::make<ast::Or>();
 
-	/*ast::VariableStack variableStack;
+	assert(predicate.arguments.size() == parameters.size());
-	variableStack.push(&parameters);
 
-	// Build the conjunction of all formulas with the predicate as consequent
+	// Build the disjunction of all formulas with the predicate as consequent
 	for (auto &scopedFormula : scopedFormulas)
 	{
 		assert(scopedFormula.formula.is<ast::Implies>());
@@ -54,18 +37,36 @@ ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, s
 		if (!ast::matches(predicate, otherPredicate))
 			continue;
 
-		auto variables = ast::collectFreeVariables(implies.antecedent, variableStack);
+		assert(otherPredicate.arguments.size() == parameters.size());
 
-		// TODO: avoid deep copies
+		// Each formula with the predicate as its consequent currently has its own copy of the predicate’s parameters
-		// TODO: reimplement
+		// These need to be linked to the new, unique set of parameters
-		if (variables.empty())
+		for (size_t i = 0; i < parameters.size(); i++)
-			disjunction.get<ast::Or>().arguments.emplace_back(ast::deepCopy(implies.antecedent));
+		{
+			assert(otherPredicate.arguments[i].is<ast::Variable>());
+			const auto &otherVariable = otherPredicate.arguments[i].get<ast::Variable>();
+
+			scopedFormula.formula.accept(ast::ReplaceVariableInFormulaVisitor(), scopedFormula.formula, otherVariable.declaration, parameters[i].get());
+		}
+
+		// Remove all the head variables, because they are not free variables after completion
+		const auto isHeadVariable =
+			[](const auto &variableDeclaration)
+			{
+				return variableDeclaration->type == ast::VariableDeclaration::Type::Head;
+			};
+
+		auto &freeVariables = scopedFormula.freeVariables;
+		freeVariables.erase(std::remove_if(freeVariables.begin(), freeVariables.end(), isHeadVariable), freeVariables.end());
+
+		if (freeVariables.empty())
+			disjunction.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
 		else
 		{
-			auto exists = ast::Formula::make<ast::Exists>(std::move(variables), ast::deepCopy(implies.antecedent));
+			auto exists = ast::Formula::make<ast::Exists>(std::move(freeVariables), std::move(implies.antecedent));
 			disjunction.get<ast::Or>().arguments.emplace_back(std::move(exists));
 		}
-	}*/
+	}
 
 	return disjunction;
 }
@@ -77,7 +78,7 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 {
 	assert(innerFormula.is<ast::Or>());
 
-	/*if (innerFormula.get<ast::Or>().arguments.empty())
+	if (innerFormula.get<ast::Or>().arguments.empty())
 		return ast::Formula::make<ast::Not>(std::move(predicate));
 
 	if (innerFormula.get<ast::Or>().arguments.size() == 1)
@@ -91,72 +92,77 @@ ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Fo
 			return std::move(predicate);
 		else
 			return ast::Formula::make<ast::Not>(std::move(predicate));
-	}*/
+	}
 
 	return ast::Formula::make<ast::Biconditional>(std::move(predicate), std::move(innerFormula));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void completePredicate(ast::Predicate &&predicate, std::vector<ast::ScopedFormula> &scopedFormulas, std::vector<ast::ScopedFormula> &completedScopedFormulas)
+ast::Formula completePredicate(const ast::Predicate &predicate, std::vector<ast::ScopedFormula> &scopedFormulas)
 {
-	/*auto parameters = copyParameters(predicate);
+	// Create new set of parameters for the completed definition for the predicate
-	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, scopedFormulas);
+	ast::VariableDeclarationPointers parameters;
-	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction));
+	parameters.reserve(predicate.arguments.size());
 
-	if (parameters.empty())
+	std::vector<ast::Term> arguments;
+	arguments.reserve(predicate.arguments.size());
+
+	for (size_t i = 0; i < predicate.arguments.size(); i++)
 	{
-		completedFormulas.emplace_back(std::move(completedFormulaQuantified));
+		parameters.emplace_back(std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head));
-		return;
+		arguments.emplace_back(ast::Term::make<ast::Variable>(parameters.back().get()));
 	}
 
-	auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(parameters), std::move(completedFormulaQuantified));
+	ast::Predicate predicateCopy(std::string(predicate.name), std::move(arguments));
-	completedFormulas.emplace_back(std::move(completedFormula));*/
+
+	auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicateCopy, parameters, scopedFormulas);
+	auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicateCopy), std::move(completedFormulaDisjunction));
+
+	if (parameters.empty())
+		return completedFormulaQuantified;
+
+	return ast::Formula::make<ast::ForAll>(std::move(parameters), std::move(completedFormulaQuantified));
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void completeIntegrityConstraint(ast::Formula &formula, std::vector<ast::ScopedFormula> &)
+ast::Formula completeIntegrityConstraint(ast::ScopedFormula &scopedFormula)
 {
-	/*assert(formula.is<ast::Implies>());
+	assert(scopedFormula.formula.is<ast::Implies>());
-	auto &implies = formula.get<ast::Implies>();
+	auto &implies = scopedFormula.formula.get<ast::Implies>();
 	assert(implies.consequent.is<ast::Boolean>());
 	assert(implies.consequent.get<ast::Boolean>().value == false);
 
-	auto variables = ast::collectFreeVariables(implies.antecedent);
+	auto argument = ast::Formula::make<ast::Not>(std::move(implies.antecedent));
 
-	// TODO: avoid deep copies
+	auto &freeVariables = scopedFormula.freeVariables;
-	// TODO: reimplement
-	auto argument = ast::Formula::make<ast::Not>(ast::deepCopy(implies.antecedent));
 
-	if (variables.empty())
+	if (freeVariables.empty())
-	{
+		return argument;
-		completedFormulas.emplace_back(std::move(argument));
-		return;
-	}
 
-	auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
+	return ast::Formula::make<ast::ForAll>(std::move(freeVariables), std::move(argument));
-	completedFormulas.emplace_back(std::move(completedFormula));*/
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-void complete(std::vector<ast::ScopedFormula> &scopedFormulas)
+std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormulas)
 {
-	/*// Check whether formulas are in normal form
+	// Check whether formulas are in normal form
 	for (const auto &scopedFormula : scopedFormulas)
 	{
 		if (!scopedFormula.formula.is<ast::Implies>())
-			throw std::runtime_error("cannot perform completion, formula not in normal form");
+			throw CompletionException("cannot perform completion, formula not in normal form");
 
 		auto &implies = scopedFormula.formula.get<ast::Implies>();
 
 		if (!implies.consequent.is<ast::Predicate>() && !implies.consequent.is<ast::Boolean>())
-			throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
+			throw CompletionException("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
 	}
 
 	std::vector<const ast::Predicate *> predicates;
 
+	// Get a list of all predicates
 	for (const auto &scopedFormula : scopedFormulas)
 		ast::collectPredicates(scopedFormula.formula, predicates);
 
@@ -171,24 +177,11 @@ void complete(std::vector<ast::ScopedFormula> &scopedFormulas)
 			return lhs->arity() < rhs->arity();
 		});
 
-	std::vector<ast::ScopedFormula> completedScopedFormulas;
+	std::vector<ast::Formula> completedFormulas;
 
 	// Complete predicates
 	for (const auto *predicate : predicates)
-	{
+		completedFormulas.emplace_back(completePredicate(*predicate, scopedFormulas));
-		// Create the signature of the predicate
-		ast::Predicate signature(std::string(predicate->name));
-		signature.arguments.reserve(predicate->arguments.size());
-
-		// TODO: reimplement
-		for (std::size_t i = 0; i < predicate->arguments.size(); i++)
-		{
-			auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1);
-			signature.arguments.emplace_back(ast::Term::make<ast::Variable>(std::move(variableName), ast::VariableDeclaration::Type::Reserved));
-		}
-
-		completePredicate(std::move(signature), scopedFormulas, completedScopedFormulas);
-	}
 
 	// Complete integrity constraints
 	for (auto &scopedFormula : scopedFormulas)
@@ -204,10 +197,10 @@ void complete(std::vector<ast::ScopedFormula> &scopedFormulas)
 		if (boolean.value == true)
 			continue;
 
-		completeIntegrityConstraint(scopedFormula.formula, completedScopedFormulas);
+		completedFormulas.emplace_back(completeIntegrityConstraint(scopedFormula));
 	}
 
-	std::swap(scopedFormulas, completedScopedFormulas);*/
+	return completedFormulas;
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

src/anthem/Translation.cpp

@@ -59,16 +59,26 @@ void translate(const char *fileName, std::istream &stream, Context &context)
 		for (auto &scopedFormula : scopedFormulas)
 			simplify(scopedFormula.formula);
 
-	if (context.complete)
-		complete(scopedFormulas);
-
 	ast::PrintContext printContext;
 
+	if (!context.complete)
+	{
 		for (const auto &scopedFormula : scopedFormulas)
 		{
 			ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
 			context.logger.outputStream() << std::endl;
 		}
+
+		return;
+	}
+
+	auto completedFormulas = complete(std::move(scopedFormulas));
+
+	for (const auto &completedFormula : completedFormulas)
+	{
+		ast::print(context.logger.outputStream(), completedFormula, printContext);
+		context.logger.outputStream() << std::endl;
+	}
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////

tests/TestCompletion.cpp

@@ -8,7 +8,7 @@
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
-/*TEST_CASE("[completion] Rules are completed", "[completion]")
+TEST_CASE("[completion] Rules are completed", "[completion]")
 {
 	std::stringstream input;
 	std::stringstream output;
@@ -75,12 +75,12 @@
 		CHECK(output.str() ==
 			"not q\n"
 			"forall V1 not r(V1)\n"
-			"forall V1 not s(V1)\n"
+			"forall V2 not s(V2)\n"
 			"not t\n"
-			"forall V1 not u(V1)\n"
+			"forall V3 not u(V3)\n"
 			"not q\n"
 			"not r(5)\n"
-			"forall N not s(N)\n"
+			"forall U1 not s(U1)\n"
 			"not t\n"
 			"not u(5)\n");
 	}
@@ -126,7 +126,7 @@
 		CHECK(output.str() ==
 			"not p\n"
 			"forall V1 not q(V1)\n"
-			"forall V1, V2 not t(V1, V2)\n"
+			"forall V2, V3 not t(V2, V3)\n"
 			"not v\n");
 	}
 
@@ -140,12 +140,9 @@
 		anthem::translate("input", input, context);
 
 		CHECK(output.str() ==
-			"forall V1 (covered(V1) <-> exists I, S (V1 = I and in(I, S)))\n"
+			"forall V1 (covered(V1) <-> exists U1, U2 (V1 = U1 and in(U1, U2)))\n"
-			"forall V1, V2 (in(V1, V2) <-> (V1 in 1..n and V2 in 1..r and in(V1, V2)))\n"
+			"forall V2, V3 (in(V2, V3) <-> (V2 in 1..n and V3 in 1..r and in(V2, V3)))\n"
-			"forall I not (I in 1..n and not covered(I))\n"
+			"forall U3 not (U3 in 1..n and not covered(U3))\n"
-			"forall I, S, J not (in(I, S) and in(J, S) and exists X5 (X5 in (I + J) and in(X5, S)))\n");
+			"forall U4, U5, U6 not (in(U4, U5) and in(U6, U5) and exists X1 (X1 in (U4 + U6) and in(X1, U5)))\n");
 	}
-
-	// TODO: test collecting free variables
 }
-*/