patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Partly implemented completion.

Browse Source
This commit is contained in:
Patrick Lühne 2017-04-06 17:46:16 +02:00
parent c3351206b9
commit 811eb3054c
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 94 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
include/anthem/AST.h
View File

@ -174,6 +174,11 @@ struct Predicate
{
}
std::size_t arity() const
{
return arguments.size();
}
std::string name;
std::vector<Term> arguments;
};

90
src/anthem/Completion.cpp
View File

@ -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);
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////