Compare commits

...

2 Commits

Author SHA1 Message Date
b8bfa7db7a
Version bump for release 0.1.7 RC 2 2018-04-06 23:12:27 +02:00
3e096e39aa
Support placeholders with #external declarations
This adds support for declaring predicates as placeholders through the
“#external” directive in the input language of clingo.

Placeholders are not subject to completion. This prevents predicates
that represent instance-specific facts from being assumed as universally
false by default negation when translating an encoding.

This stretches clingo’s usual syntax a bit in order to make the
implementation lightweight. In order to declare a predicate with a
specific arity as a placeholder, the following statement needs to be
added to the input program:
2018-04-06 23:09:14 +02:00
7 changed files with 103 additions and 8 deletions

View File

@ -1,6 +1,10 @@
# Change Log # Change Log
## (unreleased) ## 0.1.7 RC 2 (2018-04-06)
### Features
* support for declaring placeholders with the `#external` directive
### Internal ### Internal

View File

@ -70,7 +70,7 @@ int main(int argc, char **argv)
if (version) if (version)
{ {
std::cout << "anthem version 0.1.7-git" << std::endl; std::cout << "anthem version 0.1.7-rc.2" << std::endl;
return EXIT_SUCCESS; return EXIT_SUCCESS;
} }

View File

@ -31,6 +31,7 @@ struct Context
bool performCompletion = false; bool performCompletion = false;
std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures; std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
std::optional<std::vector<ast::PredicateSignature>> externalPredicateSignatures;
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal; ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
}; };

View File

@ -184,6 +184,43 @@ struct StatementVisitor
throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently"); throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently");
} }
void visit(const Clingo::AST::External &external, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &context)
{
const auto fail =
[&]()
{
throw LogicException(statement.location, "only #external declarations of the form “#external <predicate name>(<arity>). supported");
};
if (!external.body.empty())
fail();
if (!external.atom.data.is<Clingo::AST::Function>())
fail();
const auto &predicate = external.atom.data.get<Clingo::AST::Function>();
if (predicate.arguments.size() != 1)
fail();
const auto &arityArgument = predicate.arguments.front();
if (!arityArgument.data.is<Clingo::Symbol>())
fail();
const auto &aritySymbol = arityArgument.data.get<Clingo::Symbol>();
if (aritySymbol.type() != Clingo::SymbolType::Number)
fail();
const auto &arity = arityArgument.data.get<Clingo::Symbol>().number();
if (!context.externalPredicateSignatures)
context.externalPredicateSignatures.emplace();
context.externalPredicateSignatures->emplace_back(std::string(predicate.name), arity);
}
template<class T> template<class T>
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &) void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
{ {

View File

@ -180,9 +180,47 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
std::vector<ast::Formula> completedFormulas; std::vector<ast::Formula> completedFormulas;
// Warn about incorrect #external declarations
if (context.externalPredicateSignatures)
for (const auto &externalPredicateSignature : *context.externalPredicateSignatures)
{
// TODO: avoid code duplication
const auto matchesPredicateSignature =
[&](const auto &otherPredicateSignature)
{
return ast::matches(externalPredicateSignature, otherPredicateSignature);
};
const auto matchingPredicateSignature =
std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
if (matchingPredicateSignature == predicateSignatures.cend())
context.logger.log(output::Priority::Warning) << "#external declaration of “" << externalPredicateSignature.name << "/" << externalPredicateSignature.arity <<"” does not match any known predicate";
}
// Complete predicates // Complete predicates
for (const auto &predicateSignature : predicateSignatures) for (const auto &predicateSignature : predicateSignatures)
{
// Dont complete predicates that are declared #external
if (context.externalPredicateSignatures)
{
const auto matchesPredicateSignature =
[&](const auto &otherPredicateSignature)
{
return ast::matches(predicateSignature, otherPredicateSignature);
};
const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
const auto matchingExternalPredicateSignature =
std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
continue;
}
completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas)); completedFormulas.emplace_back(completePredicate(predicateSignature, scopedFormulas));
}
// Complete integrity constraints // Complete integrity constraints
for (auto &scopedFormula : scopedFormulas) for (auto &scopedFormula : scopedFormulas)

View File

@ -217,19 +217,31 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
{ {
auto &predicateSignature = predicateSignatures[i]; auto &predicateSignature = predicateSignatures[i];
const auto matchesVisiblePredicateSignature = const auto matchesPredicateSignature =
[&](const auto &visiblePredicateSignature) [&](const auto &otherPredicateSignature)
{ {
return ast::matches(predicateSignature, visiblePredicateSignature); return ast::matches(predicateSignature, otherPredicateSignature);
}; };
const auto matchingPredicateSignature = const auto matchingVisiblePredicateSignature =
std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature); std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesPredicateSignature);
// If the predicate ought to be visible, dont eliminate it // If the predicate ought to be visible, dont eliminate it
if (matchingPredicateSignature != visiblePredicateSignatures.cend()) if (matchingVisiblePredicateSignature != visiblePredicateSignatures.cend())
continue; continue;
// Check that the predicate is not declared #external
if (context.externalPredicateSignatures)
{
const auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
const auto matchingExternalPredicateSignature =
std::find_if(externalPredicateSignatures.cbegin(), externalPredicateSignatures.cend(), matchesPredicateSignature);
if (matchingExternalPredicateSignature != externalPredicateSignatures.cend())
continue;
}
context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << ""; context.logger.log(output::Priority::Debug) << "eliminating “" << predicateSignature.name << "/" << predicateSignature.arity << "";
const auto &completedPredicateDefinition = completedFormulas[i]; const auto &completedPredicateDefinition = completedFormulas[i];

View File

@ -70,6 +70,9 @@ void translate(const char *fileName, std::istream &stream, Context &context)
if (context.visiblePredicateSignatures) if (context.visiblePredicateSignatures)
context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled"; context.logger.log(output::Priority::Warning) << "#show statements are ignored because completion is not enabled";
if (context.externalPredicateSignatures)
context.logger.log(output::Priority::Warning) << "#external statements are ignored because completion is not enabled";
for (const auto &scopedFormula : scopedFormulas) for (const auto &scopedFormula : scopedFormulas)
{ {
ast::print(context.logger.outputStream(), scopedFormula.formula, printContext); ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);