testing inc-sat solver

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

src/opt/dual_maxres.cpp

@@ -134,7 +134,7 @@ public:
                 case l_undef:
                     break;
                 case l_false:
-                    is_sat = get_cores(soft_compl, cores);
+                    is_sat = get_cores(cores);
                     for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
                         is_sat = process_unsat(cores[i]);
                     }
@@ -177,57 +177,61 @@ public:
     // TBD: when the remaining are satisfiable, then extend the
     // satisfying model to improve upper bound.
     // 
-    lbool get_cores(ptr_vector<expr>& core, vector<ptr_vector<expr> >& cores) {
+    lbool get_cores(vector<ptr_vector<expr> >& cores) {
-        // assume 'core' is minimal.
+        // assume m_s is unsat.
+        lbool is_sat = l_false;
         expr_ref_vector asms(m);
         asms.append(m_asms.size(), m_asms.c_ptr());
-        remove_soft(core, asms);
         cores.reset();
-        cores.push_back(core);        
+        ptr_vector<expr> core;
-        ptr_vector<expr> new_core;
+        while (is_sat == l_false) {
-        while (true) {
+            core.reset();
-            lbool is_sat = m_s->check_sat(asms.size(), asms.c_ptr());
+            m_s->get_unsat_core(core);
-            switch (is_sat) {
+            is_sat = minimize_core(core);
-            case l_false:
+            if (is_sat != l_true) {
-                new_core.reset();
-                m_s->get_unsat_core(new_core);
-                switch (minimize_core(new_core)) {
-                case l_false:
-                    return l_false;
-                case l_true:
-                    cores.push_back(new_core);
-                    remove_soft(new_core, asms);
                 break;
-                default:
-                    return l_undef;
             }
+            cores.push_back(core);
             break;
-            case l_true:
+            // 
+            // TBD: multiple core refinement 
+            // produces unsound results.
+            // what is a sound variant?
+            // 
+            remove_soft(core, asms);
+            is_sat = m_s->check_sat(asms.size(), asms.c_ptr());
+            
+        }
         TRACE("opt", 
               tout << "num cores: " << cores.size() << "\n";
+              for (unsigned i = 0; i < cores.size(); ++i) {
+                  for (unsigned j = 0; j < cores[i].size(); ++j) {
+                      tout << mk_pp(cores[i][j], m) << " ";
+                  }
+                  tout << "\n";
+              }
               tout << "num satisfying: " << asms.size() << "\n";);
-                return l_true;
+        
-            default:
+        return is_sat;
-                return l_undef;
-            }
-        }        
     }
 
     lbool process_unsat(ptr_vector<expr>& core) {
         expr_ref fml(m);
-        TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()););
         SASSERT(!core.empty());
         if (core.empty()) {
             return l_false;
         }
         remove_soft(core);
         rational w = split_soft(core);
-        TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr()););
+        TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr());
+              for (unsigned i = 0; i < core.size(); ++i) {
+                  tout << get_weight(core[i]) << " ";
+              }
+              tout << "min-weight: " << w << "\n";);
         max_resolve(core, w);
         m_lower += w;        
         IF_VERBOSE(1, verbose_stream() << 
                    "(opt.dual_max_res [" << m_lower << ":" << m_upper << "])\n";);
-
         return l_true;
     }
 
@@ -261,9 +265,7 @@ public:
                 switch (is_sat) {
                 case l_false:
                     if (num_true*2 < m_asms.size()) {
-                        soft_compl.reset();
+                        return l_false;
-                        m_s->get_unsat_core(soft_compl);
-                        return minimize_core(soft_compl);        
                     }
                     break;
                 case l_true:

src/opt/inc_sat_solver.cpp

@@ -11,6 +11,7 @@
 #include "bit_blaster_tactic.h"
 #include "simplify_tactic.h"
 #include "goal2sat.h"
+#include "ast_pp.h"
 
 // incremental SAT solver.
 class inc_sat_solver : public solver {
@@ -78,11 +79,10 @@ public:
             for (unsigned i = 0; i < num_assumptions; ++i) {
                 g->assert_expr(assumptions[i], m.mk_leaf(assumptions[i]));
             }
-            TRACE("opt", g->display(tout););
+            TRACE("opt", g->display_with_dependencies(tout););
             m_fmls.reset();
             try {                   
                 (*m_preprocess)(g, result, mc, pc, core);
-                TRACE("opt", result[0]->display(tout););
             }
             catch (tactic_exception & ex) {
                 IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
@@ -95,7 +95,7 @@ public:
                 return l_undef;
             }
             g = result[0];
-            TRACE("opt", g->display(tout););
+            TRACE("opt", g->display_with_dependencies(tout););
             m_goal2sat(*g, m_params, m_solver, m_map, dep2asm);
         }
         
@@ -185,8 +185,24 @@ private:
             asm2dep.insert(it->m_value.index(), it->m_key);
         }
         sat::literal_vector const& core = m_solver.get_core();
+
+        TRACE("opt",
+              dep2asm_t::iterator it = dep2asm.begin();
+              dep2asm_t::iterator end = dep2asm.end();
+              for (; it != end; ++it) {
+                  tout << mk_pp(it->m_key, m) << " |-> " << it->m_value << "\n";
+              }
+              tout << "core: ";
               for (unsigned i = 0; i < core.size(); ++i) {
-            m_core.push_back(asm2dep.find(core[i].index()));
+                  tout << core[i] << " ";
+              }
+              tout << "\n";
+              );              
+
+        for (unsigned i = 0; i < core.size(); ++i) {
+            expr* e;
+            if (asm2dep.find(core[i].index(), e))
+                m_core.push_back(e);
         }
     }
 

src/opt/mus.cpp

@@ -160,6 +160,14 @@ struct mus::imp {
                 break;
             }
         }
+        DEBUG_CODE(
+            assumptions.reset();
+            for (unsigned i = 0; i < mus.size(); ++i) {
+                assumptions.push_back(m_cls2expr[mus[i]].get());
+            }
+            lbool is_sat = m_s->check_sat(assumptions.size(), assumptions.c_ptr());
+            SASSERT(is_sat == l_false);
+                   );
         return l_true;
     }
 

src/sat/sat_solver.cpp

@@ -2141,6 +2141,9 @@ namespace sat {
     // 
 
     void solver::user_push() {
+        if (m_level.size() == 0) {
+            return;
+        }
         literal lit;
         if (m_user_scope_literal_pool.empty()) {
             bool_var new_v = mk_var(true, false);
@@ -2183,7 +2186,7 @@ namespace sat {
 
     void solver::user_pop(unsigned num_scopes) {
         pop_to_base_level();
-        while (num_scopes > 0) {
+        while (num_scopes > 0 && !m_user_scope_literals.empty()) {
             literal lit = m_user_scope_literals.back();
             m_user_scope_literal_pool.push_back(lit);   
             m_user_scope_literals.pop_back();

src/tactic/arith/card2bv_tactic.cpp

@@ -198,7 +198,7 @@ public:
             m_rw1(g->form(idx), new_f1);
             TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;);
             m_rw2(new_f1, new_f2);
-            g->update(idx, new_f2);
+            g->update(idx, new_f2, g->pr(idx), g->dep(idx));
         }
 
         g->inc_depth();