From 811eb3054cb29d147c79b06d234906b0a86b4f86 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Thu, 6 Apr 2017 17:46:16 +0200
Subject: [PATCH] Partly implemented completion.

---
 include/anthem/AST.h      |  5 +++
 src/anthem/Completion.cpp | 90 ++++++++++++++++++++++++++++++++++++++-
 2 files changed, 94 insertions(+), 1 deletion(-)

diff --git a/include/anthem/AST.h b/include/anthem/AST.h
index d36cae0..f12a5a8 100644
--- a/include/anthem/AST.h
+++ b/include/anthem/AST.h
@@ -174,6 +174,11 @@ struct Predicate
 	{
 	}
 
+	std::size_t arity() const
+	{
+		return arguments.size();
+	}
+
 	std::string name;
 	std::vector<Term> arguments;
 };
diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp
index dce67bb..7165dc3 100644
--- a/src/anthem/Completion.cpp
+++ b/src/anthem/Completion.cpp
@@ -11,9 +11,88 @@ namespace anthem
 //
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 
+// Checks that two matching predicates (same name, same arity) have the same arguments
+void checkMatchingPredicates(const ast::Term &lhs, const ast::Term &rhs)
+{
+	if (!lhs.is<ast::Variable>() || !rhs.is<ast::Variable>())
+		throw std::runtime_error("cannot preform completion, only variables supported in predicates currently");
+
+	if (lhs.get<ast::Variable>().name != rhs.get<ast::Variable>().name)
+		throw std::runtime_error("cannot perform completion, inconsistent predicate argument naming");
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula> &formulas, std::size_t formulasBegin)
+{
+	// Check that predicate is in normal form
+	for (auto i = formulasBegin; i < formulas.size(); i++)
+	{
+		auto &formula = formulas[i];
+		assert(formula.is<ast::Implies>());
+		auto &implies = formula.get<ast::Implies>();
+		assert(implies.consequent.is<ast::Predicate>());
+		auto &otherPredicate = implies.consequent.get<ast::Predicate>();
+
+		if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
+			continue;
+
+		for (std::size_t i = 0; i < predicate.arguments.size(); i++)
+			checkMatchingPredicates(predicate.arguments[i], otherPredicate.arguments[i]);
+	}
+
+	auto or_ = ast::Formula::make<ast::Or>();
+
+	// Build the conjunction of all formulas with the predicate as consequent
+	for (auto i = formulasBegin; i < formulas.size();)
+	{
+		auto &formula = formulas[i];
+		assert(formula.is<ast::Implies>());
+		auto &implies = formula.get<ast::Implies>();
+		assert(implies.consequent.is<ast::Predicate>());
+		auto &otherPredicate = implies.consequent.get<ast::Predicate>();
+
+		if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
+		{
+			i++;
+			continue;
+		}
+
+		// TODO: implement variable lists
+		std::vector<ast::Variable> variables = {ast::Variable("dummy", ast::Variable::Type::UserDefined)};
+		auto exists = ast::Formula::make<ast::Exists>(std::move(variables), std::move(implies.antecedent));
+
+		or_.get<ast::Or>().arguments.emplace_back(exists);
+
+		if (i > formulasBegin)
+			formulas.erase(formulas.begin() + i);
+		else
+			i++;
+	}
+
+	// Copy the predicate’s arguments for the completed formula
+	std::vector<ast::Variable> variables;
+	variables.reserve(predicate.arguments.size());
+
+	for (const auto &argument : predicate.arguments)
+	{
+		assert(argument.is<ast::Variable>());
+		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);
+}
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
 void complete(std::vector<ast::Formula> &formulas)
 {
-	for (auto &formula : formulas)
+	for (const auto &formula : formulas)
 	{
 		if (!formula.is<ast::Implies>())
 			throw std::runtime_error("cannot perform completion, formula not in normal form");
@@ -23,6 +102,15 @@ void complete(std::vector<ast::Formula> &formulas)
 		if (!implies.consequent.is<ast::Predicate>())
 			throw std::runtime_error("cannot perform completion, only single predicates supported as formula consequent currently");
 	}
+
+	for (std::size_t i = 0; i < formulas.size(); i++)
+	{
+		auto &formula = formulas[i];
+		auto &implies = formula.get<ast::Implies>();
+		auto &predicate = implies.consequent.get<ast::Predicate>();
+
+		completePredicate(predicate, formulas, i);
+	}
 }
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////