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>
|
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-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
|
|
|
|
|
//
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
struct StatementVisitor
|
|
|
|
|
{
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 03:36:14 +01:00
|
|
|
|
// TODO: refactor
|
|
|
|
|
context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str());
|
2016-11-22 03:15:52 +01:00
|
|
|
|
|
|
|
|
|
if (!program.parameters.empty())
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "program parameters currently unsupported", context);
|
2017-03-15 16:00:00 +01:00
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 16:50:35 +01:00
|
|
|
|
context.reset();
|
2016-11-24 03:08:36 +01:00
|
|
|
|
|
2016-11-23 03:29:26 +01:00
|
|
|
|
// Concatenate all head terms
|
2016-11-24 00:52:28 +01:00
|
|
|
|
rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, context);
|
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
|
|
|
|
|
auto consequent = rule.head.data.accept(HeadLiteralTranslateToConsequentVisitor(), rule.head, context);
|
|
|
|
|
|
|
|
|
|
if (!consequent)
|
|
|
|
|
{
|
|
|
|
|
context.logger.log(output::Priority::Error, "could not translate formula consequent");
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
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-03-06 15:42:38 +01:00
|
|
|
|
for (auto i = context.headTerms.cbegin(); i != context.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-03-15 16:00:00 +01:00
|
|
|
|
auto variableName = std::string(AuxiliaryHeadVariablePrefix) + std::to_string(i - context.headTerms.cbegin() + 1);
|
2017-03-23 00:44:10 +01:00
|
|
|
|
auto element = ast::Variable(std::move(variableName), ast::Variable::Type::Reserved);
|
2017-03-15 16:00:00 +01:00
|
|
|
|
auto set = translate(headTerm, context);
|
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-03-06 15:42:38 +01:00
|
|
|
|
if (bodyLiteral.sign != Clingo::AST::Sign::None)
|
|
|
|
|
throwErrorAtLocation(bodyLiteral.location, "only positive literals currently supported", context);
|
2016-11-22 03:15:52 +01:00
|
|
|
|
|
2017-03-15 16:00:00 +01:00
|
|
|
|
auto argument = bodyLiteral.data.accept(BodyBodyLiteralTranslateVisitor(), bodyLiteral, context);
|
2016-11-23 04:41:38 +01:00
|
|
|
|
|
2017-03-15 16:00:00 +01:00
|
|
|
|
if (!argument)
|
|
|
|
|
throwErrorAtLocation(bodyLiteral.location, "could not translate body literal", context);
|
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-03-23 02:06:19 +01:00
|
|
|
|
std::vector<ast::Formula> formulas;
|
2016-11-23 03:29:26 +01:00
|
|
|
|
|
2017-03-23 02:06:19 +01:00
|
|
|
|
if (!context.isChoiceRule)
|
|
|
|
|
formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value())));
|
|
|
|
|
else
|
|
|
|
|
{
|
|
|
|
|
const auto createFormula =
|
|
|
|
|
[&](ast::Formula &argument, bool isLastOne)
|
|
|
|
|
{
|
|
|
|
|
auto consequent = std::move(argument);
|
|
|
|
|
|
|
|
|
|
if (!isLastOne)
|
|
|
|
|
formulas.emplace_back(ast::Formula::make<ast::Implies>(ast::deepCopy(antecedent), std::move(consequent)));
|
|
|
|
|
else
|
|
|
|
|
formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent)));
|
|
|
|
|
|
|
|
|
|
auto &implies = formulas.back().get<ast::Implies>();
|
|
|
|
|
auto &antecedent = implies.antecedent.get<ast::And>();
|
|
|
|
|
antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent));
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
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);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
for (auto &formula : formulas)
|
|
|
|
|
{
|
|
|
|
|
auto &implies = formula.get<ast::Implies>();
|
|
|
|
|
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)
|
|
|
|
|
{
|
|
|
|
|
// TODO: remove workaround
|
|
|
|
|
auto tmp = std::move(antecedent.arguments[0]);
|
|
|
|
|
implies.antecedent = std::move(tmp);
|
|
|
|
|
}
|
|
|
|
|
}
|
2016-11-24 14:47:02 +01:00
|
|
|
|
|
2017-03-23 02:06:19 +01:00
|
|
|
|
return formulas;
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“definition” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“show signature” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“show term” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“minimize” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“script” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“external” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“edge” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“heuristic” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“project atom” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“project signature” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
|
2017-03-23 01:23:17 +01:00
|
|
|
|
std::vector<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
|
2016-11-22 03:15:52 +01:00
|
|
|
|
{
|
2016-11-24 00:52:28 +01:00
|
|
|
|
throwErrorAtLocation(statement.location, "“theory definition” statements currently unsupported", context);
|
2017-03-23 01:23:17 +01:00
|
|
|
|
return {};
|
2016-11-22 03:15:52 +01:00
|
|
|
|
}
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
#endif
|