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

Preparations for returning multiple formulas per input rule (as necessary with head aggregates).

This commit is contained in:
Patrick Lühne 2017-03-23 01:23:17 +01:00
parent 9084e72303
commit 283cdd2abf
No known key found for this signature in database
GPG Key ID: 05F3611E97A70ABF
2 changed files with 49 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

58
include/anthem/StatementVisitor.h
View File

@ -18,7 +18,7 @@ namespace anthem
struct StatementVisitor
{
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context)
{
// TODO: refactor
context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str());
@ -26,10 +26,10 @@ struct StatementVisitor
if (!program.parameters.empty())
throwErrorAtLocation(statement.location, "program parameters currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context)
{
context.reset();
@ -44,7 +44,7 @@ struct StatementVisitor
if (!consequent)
{
context.logger.log(output::Priority::Error, "could not translate formula consequent");
return std::experimental::nullopt;
return {};
}
// Print auxiliary variables replacing the head atom’s arguments
@ -82,77 +82,77 @@ struct StatementVisitor
// Use “true” as the consequent in case it is empty
if (antecedent.arguments.empty())
return ast::Formula::make<ast::Implies>(ast::Boolean(true), std::move(consequent.value()));
return {ast::Formula::make<ast::Implies>(ast::Boolean(true), std::move(consequent.value()))};
else if (antecedent.arguments.size() == 1)
return ast::Formula::make<ast::Implies>(std::move(antecedent.arguments[0]), std::move(consequent.value()));
return {ast::Formula::make<ast::Implies>(std::move(antecedent.arguments[0]), std::move(consequent.value()))};
return ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()));
return {ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()))};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“definition” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“show signature” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“show term” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“minimize” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“script” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“external” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“edge” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“heuristic” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“project atom” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“project signature” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
std::experimental::optional<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
std::vector<ast::Formula> visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context)
{
throwErrorAtLocation(statement.location, "“theory definition” statements currently unsupported", context);
return std::experimental::nullopt;
return {};
}
};

31
src/anthem/Translation.cpp
View File

@ -39,22 +39,31 @@ void translate(const char *fileName, std::istream &stream, Context &context)
auto fileContent = std::string(std::istreambuf_iterator<char>(stream), {});
const auto translateStatement =
[&context](const Clingo::AST::Statement &statement)
bool isFirstStatement = true;
const auto printFormula =
[&context, &isFirstStatement](const ast::Formula &formula)
{
auto formula = statement.data.accept(StatementVisitor(), statement, context);
if (!isFirstStatement)
context.logger.outputStream() << std::endl;
if (!formula)
return;
context.logger.outputStream() << formula << std::endl;
if (!context.simplify)
isFirstStatement = false;
};
const auto translateStatement =
[&context, &printFormula](const Clingo::AST::Statement &statement)
{
auto formulas = statement.data.accept(StatementVisitor(), statement, context);
for (auto &formula : formulas)
{
context.logger.outputStream() << formula.value() << std::endl;
return;
}
if (context.simplify)
simplify(formula);
simplify(formula.value());
context.logger.outputStream() << formula.value() << std::endl;
printFormula(formula);
}
};
const auto logger =