mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 23:53:25 +00:00
Code Activity

better help

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-02 17:18:25 -08:00
parent 0934cb06d8
commit 91096b638a
5 changed files with 133 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/shell/main.cpp
View file

@ -77,8 +77,11 @@ void display_usage() {
std::cout << " " << OPT << "version prints version number of Z3.\n"; std::cout << " " << OPT << "version prints version number of Z3.\n";
std::cout << " " << OPT << "v:level be verbose, where <level> is the verbosity level.\n"; std::cout << " " << OPT << "v:level be verbose, where <level> is the verbosity level.\n";
std::cout << " " << OPT << "nw disable warning messages.\n"; std::cout << " " << OPT << "nw disable warning messages.\n";
std::cout << " " << OPT << "ps display Z3 global (and module) parameters.\n"; std::cout << " " << OPT << "p 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 << "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"; std::cout << "\nResources:\n";
// timeout and memout are now available on Linux and OSX too. // timeout and memout are now available on Linux and OSX too.
std::cout << " " << OPT << "T:timeout set the timeout (in seconds).\n"; 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) { else if (strcmp(opt_name, "v") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/v:level) is missing."); error("option argument (-v:level) is missing.");
long lvl = strtol(opt_arg, 0, 10); long lvl = strtol(opt_arg, 0, 10);
set_verbosity_level(lvl); set_verbosity_level(lvl);
} }
@ -175,39 +178,55 @@ void parse_cmd_line_args(int argc, char ** argv) {
} }
else if (strcmp(opt_name, "T") == 0) { else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/T:timeout) is missing."); error("option argument (-T:timeout) is missing.");
long tm = strtol(opt_arg, 0, 10); long tm = strtol(opt_arg, 0, 10);
set_timeout(tm * 1000); set_timeout(tm * 1000);
} }
else if (strcmp(opt_name, "t") == 0) { else if (strcmp(opt_name, "t") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/t:timeout) is missing."); error("option argument (-t:timeout) is missing.");
gparams::set("timeout", opt_arg); gparams::set("timeout", opt_arg);
} }
else if (strcmp(opt_name, "nw") == 0) { else if (strcmp(opt_name, "nw") == 0) {
enable_warning_messages(false); enable_warning_messages(false);
} }
else if (strcmp(opt_name, "ps") == 0) { else if (strcmp(opt_name, "p") == 0) {
gparams::display(std::cout); 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); exit(0);
} }
#ifdef _TRACE #ifdef _TRACE
else if (strcmp(opt_name, "tr") == 0) { else if (strcmp(opt_name, "tr") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/tr:tag) is missing."); error("option argument (-tr:tag) is missing.");
enable_trace(opt_arg); enable_trace(opt_arg);
} }
#endif #endif
#ifdef Z3DEBUG #ifdef Z3DEBUG
else if (strcmp(opt_name, "dbg") == 0) { else if (strcmp(opt_name, "dbg") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/dbg:tag) is missing."); error("option argument (-dbg:tag) is missing.");
enable_debug(opt_arg); enable_debug(opt_arg);
} }
#endif #endif
else if (strcmp(opt_name, "memory") == 0) { else if (strcmp(opt_name, "memory") == 0) {
if (!opt_arg) if (!opt_arg)
error("option argument (/memory:val) is missing."); error("option argument (-memory:val) is missing.");
gparams::set("memory_max_size", opt_arg); gparams::set("memory_max_size", opt_arg);
} }
else { else {

113
src/util/gparams.cpp
View file

@ -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<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::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) { void normalize(char const * name, /* out */ symbol & mod_name, /* out */ symbol & param_name) {
if (*name == ':') if (*name == ':')
name++; name++;
@ -315,6 +295,80 @@ public:
return result; 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 <module-name>.<parameter-name>=value\n";
out << "Example: pp.decimal=true\n";
out << "\n";
}
dictionary<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::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<param_descrs*>::iterator it = m_module_param_descrs.begin();
dictionary<param_descrs*>::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; gparams::imp * gparams::g_imp = 0;
@ -370,9 +424,24 @@ params_ref gparams::get() {
return g_imp->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); 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() { void gparams::init() {

7
src/util/gparams.h
View file

@ -106,8 +106,13 @@ public:
/** /**
\brief Dump information about available parameters in the given output stream. \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. \brief Initialize the global parameter management module.

10
src/util/params.cpp
View file

@ -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; } 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<symbol> names; svector<symbol> names;
dictionary<info>::iterator it = m_info.begin(); dictionary<info>::iterator it = m_info.begin();
dictionary<info>::iterator end = m_info.end(); dictionary<info>::iterator end = m_info.end();
@ -124,7 +124,9 @@ struct param_descrs::imp {
info d; info d;
m_info.find(*it2, d); m_info.find(*it2, d);
SASSERT(d.m_descr); 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) if (d.m_default != 0)
out << " (default: " << d.m_default << ")"; out << " (default: " << d.m_default << ")";
out << "\n"; out << "\n";
@ -209,8 +211,8 @@ symbol param_descrs::get_param_name(unsigned i) const {
return m_imp->get_param_name(i); return m_imp->get_param_name(i);
} }
void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style) const { void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
return m_imp->display(out, indent, smt2_style); return m_imp->display(out, indent, smt2_style, include_descr);
} }
void insert_max_memory(param_descrs & r) { void insert_max_memory(param_descrs & r) {

2
src/util/params.h
View file

@ -119,7 +119,7 @@ public:
char const * get_descr(symbol const & name) const; char const * get_descr(symbol const & name) const;
char const * get_default(char const * name) const; char const * get_default(char const * name) const;
char const * get_default(symbol 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; unsigned size() const;
symbol get_param_name(unsigned idx) const; symbol get_param_name(unsigned idx) const;
}; };