Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847

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

src/opt/maxres.cpp

@@ -109,6 +109,7 @@ private:
     bool             m_pivot_on_cs;            // prefer smaller correction set to core.
     bool             m_dump_benchmarks;        // display benchmarks (into wcnf format)
 
+
     std::string      m_trace_id;
     typedef ptr_vector<expr> exprs;
 
@@ -152,8 +153,6 @@ public:
             (m.is_not(l, l) && is_uninterp_const(l));
     }    
 
-    
-
     void add_soft(expr* e, rational const& w) {
         TRACE("opt", tout << mk_pp(e, m) << " |-> " << w << "\n";);
         expr_ref asum(m), fml(m);
@@ -290,7 +289,7 @@ public:
                     index = next_index(asms, index);
                 }
                 first = false;
-                IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
+                // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";);
                 m_last_index = index;
                 is_sat = check_sat(index, asms.c_ptr());
             }            
@@ -490,7 +489,7 @@ public:
         TRACE("opt", display_vec(tout << "minimized core: ", core););
         IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
         max_resolve(core, w);
-        fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
+        fml = mk_not(m, mk_and(m, core.size(), core.c_ptr()));
         s().assert_expr(fml);
         m_lower += w;
         if (m_st == s_primal_dual) {
@@ -530,7 +529,10 @@ public:
     }
 
     lbool minimize_core(exprs& core) {
-        if (m_c.sat_enabled() || core.empty()) {
+        if (core.empty()) {
+            return l_true;
+        }
+        if (m_c.sat_enabled()) {
             return l_true;
         }
         m_mus.reset();
@@ -607,8 +609,8 @@ public:
         // Soundness of this rule can be established using MaxRes
         // 
         for (unsigned i = 1; i < core.size(); ++i) {
-            expr* b_i = m_B[i-1].get();
+            expr* b_i = core[i-1];
-            expr* b_i1 = m_B[i].get();
+            expr* b_i1 = core[i];
             if (i == 1) {
                 d = to_app(b_i);
             }
@@ -658,8 +660,8 @@ public:
         // d_i => d_{i-1} or b_{i-1}
         //
         for (unsigned i = 1; i < cs.size(); ++i) {
-            expr* b_i = m_B[i-1].get();
+            expr* b_i = cs[i - 1];
-            expr* b_i1 = m_B[i].get();
+            expr* b_i1 = cs[i];
             cls = m.mk_or(b_i, d);
             if (i > 2) {
                 d = mk_fresh_bool("d");
@@ -680,10 +682,11 @@ public:
             s().assert_expr(fml);
             m_defs.push_back(fml);
             new_assumption(asum, w);
+
             fml = m.mk_and(b_i1, cls);
             update_model(asum, fml);
         }
-        fml = m.mk_or(m_B.size(), m_B.c_ptr());
+        fml = m.mk_or(cs.size(), cs.c_ptr());
         s().assert_expr(fml);
     }
 
@@ -757,10 +760,9 @@ public:
     }
 
     bool is_true(expr_ref_vector const& es) {
-        for (unsigned i = 0; i < es.size(); ++i) {
+        unsigned i = 0;
-            if (!is_true(es[i])) return false;
+        for (; i < es.size() && is_true(es[i]); ++i) { }
-        }
+        return i == es.size();
-        return true;
     }
 
     void remove_soft(exprs const& core, expr_ref_vector& asms) {
@@ -780,7 +782,6 @@ public:
     virtual void updt_params(params_ref& p) {
         maxsmt_solver_base::updt_params(p);
         opt_params _p(p);
-
         m_hill_climb = _p.maxres_hill_climb();
         m_add_upper_bound_block = _p.maxres_add_upper_bound_block();
         m_max_num_cores = _p.maxres_max_num_cores();
@@ -858,7 +859,6 @@ public:
             IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
         }
     }
-
 };
 
 opt::maxsmt_solver_base* opt::mk_maxres(

src/opt/wmax.cpp

@@ -62,20 +62,21 @@ namespace opt {
             }
             m_upper = m_lower;
             bool was_sat = false;
-            expr_ref_vector disj(m), asms(m);
+            expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
             obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
             for (; it != end; ++it) {
                 expr* c = assert_weighted(wth(), it->m_key, it->m_value);
                 if (!is_true(it->m_key)) {
-                    disj.push_back(m.mk_not(c));
                     m_upper += it->m_value;
                 }
             }
             wth().init_min_cost(m_upper - m_lower);
-            s().assert_expr(mk_or(disj));
             trace_bounds("wmax");
             
+            TRACE("opt", 
+                  s().display(tout); tout << "\n";
+                  tout << "lower: " << m_lower << " upper: " << m_upper << "\n";);
             while (!m.canceled() && m_lower < m_upper) {
                 //mk_assumptions(asms);
                 //is_sat = s().preferred_sat(asms, cores);
@@ -84,6 +85,7 @@ namespace opt {
                     is_sat = l_undef;
                 }
                 if (is_sat == l_false) {
+                    TRACE("opt", tout << "Unsat\n";);
                     break;
                 }
                 if (is_sat == l_true) {

src/sat/sat_solver.cpp

@@ -234,19 +234,18 @@ namespace sat {
     }
 
     void solver::push_reinit_stack(clause & c) {
+        TRACE("sat_reinit", tout << "adding to reinit stack: " << c << "\n";);
         m_clauses_to_reinit.push_back(clause_wrapper(c));
         c.set_reinit_stack(true);    
     }
 
+
     clause * solver::mk_ter_clause(literal * lits, bool learned) {
         m_stats.m_mk_ter_clause++;
         clause * r = m_cls_allocator.mk_clause(3, lits, learned);
-        bool reinit;
+        bool reinit = attach_ter_clause(*r);
-        attach_ter_clause(*r, reinit);
+        if (reinit && !learned) push_reinit_stack(*r);
-        if (!learned && reinit) {
+        
-            TRACE("sat_reinit", tout << "adding to reinit stack: " << *r << "\n";);
-            push_reinit_stack(*r);
-        }
         if (learned)
             m_learned.push_back(r);
         else
@@ -254,8 +253,8 @@ namespace sat {
         return r;
     }
 
-    void solver::attach_ter_clause(clause & c, bool & reinit) {
+    bool solver::attach_ter_clause(clause & c) {
-        reinit = false;
+        bool reinit = false;
         m_watches[(~c[0]).index()].push_back(watched(c[1], c[2]));
         m_watches[(~c[1]).index()].push_back(watched(c[0], c[2]));
         m_watches[(~c[2]).index()].push_back(watched(c[0], c[1]));
@@ -276,18 +275,15 @@ namespace sat {
                 reinit = true;
             }
         }
+        return reinit;
     }
 
     clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
         m_stats.m_mk_clause++;
         clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
         SASSERT(!learned || r->is_learned());
-        bool reinit;
+        bool reinit = attach_nary_clause(*r);
-        attach_nary_clause(*r, reinit);
+        if (reinit && !learned) push_reinit_stack(*r);
-        if (!learned && reinit) {
-            TRACE("sat_reinit", tout << "adding to reinit stack: " << *r << "\n";);
-            push_reinit_stack(*r);
-        }
         if (learned)
             m_learned.push_back(r);
         else
@@ -295,8 +291,8 @@ namespace sat {
         return r;
     }
 
-    void solver::attach_nary_clause(clause & c, bool & reinit) {
+    bool solver::attach_nary_clause(clause & c) {
-        reinit = false;
+        bool reinit = false;
         clause_offset cls_off = m_cls_allocator.get_offset(&c);
         if (scope_lvl() > 0) {
             if (c.is_learned()) {
@@ -325,15 +321,16 @@ namespace sat {
         literal block_lit = c[some_idx];
         m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
         m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
+        return reinit;
     }
 
     void solver::attach_clause(clause & c, bool & reinit) {
         SASSERT(c.size() > 2);
         reinit = false;
         if (c.size() == 3)
-            attach_ter_clause(c, reinit);
+            reinit = attach_ter_clause(c);
         else
-            attach_nary_clause(c, reinit);
+            reinit = attach_nary_clause(c);
     }
 
     /**

src/sat/sat_solver.h

@@ -184,11 +184,9 @@ namespace sat {
         void mk_bin_clause(literal l1, literal l2, bool learned);
         bool propagate_bin_clause(literal l1, literal l2);
         clause * mk_ter_clause(literal * lits, bool learned);
-        void attach_ter_clause(clause & c, bool & reinit);
+        bool attach_ter_clause(clause & c);
-        void attach_ter_clause(clause & c) { bool reinit; attach_ter_clause(c, reinit); }
         clause * mk_nary_clause(unsigned num_lits, literal * lits, bool learned);
-        void attach_nary_clause(clause & c, bool & reinit);
+        bool attach_nary_clause(clause & c);
-        void attach_nary_clause(clause & c) { bool reinit; attach_nary_clause(c, reinit); }
         void attach_clause(clause & c, bool & reinit);
         void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
         unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;

src/smt/theory_wmaxsat.cpp

@@ -180,7 +180,7 @@ namespace smt {
 
     final_check_status theory_wmaxsat::final_check_eh() {
         if (m_normalize) normalize();
-        // std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";
+        TRACE("opt", tout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";);
         return FC_DONE;
     }