Added support for completion of integrity constraints.
This commit is contained in:
parent
a716da4af1
commit
8210adea7c
|
@ -31,6 +31,7 @@ class VariableStack
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula);
|
||||||
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack);
|
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack);
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
|
@ -175,6 +175,14 @@ struct CollectFreeVariablesVisitor
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula)
|
||||||
|
{
|
||||||
|
ast::VariableStack variableStack;
|
||||||
|
return collectFreeVariables(formula, variableStack);
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack)
|
std::vector<ast::Variable> collectFreeVariables(const ast::Formula &formula, ast::VariableStack &variableStack)
|
||||||
{
|
{
|
||||||
std::vector<ast::Variable> freeVariables;
|
std::vector<ast::Variable> freeVariables;
|
||||||
|
|
|
@ -32,7 +32,10 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
|
||||||
auto &formula = formulas[i];
|
auto &formula = formulas[i];
|
||||||
assert(formula.is<ast::Implies>());
|
assert(formula.is<ast::Implies>());
|
||||||
auto &implies = formula.get<ast::Implies>();
|
auto &implies = formula.get<ast::Implies>();
|
||||||
assert(implies.consequent.is<ast::Predicate>());
|
|
||||||
|
if (!implies.consequent.is<ast::Predicate>())
|
||||||
|
continue;
|
||||||
|
|
||||||
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
||||||
|
|
||||||
if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
|
if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
|
||||||
|
@ -60,7 +63,13 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
|
||||||
auto &formula = formulas[i];
|
auto &formula = formulas[i];
|
||||||
assert(formula.is<ast::Implies>());
|
assert(formula.is<ast::Implies>());
|
||||||
auto &implies = formula.get<ast::Implies>();
|
auto &implies = formula.get<ast::Implies>();
|
||||||
assert(implies.consequent.is<ast::Predicate>());
|
|
||||||
|
if (!implies.consequent.is<ast::Predicate>())
|
||||||
|
{
|
||||||
|
i++;
|
||||||
|
continue;
|
||||||
|
}
|
||||||
|
|
||||||
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
auto &otherPredicate = implies.consequent.get<ast::Predicate>();
|
||||||
|
|
||||||
if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
|
if (predicate.arity() != otherPredicate.arity() || predicate.name != otherPredicate.name)
|
||||||
|
@ -107,6 +116,30 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
void completeBoolean(ast::Formula &formula)
|
||||||
|
{
|
||||||
|
assert(formula.is<ast::Implies>());
|
||||||
|
auto &implies = formula.get<ast::Implies>();
|
||||||
|
assert(implies.consequent.is<ast::Boolean>());
|
||||||
|
auto &boolean = implies.consequent.get<ast::Boolean>();
|
||||||
|
|
||||||
|
auto variables = ast::collectFreeVariables(implies.antecedent);
|
||||||
|
|
||||||
|
auto argument = (boolean.value == true)
|
||||||
|
? std::move(implies.antecedent)
|
||||||
|
: ast::Formula::make<ast::Not>(std::move(implies.antecedent));
|
||||||
|
|
||||||
|
if (variables.empty())
|
||||||
|
{
|
||||||
|
formula = std::move(argument);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
|
||||||
|
formula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(argument));
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
void complete(std::vector<ast::Formula> &formulas)
|
void complete(std::vector<ast::Formula> &formulas)
|
||||||
{
|
{
|
||||||
for (const auto &formula : formulas)
|
for (const auto &formula : formulas)
|
||||||
|
@ -116,17 +149,22 @@ void complete(std::vector<ast::Formula> &formulas)
|
||||||
|
|
||||||
auto &implies = formula.get<ast::Implies>();
|
auto &implies = formula.get<ast::Implies>();
|
||||||
|
|
||||||
if (!implies.consequent.is<ast::Predicate>())
|
if (!implies.consequent.is<ast::Predicate>() && !implies.consequent.is<ast::Boolean>())
|
||||||
throw std::runtime_error("cannot perform completion, only single predicates supported as formula consequent currently");
|
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(); i++)
|
for (std::size_t i = 0; i < formulas.size(); i++)
|
||||||
{
|
{
|
||||||
auto &formula = formulas[i];
|
auto &formula = formulas[i];
|
||||||
auto &implies = formula.get<ast::Implies>();
|
auto &implies = formula.get<ast::Implies>();
|
||||||
auto &predicate = implies.consequent.get<ast::Predicate>();
|
|
||||||
|
|
||||||
completePredicate(predicate, formulas, i);
|
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(formula);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue