From 0b0dc06f6ad3eb82fac9b4871e291bcf87bb18ee Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Tue, 7 Mar 2017 20:11:52 +1100 Subject: [PATCH] TUI prints normalised formulas now; fixed PRINT_ABBREVIATIONS. --- ...{test-ws-1.lela => test-ws-zoomed-by.lela} | 1 - examples/tui/tui-js.cc | 6 +- examples/tui/tui.cc | 60 ++++++++++--------- src/lela/format/output.h | 28 ++++++++- 4 files changed, 61 insertions(+), 34 deletions(-) rename examples/tui/{test-ws-1.lela => test-ws-zoomed-by.lela} (97%) diff --git a/examples/tui/test-ws-1.lela b/examples/tui/test-ws-zoomed-by.lela similarity index 97% rename from examples/tui/test-ws-1.lela rename to examples/tui/test-ws-zoomed-by.lela index 95ca7f4..ac71423 100644 --- a/examples/tui/test-ws-1.lela +++ b/examples/tui/test-ws-zoomed-by.lela @@ -1,5 +1,4 @@ // Which party is more plausible? -// Author: Denis Golovin Sort PARTY Sort BOOL diff --git a/examples/tui/tui-js.cc b/examples/tui/tui-js.cc index 8e098a6..8c4bfdf 100644 --- a/examples/tui/tui-js.cc +++ b/examples/tui/tui-js.cc @@ -67,7 +67,7 @@ struct Callback : public lela::format::pdl::DefaultCallback { void operator()(T* ctx, const std::string& proc, const std::vector& args) { if (proc == "print_kb") { for (lela::KnowledgeBase::sphere_index p = 0; p < ctx->kb()->n_spheres(); ++p) { - std::cerr << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl; + std::cout << "Setup[" << p << "] = " << std::endl << ctx->kb()->sphere(p)->setup() << std::endl; } } else if (proc == "print") { lela::format::print_range(std::cout, args, "", "", " "); @@ -81,9 +81,9 @@ struct Callback : public lela::format::pdl::DefaultCallback { } else if (su_(ctx, proc, args)) { // it's a call for Sudoku } else { - std::cerr << "Calling " << proc; + std::cout << "Calling " << proc; lela::format::print_range(std::cerr, args, "(", ")", ","); - std::cerr << " failed" << std::endl; + std::cout << " failed" << std::endl; } } diff --git a/examples/tui/tui.cc b/examples/tui/tui.cc index 77440e5..066c2ec 100644 --- a/examples/tui/tui.cc +++ b/examples/tui/tui.cc @@ -3,6 +3,8 @@ // // Command line application that interprets a problem description and queries. +//#define PRINT_ABBREVIATIONS + #include #include @@ -108,33 +110,6 @@ class multi_pass_iterator { size_t index_ = 0; }; -struct Logger : public lela::format::pdl::DefaultLogger { - void operator()(const LogData&) const { std::cerr << "Unknown log data" << std::endl; } - void operator()(const RegisterData& d) const { std::cerr << "Registered " << d.id << std::endl; } - void operator()(const RegisterSortData& d) const { std::cerr << "Registered sort " << d.id << std::endl; } - void operator()(const RegisterVariableData& d) const { std::cerr << "Registered variable " << d.id << " of sort " << d.sort_id << std::endl; } - void operator()(const RegisterNameData& d) const { std::cerr << "Registered name " << d.id << " of sort " << d.sort_id << std::endl; } - void operator()(const RegisterFunctionData& d) const { std::cerr << "Registered function symbol " << d.id << " with arity " << int(d.arity) << " of sort " << d.sort_id << std::endl; } - void operator()(const RegisterMetaVariableData& d) const { std::cerr << "Registered meta variable " << d.id << " for " << d.term << std::endl; } - void operator()(const RegisterFormulaData& d) const { std::cerr << "Registered formula " << d.id << " as " << *d.phi << std::endl; } - void operator()(const UnregisterData& d) const { std::cerr << "Unregistered " << d.id << std::endl; } - void operator()(const UnregisterMetaVariableData& d) const { std::cerr << "Unregistered meta variable " << d.id << std::endl; } - void operator()(const AddToKbData& d) const { std::cerr << "Added " << d.alpha << " " << (d.ok ? "" : "un") << "successfully" << std::endl; } - void operator()(const QueryData& d) const { - //for (lela::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) { - // std::cout << "Setup[" << p << "] = " << std::endl << d.kb.sphere(p).setup() << std::endl; - //} - if (print_queries) { - std::cout << "Query: " << *d.phi << " = " << in_color(d.yes ? "Yes" : "No", d.yes ? GREEN : RED) << std::endl; - } else { - std::cout << "Query: " << *d.phi << " = " << in_color(d.yes ? "Yes" : "No", d.yes ? GREEN : RED) << std::endl; - } - //std::cout << std::endl; - //std::cout << std::endl; - } - bool print_queries = true; -}; - struct Callback : public lela::format::pdl::DefaultCallback { template void operator()(T* ctx, const std::string& proc, const std::vector& args) { @@ -165,6 +140,36 @@ struct Callback : public lela::format::pdl::DefaultCallback { SudokuCallbacks su_; }; +struct Logger : public lela::format::pdl::DefaultLogger { + void operator()(const LogData&) const { std::cerr << "Unknown log data" << std::endl; } + void operator()(const RegisterData& d) const { std::cerr << "Registered " << d.id << std::endl; } + void operator()(const RegisterSortData& d) const { std::cerr << "Registered sort " << d.id << std::endl; } + void operator()(const RegisterVariableData& d) const { std::cerr << "Registered variable " << d.id << " of sort " << d.sort_id << std::endl; } + void operator()(const RegisterNameData& d) const { std::cerr << "Registered name " << d.id << " of sort " << d.sort_id << std::endl; } + void operator()(const RegisterFunctionData& d) const { std::cerr << "Registered function symbol " << d.id << " with arity " << int(d.arity) << " of sort " << d.sort_id << std::endl; } + void operator()(const RegisterMetaVariableData& d) const { std::cerr << "Registered meta variable " << d.id << " for " << d.term << std::endl; } + void operator()(const RegisterFormulaData& d) const { std::cerr << "Registered formula " << d.id << " as " << *d.phi << std::endl; } + void operator()(const UnregisterData& d) const { std::cerr << "Unregistered " << d.id << std::endl; } + void operator()(const UnregisterMetaVariableData& d) const { std::cerr << "Unregistered meta variable " << d.id << std::endl; } + void operator()(const AddToKbData& d) const { std::cerr << "Added " << d.alpha << " " << (d.ok ? "" : "un") << "successfully" << std::endl; } + void operator()(const QueryData& d) const { + //for (lela::KnowledgeBase::sphere_index p = 0; p < d.kb.n_spheres(); ++p) { + // std::cout << "Setup[" << p << "] = " << std::endl << d.kb.sphere(p).setup() << std::endl; + //} + std::ostream* os; + if (print_queries) { + os = &std::cout; + } else { + os = &std::cerr; + } + *os << "Query: " << d.phi->NF(ctx->sf(), ctx->tf()) << " = " << in_color(d.yes ? "Yes" : "No", d.yes ? GREEN : RED) << std::endl; + //std::cout << std::endl; + //std::cout << std::endl; + } + bool print_queries = true; + lela::format::pdl::Context* ctx; +}; + int main(int argc, char** argv) { const int kFailCode = 1; const int kHelpCode = 2; @@ -206,6 +211,7 @@ int main(int argc, char** argv) { std::ios_base::sync_with_stdio(true); lela::format::pdl::Context ctx; + ctx.logger()->ctx = &ctx; for (const std::string& arg : args) { std::ifstream stream(arg); diff --git a/src/lela/format/output.h b/src/lela/format/output.h index 5d803b9..09dedca 100644 --- a/src/lela/format/output.h +++ b/src/lela/format/output.h @@ -242,9 +242,22 @@ std::ostream& operator<<(std::ostream& os, const Setup& s) { #define LELA_FORMULA_OUTPUT std::ostream& operator<<(std::ostream& os, const Formula& alpha) { switch (alpha.type()) { - case Formula::kAtomic: - os << alpha.as_atomic().arg(); + case Formula::kAtomic: { + const Clause& c = alpha.as_atomic().arg(); +#ifdef PRINT_ABBREVIATIONS + if (c.empty()) { + os << "\u22A5"; + } else if (c.unit()) { + os << c.first(); + } else { + auto as = internal::transform_range(c.begin(), c.end(), [](Literal a) { return a; }); + print_sequence(os, as.begin(), as.end(), "[", "]", " \u2227 "); + } +#else + os << c; +#endif break; + } case Formula::kNot: #ifdef PRINT_ABBREVIATIONS if (alpha.as_not().arg().type() == Formula::kOr && @@ -255,9 +268,18 @@ std::ostream& operator<<(std::ostream& os, const Formula& alpha) { << ' ' << "\u2227" << ' ' << alpha.as_not().arg().as_or().rhs().as_not().arg() << ')'; + } else if (alpha.as_not().arg().type() == Formula::kNot) { + os << alpha.as_not().arg().as_not().arg(); } else if (alpha.as_not().arg().type() == Formula::kAtomic) { const Clause& c = alpha.as_not().arg().as_atomic().arg(); - print_sequence(os, c.begin(), c.end(), "[", "]", " \u2227 "); + if (c.empty()) { + os << "\u22A4"; + } else if (c.unit()) { + os << c.first().flip(); + } else { + auto as = internal::transform_range(c.begin(), c.end(), [](Literal a) { return a.flip(); }); + print_sequence(os, as.begin(), as.end(), "[", "]", " \u2227 "); + } } else if (alpha.as_not().arg().type() == Formula::kExists && alpha.as_not().arg().as_exists().arg().type() == Formula::kNot) { os << "\u2200" << alpha.as_not().arg().as_exists().x() << alpha.as_not().arg().as_exists().arg().as_not().arg(); -- GitLab