fix bug in unsat core extraction in sat solver

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

src/opt/bcd2.cpp

@@ -57,7 +57,7 @@ namespace opt {
                 es.push_back(m.mk_not(*it));
             }
         }
-        void bcd2_init_soft(vector<rational> const& weights, expr_ref_vector const& soft) {
+        void bcd2_init_soft(weights_t& weights, expr_ref_vector const& soft) {
 
             // normalize weights to be integral:
             m_den = rational::one();
@@ -100,7 +100,7 @@ namespace opt {
 
     public:
         bcd2(context& c,
-             vector<rational> const& ws, expr_ref_vector const& soft): 
+             weights_t& ws, expr_ref_vector const& soft): 
             maxsmt_solver_base(c, ws, soft),
             pb(m),
             m_soft_aux(m),
@@ -116,7 +116,6 @@ namespace opt {
             expr_ref fml(m), r(m);
             lbool is_sat = l_undef;
             expr_ref_vector asms(m);
-            solver::scoped_push _scope1(s());
             init();
             init_bcd();
             if (m_cancel) {
@@ -399,8 +398,8 @@ namespace opt {
         }
     };
 
-    maxsmt_solver_base* opt::mk_bcd2(context& c,
+    maxsmt_solver_base* opt::mk_bcd2(
-                                     vector<rational> const& ws, expr_ref_vector const& soft) {
+        context& c, weights_t& ws, expr_ref_vector const& soft) {
         return alloc(bcd2, c, ws, soft);
     }
 

src/opt/bcd2.h

@@ -23,6 +23,6 @@ Notes:
 #include "maxsmt.h"
 
 namespace opt {
-    maxsmt_solver_base* mk_bcd2(context& c, vector<rational> const& ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_bcd2(context& c, weights_t& ws, expr_ref_vector const& soft);
 }
 #endif

src/opt/maxhs.cpp

@@ -75,7 +75,7 @@ namespace opt {
 
 
     public:
-        maxhs(context& c, vector<rational> const& ws, expr_ref_vector const& soft):
+        maxhs(context& c, weights_t& ws, expr_ref_vector const& soft):
             maxsmt_solver_base(c, ws, soft), 
             m_aux(m), 
             m_at_lower_bound(false) {
@@ -554,8 +554,8 @@ namespace opt {
         
     };
 
-    maxsmt_solver_base* opt::mk_maxhs(context& c,
+    maxsmt_solver_base* opt::mk_maxhs(
-                                     vector<rational> const& ws, expr_ref_vector const& soft) {
+        context& c, weights_t& ws, expr_ref_vector const& soft) {
         return alloc(maxhs, c, ws, soft);
     }
 

src/opt/maxres.cpp

@@ -85,7 +85,7 @@ private:
 
 public:
     maxres(context& c,
-           vector<rational> const& ws, expr_ref_vector const& soft, 
+           weights_t& ws, expr_ref_vector const& soft, 
            strategy_t st):
         maxsmt_solver_base(c, ws, soft),
         m_B(m), m_asms(m),
@@ -658,18 +658,18 @@ public:
 
 };
 
-opt::maxsmt_solver_base* opt::mk_maxres(context& c,
+opt::maxsmt_solver_base* opt::mk_maxres(
-                                        vector<rational> const& ws, expr_ref_vector const& soft) {
+    context& c, weights_t& ws, expr_ref_vector const& soft) {
     return alloc(maxres, c, ws, soft, maxres::s_mus);
 }
 
-opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(context& c,
+opt::maxsmt_solver_base* opt::mk_mus_mss_maxres(
-                                        vector<rational> const& ws, expr_ref_vector const& soft) {
+    context& c, weights_t& ws, expr_ref_vector const& soft) {
     return alloc(maxres, c, ws, soft, maxres::s_mus_mss);
 }
 
-opt::maxsmt_solver_base* opt::mk_mss_maxres(context& c,
+opt::maxsmt_solver_base* opt::mk_mss_maxres(
-                                        vector<rational> const& ws, expr_ref_vector const& soft) {
+    context& c, weights_t& ws, expr_ref_vector const& soft) {
     return alloc(maxres, c, ws, soft, maxres::s_mss);
 }
 

src/opt/maxres.h

@@ -22,17 +22,11 @@ Notes:
 
 namespace opt {
 
-    maxsmt_solver_base* mk_maxres(
+    maxsmt_solver_base* mk_maxres(context& c, weights_t & ws, expr_ref_vector const& soft);
-        context& c,
-        vector<rational> const& ws, expr_ref_vector const& soft);
 
-    maxsmt_solver_base* mk_mus_mss_maxres(
+    maxsmt_solver_base* mk_mus_mss_maxres(context& c, weights_t & ws, expr_ref_vector const& soft);
-        context& c,
-        vector<rational> const& ws, expr_ref_vector const& soft);
 
-    maxsmt_solver_base* mk_mss_maxres(
+    maxsmt_solver_base* mk_mss_maxres(context& c, weights_t & ws, expr_ref_vector const& soft);
-        context& c,
-        vector<rational> const& ws, expr_ref_vector const& soft);
 
 };
 

src/opt/maxsls.cpp

@@ -26,7 +26,7 @@ namespace opt {
 
     class sls : public maxsmt_solver_base {
     public:
-        sls(context& c, vector<rational> const& ws, expr_ref_vector const& soft): 
+        sls(context& c, weights_t& ws, expr_ref_vector const& soft): 
             maxsmt_solver_base(c, ws, soft) {
         }
         virtual ~sls() {}
@@ -52,8 +52,8 @@ namespace opt {
 
     };
 
-    maxsmt_solver_base* opt::mk_sls(context& c,
+    maxsmt_solver_base* opt::mk_sls(
-                                    vector<rational> const& ws, expr_ref_vector const& soft) {
+        context& c, weights_t& ws, expr_ref_vector const& soft) {
         return alloc(sls, c, ws, soft);
     }
 

src/opt/maxsls.h

@@ -27,8 +27,7 @@ Notes:
 namespace opt {
 
 
-    maxsmt_solver_base* mk_sls(context& c,
+    maxsmt_solver_base* mk_sls(context& c, weights_t& ws, expr_ref_vector const& soft);
-                               vector<rational> const& ws, expr_ref_vector const& soft);
 
     
 };

src/opt/maxsmt.h

@@ -27,6 +27,8 @@ Notes:
 
 namespace opt {
 
+    typedef vector<rational> const weights_t;
+
     class context;
 
     class maxsmt_solver {
@@ -63,7 +65,7 @@ namespace opt {
         params_ref       m_params;           // config
 
     public:
-        maxsmt_solver_base(context& c, vector<rational> const& ws, expr_ref_vector const& soft); 
+        maxsmt_solver_base(context& c, weights_t& ws, expr_ref_vector const& soft); 
 
         virtual ~maxsmt_solver_base() {}        
         virtual rational get_lower() const { return m_lower; }
@@ -74,14 +76,14 @@ namespace opt {
         virtual void get_model(model_ref& mdl) { mdl = m_model.get(); }
         void set_model() { s().get_model(m_model); }
         virtual void updt_params(params_ref& p);
-        virtual void init_soft(vector<rational> const& weights, expr_ref_vector const& soft);
+        virtual void init_soft(weights_t& weights, expr_ref_vector const& soft);
         solver& s() { return m_s; }
         void init();
         expr* mk_not(expr* e);
         void set_mus(bool f);
         app* mk_fresh_bool(char const* name);
     protected:
-        void enable_sls(expr_ref_vector const& soft, vector<rational> const& ws);
+        void enable_sls(expr_ref_vector const& soft, weights_t& ws);
     };
 
     /**
@@ -122,7 +124,7 @@ namespace opt {
         void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;
     private:
-        bool is_maxsat_problem(vector<rational> const& ws) const;        
+        bool is_maxsat_problem(weights_t& ws) const;        
         void verify_assignment();
     };
 

src/opt/opt_context.h

@@ -34,6 +34,7 @@ namespace opt {
 
     class opt_solver;
 
+
     class context : public opt_wrapper, public pareto_callback {
         struct free_func_visitor;
         typedef map<symbol, maxsmt*, symbol_hash_proc, symbol_eq_proc> map_t;
@@ -175,7 +176,7 @@ namespace opt {
         solver& get_solver();
         ast_manager& get_manager() { return this->m; }
         params_ref& params() { return m_params; }
-        void enable_sls(expr_ref_vector const& soft, vector<rational> const& weights);
+        void enable_sls(expr_ref_vector const& soft, weights_t& weights);
         symbol const& maxsat_engine() const { return m_maxsat_engine; }
 
 

src/opt/pbmax.cpp

@@ -31,8 +31,7 @@ namespace opt {
 
     class pbmax : public maxsmt_solver_base {
     public:
-        pbmax(context& c,
+        pbmax(context& c, weights_t& ws, expr_ref_vector const& soft): 
-              vector<rational> const& ws, expr_ref_vector const& soft): 
             maxsmt_solver_base(c, ws, soft) {
         }
         
@@ -88,8 +87,8 @@ namespace opt {
         }
     };
 
-    maxsmt_solver_base* opt::mk_pbmax(context & c,
+    maxsmt_solver_base* opt::mk_pbmax(
-                                     vector<rational> const& ws, expr_ref_vector const& soft) {
+        context & c, weights_t& ws, expr_ref_vector const& soft) {
         return alloc(pbmax, c, ws, soft);
     }
 

src/opt/pbmax.h

@@ -23,8 +23,7 @@ Notes:
 #include "maxsmt.h"
 
 namespace opt {
-    maxsmt_solver_base* mk_pbmax(context& c,
+    maxsmt_solver_base* mk_pbmax(context& c, weights_t& ws, expr_ref_vector const& soft);
-                               vector<rational> const& ws, expr_ref_vector const& soft);
 
 }
 #endif

src/opt/wmax.cpp

@@ -84,11 +84,13 @@ namespace opt {
         lbool operator()() {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
+            solver::scoped_push _s1(s());
             lbool is_sat = l_true;
             bool was_sat = false;
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 wth().assert_weighted(m_soft[i].get(), m_weights[i]);
             }
+            solver::scoped_push _s2(s());
             while (l_true == is_sat) {
                 is_sat = s().check_sat(0,0);
                 if (m_cancel) {

src/sat/sat_solver.cpp

@@ -727,11 +727,7 @@ namespace sat {
             if (inconsistent()) return l_false;
             init_assumptions(num_lits, lits);
             propagate(false);
-            if (inconsistent()) {
+            if (check_inconsistent()) return l_false;
-                if (tracking_assumptions()) 
-                    resolve_conflict();
-                return l_false;
-            }
             cleanup();
             if (m_config.m_max_conflicts > 0 && m_config.m_burst_search > 0) {
                 m_restart_threshold = m_config.m_burst_search;
@@ -745,8 +741,8 @@ namespace sat {
 
             // iff3_finder(*this)();            
             simplify_problem();
+            if (check_inconsistent()) return l_false;
 
-            if (inconsistent()) return l_false;
             m_next_simplify = m_config.m_restart_initial * m_config.m_simplify_mult1;
 
             if (m_config.m_max_conflicts == 0) {
@@ -769,6 +765,7 @@ namespace sat {
                 restart();
                 if (m_conflicts >= m_next_simplify) {
                     simplify_problem();
+                    if (check_inconsistent()) return l_false;
                     m_next_simplify = static_cast<unsigned>(m_conflicts * m_config.m_simplify_mult2);
                     if (m_next_simplify > m_conflicts + m_config.m_simplify_max)
                         m_next_simplify = m_conflicts + m_config.m_simplify_max;
@@ -886,6 +883,17 @@ namespace sat {
         }
     }
 
+    bool solver::check_inconsistent() {
+        if (inconsistent()) {
+            if (tracking_assumptions()) 
+                resolve_conflict();
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
     void solver::init_assumptions(unsigned num_lits, literal const* lits) {
         if (num_lits == 0 && m_user_scope_literals.empty()) {
             return;
@@ -1575,32 +1583,37 @@ namespace sat {
         bool_var var     = antecedent.var();
         unsigned var_lvl = lvl(var);
         SASSERT(var < num_vars());
+        TRACE("sat", tout << antecedent << " " << (is_marked(var)?"+":"-") << "\n";);
         if (!is_marked(var)) {
             mark(var);
             m_unmark.push_back(var);
             if (is_assumption(antecedent)) {
                 m_core.push_back(antecedent);
             }
-        }        
+        }
     }
 
     void solver::process_consequent_for_unsat_core(literal consequent, justification const& js) {
-        TRACE("sat", tout << "processing consequent: " << consequent << "\n";
+        TRACE("sat", tout << "processing consequent: ";
+              if (consequent == null_literal) tout << "null\n";
+              else tout << consequent << "\n";
               display_justification(tout << "js kind: ", js);
               tout << "\n";);
         switch (js.get_kind()) {
         case justification::NONE:
             break;
         case justification::BINARY:
+            SASSERT(consequent != null_literal);
             process_antecedent_for_unsat_core(~(js.get_literal()));
             break;
         case justification::TERNARY:
+            SASSERT(consequent != null_literal);
             process_antecedent_for_unsat_core(~(js.get_literal1()));
             process_antecedent_for_unsat_core(~(js.get_literal2()));
             break;
         case justification::CLAUSE: {
             clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
-            unsigned i   = 0;
+            unsigned i = 0;
             if (consequent != null_literal) {
                 SASSERT(c[0] == consequent || c[1] == consequent);
                 if (c[0] == consequent) {
@@ -1611,7 +1624,7 @@ namespace sat {
                     i = 2;
                 }
             }
-            unsigned sz  = c.size();
+            unsigned sz = c.size();
             for (; i < sz; i++)
                 process_antecedent_for_unsat_core(~c[i]);
             break;
@@ -1652,6 +1665,11 @@ namespace sat {
         if (m_conflict_lvl == 0) {
             return;
         }
+        SASSERT(m_unmark.empty());
+        DEBUG_CODE({
+                for (unsigned i = 0; i < m_trail.size(); ++i) {
+                    SASSERT(!is_marked(m_trail[i].var()));
+                }});
 
         unsigned old_size = m_unmark.size();        
         int idx = skip_literals_above_conflict_level();
@@ -1674,9 +1692,9 @@ namespace sat {
         literal consequent = m_not_l;
         justification js   = m_conflict;
 
+
         while (true) {
             process_consequent_for_unsat_core(consequent, js);
-            idx--;
             while (idx >= 0) {
                 literal l = m_trail[idx];
                 if (is_marked(l.var()))
@@ -1695,6 +1713,7 @@ namespace sat {
             bool_var c_var = consequent.var();
             SASSERT(lvl(consequent) == m_conflict_lvl);
             js             = m_justification[c_var];
+            idx--;
         }        
         reset_unmark(old_size);
         if (m_config.m_minimize_core) {
@@ -1983,7 +2002,8 @@ namespace sat {
        assigned at level 0.
     */
     void solver::minimize_lemma() {
-        m_unmark.reset();
+        SASSERT(m_unmark.empty());
+        //m_unmark.reset();
         updt_lemma_lvl_set();
 
         unsigned sz   = m_lemma.size();

src/sat/sat_solver.h

@@ -247,6 +247,8 @@ namespace sat {
         bool is_marked_lit(literal l) const { return m_lit_mark[l.index()] != 0; }
         void mark_lit(literal l) { SASSERT(!is_marked_lit(l)); m_lit_mark[l.index()] = true; }
         void unmark_lit(literal l) { SASSERT(is_marked_lit(l)); m_lit_mark[l.index()] = false; }
+        bool check_inconsistent();
+
 
         // -----------------------
         //