mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

add command-line help descriptions on tactics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-14 19:29:35 -07:00
parent c0a07f9229
commit fae206b738
7 changed files with 65 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ackermannization/lackr.cpp
View file

@ -73,8 +73,9 @@ bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
if (!init())
return false;
if (lemmas_upper_bound != std::numeric_limits<double>::infinity() &&
ackr_helper::calculate_lemma_bound(m_fun2terms, m_sel2terms) > lemmas_upper_bound)
ackr_helper::calculate_lemma_bound(m_fun2terms, m_sel2terms) > lemmas_upper_bound) {
return false;
}
eager_enc();
for (expr* a : m_abstr)
g->assert_expr(a);

10
src/cmd_context/tactic_cmds.cpp
View file

@ -94,10 +94,7 @@ void help_tactic(cmd_context & ctx) {
buf << "- (fail-if <probe>) fail if <probe> evaluates to true.\n";
buf << "- (using-params <tactic> <attribute>*) executes the given tactic using the given attributes, where <attribute> ::= <keyword> <value>. ! is a syntax sugar for using-params.\n";
buf << "builtin tactics:\n";
cmd_context::tactic_cmd_iterator it = ctx.begin_tactic_cmds();
cmd_context::tactic_cmd_iterator end = ctx.end_tactic_cmds();
for (; it != end; ++it) {
tactic_cmd * cmd = *it;
for (tactic_cmd* cmd : ctx.tactics()) {
buf << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
tactic_ref t = cmd->mk(ctx.m());
param_descrs descrs;
@ -105,10 +102,7 @@ void help_tactic(cmd_context & ctx) {
descrs.display(buf, 4);
}
buf << "builtin probes:\n";
cmd_context::probe_iterator it2 = ctx.begin_probes();
cmd_context::probe_iterator end2 = ctx.end_probes();
for (; it2 != end2; ++it2) {
probe_info * pinfo = *it2;
for (probe_info * pinfo : ctx.probes()) {
buf << "- " << pinfo->get_name() << " " << pinfo->get_descr() << "\n";
}
ctx.regular_stream() << '"' << escaped(buf.str()) << "\"\n";

19
src/cmd_context/tactic_manager.h
View file

@ -44,10 +44,29 @@ public:
typedef ptr_vector<tactic_cmd>::const_iterator tactic_cmd_iterator;
tactic_cmd_iterator begin_tactic_cmds() const { return m_tactics.begin(); }
tactic_cmd_iterator end_tactic_cmds() const { return m_tactics.end(); }
class tactics_iterator {
tactic_manager const& m;
public:
tactics_iterator(tactic_manager const& m):m(m) {}
tactic_cmd_iterator begin() const { return m.begin_tactic_cmds(); }
tactic_cmd_iterator end() const { return m.end_tactic_cmds(); }
};
tactics_iterator tactics() const { return tactics_iterator(*this); }
typedef ptr_vector<probe_info>::const_iterator probe_iterator;
probe_iterator begin_probes() const { return m_probes.begin(); }
probe_iterator end_probes() const { return m_probes.end(); }
class probes_iterator {
tactic_manager const& m;
public:
probes_iterator(tactic_manager const& m):m(m) {}
probe_iterator begin() const { return m.begin_probes(); }
probe_iterator end() const { return m.end_probes(); }
};
probes_iterator probes() const { return probes_iterator(*this); }
};

11
src/shell/main.cpp
View file

@ -93,6 +93,8 @@ void display_usage() {
std::cout << " -pd display Z3 global (and module) parameter descriptions.\n";
std::cout << " -pm:name display Z3 module ('name') parameters.\n";
std::cout << " -pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
std::cout << " -tactics[:name] display built-in tactics or if argument is given, display detailed information on tactic.\n";
std::cout << " -probes display avilable probes.\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 macOS too.
@ -272,6 +274,15 @@ static void parse_cmd_line_args(int argc, char ** argv) {
error("option argument (-memory:val) is missing.");
gparams::set("memory_max_size", opt_arg);
}
else if (strcmp(opt_name, "tactics") == 0) {
if (!opt_arg)
help_tactics();
else
help_tactic(opt_arg);
}
else if (strcmp(opt_name, "probes") == 0) {
help_probes();
}
else {
std::cerr << "Error: invalid command line option: " << arg << "\n";
std::cerr << "For usage information: z3 -h\n";

25
src/shell/smtlib_frontend.cpp
View file

@ -62,6 +62,31 @@ static void STD_CALL on_ctrl_c(int) {
raise(SIGINT);
}
void help_tactics() {
cmd_context ctx;
for (auto cmd : ctx.tactics()) {
std::cout << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
}
}
void help_tactic(char const* name) {
cmd_context ctx;
for (auto cmd : ctx.tactics()) {
if (cmd->get_name() == name) {
tactic_ref t = cmd->mk(ctx.m());
param_descrs descrs;
t->collect_param_descrs(descrs);
descrs.display(std::cout, 4);
}
}
}
void help_probes() {
cmd_context ctx;
for (auto cmd : ctx.probes()) {
std::cout << "- " << cmd->get_name() << " " << cmd->get_descr() << "\n";
}
}
unsigned read_smtlib2_commands(char const * file_name) {
g_start_time = clock();

4
src/shell/smtlib_frontend.h
View file

@ -20,6 +20,8 @@ Revision History:
unsigned read_smtlib_file(char const * benchmark_file);
unsigned read_smtlib2_commands(char const * command_file);
void help_tactics();
void help_probes();
void help_tactic(char const* name);

6
src/solver/parallel_tactic.cpp
View file

@ -376,9 +376,9 @@ private:
}
void log_branches(lbool status) {
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "% ";
if (status == l_true) verbose_stream() << ":status sat";
if (status == l_undef) verbose_stream() << ":status unknown";
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << "%";
if (status == l_true) verbose_stream() << " :status sat";
if (status == l_undef) verbose_stream() << " :status unknown";
if (m_num_unsat > 0) verbose_stream() << " :closed " << m_num_unsat << "@" << m_last_depth;
verbose_stream() << " :open " << m_branches << ")\n";);
}