Merge branch 'master' of https://github.com/z3prover/z3 into opt

src/sat/sat_config.cpp

@@ -35,6 +35,7 @@ namespace sat {
         m_glue("glue"),
         m_glue_psm("glue_psm"),
         m_psm_glue("psm_glue") {
+        m_num_parallel = 1;
         updt_params(p); 
     }
 

src/sat/sat_solver.cpp

@@ -808,20 +808,24 @@ namespace sat {
 
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         int num_threads = static_cast<int>(m_config.m_num_parallel);
+        int num_extra_solvers = num_threads - 1;
         scoped_limits scoped_rlimit(rlimit());
-        vector<reslimit> rlims(num_threads);
+        vector<reslimit> rlims(num_extra_solvers);
-        ptr_vector<sat::solver> solvers(num_threads);
+        ptr_vector<sat::solver> solvers(num_extra_solvers);
         sat::par par;
-        for (int i = 0; i < num_threads; ++i) {
+        symbol saved_phase = m_params.get_sym("phase", symbol("caching"));
-            m_params.set_uint("random_seed", i);
+        for (int i = 0; i < num_extra_solvers; ++i) {
-            if (i < num_threads/2) {
+            m_params.set_uint("random_seed", m_rand());
+            if (i == 1 + num_threads/2) {
                 m_params.set_sym("phase", symbol("random"));
-            }
+            }                        
             solvers[i] = alloc(sat::solver, m_params, rlims[i], 0);
             solvers[i]->copy(*this);
             solvers[i]->set_par(&par);
-            scoped_rlimit.push_child(&solvers[i]->rlimit());
+            scoped_rlimit.push_child(&solvers[i]->rlimit());            
         }
+        set_par(&par);
+        m_params.set_sym("phase", saved_phase);
         int finished_id = -1;
         std::string        ex_msg;
         par_exception_kind ex_kind;
@@ -830,7 +834,13 @@ namespace sat {
         #pragma omp parallel for
         for (int i = 0; i < num_threads; ++i) {
             try {                
-                lbool r = solvers[i]->check(num_lits, lits);
+                lbool r = l_undef;
+                if (i < num_extra_solvers) {
+                    r = solvers[i]->check(num_lits, lits);
+                }
+                else {
+                    r = check(num_lits, lits);
+                }
                 bool first = false;
                 #pragma omp critical (par_solver)
                 {
@@ -841,14 +851,14 @@ namespace sat {
                     }
                 }
                 if (first) {
-                    if (r == l_true) {
+                    if (r == l_true && i < num_extra_solvers) {
                         set_model(solvers[i]->get_model());
                     }
-                    else if (r == l_false) {
+                    else if (r == l_false && i < num_extra_solvers) {
                         m_core.reset();
                         m_core.append(solvers[i]->get_core());
                     }
-                    for (int j = 0; j < num_threads; ++j) {
+                    for (int j = 0; j < num_extra_solvers; ++j) {
                         if (i != j) {
                             rlims[j].cancel();
                         }
@@ -868,7 +878,12 @@ namespace sat {
                 }
             }
         }
-        for (int i = 0; i < num_threads; ++i) {
+        set_par(0);
+        if (finished_id != -1 && finished_id < num_extra_solvers) {
+            m_stats = solvers[finished_id]->m_stats;
+        }
+
+        for (int i = 0; i < num_extra_solvers; ++i) {            
             dealloc(solvers[i]);
         }
         if (finished_id == -1) {

src/solver/solver.h

@@ -54,7 +54,7 @@ public:
     /**
        \brief Update the solver internal settings. 
     */
-    virtual void updt_params(params_ref const & p) {}
+    virtual void updt_params(params_ref const & p) { }
 
     /**
        \brief Store in \c r a description of the configuration

src/solver/solver2tactic.cpp

@@ -93,6 +93,7 @@ public:
     {}
     
     virtual void updt_params(params_ref const & p) {
+        m_params.append(p);
         m_solver->updt_params(p);
     }
 

src/solver/tactic2solver.cpp

@@ -96,7 +96,7 @@ tactic2solver::~tactic2solver() {
 }
 
 void tactic2solver::updt_params(params_ref const & p) {
-    m_params = p;
+    m_params.append(p);
 }
 
 void tactic2solver::collect_param_descrs(param_descrs & r) {

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -98,13 +98,20 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_default_tactic(m, p);
 }
 
-static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
+static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
-    bv_rewriter rw(m);
-    if (logic == "QF_BV" && rw.hi_div0()) 
-        return mk_inc_sat_solver(m, p);
     if (logic == "QF_FD") 
         return mk_fd_solver(m, p);
-    return mk_smt_solver(m, p, logic);
+    return 0;
+}
+
+static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
+    bv_rewriter rw(m);
+    solver* s = mk_special_solver_for_logic(m, p, logic);
+    if (!s && logic == "QF_BV" && rw.hi_div0()) 
+        s = mk_inc_sat_solver(m, p);
+    if (!s) 
+        s = mk_smt_solver(m, p, logic);
+    return s;
 }
 
 class smt_strategic_solver_factory : public solver_factory {
@@ -119,6 +126,8 @@ 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),
                                   mk_solver_for_logic(m, p, l),