add default tactic as option to overwrite the behavior of strategic solver factory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/parsers/smt2/smt2parser.cpp

@@ -3110,6 +3110,24 @@ namespace smt2 {
             m_var_shifter       = nullptr;
         }
 
+        sexpr_ref parse_sexpr_ref() {
+            m_num_bindings    = 0;
+            unsigned found_errors = 0;
+            m_num_open_paren = 0;
+
+            try {
+                scan_core();
+                parse_sexpr();
+                if (!sexpr_stack().empty()) {
+                    return sexpr_ref(sexpr_stack().back(), sm());
+                }
+            }
+            catch (z3_exception & ex) {
+                error(ex.msg());
+            }
+            return sexpr_ref(nullptr, sm());
+        }
+
         bool operator()() {
             m_num_bindings    = 0;
             unsigned found_errors = 0;
@@ -3182,3 +3200,10 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive,
     return p();
 }
 
+sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename) {
+    smt2::parser p(ctx, is, false, ps, filename);
+    return p.parse_sexpr_ref();
+    
+}
+
+

src/parsers/smt2/smt2parser.h

@@ -23,4 +23,6 @@ Revision History:
 
 bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive = false, params_ref const & p = params_ref(), char const * filename = nullptr);
 
+sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename);
+
 #endif

src/parsers/smt2/smt2scanner.cpp

@@ -126,6 +126,11 @@ namespace smt2 {
                 return SYMBOL_TOKEN;
             }
         }
+        if (!m_string.empty()) {
+            m_string.push_back(0);
+            m_id = m_string.begin();
+            return SYMBOL_TOKEN;
+        }
         return EOF_TOKEN;
     }
 

src/shell/smtlib_frontend.cpp

@@ -73,7 +73,6 @@ unsigned read_smtlib2_commands(char const * file_name) {
     cmd_context ctx;
 
     ctx.set_solver_factory(mk_smt_strategic_solver_factory());
-
     install_dl_cmds(ctx);
     install_dbg_cmds(ctx);
     install_polynomial_cmds(ctx);

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -43,6 +43,8 @@ Notes:
 #include "solver/solver2tactic.h"
 #include "solver/parallel_tactic.h"
 #include "solver/parallel_params.hpp"
+#include "tactic/tactic_params.hpp"
+#include "parsers/smt2/smt2parser.h"
 
 
 
@@ -130,10 +132,30 @@ public:
             l = m_logic;
         else
             l = logic;
-        solver* s = mk_special_solver_for_logic(m, p, l);
-        if (s) return s;
-        tactic * t = mk_tactic_for_logic(m, p, l);
-        return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l),
+
+        tactic_params tp;
+        tactic_ref t;
+        if (tp.default_tactic() != symbol::null &&
+            !tp.default_tactic().is_numerical() && 
+            tp.default_tactic().bare_str() && 
+            tp.default_tactic().bare_str()[0]) {
+            cmd_context ctx(false, &m, l);
+            std::istringstream is(tp.default_tactic().bare_str());
+            char const* file_name = "";
+            sexpr_ref se = parse_sexpr(ctx, is, p, file_name);
+            if (se) {
+                t = sexpr2tactic(ctx, se.get());
+            }
+        }
+
+        if (!t) {
+            solver* s = mk_special_solver_for_logic(m, p, l);
+            if (s) return s;
+        }
+        if (!t) {
+            t = mk_tactic_for_logic(m, p, l);
+        }
+        return mk_combined_solver(mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l),
                                   mk_solver_for_logic(m, p, l), 
                                   p);
     }

src/tactic/tactic_params.pyg

@@ -9,6 +9,8 @@ def_module_params('tactic',
                           ('blast_term_ite.max_inflation', UINT, UINT_MAX, "multiplicative factor of initial term size."),
                           ('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."),
                           ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."),
+                          ('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"),
+
                      #     ('aig.per_assertion', BOOL, True, "process one assertion at a time"),
                      #     ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."),
                      #     ('add_bounds.upper, INT, 2, "upper bound to be added to unbounded variables."),