From 283cdd2abff1713b2dc8d426e35e905c028c95eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Thu, 23 Mar 2017 01:23:17 +0100 Subject: [PATCH] Preparations for returning multiple formulas per input rule (as necessary with head aggregates). --- include/anthem/StatementVisitor.h | 58 +++++++++++++++---------------- src/anthem/Translation.cpp | 31 +++++++++++------ 2 files changed, 49 insertions(+), 40 deletions(-) diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index 7563be4..2aa14c4 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -18,7 +18,7 @@ namespace anthem struct StatementVisitor { - std::experimental::optional visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context) + std::vector 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::Boolean(true), std::move(consequent.value())); + return {ast::Formula::make(ast::Boolean(true), std::move(consequent.value()))}; else if (antecedent.arguments.size() == 1) - return ast::Formula::make(std::move(antecedent.arguments[0]), std::move(consequent.value())); + return {ast::Formula::make(std::move(antecedent.arguments[0]), std::move(consequent.value()))}; - return ast::Formula::make(std::move(antecedent), std::move(consequent.value())); + return {ast::Formula::make(std::move(antecedent), std::move(consequent.value()))}; } - std::experimental::optional visit(const Clingo::AST::Definition &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::ShowSignature &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::ShowTerm &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::Minimize &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::Script &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::External &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::Edge &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::Heuristic &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::ProjectAtom &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::ProjectSignature &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 visit(const Clingo::AST::TheoryDefinition &, const Clingo::AST::Statement &statement, Context &context) + std::vector 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 {}; } }; diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index d71c919..e03b510 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -39,22 +39,31 @@ void translate(const char *fileName, std::istream &stream, Context &context) auto fileContent = std::string(std::istreambuf_iterator(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 =