Implemented translation of positive body literals.

This commit is contained in:
Patrick Lühne 2016-11-23 04:41:38 +01:00
parent ba8f68c5d4
commit 29d1c15137
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
5 changed files with 248 additions and 13 deletions

208
include/anthem/Body.h Normal file
View File

@ -0,0 +1,208 @@
#ifndef __ANTHEM__BODY_H
#define __ANTHEM__BODY_H
#include <algorithm>
#include <anthem/Context.h>
#include <anthem/Utils.h>
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

22
include/anthem/Context.h Normal file
View File

@ -0,0 +1,22 @@
#ifndef __ANTHEM__CONTEXT_H
#define __ANTHEM__CONTEXT_H
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Context
//
////////////////////////////////////////////////////////////////////////////////////////////////////
struct Context
{
int auxiliaryBodyLiteralID = 0;
};
////////////////////////////////////////////////////////////////////////////////////////////////////
}
#endif

View File

@ -170,7 +170,7 @@ struct TermPrintSubstitutedVisitor
assert(matchingTerm != terms.cend()); assert(matchingTerm != terms.cend());
std::cout << AuxiliaryVariablePrefix << (matchingTerm - terms.cbegin()); std::cout << AuxiliaryHeadVariablePrefix << (matchingTerm - terms.cbegin());
} }
std::cout << ")"; std::cout << ")";

View File

@ -1,7 +1,7 @@
#ifndef __ANTHEM__STATEMENT_VISITOR_H #ifndef __ANTHEM__STATEMENT_VISITOR_H
#define __ANTHEM__STATEMENT_VISITOR_H #define __ANTHEM__STATEMENT_VISITOR_H
#include <anthem/BodyLiteralVisitor.h> #include <anthem/Body.h>
#include <anthem/Head.h> #include <anthem/Head.h>
#include <anthem/Utils.h> #include <anthem/Utils.h>
@ -37,6 +37,8 @@ struct StatementVisitor
void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &) void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &)
{ {
Context context;
// Concatenate all head terms // Concatenate all head terms
std::vector<const Clingo::AST::Term *> headTerms; std::vector<const Clingo::AST::Term *> headTerms;
rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, headTerms); rule.head.data.accept(HeadLiteralCollectFunctionTermsVisitor(), rule.head, headTerms);
@ -52,24 +54,26 @@ struct StatementVisitor
std::cout << ", "; std::cout << ", ";
std::cout std::cout
<< AuxiliaryVariablePrefix << (i - headTerms.cbegin()) << AuxiliaryHeadVariablePrefix << (i - headTerms.cbegin())
<< " in " << headTerm; << " in " << headTerm;
} }
std::cout << " and ";
} }
std::cout << "[body] -> "; // Print translated body literals
for (auto i = rule.body.cbegin(); i != rule.body.cend(); i++)
/*rule.head.data.accept(HeadLiteralVisitor(), rule.head);
for (const auto &bodyLiteral : rule.body)
{ {
const auto &bodyLiteral = *i;
if (!headTerms.empty())
std::cout << " and ";
if (bodyLiteral.sign != Clingo::AST::Sign::None) if (bodyLiteral.sign != Clingo::AST::Sign::None)
throwErrorAtLocation(bodyLiteral.location, "only positive literals currently supported"); 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 // Print consequent of the implication
rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, headTerms); rule.head.data.accept(HeadLiteralPrintSubstitutedVisitor(), rule.head, headTerms);

View File

@ -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";
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////