From 9ccbda49b7bd18b47d1a8dbf5169f46b4b4a2a3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 23 Nov 2016 03:29:26 +0100 Subject: [PATCH] Implemented head translation. --- include/anthem/Head.h | 257 ++++++++++++++++++++++++++++ include/anthem/HeadLiteralVisitor.h | 33 +--- include/anthem/LiteralVisitor.h | 28 +-- include/anthem/StatementVisitor.h | 27 +-- include/anthem/TermVisitor.h | 23 +-- include/anthem/Utils.h | 6 + 6 files changed, 288 insertions(+), 86 deletions(-) create mode 100644 include/anthem/Head.h diff --git a/include/anthem/Head.h b/include/anthem/Head.h new file mode 100644 index 0000000..ed27079 --- /dev/null +++ b/include/anthem/Head.h @@ -0,0 +1,257 @@ +#ifndef __ANTHEM__HEAD_H +#define __ANTHEM__HEAD_H + +#include + +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Head +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermCollectFunctionTermsVisitor +{ + void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected"); + } + + void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, std::vector &terms) + { + if (function.external) + throwErrorAtLocation(term.location, "external functions currently unsupported"); + + terms.reserve(terms.size() + function.arguments.size()); + + for (const auto &argument : function.arguments) + terms.emplace_back(&argument); + } + + void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, std::vector &) + { + throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct LiteralCollectFunctionTermsVisitor +{ + void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } + + void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, std::vector &terms) + { + term.data.accept(TermCollectFunctionTermsVisitor(), term, terms); + } + + void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } + + void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct HeadLiteralCollectFunctionTermsVisitor +{ + void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, std::vector &terms) + { + literal.data.accept(LiteralCollectFunctionTermsVisitor(), literal, terms); + } + + void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, std::vector &terms) + { + for (const auto &conditionLiteral : disjunction.elements) + { + if (!conditionLiteral.condition.empty()) + throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported"); + + conditionLiteral.literal.data.accept(LiteralCollectFunctionTermsVisitor(), conditionLiteral.literal, terms); + } + } + + void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“aggregate” head literals currently unsupported"); + } + + void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported"); + } + + void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermPrintSubstitutedVisitor +{ + void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected"); + } + + void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected"); + } + + void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, const std::vector &terms) + { + if (function.external) + throwErrorAtLocation(term.location, "external functions currently unsupported"); + + std::cout << function.name; + + if (function.arguments.empty()) + return; + + std::cout << "("; + + for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) + { + if (i != function.arguments.cbegin()) + std::cout << ","; + + const auto &argument = *i; + + const auto matchingTerm = std::find(terms.cbegin(), terms.cend(), &argument); + + assert(matchingTerm != terms.cend()); + + std::cout << AuxiliaryVariablePrefix << (matchingTerm - terms.cbegin()); + } + + std::cout << ")"; + } + + void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, const std::vector &) + { + throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct LiteralPrintSubstitutedVisitor +{ + void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, const std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } + + void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, const std::vector &terms) + { + term.data.accept(TermPrintSubstitutedVisitor(), term, terms); + } + + void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, const std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } + + void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, const std::vector &) + { + throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct HeadLiteralPrintSubstitutedVisitor +{ + void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, const std::vector &terms) + { + literal.data.accept(LiteralPrintSubstitutedVisitor(), literal, terms); + } + + void visit(const Clingo::AST::Disjunction &disjunction, const Clingo::AST::HeadLiteral &headLiteral, const std::vector &terms) + { + for (auto i = disjunction.elements.cbegin(); i != disjunction.elements.cend(); i++) + { + const auto &conditionLiteral = *i; + + if (!conditionLiteral.condition.empty()) + throwErrorAtLocation(headLiteral.location, "conditional head literals currently unsupported"); + + if (i != disjunction.elements.cbegin()) + std::cout << " or "; + + conditionLiteral.literal.data.accept(LiteralPrintSubstitutedVisitor(), conditionLiteral.literal, terms); + } + } + + void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“aggregate” head literals currently unsupported"); + } + + void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported"); + } + + void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, const std::vector &) + { + throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/HeadLiteralVisitor.h b/include/anthem/HeadLiteralVisitor.h index f548451..7da0f60 100644 --- a/include/anthem/HeadLiteralVisitor.h +++ b/include/anthem/HeadLiteralVisitor.h @@ -15,7 +15,7 @@ namespace anthem void throwErrorUnsupportedHeadLiteral(const char *statementType, const Clingo::AST::HeadLiteral &headLiteral) { - const auto errorMessage = std::string("“") + statementType + "” head literals currently not supported"; + const auto errorMessage = std::string("“") + statementType + "” head literals currently unsupported"; throwErrorAtLocation(headLiteral.location, errorMessage.c_str()); @@ -58,37 +58,6 @@ struct HeadLiteralVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -struct HeadLiteralCollectTermsVisitor -{ - void visit(const Clingo::AST::Literal &literal, const Clingo::AST::HeadLiteral &, std::vector &terms) - { - literal.data.accept(LiteralCollectTermsVisitor(), literal, terms); - } - - void visit(const Clingo::AST::Disjunction &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) - { - // TODO: implement - throwErrorUnsupportedHeadLiteral("disjunction", headLiteral); - } - - void visit(const Clingo::AST::Aggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) - { - throwErrorUnsupportedHeadLiteral("aggregate", headLiteral); - } - - void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) - { - throwErrorUnsupportedHeadLiteral("head aggregate", headLiteral); - } - - void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, std::vector &) - { - throwErrorUnsupportedHeadLiteral("theory", headLiteral); - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } #endif diff --git a/include/anthem/LiteralVisitor.h b/include/anthem/LiteralVisitor.h index ee0c79a..ee631e4 100644 --- a/include/anthem/LiteralVisitor.h +++ b/include/anthem/LiteralVisitor.h @@ -15,7 +15,7 @@ namespace anthem void throwErrorUnsupportedLiteral(const char *statementType, const Clingo::AST::Literal &literal) { - const auto errorMessage = std::string("“") + statementType + "” literals currently not supported"; + const auto errorMessage = std::string("“") + statementType + "” literals currently unsupported"; throwErrorAtLocation(literal.location, errorMessage.c_str()); @@ -52,32 +52,6 @@ struct LiteralVisitor //////////////////////////////////////////////////////////////////////////////////////////////////// -struct LiteralCollectTermsVisitor -{ - void visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &, std::vector &) - { - } - - void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, std::vector &terms) - { - terms.push_back(term); - } - - void visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &, std::vector &terms) - { - terms.reserve(terms.size() + 2); - terms.push_back(comparison.left); - terms.push_back(comparison.right); - } - - void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, std::vector &) - { - throwErrorUnsupportedLiteral("CSP literal", literal); - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - } #endif diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 5f5f01b..8d9ed3b 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -2,7 +2,7 @@ #define __ANTHEM__STATEMENT_VISITOR_H #include -#include +#include #include namespace anthem @@ -16,7 +16,7 @@ namespace anthem void throwErrorUnsupportedStatement(const char *statementType, const Clingo::AST::Statement &statement) { - const auto errorMessage = std::string("“") + statementType + "” statements currently not supported"; + const auto errorMessage = std::string("“") + statementType + "” statements currently unsupported"; throwErrorAtLocation(statement.location, errorMessage.c_str()); @@ -32,30 +32,34 @@ struct StatementVisitor std::cout << "[program] " << program.name << std::endl; if (!program.parameters.empty()) - throwErrorAtLocation(statement.location, "program parameters currently not supported"); + throwErrorAtLocation(statement.location, "program parameters currently unsupported"); } void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &) { - std::vector headTerms; - rule.head.data.accept(HeadLiteralCollectTermsVisitor(), rule.head, headTerms); + // Concatenate all head terms + std::vector headTerms; + rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, headTerms); + // Print auxiliary variables replacing the head atom’s arguments if (!headTerms.empty()) { - std::cout << "exists "; - for (auto i = headTerms.cbegin(); i != headTerms.cend(); i++) { + const auto &headTerm = **i; + if (i != headTerms.cbegin()) std::cout << ", "; - std::cout << "AUX" << (i - headTerms.cbegin()); + std::cout + << AuxiliaryVariablePrefix << (i - headTerms.cbegin()) + << " in " << headTerm; } - std::cout << ": "; + std::cout << " and "; } - std::cout << "body -> "; + std::cout << "[body] -> "; /*rule.head.data.accept(HeadLiteralVisitor(), rule.head); @@ -66,6 +70,9 @@ struct StatementVisitor bodyLiteral.data.accept(BodyLiteralVisitor(), bodyLiteral); }*/ + + // Print consequent of the implication + rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, headTerms); } void visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement) diff --git a/include/anthem/TermVisitor.h b/include/anthem/TermVisitor.h index b853a8d..3c96e8f 100644 --- a/include/anthem/TermVisitor.h +++ b/include/anthem/TermVisitor.h @@ -12,17 +12,6 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -void throwErrorUnsupportedTerm(const char *statementType, const Clingo::AST::Term &term) -{ - const auto errorMessage = std::string("“") + statementType + "” terms currently not supported"; - - throwErrorAtLocation(term.location, errorMessage.c_str()); - - throw std::runtime_error(errorMessage); -} - -//////////////////////////////////////////////////////////////////////////////////////////////////// - struct TermVisitor { void visit(const Clingo::Symbol &symbol, const Clingo::AST::Term &) @@ -32,34 +21,34 @@ struct TermVisitor void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term) { - throwErrorUnsupportedTerm("variable", term); + throwErrorAtLocation(term.location, "“variable” terms currently unsupported"); } void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term) { - throwErrorUnsupportedTerm("unary operation", term); + throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported"); } void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term) { - throwErrorUnsupportedTerm("binary operation", term); + throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported"); } void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term) { - throwErrorUnsupportedTerm("interval", term); + throwErrorAtLocation(term.location, "“interval” terms currently unsupported"); } void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term) { std::cout << "[" << function.name << "]"; - throwErrorUnsupportedTerm("function", term); + throwErrorAtLocation(term.location, "“function” terms currently unsupported"); } void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term) { - throwErrorUnsupportedTerm("pool", term); + throwErrorAtLocation(term.location, "“pool” terms currently unsupported"); } }; diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index f9fc9a9..c8eb43a 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -21,10 +21,16 @@ inline void throwErrorAtLocation(const Clingo::Location &location, const char *e << location.begin_line() << ":" << location.begin_column() << ": error: " << errorMessage << std::endl; + + throw std::runtime_error(errorMessage); } //////////////////////////////////////////////////////////////////////////////////////////////////// +constexpr const auto AuxiliaryVariablePrefix = "AUX"; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } #endif