2017-04-05 18:21:38 +02:00
|
|
|
#include <anthem/Completion.h>
|
|
|
|
|
2017-04-08 16:21:24 +02:00
|
|
|
#include <anthem/ASTUtils.h>
|
2017-04-05 18:21:38 +02:00
|
|
|
#include <anthem/ASTVisitors.h>
|
2017-04-10 16:32:12 +02:00
|
|
|
#include <anthem/Utils.h>
|
2017-04-05 18:21:38 +02:00
|
|
|
|
|
|
|
namespace anthem
|
|
|
|
{
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
//
|
|
|
|
// Completion
|
|
|
|
//
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
// Copies the parameters of a predicate
|
|
|
|
std::vector<ast::Variable> copyParameters(const ast::Predicate &predicate)
|
2017-04-06 17:46:16 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
std::vector<ast::Variable> parameters;
|
|
|
|
parameters.reserve(predicate.arity());
|
2017-04-06 17:46:16 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
for (const auto ¶meter : predicate.arguments)
|
|
|
|
{
|
|
|
|
assert(parameter.is<ast::Variable>());
|
|
|
|
parameters.emplace_back(ast::deepCopy(parameter.get<ast::Variable>()));
|
|
|
|
}
|
|
|
|
|
|
|
|
return parameters;
|
2017-04-06 17:46:16 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
// Builds the conjunction within the completed formula for a given predicate
|
|
|
|
ast::Formula buildCompletedFormulaDisjunction(const ast::Predicate &predicate, const std::vector<ast::Variable> ¶meters, const std::vector<ast::Formula> &formulas)
|
2017-04-06 17:46:16 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
auto disjunction = ast::Formula::make<ast::Or>();
|
2017-04-08 16:21:24 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
ast::VariableStack variableStack;
|
|
|
|
variableStack.push(¶meters);
|
2017-04-06 17:46:16 +02:00
|
|
|
|
|
|
|
// Build the conjunction of all formulas with the predicate as consequent
|
2017-04-10 16:32:12 +02:00
|
|
|
for (const auto &formula : formulas)
|
2017-04-06 17:46:16 +02:00
|
|
|
{
|
|
|
|
assert(formula.is<ast::Implies>());
|
2017-04-10 17:50:19 +02:00
|
|
|
const auto &implies = formula.get<ast::Implies>();
|
2017-04-08 18:25:59 +02:00
|
|
|
|
|
|
|
if (!implies.consequent.is<ast::Predicate>())
|
|
|
|
continue;
|
|
|
|
|
2017-04-06 17:46:16 +02:00
|
|
|
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
if (!ast::matches(predicate, otherPredicate))
|
2017-04-06 17:46:16 +02:00
|
|
|
continue;
|
|
|
|
|
2017-04-08 16:21:24 +02:00
|
|
|
auto variables = ast::collectFreeVariables(implies.antecedent, variableStack);
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
// TODO: avoid deep copies
|
2017-04-08 16:21:24 +02:00
|
|
|
if (variables.empty())
|
2017-04-10 16:32:12 +02:00
|
|
|
disjunction.get<ast::Or>().arguments.emplace_back(ast::deepCopy(implies.antecedent));
|
2017-04-08 16:21:24 +02:00
|
|
|
else
|
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
auto exists = ast::Formula::make<ast::Exists>(std::move(variables), ast::deepCopy(implies.antecedent));
|
|
|
|
disjunction.get<ast::Or>().arguments.emplace_back(std::move(exists));
|
2017-04-08 16:21:24 +02:00
|
|
|
}
|
2017-04-06 17:46:16 +02:00
|
|
|
}
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
return disjunction;
|
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
// Builds the quantified inner part of the completed formula
|
|
|
|
ast::Formula buildCompletedFormulaQuantified(ast::Predicate &&predicate, ast::Formula &&innerFormula)
|
|
|
|
{
|
|
|
|
assert(innerFormula.is<ast::Or>());
|
|
|
|
|
|
|
|
if (innerFormula.get<ast::Or>().arguments.empty())
|
|
|
|
return ast::Formula::make<ast::Not>(std::move(predicate));
|
2017-04-08 20:17:01 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
if (innerFormula.get<ast::Or>().arguments.size() == 1)
|
|
|
|
innerFormula = std::move(innerFormula.get<ast::Or>().arguments.front());
|
2017-04-08 20:17:01 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
if (innerFormula.is<ast::Boolean>())
|
2017-04-08 20:17:01 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
const auto &boolean = innerFormula.get<ast::Boolean>();
|
2017-04-08 20:17:01 +02:00
|
|
|
|
|
|
|
if (boolean.value == true)
|
2017-04-10 16:32:12 +02:00
|
|
|
return std::move(predicate);
|
2017-04-08 20:17:01 +02:00
|
|
|
else
|
2017-04-10 16:32:12 +02:00
|
|
|
return ast::Formula::make<ast::Not>(std::move(predicate));
|
2017-04-08 20:17:01 +02:00
|
|
|
}
|
2017-04-08 16:21:24 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
return ast::Formula::make<ast::Biconditional>(std::move(predicate), std::move(innerFormula));
|
|
|
|
}
|
2017-04-08 14:51:16 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
void completePredicate(ast::Predicate &&predicate, const std::vector<ast::Formula> &formulas, std::vector<ast::Formula> &completedFormulas)
|
|
|
|
{
|
|
|
|
auto parameters = copyParameters(predicate);
|
|
|
|
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction(predicate, parameters, formulas);
|
|
|
|
auto completedFormulaQuantified = buildCompletedFormulaQuantified(std::move(predicate), std::move(completedFormulaDisjunction));
|
|
|
|
|
|
|
|
if (parameters.empty())
|
2017-04-08 14:51:16 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
completedFormulas.emplace_back(std::move(completedFormulaQuantified));
|
2017-04-08 14:51:16 +02:00
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(parameters), std::move(completedFormulaQuantified));
|
|
|
|
completedFormulas.emplace_back(std::move(completedFormula));
|
2017-04-06 17:46:16 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
void completeIntegrityConstraint(const ast::Formula &formula, std::vector<ast::Formula> &completedFormulas)
|
2017-04-08 18:25:59 +02:00
|
|
|
{
|
|
|
|
assert(formula.is<ast::Implies>());
|
|
|
|
auto &implies = formula.get<ast::Implies>();
|
|
|
|
assert(implies.consequent.is<ast::Boolean>());
|
2017-04-10 16:32:12 +02:00
|
|
|
assert(implies.consequent.get<ast::Boolean>().value == false);
|
2017-04-08 18:25:59 +02:00
|
|
|
|
|
|
|
auto variables = ast::collectFreeVariables(implies.antecedent);
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
// TODO: avoid deep copies
|
|
|
|
auto argument = ast::Formula::make<ast::Not>(ast::deepCopy(implies.antecedent));
|
2017-04-08 18:25:59 +02:00
|
|
|
|
|
|
|
if (variables.empty())
|
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
completedFormulas.emplace_back(std::move(argument));
|
2017-04-08 18:25:59 +02:00
|
|
|
return;
|
|
|
|
}
|
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
|
|
|
|
completedFormulas.emplace_back(std::move(completedFormula));
|
2017-04-08 18:25:59 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
2017-04-05 18:21:38 +02:00
|
|
|
void complete(std::vector<ast::Formula> &formulas)
|
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
// Check whether formulas are in normal form
|
2017-04-06 17:46:16 +02:00
|
|
|
for (const auto &formula : formulas)
|
2017-04-05 18:21:38 +02:00
|
|
|
{
|
|
|
|
if (!formula.is<ast::Implies>())
|
|
|
|
throw std::runtime_error("cannot perform completion, formula not in normal form");
|
|
|
|
|
|
|
|
auto &implies = formula.get<ast::Implies>();
|
|
|
|
|
2017-04-08 18:25:59 +02:00
|
|
|
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");
|
2017-04-05 18:21:38 +02:00
|
|
|
}
|
2017-04-06 17:46:16 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
std::vector<const ast::Predicate *> predicates;
|
|
|
|
|
|
|
|
for (const auto &formula : formulas)
|
|
|
|
ast::collectPredicates(formula, predicates);
|
|
|
|
|
|
|
|
std::sort(predicates.begin(), predicates.end(),
|
|
|
|
[](const auto *lhs, const auto *rhs)
|
|
|
|
{
|
|
|
|
const auto order = std::strcmp(lhs->name.c_str(), rhs->name.c_str());
|
|
|
|
|
|
|
|
if (order != 0)
|
|
|
|
return order < 0;
|
|
|
|
|
|
|
|
return lhs->arity() < rhs->arity();
|
|
|
|
});
|
|
|
|
|
|
|
|
std::vector<ast::Formula> completedFormulas;
|
|
|
|
|
|
|
|
// Complete predicates
|
|
|
|
for (const auto *predicate : predicates)
|
2017-04-06 17:46:16 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
// Create the signature of the predicate
|
|
|
|
ast::Predicate signature(std::string(predicate->name));
|
|
|
|
signature.arguments.reserve(predicate->arguments.size());
|
2017-04-06 17:46:16 +02:00
|
|
|
|
2017-04-10 16:32:12 +02:00
|
|
|
for (std::size_t i = 0; i < predicate->arguments.size(); i++)
|
2017-04-08 18:25:59 +02:00
|
|
|
{
|
2017-04-10 16:32:12 +02:00
|
|
|
auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i + 1);
|
|
|
|
signature.arguments.emplace_back(ast::Term::make<ast::Variable>(std::move(variableName), ast::Variable::Type::Reserved));
|
2017-04-08 18:25:59 +02:00
|
|
|
}
|
2017-04-10 16:32:12 +02:00
|
|
|
|
|
|
|
completePredicate(std::move(signature), formulas, completedFormulas);
|
2017-04-06 17:46:16 +02:00
|
|
|
}
|
2017-04-10 16:32:12 +02:00
|
|
|
|
|
|
|
// Complete integrity constraints
|
|
|
|
for (const auto &formula : formulas)
|
|
|
|
{
|
|
|
|
auto &implies = formula.get<ast::Implies>();
|
|
|
|
|
|
|
|
if (!implies.consequent.is<ast::Boolean>())
|
|
|
|
continue;
|
|
|
|
|
|
|
|
const auto &boolean = implies.consequent.get<ast::Boolean>();
|
|
|
|
|
|
|
|
// Rules of the form “F -> #true” are useless
|
|
|
|
if (boolean.value == true)
|
|
|
|
continue;
|
|
|
|
|
|
|
|
completeIntegrityConstraint(formula, completedFormulas);
|
|
|
|
}
|
|
|
|
|
|
|
|
std::swap(formulas, completedFormulas);
|
2017-04-05 18:21:38 +02:00
|
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
}
|