diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp index 1f50c2c9e..0b3cda595 100644 --- a/src/ackermannization/lackr.cpp +++ b/src/ackermannization/lackr.cpp @@ -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::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); diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 927a03306..acbeef07e 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -94,10 +94,7 @@ void help_tactic(cmd_context & ctx) { buf << "- (fail-if ) fail if evaluates to true.\n"; buf << "- (using-params *) executes the given tactic using the given attributes, where ::= . ! 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"; diff --git a/src/cmd_context/tactic_manager.h b/src/cmd_context/tactic_manager.h index 9225a4555..3a57d6297 100644 --- a/src/cmd_context/tactic_manager.h +++ b/src/cmd_context/tactic_manager.h @@ -44,10 +44,29 @@ public: typedef ptr_vector::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::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); } + }; diff --git a/src/shell/main.cpp b/src/shell/main.cpp index b2d48b1be..36eb92a6d 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -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"; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index 6cea70755..5f2b1e3dc 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -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(); diff --git a/src/shell/smtlib_frontend.h b/src/shell/smtlib_frontend.h index 6d5bd6e60..04f35c5c8 100644 --- a/src/shell/smtlib_frontend.h +++ b/src/shell/smtlib_frontend.h @@ -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); diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 5ec1e908b..7dc1d06d3 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -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";); }