Refactoring to prepare for implementing completion.

This commit is contained in:
Patrick Lühne 2017-04-05 18:15:42 +02:00
parent 5940fc4a3b
commit 838a68e230
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
5 changed files with 44 additions and 41 deletions

View File

@ -17,7 +17,8 @@ int main(int argc, char **argv)
("version,v", "Display version information") ("version,v", "Display version information")
("input,i", po::value<std::vector<std::string>>(), "Input files") ("input,i", po::value<std::vector<std::string>>(), "Input files")
("simplify,s", po::bool_switch(&context.simplify), "Simplify the output") ("simplify,s", po::bool_switch(&context.simplify), "Simplify the output")
("color,c", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)") ("complete,c", po::bool_switch(&context.complete), "Perform completion")
("color", po::value<std::string>()->default_value("auto"), "Colorize output (always, never, auto)")
("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)"); ("log-priority,p", po::value<std::string>()->default_value("warning"), "Log messages starting from this priority (debug, info, warning, error)");
po::positional_options_description positionalOptionsDescription; po::positional_options_description positionalOptionsDescription;

View File

@ -34,6 +34,7 @@ struct Context
size_t anonymousVariableID = 1; size_t anonymousVariableID = 1;
bool simplify = false; bool simplify = false;
bool complete = false;
}; };
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@ -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<ast::And>())
return;
auto &antecedent = implies.antecedent.get<ast::And>();
// Use “true” as the consequent in case it is empty
if (antecedent.arguments.empty())
implies.antecedent = ast::Formula::make<ast::Boolean>(true);
else if (antecedent.arguments.size() == 1)
implies.antecedent = std::move(antecedent.arguments[0]);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
struct StatementVisitor struct StatementVisitor
{ {
std::vector<ast::Formula> 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<ast::Formula> &, Context &context)
{ {
// TODO: refactor // TODO: refactor
context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str()); context.logger.log(output::Priority::Debug, (std::string("[program] ") + program.name).c_str());
if (!program.parameters.empty()) if (!program.parameters.empty())
throwErrorAtLocation(statement.location, "program parameters currently unsupported", context); throwErrorAtLocation(statement.location, "program parameters currently unsupported", context);
return {};
} }
std::vector<ast::Formula> 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<ast::Formula> &formulas, Context &context)
{ {
context.reset(); context.reset();
@ -43,8 +58,9 @@ struct StatementVisitor
if (!consequent) if (!consequent)
{ {
// TODO: think about throwing an exception instead
context.logger.log(output::Priority::Error, "could not translate formula consequent"); context.logger.log(output::Priority::Error, "could not translate formula consequent");
return {}; return;
} }
// Generate auxiliary variables replacing the head atoms arguments // Generate auxiliary variables replacing the head atoms arguments
@ -73,10 +89,11 @@ struct StatementVisitor
antecedent.arguments.emplace_back(std::move(argument.value())); antecedent.arguments.emplace_back(std::move(argument.value()));
} }
std::vector<ast::Formula> formulas;
if (!context.isChoiceRule) if (!context.isChoiceRule)
{
formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value()))); formulas.emplace_back(ast::Formula::make<ast::Implies>(std::move(antecedent), std::move(consequent.value())));
reduce(formulas.back().get<ast::Implies>());
}
else else
{ {
const auto createFormula = const auto createFormula =
@ -92,6 +109,8 @@ struct StatementVisitor
auto &implies = formulas.back().get<ast::Implies>(); auto &implies = formulas.back().get<ast::Implies>();
auto &antecedent = implies.antecedent.get<ast::And>(); auto &antecedent = implies.antecedent.get<ast::And>();
antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent)); antecedent.arguments.emplace_back(ast::deepCopy(implies.consequent));
reduce(implies);
}; };
if (consequent.value().is<ast::Or>()) if (consequent.value().is<ast::Or>())
@ -105,27 +124,12 @@ struct StatementVisitor
else else
createFormula(consequent.value(), true); createFormula(consequent.value(), true);
} }
for (auto &formula : formulas)
{
auto &implies = formula.get<ast::Implies>();
auto &antecedent = implies.antecedent.get<ast::And>();
// Use “true” as the consequent in case it is empty
if (antecedent.arguments.empty())
implies.antecedent = ast::Formula::make<ast::Boolean>(true);
else if (antecedent.arguments.size() == 1)
implies.antecedent = std::move(antecedent.arguments[0]);;
}
return formulas;
} }
template<class T> template<class T>
std::vector<ast::Formula> visit(const T &, const Clingo::AST::Statement &statement, Context &context) void visit(const T &, const Clingo::AST::Statement &statement, std::vector<ast::Formula> &, Context &context)
{ {
throwErrorAtLocation(statement.location, "statement currently unsupported, expected rule", context); throwErrorAtLocation(statement.location, "statement currently unsupported, expected rule", context);
return {};
} }
}; };

View File

@ -36,6 +36,7 @@ inline void throwErrorAtLocation(const Clingo::Location &clingoLocation, const c
{ {
const auto location = location_cast<input::Location>(clingoLocation); const auto location = location_cast<input::Location>(clingoLocation);
// TODO: think about removing this to avoid double error messages
context.logger.log(output::Priority::Error, location, errorMessage); context.logger.log(output::Priority::Error, location, errorMessage);
throw std::runtime_error(errorMessage); throw std::runtime_error(errorMessage);

View File

@ -39,26 +39,12 @@ void translate(const char *fileName, std::istream &stream, Context &context)
auto fileContent = std::string(std::istreambuf_iterator<char>(stream), {}); auto fileContent = std::string(std::istreambuf_iterator<char>(stream), {});
bool isFirstStatement = true; std::vector<ast::Formula> formulas;
const auto translateStatement = 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); statement.data.accept(StatementVisitor(), statement, formulas, 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;
}; };
const auto logger = 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); 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;
}
} }
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////