From 29d1c15137a30b0fd7772b2bf453e15f6aa21cab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 23 Nov 2016 04:41:38 +0100 Subject: [PATCH] Implemented translation of positive body literals. --- include/anthem/Body.h | 208 ++++++++++++++++++++++++++++++ include/anthem/Context.h | 22 ++++ include/anthem/Head.h | 2 +- include/anthem/StatementVisitor.h | 26 ++-- include/anthem/Utils.h | 3 +- 5 files changed, 248 insertions(+), 13 deletions(-) create mode 100644 include/anthem/Body.h create mode 100644 include/anthem/Context.h diff --git a/include/anthem/Body.h b/include/anthem/Body.h new file mode 100644 index 0000000..f172d46 --- /dev/null +++ b/include/anthem/Body.h @@ -0,0 +1,208 @@ +#ifndef __ANTHEM__BODY_H +#define __ANTHEM__BODY_H + +#include + +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Body +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct TermPrintVisitor +{ + void visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“symbol” terms currently unsupported in this context"); + } + + void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“variable” terms currently unsupported in this context"); + } + + void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported in this context"); + } + + void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported in this context"); + } + + void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“interval” terms currently unsupported in this context"); + } + + void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context) + { + if (function.arguments.empty()) + { + std::cout << "[f " << function.name << "]"; + return; + } + + std::cout << "exists "; + + for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) + { + if (i != function.arguments.cbegin()) + std::cout << ", "; + + std::cout << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + (i - function.arguments.cbegin())); + } + + std::cout << " ("; + + for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) + { + const auto &argument = *i; + + if (i != function.arguments.cbegin()) + std::cout << " and "; + + std::cout + << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + (i - function.arguments.cbegin())) + << " in " + << argument; + } + + std::cout << " and " << function.name << "("; + + for (auto i = function.arguments.cbegin(); i != function.arguments.cend(); i++) + { + if (i != function.arguments.cbegin()) + std::cout << ", "; + + std::cout << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + (i - function.arguments.cbegin())); + } + + std::cout << "))"; + + context.auxiliaryBodyLiteralID += function.arguments.size(); + } + + void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &) + { + throwErrorAtLocation(term.location, "“pool” terms currently unsupported"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct LiteralPrintVisitor +{ + void visit(const Clingo::AST::Boolean &boolean, const Clingo::AST::Literal &, Context &) + { + if (boolean.value == true) + std::cout << "#true"; + else + std::cout << "#false"; + } + + void visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &, Context &context) + { + term.data.accept(TermPrintVisitor(), term, context); + } + + void visit(const Clingo::AST::Comparison &comparison, const Clingo::AST::Literal &literal, Context &context) + { + const char *operatorName = ""; + + switch (comparison.comparison) + { + case Clingo::AST::ComparisonOperator::GreaterThan: + operatorName = ">"; + break; + case Clingo::AST::ComparisonOperator::LessThan: + operatorName = "<"; + break; + case Clingo::AST::ComparisonOperator::LessEqual: + operatorName = "<="; + break; + case Clingo::AST::ComparisonOperator::GreaterEqual: + operatorName = ">="; + break; + case Clingo::AST::ComparisonOperator::NotEqual: + operatorName = "!="; + break; + case Clingo::AST::ComparisonOperator::Equal: + operatorName = "="; + break; + } + + std::cout + << "exists " << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID) + << ", " << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + 1) + << " (" + << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID) + << " in " << comparison.left + << " and " + << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + 1) + << " in " << comparison.right + << " and " + << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID) + << operatorName + << AuxiliaryBodyVariablePrefix << (context.auxiliaryBodyLiteralID + 1) + << ")"; + + context.auxiliaryBodyLiteralID += 2; + } + + void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &) + { + throwErrorAtLocation(literal.location, "CSP literals currently unsupported"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct BodyLiteralPrintVisitor +{ + void visit(const Clingo::AST::Literal &literal, const Clingo::AST::BodyLiteral &, Context &context) + { + if (literal.sign != Clingo::AST::Sign::None) + throwErrorAtLocation(literal.location, "only positive literals currently supported"); + + literal.data.accept(LiteralPrintVisitor(), literal, context); + } + + void visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &) + { + throwErrorAtLocation(bodyLiteral.location, "“conditional literal” body literals currently unsupported"); + } + + void visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &) + { + throwErrorAtLocation(bodyLiteral.location, "“aggregate” body literals currently unsupported"); + } + + void visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &) + { + throwErrorAtLocation(bodyLiteral.location, "“body aggregate” body literals currently unsupported"); + } + + void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &) + { + throwErrorAtLocation(bodyLiteral.location, "“theory atom” body literals currently unsupported"); + } + + void visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &) + { + throwErrorAtLocation(bodyLiteral.location, "“disjoint” body literals currently unsupported"); + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/Context.h b/include/anthem/Context.h new file mode 100644 index 0000000..0e3a17e --- /dev/null +++ b/include/anthem/Context.h @@ -0,0 +1,22 @@ +#ifndef __ANTHEM__CONTEXT_H +#define __ANTHEM__CONTEXT_H + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Context +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +struct Context +{ + int auxiliaryBodyLiteralID = 0; +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/Head.h b/include/anthem/Head.h index db50664..2f717a3 100644 --- a/include/anthem/Head.h +++ b/include/anthem/Head.h @@ -170,7 +170,7 @@ struct TermPrintSubstitutedVisitor assert(matchingTerm != terms.cend()); - std::cout << AuxiliaryVariablePrefix << (matchingTerm - terms.cbegin()); + std::cout << AuxiliaryHeadVariablePrefix << (matchingTerm - terms.cbegin()); } std::cout << ")"; diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 8d9ed3b..8722f9b 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -1,7 +1,7 @@ #ifndef __ANTHEM__STATEMENT_VISITOR_H #define __ANTHEM__STATEMENT_VISITOR_H -#include +#include #include #include @@ -37,6 +37,8 @@ struct StatementVisitor void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &) { + Context context; + // Concatenate all head terms std::vector headTerms; rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, headTerms); @@ -52,24 +54,26 @@ struct StatementVisitor std::cout << ", "; std::cout - << AuxiliaryVariablePrefix << (i - headTerms.cbegin()) + << AuxiliaryHeadVariablePrefix << (i - headTerms.cbegin()) << " in " << headTerm; } - - std::cout << " and "; } - std::cout << "[body] -> "; - - /*rule.head.data.accept(HeadLiteralVisitor(), rule.head); - - for (const auto &bodyLiteral : rule.body) + // Print translated body literals + for (auto i = rule.body.cbegin(); i != rule.body.cend(); i++) { + const auto &bodyLiteral = *i; + + if (!headTerms.empty()) + std::cout << " and "; + if (bodyLiteral.sign != Clingo::AST::Sign::None) throwErrorAtLocation(bodyLiteral.location, "only positive literals currently supported"); - bodyLiteral.data.accept(BodyLiteralVisitor(), bodyLiteral); - }*/ + bodyLiteral.data.accept(BodyLiteralPrintVisitor(), bodyLiteral, context); + } + + std::cout << " -> "; // Print consequent of the implication rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, headTerms); diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index c8eb43a..929364d 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -27,7 +27,8 @@ inline void throwErrorAtLocation(const Clingo::Location &location, const char *e //////////////////////////////////////////////////////////////////////////////////////////////////// -constexpr const auto AuxiliaryVariablePrefix = "AUX"; +constexpr const auto AuxiliaryHeadVariablePrefix = "AUX_H"; +constexpr const auto AuxiliaryBodyVariablePrefix = "AUX_B"; ////////////////////////////////////////////////////////////////////////////////////////////////////