speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase

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

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -433,6 +433,9 @@ struct pb2bv_rewriter::imp {
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
         m_rw(e, result, result_proof);
     }
+    void assert_expr(expr * e, expr_ref & result, proof_ref & result_proof) {
+        m_rw(e, result, result_proof);
+    }
     void push() {
         m_fresh_lim.push_back(m_fresh.size());
     }
@@ -469,9 +472,13 @@ unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps();
 void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
 func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
 void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void pb2bv_rewriter::assert_expr(expr* e, expr_ref & result, proof_ref & result_proof) { 
+    m_imp->assert_expr(e, result, result_proof); 
+}
 void pb2bv_rewriter::push() { m_imp->push(); }
 void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
 void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 
 unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; }
 
+
 void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); }

src/ast/rewriter/pb2bv_rewriter.h

@@ -36,6 +36,7 @@ public:
     void cleanup();
     func_decl_ref_vector const& fresh_constants() const;
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
+    void assert_expr(expr* e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
     void flush_side_constraints(expr_ref_vector& side_constraints);

src/cmd_context/cmd_context.cpp

@@ -736,7 +736,7 @@ bool cmd_context::set_logic(symbol const & s) {
 
 std::string cmd_context::reason_unknown() const {
     if (m_check_sat_result.get() == 0)
-        throw cmd_exception("state of the most recent check-sat command is not unknown");
+        throw cmd_exception("state of the most recent check-sat command is not known");
     return m_check_sat_result->reason_unknown();
 }
 

src/sat/sat_solver.cpp

@@ -3168,8 +3168,8 @@ namespace sat {
             ++num_iterations;
             checkpoint();
             literal_set::iterator it = vars.begin(), end = vars.end();
-            unsigned chunk_size = 100;
+            unsigned num_resolves = 0;
-            for (; it != end && chunk_size > 0; ++it) {
+            for (; it != end; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
                     continue;
@@ -3183,15 +3183,21 @@ namespace sat {
                         return l_false;
                     }
                     propagate(false);                    
-                    --chunk_size;
+                    ++num_resolves;
+                }
+                if (scope_lvl() == 1) {
+                    break;
                 }
             }
             lbool is_sat;
             while (true) {
+                if (scope_lvl() == 1 && num_resolves > 0) {
+                    is_sat = l_undef;
+                    break;
+                }
                 is_sat = bounded_search();
                 if (is_sat == l_undef) {
                     restart();      
-                    continue;
                 }
                 break;
             }

src/solver/combined_solver.cpp

@@ -197,8 +197,14 @@ public:
     virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         switch_inc_mode();
         m_use_solver1_results = false;
+        try {
             return m_solver2->get_consequences(asms, vars, consequences);
         }
+        catch (z3_exception& ex) {
+            set_reason_unknown(ex.msg());
+        }
+        return l_undef;
+    }
 
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
         m_check_sat_executed  = true;        

src/tactic/portfolio/pb2bv_solver.cpp

@@ -113,7 +113,7 @@ private:
         expr_ref fml(m);
         expr_ref_vector fmls(m);
         for (unsigned i = 0; i < m_assertions.size(); ++i) {
-            m_rewriter(m_assertions[i].get(), fml, proof);
+            m_rewriter.assert_expr(m_assertions[i].get(), fml, proof);
             m_solver->assert_expr(fml);
         }
         m_rewriter.flush_side_constraints(fmls);