2016-11-22 03:15:52 +01:00
|
|
|
|
#ifndef __ANTHEM__STATEMENT_VISITOR_H
|
|
|
|
|
#define __ANTHEM__STATEMENT_VISITOR_H
|
|
|
|
|
|
2017-03-15 16:00:00 +01:00
|
|
|
|
#include <anthem/AST.h>
|
2017-05-30 03:53:51 +02:00
|
|
|
|
#include <anthem/ASTCopy.h>
|
2016-11-23 04:41:38 +01:00
|
|
|
|
#include <anthem/Body.h>
|
2016-11-23 03:29:26 +01:00
|
|
|
|
#include <anthem/Head.h>
|
2017-05-30 03:53:51 +02:00
|
|
|
|
#include <anthem/RuleContext.h>
|
2017-03-15 16:00:00 +01:00
|
|
|
|
#include <anthem/Term.h>
|
2016-11-22 03:15:52 +01:00
|
|
|
|
#include <anthem/Utils.h>
|
|
|
|
|
|
|
|
|
|
namespace anthem
|
|
|
|
|
{
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
//
|
|
|
|
|
// StatementVisitor
|
|
|
|
|
//
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2017-04-05 18:15:42 +02:00
|
|
|
|
// Replaces empty and 1-element conjunctions in the antecedent of normal-form formulas
|
|
|
|
|
inline void reduce(ast::Implies &implies)
|
|
|
|
|
{
|
|
|
|
|
if (!implies.antecedent.is<ast::And>())
|
|
|
|
|
return;
|
|
|
|
|
|
|
|
|
|
auto &antecedent = implies.antecedent.get<ast::And>();
|
|
|
|
|
|
|
|
|
|
// Use “true” as the consequent in case it is empty
|
|
|
|
|
if (antecedent.arguments.empty())
|
|
|
|
|
implies.antecedent = ast::Formula::make<ast::Boolean>(true);
|
|
|
|
|
else if (antecedent.arguments.size() == 1)
|
|
|
|
|
implies.antecedent = std::move(antecedent.arguments[0]);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
2016-11-22 03:15:52 +01:00
|
|
|
|
struct StatementVisitor
|
|
|
|
|
{
|
2017-05-30 03:53:51 +02:00
|
|
|
|
void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2017-06-02 14:59:13 +02:00
|
|
|
|
context.logger.log(output::Priority::Debug, statement.location) << "reading program “" << program.name << "”";
|
|
|
|
|
|
|
|
|
|
if (std::strcmp(program.name, "base") != 0)
|
|
|
|
|
throw LogicException(statement.location, "program parts currently unsupported");
|
2016-11-22 03:15:52 +01:00
|
|
|
|
|
|
|
|
|
if (!program.parameters.empty())
|
2017-05-31 18:03:19 +02:00
|
|
|
|
throw LogicException(statement.location, "program parameters currently unsupported");
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-06-02 14:59:13 +02:00
|
|
|
|
void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &scopedFormulas, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2017-06-02 14:59:13 +02:00
|
|
|
|
context.logger.log(output::Priority::Debug, statement.location) << "reading rule";
|
|
|
|
|
|
2017-05-30 03:53:51 +02:00
|
|
|
|
RuleContext ruleContext;
|
|
|
|
|
ast::VariableStack variableStack;
|
|
|
|
|
variableStack.push(&ruleContext.freeVariables);
|
2016-11-24 03:08:36 +01:00
|
|
|
|
|
2017-05-30 03:53:51 +02:00
|
|
|
|
// Collect all head terms
|
2017-05-31 18:03:19 +02:00
|
|
|
|
rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, ruleContext);
|
2017-05-30 03:53:51 +02:00
|
|
|
|
|
|
|
|
|
// Create new variable declarations for the head terms
|
|
|
|
|
ruleContext.headVariablesStartIndex = ruleContext.freeVariables.size();
|
|
|
|
|
ruleContext.freeVariables.reserve(ruleContext.headTerms.size());
|
|
|
|
|
|
|
|
|
|
for (size_t i = 0; i < ruleContext.headTerms.size(); i++)
|
|
|
|
|
{
|
2017-05-30 16:40:56 +02:00
|
|
|
|
auto variableDeclaration = std::make_unique<ast::VariableDeclaration>(ast::VariableDeclaration::Type::Head);
|
2017-05-30 03:53:51 +02:00
|
|
|
|
ruleContext.freeVariables.emplace_back(std::move(variableDeclaration));
|
|
|
|
|
}
|
2016-11-22 03:15:52 +01:00
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
|
ast::And antecedent;
|
2017-03-15 16:00:00 +01:00
|
|
|
|
|
|
|
|
|
// Compute consequent
|
2017-05-30 03:53:51 +02:00
|
|
|
|
auto headVariableIndex = ruleContext.headVariablesStartIndex;
|
2017-05-31 18:03:19 +02:00
|
|
|
|
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, ruleContext, headVariableIndex);
|
2017-05-30 03:53:51 +02:00
|
|
|
|
|
|
|
|
|
assert(ruleContext.headTerms.size() == headVariableIndex - ruleContext.headVariablesStartIndex);
|
2017-03-15 16:00:00 +01:00
|
|
|
|
|
|
|
|
|
if (!consequent)
|
2017-05-31 18:03:19 +02:00
|
|
|
|
throw TranslationException(rule.head.location, "could not translate formula consequent");
|
2017-03-15 16:00:00 +01:00
|
|
|
|
|
2017-03-23 02:06:19 +01:00
|
|
|
|
// Generate auxiliary variables replacing the head atom’s arguments
|
2017-05-30 03:53:51 +02:00
|
|
|
|
for (auto i = ruleContext.headTerms.cbegin(); i != ruleContext.headTerms.cend(); i++)
|
2016-11-22 17:58:18 +01:00
|
|
|
|
{
|
2017-03-06 15:42:38 +01:00
|
|
|
|
const auto &headTerm = **i;
|
2016-11-23 03:29:26 +01:00
|
|
|
|
|
2017-05-30 03:53:51 +02:00
|
|
|
|
const auto auxiliaryHeadVariableID = ruleContext.headVariablesStartIndex + i - ruleContext.headTerms.cbegin();
|
|
|
|
|
auto element = ast::Variable(ruleContext.freeVariables[auxiliaryHeadVariableID].get());
|
2017-05-31 18:03:19 +02:00
|
|
|
|
auto set = translate(headTerm, ruleContext, variableStack);
|
2017-03-23 00:44:10 +01:00
|
|
|
|
auto in = ast::In(std::move(element), std::move(set));
|
2016-11-22 17:58:18 +01:00
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
|
antecedent.arguments.emplace_back(std::move(in));
|
2016-11-22 17:58:18 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 02:06:19 +01:00
|
|
|
|
// Translate body literals
|
2017-03-06 15:42:38 +01:00
|
|
|
|
for (auto i = rule.body.cbegin(); i != rule.body.cend(); i++)
|
2016-11-23 04:41:38 +01:00
|
|
|
|
{
|
2017-03-06 15:42:38 +01:00
|
|
|
|
const auto &bodyLiteral = *i;
|
2016-11-22 03:15:52 +01:00
|
|
|
|
|
2017-05-31 18:03:19 +02:00
|
|
|
|
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, ruleContext, variableStack);
|
2016-11-23 04:41:38 +01:00
|
|
|
|
|
2017-03-15 16:00:00 +01:00
|
|
|
|
if (!argument)
|
2017-05-31 18:03:19 +02:00
|
|
|
|
throw TranslationException(bodyLiteral.location, "could not translate body literal");
|
2017-03-06 15:40:23 +01:00
|
|
|
|
|
2017-03-23 00:44:10 +01:00
|
|
|
|
antecedent.arguments.emplace_back(std::move(argument.value()));
|
2017-03-06 15:40:23 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-05-30 03:53:51 +02:00
|
|
|
|
if (!ruleContext.isChoiceRule)
|
2017-04-05 18:15:42 +02:00
|
|
|
|
{
|
2017-05-30 03:53:51 +02:00
|
|
|
|
auto formula = ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()));
|
|
|
|
|
ast::ScopedFormula scopedFormula(std::move(formula), std::move(ruleContext.freeVariables));
|
|
|
|
|
scopedFormulas.emplace_back(std::move(scopedFormula));
|
|
|
|
|
reduce(scopedFormulas.back().formula.get<ast::Implies>());
|
2017-04-05 18:15:42 +02:00
|
|
|
|
}
|
2017-03-23 02:06:19 +01:00
|
|
|
|
else
|
|
|
|
|
{
|
|
|
|
|
const auto createFormula =
|
|
|
|
|
[&](ast::Formula &argument, bool isLastOne)
|
|
|
|
|
{
|
2017-05-30 03:53:51 +02:00
|
|
|
|
auto &consequent = argument;
|
2017-03-23 02:06:19 +01:00
|
|
|
|
|
|
|
|
|
if (!isLastOne)
|
2017-05-30 03:53:51 +02:00
|
|
|
|
{
|
|
|
|
|
auto formula = ast::Formula::make<ast::Implies>(ast::prepareCopy(antecedent), std::move(consequent));
|
|
|
|
|
ast::ScopedFormula scopedFormula(std::move(formula), {});
|
|
|
|
|
ast::fixDanglingVariables(scopedFormula);
|
|
|
|
|
scopedFormulas.emplace_back(std::move(scopedFormula));
|
|
|
|
|
}
|
2017-03-23 02:06:19 +01:00
|
|
|
|
else
|
2017-05-30 03:53:51 +02:00
|
|
|
|
{
|
|
|
|
|
auto formula = ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent));
|
|
|
|
|
ast::ScopedFormula scopedFormula(std::move(formula), std::move(ruleContext.freeVariables));
|
|
|
|
|
scopedFormulas.emplace_back(std::move(scopedFormula));
|
|
|
|
|
}
|
2017-03-23 02:06:19 +01:00
|
|
|
|
|
2017-05-30 03:53:51 +02:00
|
|
|
|
auto &implies = scopedFormulas.back().formula.get<ast::Implies>();
|
2017-03-23 02:06:19 +01:00
|
|
|
|
auto &antecedent = implies.antecedent.get<ast::And>();
|
2017-05-30 03:53:51 +02:00
|
|
|
|
antecedent.arguments.emplace_back(ast::prepareCopy(implies.consequent));
|
|
|
|
|
ast::fixDanglingVariables(scopedFormulas.back());
|
2017-04-05 18:15:42 +02:00
|
|
|
|
|
|
|
|
|
reduce(implies);
|
2017-03-23 02:06:19 +01:00
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
if (consequent.value().is<ast::Or>())
|
|
|
|
|
{
|
|
|
|
|
auto &disjunction = consequent.value().get<ast::Or>();
|
|
|
|
|
|
|
|
|
|
for (auto &argument : disjunction.arguments)
|
|
|
|
|
createFormula(argument, &argument == &disjunction.arguments.back());
|
|
|
|
|
}
|
|
|
|
|
// TODO: check whether this is really correct for all possible consequent types
|
|
|
|
|
else
|
|
|
|
|
createFormula(consequent.value(), true);
|
|
|
|
|
}
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-06-01 04:05:11 +02:00
|
|
|
|
void visit(const Clingo::AST::ShowSignature &showSignature, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &context)
|
|
|
|
|
{
|
|
|
|
|
if (showSignature.csp)
|
|
|
|
|
throw LogicException(statement.location, "CSP #show statements are not supported");
|
|
|
|
|
|
|
|
|
|
auto &signature = showSignature.signature;
|
|
|
|
|
|
|
|
|
|
if (signature.negative())
|
|
|
|
|
throw LogicException(statement.location, "negative #show atom signatures are currently unsupported");
|
|
|
|
|
|
|
|
|
|
if (!context.visiblePredicateSignatures)
|
|
|
|
|
context.visiblePredicateSignatures.emplace();
|
|
|
|
|
|
|
|
|
|
if (std::strlen(signature.name()) == 0)
|
2017-06-02 14:59:13 +02:00
|
|
|
|
{
|
|
|
|
|
context.logger.log(output::Priority::Debug, statement.location) << "showing no predicates by default";
|
2017-06-01 04:05:11 +02:00
|
|
|
|
return;
|
2017-06-02 14:59:13 +02:00
|
|
|
|
}
|
2017-06-01 04:05:11 +02:00
|
|
|
|
|
2017-06-02 14:59:13 +02:00
|
|
|
|
context.logger.log(output::Priority::Debug, statement.location) << "showing “" << signature.name() << "/" << signature.arity() << "”";
|
2017-06-01 04:05:11 +02:00
|
|
|
|
|
2018-04-05 23:22:25 +02:00
|
|
|
|
auto predicateSignature = ast::PredicateSignature{std::string(signature.name()), signature.arity()};
|
|
|
|
|
context.visiblePredicateSignatures.value().emplace_back(PredicateSignatureMeta{std::move(predicateSignature)});
|
2017-06-01 04:05:11 +02:00
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
void visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
|
|
|
|
{
|
|
|
|
|
throw LogicException(statement.location, "only #show statements for atoms (not terms) are supported currently");
|
|
|
|
|
}
|
|
|
|
|
|
2018-04-05 23:22:25 +02:00
|
|
|
|
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)});
|
|
|
|
|
}
|
|
|
|
|
|
2017-03-29 21:32:11 +02:00
|
|
|
|
template<class T>
|
2017-05-31 18:03:19 +02:00
|
|
|
|
void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::ScopedFormula> &, Context &)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2017-06-01 04:05:11 +02:00
|
|
|
|
throw LogicException(statement.location, "statement currently unsupported");
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#endif
|