Refactored implementation of completion.
This commit is contained in:
@@ -194,5 +194,44 @@ std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct CollectPredicatesVisitor : public RecursiveFormulaVisitor<CollectPredicatesVisitor>
|
||||
{
|
||||
static void accept(const ast::Predicate &predicate, const ast::Formula &, std::vector<const ast::Predicate *> &predicates)
|
||||
{
|
||||
const auto predicateMatches =
|
||||
[&predicate](const auto *otherPredicate)
|
||||
{
|
||||
return matches(predicate, *otherPredicate);
|
||||
};
|
||||
|
||||
if (std::find_if(predicates.cbegin(), predicates.cend(), predicateMatches) == predicates.cend())
|
||||
predicates.emplace_back(&predicate);
|
||||
}
|
||||
|
||||
// Ignore all other types of expressions
|
||||
template<class T>
|
||||
static void accept(const T &, const ast::Formula &, std::vector<const ast::Predicate *> &)
|
||||
{
|
||||
}
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
bool matches(const ast::Predicate &lhs, const ast::Predicate &rhs)
|
||||
{
|
||||
return (lhs.name == rhs.name && lhs.arity() == rhs.arity());
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// TODO: remove const_cast
|
||||
void collectPredicates(const ast::Formula &formula, std::vector<const ast::Predicate *> &predicates)
|
||||
{
|
||||
auto &formulaMutable = const_cast<ast::Formula &>(formula);
|
||||
formulaMutable.accept(CollectPredicatesVisitor(), formulaMutable, predicates);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
@@ -2,6 +2,7 @@
|
||||
|
||||
#include <anthem/ASTUtils.h>
|
||||
#include <anthem/ASTVisitors.h>
|
||||
#include <anthem/Utils.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
@@ -12,163 +13,133 @@ 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)
|
||||
// Copies the parameters of a predicate
|
||||
std::vector<ast::Variable> copyParameters(const ast::Predicate &predicate)
|
||||
{
|
||||
if (!lhs.is<ast::Variable>() || !rhs.is<ast::Variable>())
|
||||
throw std::runtime_error("cannot preform completion, only variables supported in predicates currently");
|
||||
std::vector<ast::Variable> parameters;
|
||||
parameters.reserve(predicate.arity());
|
||||
|
||||
if (lhs.get<ast::Variable>().name != rhs.get<ast::Variable>().name)
|
||||
throw std::runtime_error("cannot perform completion, inconsistent predicate argument naming");
|
||||
for (const auto ¶meter : predicate.arguments)
|
||||
{
|
||||
assert(parameter.is<ast::Variable>());
|
||||
parameters.emplace_back(ast::deepCopy(parameter.get<ast::Variable>()));
|
||||
}
|
||||
|
||||
return parameters;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula> &formulas, std::size_t &formulaIndex)
|
||||
// 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)
|
||||
{
|
||||
// Check that predicate is in normal form
|
||||
for (auto i = formulaIndex; i < formulas.size(); i++)
|
||||
{
|
||||
auto &formula = formulas[i];
|
||||
assert(formula.is<ast::Implies>());
|
||||
auto &implies = formula.get<ast::Implies>();
|
||||
auto disjunction = ast::Formula::make<ast::Or>();
|
||||
|
||||
if (!implies.consequent.is<ast::Predicate>())
|
||||
continue;
|
||||
|
||||
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]);
|
||||
}
|
||||
|
||||
// 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>()));
|
||||
}
|
||||
|
||||
auto or_ = ast::Formula::make<ast::Or>();
|
||||
ast::VariableStack variableStack;
|
||||
variableStack.push(¶meters);
|
||||
|
||||
// Build the conjunction of all formulas with the predicate as consequent
|
||||
for (auto i = formulaIndex; i < formulas.size();)
|
||||
for (const auto &formula : formulas)
|
||||
{
|
||||
auto &formula = formulas[i];
|
||||
assert(formula.is<ast::Implies>());
|
||||
auto &implies = formula.get<ast::Implies>();
|
||||
|
||||
if (!implies.consequent.is<ast::Predicate>())
|
||||
{
|
||||
i++;
|
||||
continue;
|
||||
}
|
||||
|
||||
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
||||
|
||||
if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
|
||||
{
|
||||
i++;
|
||||
if (!ast::matches(predicate, otherPredicate))
|
||||
continue;
|
||||
}
|
||||
|
||||
ast::VariableStack variableStack;
|
||||
variableStack.push(&variables);
|
||||
|
||||
auto variables = ast::collectFreeVariables(implies.antecedent, variableStack);
|
||||
|
||||
// TODO: avoid deep copies
|
||||
if (variables.empty())
|
||||
or_.get<ast::Or>().arguments.emplace_back(std::move(implies.antecedent));
|
||||
disjunction.get<ast::Or>().arguments.emplace_back(ast::deepCopy(implies.antecedent));
|
||||
else
|
||||
{
|
||||
auto exists = ast::Formula::make<ast::Exists>(std::move(variables), std::move(implies.antecedent));
|
||||
or_.get<ast::Or>().arguments.emplace_back(std::move(exists));
|
||||
auto exists = ast::Formula::make<ast::Exists>(std::move(variables), ast::deepCopy(implies.antecedent));
|
||||
disjunction.get<ast::Or>().arguments.emplace_back(std::move(exists));
|
||||
}
|
||||
|
||||
if (i > formulaIndex)
|
||||
formulas.erase(formulas.begin() + i);
|
||||
else
|
||||
i++;
|
||||
}
|
||||
|
||||
auto biconditionalRight = std::move(or_);
|
||||
|
||||
// If the disjunction contains only one element, drop the enclosing disjunction
|
||||
if (biconditionalRight.get<ast::Or>().arguments.size() == 1)
|
||||
biconditionalRight = biconditionalRight.get<ast::Or>().arguments.front();
|
||||
|
||||
// If the biconditional would be of the form “F <-> true” or “F <-> false,” simplify the output
|
||||
if (biconditionalRight.is<ast::Boolean>())
|
||||
{
|
||||
const auto &boolean = biconditionalRight.get<ast::Boolean>();
|
||||
|
||||
if (boolean.value == true)
|
||||
formulas[formulaIndex] = ast::deepCopy(predicate);
|
||||
else
|
||||
formulas[formulaIndex] = ast::Formula::make<ast::Not>(ast::deepCopy(predicate));
|
||||
|
||||
formulaIndex++;
|
||||
return;
|
||||
}
|
||||
|
||||
// Build the biconditional within the completed formula
|
||||
auto biconditional = ast::Formula::make<ast::Biconditional>(ast::deepCopy(predicate), std::move(biconditionalRight));
|
||||
|
||||
if (predicate.arguments.empty())
|
||||
{
|
||||
formulas[formulaIndex] = std::move(biconditional);
|
||||
formulaIndex++;
|
||||
return;
|
||||
}
|
||||
|
||||
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(biconditional));
|
||||
|
||||
formulas[formulaIndex] = std::move(completedFormula);
|
||||
formulaIndex++;
|
||||
return disjunction;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void completeBoolean(std::vector<ast::Formula> &formulas, std::size_t &formulaIndex)
|
||||
// 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));
|
||||
|
||||
if (innerFormula.get<ast::Or>().arguments.size() == 1)
|
||||
innerFormula = std::move(innerFormula.get<ast::Or>().arguments.front());
|
||||
|
||||
if (innerFormula.is<ast::Boolean>())
|
||||
{
|
||||
const auto &boolean = innerFormula.get<ast::Boolean>();
|
||||
|
||||
if (boolean.value == true)
|
||||
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, 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())
|
||||
{
|
||||
completedFormulas.emplace_back(std::move(completedFormulaQuantified));
|
||||
return;
|
||||
}
|
||||
|
||||
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(parameters), std::move(completedFormulaQuantified));
|
||||
completedFormulas.emplace_back(std::move(completedFormula));
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void completeIntegrityConstraint(const ast::Formula &formula, std::vector<ast::Formula> &completedFormulas)
|
||||
{
|
||||
auto &formula = formulas[formulaIndex];
|
||||
assert(formula.is<ast::Implies>());
|
||||
auto &implies = formula.get<ast::Implies>();
|
||||
assert(implies.consequent.is<ast::Boolean>());
|
||||
auto &boolean = implies.consequent.get<ast::Boolean>();
|
||||
assert(implies.consequent.get<ast::Boolean>().value == false);
|
||||
|
||||
auto variables = ast::collectFreeVariables(implies.antecedent);
|
||||
|
||||
// Implications of the form “T -> true” are useless
|
||||
if (boolean.value == true)
|
||||
{
|
||||
formulas.erase(formulas.begin() + formulaIndex);
|
||||
return;
|
||||
}
|
||||
|
||||
auto argument = ast::Formula::make<ast::Not>(std::move(implies.antecedent));
|
||||
// TODO: avoid deep copies
|
||||
auto argument = ast::Formula::make<ast::Not>(ast::deepCopy(implies.antecedent));
|
||||
|
||||
if (variables.empty())
|
||||
{
|
||||
formula = std::move(argument);
|
||||
formulaIndex++;
|
||||
completedFormulas.emplace_back(std::move(argument));
|
||||
return;
|
||||
}
|
||||
|
||||
formula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
|
||||
formulaIndex++;
|
||||
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
|
||||
completedFormulas.emplace_back(std::move(completedFormula));
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
void complete(std::vector<ast::Formula> &formulas)
|
||||
{
|
||||
// Check whether formulas are in normal form
|
||||
for (const auto &formula : formulas)
|
||||
{
|
||||
if (!formula.is<ast::Implies>())
|
||||
@@ -180,19 +151,58 @@ void complete(std::vector<ast::Formula> &formulas)
|
||||
throw std::runtime_error("cannot perform completion, only single predicates and Booleans supported as formula consequent currently");
|
||||
}
|
||||
|
||||
for (std::size_t i = 0; i < formulas.size();)
|
||||
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)
|
||||
{
|
||||
// Create the signature of the predicate
|
||||
ast::Predicate signature(std::string(predicate->name));
|
||||
signature.arguments.reserve(predicate->arguments.size());
|
||||
|
||||
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::Variable::Type::Reserved));
|
||||
}
|
||||
|
||||
completePredicate(std::move(signature), formulas, completedFormulas);
|
||||
}
|
||||
|
||||
// Complete integrity constraints
|
||||
for (const auto &formula : formulas)
|
||||
{
|
||||
auto &formula = formulas[i];
|
||||
auto &implies = formula.get<ast::Implies>();
|
||||
|
||||
if (implies.consequent.is<ast::Predicate>())
|
||||
{
|
||||
auto &predicate = implies.consequent.get<ast::Predicate>();
|
||||
completePredicate(predicate, formulas, i);
|
||||
}
|
||||
else if (implies.consequent.is<ast::Boolean>())
|
||||
completeBoolean(formulas, i);
|
||||
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);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
Reference in New Issue
Block a user