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:
This commit is contained in:
parent
c91cbaf58b
commit
bf6bf7f9c3
|
@ -5,6 +5,7 @@
|
|||
|
||||
#include <anthem/AST.h>
|
||||
#include <anthem/ASTVisitors.h>
|
||||
#include <anthem/Context.h>
|
||||
|
||||
namespace anthem
|
||||
{
|
||||
|
@ -40,7 +41,7 @@ class VariableStack
|
|||
bool matches(const Predicate &lhs, const Predicate &rhs);
|
||||
bool matches(const Predicate &predicate, const PredicateSignature &signature);
|
||||
bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs);
|
||||
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures);
|
||||
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context);
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
// Replacing Variables
|
||||
|
|
|
@ -16,6 +16,14 @@ namespace anthem
|
|||
//
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct PredicateSignatureMeta
|
||||
{
|
||||
ast::PredicateSignature predicateSignature;
|
||||
bool used{false};
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
struct Context
|
||||
{
|
||||
Context() = default;
|
||||
|
@ -30,7 +38,8 @@ struct Context
|
|||
bool performSimplification = false;
|
||||
bool performCompletion = false;
|
||||
|
||||
std::optional<std::vector<ast::PredicateSignature>> visiblePredicateSignatures;
|
||||
std::optional<std::vector<PredicateSignatureMeta>> visiblePredicateSignatures;
|
||||
std::optional<std::vector<PredicateSignatureMeta>> externalPredicateSignatures;
|
||||
|
||||
ast::ParenthesisStyle parenthesisStyle = ast::ParenthesisStyle::Normal;
|
||||
};
|
||||
|
|
|
@ -176,7 +176,8 @@ struct StatementVisitor
|
|||
|
||||
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
|
||||
|
||||
context.visiblePredicateSignatures.value().emplace_back(std::string(signature.name()), signature.arity());
|
||||
auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
|
||||
context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
|
||||
}
|
||||
|
||||
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
||||
|
@ -184,6 +185,44 @@ struct StatementVisitor
|
|||
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 size_t arity = arityArgument.data.get<Clingo::Symbol>().number();
|
||||
|
||||
if (!context.externalPredicateSignatures)
|
||||
context.externalPredicateSignatures.emplace();
|
||||
|
||||
auto predicateSignature = ast::PredicateSignature{std::string(predicate.name), arity};
|
||||
context.externalPredicateSignatures->emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
||||
{
|
||||
|
|
|
@ -194,7 +194,7 @@ struct CollectFreeVariablesVisitor
|
|||
|
||||
struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<CollectPredicateSignaturesVisitor>
|
||||
{
|
||||
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures)
|
||||
static void accept(const Predicate &predicate, const Formula &, std::vector<PredicateSignature> &predicateSignatures, Context &context)
|
||||
{
|
||||
const auto predicateSignatureMatches =
|
||||
[&predicate](const auto &predicateSignature)
|
||||
|
@ -206,12 +206,35 @@ struct CollectPredicateSignaturesVisitor : public RecursiveFormulaVisitor<Collec
|
|||
return;
|
||||
|
||||
// TODO: avoid copies
|
||||
predicateSignatures.emplace_back(std::string(predicate.name), predicate.arity());
|
||||
auto predicateSignature = PredicateSignature(std::string(predicate.name), predicate.arity());
|
||||
|
||||
// Ignore predicates that are declared #external
|
||||
if (context.externalPredicateSignatures)
|
||||
{
|
||||
const auto matchesPredicateSignature =
|
||||
[&](const auto &otherPredicateSignature)
|
||||
{
|
||||
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
|
||||
};
|
||||
|
||||
auto &externalPredicateSignatures = context.externalPredicateSignatures.value();
|
||||
|
||||
const auto matchingExternalPredicateSignature =
|
||||
std::find_if(externalPredicateSignatures.begin(), externalPredicateSignatures.end(), matchesPredicateSignature);
|
||||
|
||||
if (matchingExternalPredicateSignature != externalPredicateSignatures.end())
|
||||
{
|
||||
matchingExternalPredicateSignature->used = true;
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
predicateSignatures.emplace_back(std::move(predicateSignature));
|
||||
}
|
||||
|
||||
// Ignore all other types of expressions
|
||||
template<class T>
|
||||
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &)
|
||||
static void accept(const T &, const Formula &, std::vector<PredicateSignature> &, const Context &)
|
||||
{
|
||||
}
|
||||
};
|
||||
|
@ -240,10 +263,10 @@ bool matches(const PredicateSignature &lhs, const PredicateSignature &rhs)
|
|||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// TODO: remove const_cast
|
||||
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures)
|
||||
void collectPredicateSignatures(const Formula &formula, std::vector<PredicateSignature> &predicateSignatures, Context &context)
|
||||
{
|
||||
auto &formulaMutable = const_cast<Formula &>(formula);
|
||||
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures);
|
||||
formulaMutable.accept(CollectPredicateSignaturesVisitor(), formulaMutable, predicateSignatures, context);
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
@ -165,7 +165,7 @@ std::vector<ast::Formula> complete(std::vector<ast::ScopedFormula> &&scopedFormu
|
|||
|
||||
// Get a list of all predicates
|
||||
for (const auto &scopedFormula : scopedFormulas)
|
||||
ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures);
|
||||
ast::collectPredicateSignatures(scopedFormula.formula, predicateSignatures, context);
|
||||
|
||||
std::sort(predicateSignatures.begin(), predicateSignatures.end(),
|
||||
[](const auto &lhs, const auto &rhs)
|
||||
|
|
|
@ -194,41 +194,40 @@ void eliminateHiddenPredicates(const std::vector<ast::PredicateSignature> &predi
|
|||
return;
|
||||
}
|
||||
|
||||
const auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
|
||||
|
||||
// Check for undeclared predicates that are requested to be shown
|
||||
for (const auto &visiblePredicateSignature : visiblePredicateSignatures)
|
||||
{
|
||||
const auto matchesPredicateSignature =
|
||||
[&](const auto &predicateSignature)
|
||||
{
|
||||
return ast::matches(predicateSignature, visiblePredicateSignature);
|
||||
};
|
||||
|
||||
const auto matchingPredicateSignature =
|
||||
std::find_if(predicateSignatures.cbegin(), predicateSignatures.cend(), matchesPredicateSignature);
|
||||
|
||||
if (matchingPredicateSignature == predicateSignatures.cend())
|
||||
context.logger.log(output::Priority::Warning) << "cannot show undeclared predicate “" << visiblePredicateSignature.name << "/" << visiblePredicateSignature.arity <<"”";
|
||||
}
|
||||
auto &visiblePredicateSignatures = context.visiblePredicateSignatures.value();
|
||||
|
||||
// Replace all occurrences of hidden predicates
|
||||
for (size_t i = 0; i < predicateSignatures.size(); i++)
|
||||
{
|
||||
auto &predicateSignature = predicateSignatures[i];
|
||||
|
||||
const auto matchesVisiblePredicateSignature =
|
||||
[&](const auto &visiblePredicateSignature)
|
||||
const auto matchesPredicateSignature =
|
||||
[&](const auto &otherPredicateSignature)
|
||||
{
|
||||
return ast::matches(predicateSignature, visiblePredicateSignature);
|
||||
return ast::matches(predicateSignature, otherPredicateSignature.predicateSignature);
|
||||
};
|
||||
|
||||
const auto matchingPredicateSignature =
|
||||
std::find_if(visiblePredicateSignatures.cbegin(), visiblePredicateSignatures.cend(), matchesVisiblePredicateSignature);
|
||||
const auto matchingVisiblePredicateSignature =
|
||||
std::find_if(visiblePredicateSignatures.begin(), visiblePredicateSignatures.end(), matchesPredicateSignature);
|
||||
|
||||
// If the predicate ought to be visible, don’t eliminate it
|
||||
if (matchingPredicateSignature != visiblePredicateSignatures.cend())
|
||||
if (matchingVisiblePredicateSignature != visiblePredicateSignatures.end())
|
||||
{
|
||||
matchingVisiblePredicateSignature->used = true;
|
||||
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 << "”";
|
||||
|
||||
|
|
|
@ -70,6 +70,9 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||
if (context.visiblePredicateSignatures)
|
||||
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)
|
||||
{
|
||||
ast::print(context.logger.outputStream(), scopedFormula.formula, printContext);
|
||||
|
@ -82,6 +85,26 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||
// Perform completion
|
||||
auto completedFormulas = complete(std::move(scopedFormulas), context);
|
||||
|
||||
// Check for #show statements with undeclared predicates
|
||||
if (context.visiblePredicateSignatures)
|
||||
for (const auto &predicateSignature : context.visiblePredicateSignatures.value())
|
||||
if (!predicateSignature.used)
|
||||
context.logger.log(output::Priority::Warning)
|
||||
<< "#show declaration of “"
|
||||
<< predicateSignature.predicateSignature.name
|
||||
<< "/" << predicateSignature.predicateSignature.arity
|
||||
<< "” does not match any eligible predicate";
|
||||
|
||||
// Check for #external statements with undeclared predicates
|
||||
if (context.externalPredicateSignatures)
|
||||
for (const auto &predicateSignature : context.externalPredicateSignatures.value())
|
||||
if (!predicateSignature.used)
|
||||
context.logger.log(output::Priority::Warning)
|
||||
<< "#external declaration of “"
|
||||
<< predicateSignature.predicateSignature.name
|
||||
<< "/" << predicateSignature.predicateSignature.arity
|
||||
<< "” does not match any eligible predicate";
|
||||
|
||||
// Simplify output if specified
|
||||
if (context.performSimplification)
|
||||
for (auto &completedFormula : completedFormulas)
|
||||
|
|
Loading…
Reference in New Issue