diff --git a/src/shell/main.cpp b/src/shell/main.cpp index fb205c872..6dd4aa2e8 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -77,8 +77,11 @@ void display_usage() { std::cout << " " << OPT << "version prints version number of Z3.\n"; std::cout << " " << OPT << "v:level be verbose, where is the verbosity level.\n"; std::cout << " " << OPT << "nw disable warning messages.\n"; - std::cout << " " << OPT << "ps display Z3 global (and module) parameters.\n"; - std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; + std::cout << " " << OPT << "p display Z3 global (and module) parameters.\n"; + std::cout << " " << OPT << "pd display Z3 global (and module) parameter descriptions.\n"; + std::cout << " " << OPT << "pm:name display Z3 module ('name') parameters.\n"; + std::cout << " " << OPT << "pp:name display Z3 parameter description.\n"; + std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; std::cout << "\nResources:\n"; // timeout and memout are now available on Linux and OSX too. std::cout << " " << OPT << "T:timeout set the timeout (in seconds).\n"; @@ -166,7 +169,7 @@ void parse_cmd_line_args(int argc, char ** argv) { } else if (strcmp(opt_name, "v") == 0) { if (!opt_arg) - error("option argument (/v:level) is missing."); + error("option argument (-v:level) is missing."); long lvl = strtol(opt_arg, 0, 10); set_verbosity_level(lvl); } @@ -175,39 +178,55 @@ void parse_cmd_line_args(int argc, char ** argv) { } else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) - error("option argument (/T:timeout) is missing."); + error("option argument (-T:timeout) is missing."); long tm = strtol(opt_arg, 0, 10); set_timeout(tm * 1000); } else if (strcmp(opt_name, "t") == 0) { if (!opt_arg) - error("option argument (/t:timeout) is missing."); + error("option argument (-t:timeout) is missing."); gparams::set("timeout", opt_arg); } else if (strcmp(opt_name, "nw") == 0) { enable_warning_messages(false); } - else if (strcmp(opt_name, "ps") == 0) { - gparams::display(std::cout); + else if (strcmp(opt_name, "p") == 0) { + gparams::display(std::cout, 0, false, false); + exit(0); + } + else if (strcmp(opt_name, "pd") == 0) { + gparams::display(std::cout, 0, false, true); + exit(0); + } + else if (strcmp(opt_name, "pm") == 0) { + if (!opt_arg) + error("option argument (-pm:name) is missing."); + gparams::display_module(std::cout, opt_arg); + exit(0); + } + else if (strcmp(opt_name, "pp") == 0) { + if (!opt_arg) + error("option argument (-pp:name) is missing."); + gparams::display_parameter(std::cout, opt_arg); exit(0); } #ifdef _TRACE else if (strcmp(opt_name, "tr") == 0) { if (!opt_arg) - error("option argument (/tr:tag) is missing."); + error("option argument (-tr:tag) is missing."); enable_trace(opt_arg); } #endif #ifdef Z3DEBUG else if (strcmp(opt_name, "dbg") == 0) { if (!opt_arg) - error("option argument (/dbg:tag) is missing."); + error("option argument (-dbg:tag) is missing."); enable_debug(opt_arg); } #endif else if (strcmp(opt_name, "memory") == 0) { if (!opt_arg) - error("option argument (/memory:val) is missing."); + error("option argument (-memory:val) is missing."); gparams::set("memory_max_size", opt_arg); } else { diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp index 8a5532ee0..314049727 100644 --- a/src/util/gparams.cpp +++ b/src/util/gparams.cpp @@ -91,26 +91,6 @@ public: } } - void display(std::ostream & out, unsigned indent, bool smt2_style) { - #pragma omp critical (gparams) - { - out << "Global parameters\n"; - m_param_descrs.display(out, indent + 4, smt2_style); - out << "\n"; - dictionary::iterator it = m_module_param_descrs.begin(); - dictionary::iterator end = m_module_param_descrs.end(); - for (; it != end; ++it) { - out << "[module] " << it->m_key; - char const * descr = 0; - if (m_module_descrs.find(it->m_key, descr)) { - out << ", description: " << descr; - } - out << "\n"; - it->m_value->display(out, indent + 4, smt2_style); - } - } - } - void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) { if (*name == ':') name++; @@ -315,6 +295,80 @@ public: return result; } + void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { + #pragma omp critical (gparams) + { + out << "Global parameters\n"; + m_param_descrs.display(out, indent + 4, smt2_style, include_descr); + out << "\n"; + if (!smt2_style) { + out << "To set a module parameter, use .=value\n"; + out << "Example: pp.decimal=true\n"; + out << "\n"; + } + dictionary::iterator it = m_module_param_descrs.begin(); + dictionary::iterator end = m_module_param_descrs.end(); + for (; it != end; ++it) { + out << "[module] " << it->m_key; + char const * descr = 0; + if (m_module_descrs.find(it->m_key, descr)) { + out << ", description: " << descr; + } + out << "\n"; + it->m_value->display(out, indent + 4, smt2_style, include_descr); + } + } + } + + void display_modules(std::ostream & out) { + dictionary::iterator it = m_module_param_descrs.begin(); + dictionary::iterator end = m_module_param_descrs.end(); + for (; it != end; ++it) { + out << "[module] " << it->m_key; + char const * descr = 0; + if (m_module_descrs.find(it->m_key, descr)) { + out << ", description: " << descr; + } + out << "\n"; + } + } + + void display_module(std::ostream & out, symbol const & module_name) { + param_descrs * d = 0; + if (!m_module_param_descrs.find(module_name, d)) + throw exception("unknown module '%s'", module_name.bare_str()); + out << "[module] " << module_name; + char const * descr = 0; + if (m_module_descrs.find(module_name, descr)) { + out << ", description: " << descr; + } + out << "\n"; + d->display(out, 4, false); + } + + void display_parameter(std::ostream & out, char const * name) { + symbol m, p; + normalize(name, m, p); + std::cout << name << " " << m << " " << p << "\n"; + param_descrs * d; + if (m == symbol::null) { + d = &m_param_descrs; + } + else { + if (!m_module_param_descrs.find(m, d)) + throw exception("unknown module '%s'", m.bare_str()); + } + if (!d->contains(p)) + throw_unknown_parameter(p, m); + out << " name: " << p << "\n"; + if (m != symbol::null) { + out << " module: " << m << "\n"; + out << " qualified name: " << m << "." << p << "\n"; + } + out << " type: " << d->get_kind(p) << "\n"; + out << " description: " << d->get_descr(p) << "\n"; + out << " default value: " << d->get_default(p) << "\n"; + } }; gparams::imp * gparams::g_imp = 0; @@ -370,9 +424,24 @@ params_ref gparams::get() { return g_imp->get(); } -void gparams::display(std::ostream & out, unsigned indent, bool smt2_style) { +void gparams::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) { SASSERT(g_imp != 0); - g_imp->display(out, indent, smt2_style); + g_imp->display(out, indent, smt2_style, include_descr); +} + +void gparams::display_modules(std::ostream & out) { + SASSERT(g_imp != 0); + g_imp->display_modules(out); +} + +void gparams::display_module(std::ostream & out, char const * module_name) { + SASSERT(g_imp != 0); + g_imp->display_module(out, symbol(module_name)); +} + +void gparams::display_parameter(std::ostream & out, char const * name) { + SASSERT(g_imp != 0); + g_imp->display_parameter(out, name); } void gparams::init() { diff --git a/src/util/gparams.h b/src/util/gparams.h index 2a784a239..a41044c84 100644 --- a/src/util/gparams.h +++ b/src/util/gparams.h @@ -106,8 +106,13 @@ public: /** \brief Dump information about available parameters in the given output stream. */ - static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false); + static void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true); + // Auxiliary APIs for better command line support + static void display_modules(std::ostream & out); + static void display_module(std::ostream & out, char const * module_name); + static void display_parameter(std::ostream & out, char const * name); + /** \brief Initialize the global parameter management module. diff --git a/src/util/params.cpp b/src/util/params.cpp index 4f2a73e99..c0b8653ae 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -95,7 +95,7 @@ struct param_descrs::imp { bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; } }; - void display(std::ostream & out, unsigned indent, bool smt2_style) const { + void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { svector names; dictionary::iterator it = m_info.begin(); dictionary::iterator end = m_info.end(); @@ -124,7 +124,9 @@ struct param_descrs::imp { info d; m_info.find(*it2, d); SASSERT(d.m_descr); - out << " (" << d.m_kind << ") " << d.m_descr; + out << " (" << d.m_kind << ")"; + if (include_descr) + out << " " << d.m_descr; if (d.m_default != 0) out << " (default: " << d.m_default << ")"; out << "\n"; @@ -209,8 +211,8 @@ symbol param_descrs::get_param_name(unsigned i) const { return m_imp->get_param_name(i); } -void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style) const { - return m_imp->display(out, indent, smt2_style); +void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { + return m_imp->display(out, indent, smt2_style, include_descr); } void insert_max_memory(param_descrs & r) { diff --git a/src/util/params.h b/src/util/params.h index 68f4c967b..164de9ab3 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -119,7 +119,7 @@ public: char const * get_descr(symbol const & name) const; char const * get_default(char const * name) const; char const * get_default(symbol const & name) const; - void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false) const; + void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const; unsigned size() const; symbol get_param_name(unsigned idx) const; };