patrick
/
anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Cleaned up clingo rule head and body visitors.

This commit is contained in:
Patrick Lühne 2017-03-28 18:07:06 +02:00
parent c63d74092e
commit a93d59c2a4
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
2 changed files with 28 additions and 157 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

78
include/anthem/Body.h
View File

@ -51,36 +51,6 @@ ast::Variable makeAuxiliaryBodyVariable(int i)
struct BodyTermTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::Symbol &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“symbol” terms currently unsupported in this context", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Variable &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“variable” terms currently unsupported in this context", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported in this context", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported in this context", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Interval &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“interval” terms currently unsupported in this context", context);
return std::experimental::nullopt;
}
// TODO: refactor
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Literal &literal, const Clingo::AST::Term &, Context &context)
{
@ -120,9 +90,10 @@ struct BodyTermTranslateVisitor
return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Pool &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“pool” terms currently unsupported", context);
throwErrorAtLocation(term.location, "term currently unsupported in this context, expected function", context);
return std::experimental::nullopt;
}
};
@ -131,16 +102,9 @@ struct BodyTermTranslateVisitor
struct BodyLiteralTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Boolean &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "“boolean” literals currently unsupported in this context", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Term &term, const Clingo::AST::Literal &literal, Context &context)
{
return term.data.accept(BodyTermTranslateVisitor(), literal, term, context);
return std::experimental::nullopt;
}
// TODO: refactor
@ -148,7 +112,7 @@ struct BodyLiteralTranslateVisitor
{
// Comparisons should never have a sign, because these are converted to positive comparisons by clingo
if (literal.sign != Clingo::AST::Sign::None)
throwErrorAtLocation(literal.location, "negated comparisons in body currently unsupported", context);
throwErrorAtLocation(literal.location, "negated comparisons currently unsupported", context);
const auto operator_ = translate(comparison.comparison);
@ -168,9 +132,10 @@ struct BodyLiteralTranslateVisitor
return ast::Formula::make<ast::Exists>(std::move(variables), std::move(conjunction));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "CSP literals currently unsupported", context);
throwErrorAtLocation(literal.location, "literal currently unsupported in this context, expected function or term", context);
return std::experimental::nullopt;
}
};
@ -184,33 +149,10 @@ struct BodyBodyLiteralTranslateVisitor
return literal.data.accept(BodyLiteralTranslateVisitor(), literal, context);
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::ConditionalLiteral &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
{
throwErrorAtLocation(bodyLiteral.location, "“conditional literal” body literals currently unsupported", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
{
throwErrorAtLocation(bodyLiteral.location, "“aggregate” body literals currently unsupported", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::BodyAggregate &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
{
throwErrorAtLocation(bodyLiteral.location, "“body aggregate” body literals currently unsupported", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
{
throwErrorAtLocation(bodyLiteral.location, "“theory atom” body literals currently unsupported", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Disjoint &, const Clingo::AST::BodyLiteral &bodyLiteral, Context &context)
{
throwErrorAtLocation(bodyLiteral.location, "“disjoint” body literals currently unsupported", context);
throwErrorAtLocation(bodyLiteral.location, "body literal currently unsupported in this context, expected literal", context);
return std::experimental::nullopt;
}
};

107
include/anthem/Head.h
View File

@ -18,31 +18,6 @@ namespace anthem
struct TermCollectFunctionTermsVisitor
{
void visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected", context);
}
void visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected", context);
}
void visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected", context);
}
void visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected", context);
}
void visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected", context);
}
void visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context)
{
if (function.external)
@ -54,9 +29,10 @@ struct TermCollectFunctionTermsVisitor
context.headTerms.emplace_back(&argument);
}
void visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context)
template<class T>
void visit(const T &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected", context);
throwErrorAtLocation(term.location, "term currently unsupported in this context, function expected", context);
}
};
@ -73,12 +49,8 @@ struct LiteralCollectFunctionTermsVisitor
term.data.accept(TermCollectFunctionTermsVisitor(), term, context);
}
void visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
}
void visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
template<class T>
void visit(const T &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
}
@ -115,7 +87,7 @@ struct HeadLiteralCollectFunctionTermsVisitor
context.numberOfHeadLiterals = aggregate.elements.size();
if (aggregate.left_guard || aggregate.right_guard)
throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards not allowed", context);
throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards currently unsupported", context);
for (const auto &conditionalLiteral : aggregate.elements)
{
@ -126,14 +98,10 @@ struct HeadLiteralCollectFunctionTermsVisitor
}
}
void visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
template<class T>
void visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
{
throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported", context);
}
void visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
{
throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported", context);
throwErrorAtLocation(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate", context);
}
};
@ -141,36 +109,6 @@ struct HeadLiteralCollectFunctionTermsVisitor
struct FunctionTermTranslateVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::Symbol &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“symbol” terms not allowed, function expected", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Variable &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“variable” terms currently unsupported, function expected", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::UnaryOperation &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“unary operation” terms currently unsupported, function expected", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::BinaryOperation &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“binary operation” terms currently unsupported, function expected", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Interval &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“interval” terms currently unsupported, function expected", context);
return std::experimental::nullopt;
}
// TODO: check correctness
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Function &function, const Clingo::AST::Term &term, Context &context)
{
@ -194,9 +132,10 @@ struct FunctionTermTranslateVisitor
return ast::Formula::make<ast::Predicate>(function.name, std::move(arguments));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Pool &, const Clingo::AST::Term &term, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Term &term, Context &context)
{
throwErrorAtLocation(term.location, "“pool” terms currently unsupported, function expected", context);
throwErrorAtLocation(term.location, "term currently unsupported in this context, function expected", context);
return std::experimental::nullopt;
}
};
@ -215,13 +154,8 @@ struct LiteralTranslateVisitor
return term.data.accept(FunctionTermTranslateVisitor(), term, context);
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Comparison &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::CSPLiteral &, const Clingo::AST::Literal &literal, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::Literal &literal, Context &context)
{
throwErrorAtLocation(literal.location, "only disjunctions of literals allowed as head literals", context);
return std::experimental::nullopt;
@ -272,7 +206,7 @@ struct HeadLiteralTranslateToConsequentVisitor
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Aggregate &aggregate, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
{
if (aggregate.left_guard || aggregate.right_guard)
throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards not allowed", context);
throwErrorAtLocation(headLiteral.location, "aggregates with left or right guards currently unsupported", context);
const auto translateConditionalLiteral =
[&](const auto &conditionalLiteral)
@ -302,15 +236,10 @@ struct HeadLiteralTranslateToConsequentVisitor
return ast::Formula::make<ast::Or>(std::move(arguments));
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::HeadAggregate &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
template<class T>
std::experimental::optional<ast::Formula> visit(const T &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
{
throwErrorAtLocation(headLiteral.location, "“head aggregate” head literals currently unsupported", context);
return std::experimental::nullopt;
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryAtom &, const Clingo::AST::HeadLiteral &headLiteral, Context &context)
{
throwErrorAtLocation(headLiteral.location, "“theory” head literals currently unsupported", context);
throwErrorAtLocation(headLiteral.location, "head literal currently unsupported in this context, expected literal, disjunction, or aggregate", context);
return std::experimental::nullopt;
}
};