From 838a68e2306b8bc848f3d1afe1fb1b4d1123c4c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Wed, 5 Apr 2017 18:15:42 +0200 Subject: [PATCH] Refactoring to prepare for implementing completion. --- app/main.cpp | 3 +- include/anthem/Context.h | 1 + include/anthem/StatementVisitor.h | 50 +++++++++++++++++-------------- include/anthem/Utils.h | 1 + src/anthem/Translation.cpp | 30 ++++++++----------- 5 files changed, 44 insertions(+), 41 deletions(-) diff --git a/app/main.cpp b/app/main.cpp index e09adb2..c2eb7bc 100644 --- a/app/main.cpp +++ b/app/main.cpp @@ -17,7 +17,8 @@ int main(int argc, char **argv) ("version,v", "Display version information") ("input,i", po::value>(), "Input files") ("simplify,s", po::bool_switch(&context.simplify), "Simplify the output") - ("color,c", po::value()->default_value("auto"), "Colorize output (always, never, auto)") + ("complete,c", po::bool_switch(&context.complete), "Perform completion") + ("color", po::value()->default_value("auto"), "Colorize output (always, never, auto)") ("log-priority,p", po::value()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)"); po::positional_options_description positionalOptionsDescription; diff --git a/include/anthem/Context.h b/include/anthem/Context.h index 3129f37..026ebd1 100644 --- a/include/anthem/Context.h +++ b/include/anthem/Context.h @@ -34,6 +34,7 @@ struct Context size_t anonymousVariableID = 1; bool simplify = false; + bool complete = false; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/StatementVisitor.h b/include/anthem/StatementVisitor.h index cede5af..b895d3b 100644 --- a/include/anthem/StatementVisitor.h +++ b/include/anthem/StatementVisitor.h @@ -16,20 +16,35 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// +// Replaces empty and 1-element conjunctions in the antecedent of normal-form formulas +inline void reduce(ast::Implies &implies) +{ + if (!implies.antecedent.is()) + return; + + auto &antecedent = implies.antecedent.get(); + + // Use “true” as the consequent in case it is empty + if (antecedent.arguments.empty()) + implies.antecedent = ast::Formula::make(true); + else if (antecedent.arguments.size() == 1) + implies.antecedent = std::move(antecedent.arguments[0]); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + struct StatementVisitor { - std::vector visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, Context &context) + void visit(const Clingo::AST::Program &program, const Clingo::AST::Statement &statement, std::vector &, Context &context) { // TODO: refactor context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str()); if (!program.parameters.empty()) throwErrorAtLocation(statement.location, "program parameters currently unsupported", context); - - return {}; } - std::vector visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, Context &context) + void visit(const Clingo::AST::Rule &rule, const Clingo::AST::Statement &, std::vector &formulas, Context &context) { context.reset(); @@ -43,8 +58,9 @@ struct StatementVisitor if (!consequent) { + // TODO: think about throwing an exception instead context.logger.log(output::Priority::Error, "could not translate formula consequent"); - return {}; + return; } // Generate auxiliary variables replacing the head atom’s arguments @@ -73,10 +89,11 @@ struct StatementVisitor antecedent.arguments.emplace_back(std::move(argument.value())); } - std::vector formulas; - if (!context.isChoiceRule) + { formulas.emplace_back(ast::Formula::make(std::move(antecedent), std::move(consequent.value()))); + reduce(formulas.back().get()); + } else { const auto createFormula = @@ -92,6 +109,8 @@ struct StatementVisitor auto &implies = formulas.back().get(); auto &antecedent = implies.antecedent.get(); antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent)); + + reduce(implies); }; if (consequent.value().is()) @@ -105,27 +124,12 @@ struct StatementVisitor else createFormula(consequent.value(), true); } - - for (auto &formula : formulas) - { - auto &implies = formula.get(); - auto &antecedent = implies.antecedent.get(); - - // Use “true” as the consequent in case it is empty - if (antecedent.arguments.empty()) - implies.antecedent = ast::Formula::make(true); - else if (antecedent.arguments.size() == 1) - implies.antecedent = std::move(antecedent.arguments[0]);; - } - - return formulas; } template - std::vector visit(const T &, const Clingo::AST::Statement &statement, Context &context) + void visit(const T &, const Clingo::AST::Statement &statement, std::vector &, Context &context) { throwErrorAtLocation(statement.location, "statement currently unsupported, expected rule", context); - return {}; } }; diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index a6f4fdd..6f365d8 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -36,6 +36,7 @@ inline void throwErrorAtLocation(const Clingo::Location &clingoLocation, const c { const auto location = location_cast(clingoLocation); + // TODO: think about removing this to avoid double error messages context.logger.log(output::Priority::Error, location, errorMessage); throw std::runtime_error(errorMessage); diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 9ba0278..432eb52 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -39,26 +39,12 @@ void translate(const char *fileName, std::istream &stream, Context &context) auto fileContent = std::string(std::istreambuf_iterator(stream), {}); - bool isFirstStatement = true; + std::vector formulas; const auto translateStatement = - [&context, &isFirstStatement](const Clingo::AST::Statement &statement) + [&formulas, &context](const Clingo::AST::Statement &statement) { - auto formulas = statement.data.accept(StatementVisitor(), statement, context); - - if (!isFirstStatement) - context.logger.outputStream() << std::endl; - - for (auto &formula : formulas) - { - if (context.simplify) - simplify(formula); - - context.logger.outputStream() << formula << std::endl; - } - - if (!formulas.empty()) - isFirstStatement = false; + statement.data.accept(StatementVisitor(), statement, formulas, context); }; const auto logger = @@ -68,6 +54,16 @@ void translate(const char *fileName, std::istream &stream, Context &context) }; Clingo::parse_program(fileContent.c_str(), translateStatement, logger); + + for (auto i = formulas.begin(); i != formulas.end(); i++) + { + auto &formula = *i; + + if (context.simplify) + simplify(formula); + + context.logger.outputStream() << formula << std::endl; + } } ////////////////////////////////////////////////////////////////////////////////////////////////////