add command-line help descriptions on tactics

Signed-off-by: Nikolaj Bjorner <[email protected]>

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<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);

src/cmd_context/tactic_cmds.cpp

@@ -94,21 +94,15 @@ 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;
         t->collect_param_descrs(descrs);
         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";

src/cmd_context/tactic_manager.h

@@ -44,10 +44,29 @@ class tactic_manager {
     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); }
+
 };
 
 

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";

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();

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);
 
 

src/solver/parallel_tactic.cpp

@@ -376,9 +376,9 @@ class parallel_tactic : public tactic {
     }
 
     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";);
     }