Merge branch 'master' of https://github.com/Z3Prover/z3

src/opt/opt_context.cpp

@@ -570,11 +570,11 @@ namespace opt {
         m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
         m_opt_solver->set_logic(m_logic);
         m_solver = m_opt_solver.get();
+        m_opt_solver->ensure_pb();
     
-        if (opt_params(m_params).priority() == symbol("pareto") ||
+        //if (opt_params(m_params).priority() == symbol("pareto") ||
-            (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
+        //    (opt_params(m_params).priority() == symbol("lex") && m_objectives.size() > 1)) {
-            m_opt_solver->ensure_pb();
+        //}        
-        }        
     }
 
     void context::setup_arith_solver() {

src/sat/sat_simplifier.cpp

@@ -154,7 +154,6 @@ namespace sat {
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
-
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());

src/sat/sat_solver.cpp

@@ -84,7 +84,7 @@ namespace sat {
                 VERIFY(v == mk_var(ext, dvar));
             }
         }
-        unsigned sz = src.scope_lvl() == 0 ? src.m_trail.size() : src.m_scopes[0].m_trail_lim;
+        unsigned sz = src.init_trail_size();
         for (unsigned i = 0; i < sz; ++i) {
             assign(src.m_trail[i], justification());
         }
@@ -774,7 +774,6 @@ namespace sat {
 
                 restart();
                 simplify_problem();
-                exchange_par();
                 if (check_inconsistent()) return l_false;
                 gc();
 
@@ -890,9 +889,8 @@ namespace sat {
      */
     void solver::exchange_par() {
         if (m_par && scope_lvl() == 0) {
-            unsigned sz = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
+            unsigned sz = init_trail_size();
             unsigned num_in = 0, num_out = 0;
-            SASSERT(scope_lvl() == 0); // parallel with assumptions is TBD
             literal_vector in, out;
             for (unsigned i = m_par_limit_out; i < sz; ++i) {
                 literal lit = m_trail[i];
@@ -2544,6 +2542,7 @@ namespace sat {
 
     void solver::pop_reinit(unsigned num_scopes) {
         pop(num_scopes);
+        exchange_par();
         reinit_assumptions();
     }
 
@@ -2863,7 +2862,7 @@ namespace sat {
     }
 
     void solver::display_units(std::ostream & out) const {
-        unsigned end = scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim;
+        unsigned end = init_trail_size();
         for (unsigned i = 0; i < end; i++) {
             out << m_trail[i] << " ";
         }

src/sat/sat_solver.h

@@ -223,6 +223,7 @@ namespace sat {
         lbool value(bool_var v) const { return static_cast<lbool>(m_assignment[literal(v, false).index()]); }
         unsigned lvl(bool_var v) const { return m_level[v]; }
         unsigned lvl(literal l) const { return m_level[l.var()]; }
+        unsigned init_trail_size() const { return scope_lvl() == 0 ? m_trail.size() : m_scopes[0].m_trail_lim; }
         void assign(literal l, justification j) {
             TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
             switch (value(l)) {

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