fix conflict level detection bug with plugins

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

src/opt/maxres.cpp

@@ -193,7 +193,6 @@ public:
         trace();
         if (is_sat != l_true) return is_sat;
         while (m_lower < m_upper) {
-            if (m_lower >= m_upper) break;
             TRACE("opt", 
                   display_vec(tout, m_asms);
                   s().display(tout);
@@ -206,6 +205,7 @@ public:
             }
             switch (is_sat) {
             case l_true: 
+                SASSERT(is_true(m_asms));
                 found_optimum();
                 return l_true;
             case l_false:
@@ -223,6 +223,7 @@ public:
                 break;
             }
         }
+        found_optimum();
         trace();
         return l_true;
     }
@@ -296,18 +297,24 @@ public:
         }
         else {
             is_sat = check_sat(asms.size(), asms.c_ptr());            
-        }
+        }              
         return is_sat;
     }
 
     lbool check_sat(unsigned sz, expr* const* asms) {
-        return s().check_sat(sz, asms);        
+        lbool r = s().check_sat(sz, asms);        
+        if (r == l_true) {
+            model_ref mdl;
+            s().get_model(mdl);
+            if (mdl.get()) {
+                update_assignment(mdl.get());            
+            }
+        }
+        return r;
     }
 
     void found_optimum() {
         IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
-        s().get_model(m_model);
-        SASSERT(is_true(m_asms));
         rational upper(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
@@ -745,6 +752,7 @@ public:
             nsoft.push_back(mk_not(m, m_soft[i]));
         }            
         fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper);
+        TRACE("opt", tout << "block upper bound " << fml << "\n";);;
         s().assert_expr(fml); 
     }
 

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_clause.cpp

@@ -198,13 +198,13 @@ namespace sat {
         size_t size = clause::get_obj_size(num_lits);
         void * mem = m_allocator.allocate(size);
         clause * cls = new (mem) clause(m_id_gen.mk(), num_lits, lits, learned);
-        TRACE("sat", tout << "alloc: " << cls->id() << " " << cls << " " << *cls << " " << (learned?"l":"a") << "\n";);
+        TRACE("sat", tout << "alloc: " << cls->id() << " " << *cls << " " << (learned?"l":"a") << "\n";);
         SASSERT(!learned || cls->is_learned());
         return cls;
     }
 
     void clause_allocator::del_clause(clause * cls) {
-        TRACE("sat", tout << "delete: " << cls->id() << " " << cls << " " << *cls << "\n";);
+        TRACE("sat", tout << "delete: " << cls->id() << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());
 #if defined(_AMD64_)
 #if defined(Z3DEBUG)

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

@@ -205,7 +205,7 @@ namespace sat {
     }
 
     clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
-        TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << "\n";);
+        TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << (learned?" learned":" aux") << "\n";);
         if (!learned) {
             bool keep = simplify_clause(num_lits, lits);
             TRACE("sat_mk_clause", tout << "mk_clause (after simp), keep: " << keep << "\n" << mk_lits_pp(num_lits, lits) << "\n";);
@@ -515,7 +515,7 @@ namespace sat {
 
     void solver::assign_core(literal l, justification j) {
         SASSERT(value(l) == l_undef);
-        TRACE("sat_assign_core", tout << l << "\n";);
+        TRACE("sat_assign_core", tout << l << " " << j << " level: " << scope_lvl() << "\n";);
         if (at_base_lvl())
             j = justification(); // erase justification for level 0
         m_assignment[l.index()]    = l_true;
@@ -1086,9 +1086,7 @@ namespace sat {
         }
 
         TRACE("sat",
-              for (unsigned i = 0; i < num_lits; ++i)
+              tout << literal_vector(num_lits, lits) << "\n";
-                  tout << lits[i] << " ";
-              tout << "\n";
               if (!m_user_scope_literals.empty()) {
                   tout << "user literals: " << m_user_scope_literals << "\n";
               }
@@ -1705,7 +1703,7 @@ namespace sat {
         m_conflicts_since_restart++;
         m_conflicts_since_gc++;
 
-        m_conflict_lvl = get_max_lvl(m_not_l == literal() ? m_not_l : ~m_not_l, m_conflict);
+        m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
         TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for ";
               if (m_not_l == literal()) tout << "null literal\n";
               else tout << m_not_l << "\n";);
@@ -1733,7 +1731,7 @@ namespace sat {
             process_antecedent(m_not_l, num_marks);
         }
 
-        literal consequent = m_not_l == null_literal ? m_not_l : ~m_not_l;
+        literal consequent = m_not_l; 
         justification js   = m_conflict;
 
         do {
@@ -2056,10 +2054,9 @@ namespace sat {
             }
         }
 
-        literal consequent = m_not_l == null_literal ? m_not_l : ~m_not_l;
+        literal consequent = m_not_l;
         justification js   = m_conflict;
 
-
         while (true) {
             process_consequent_for_unsat_core(consequent, js);
             while (idx >= 0) {
@@ -2099,59 +2096,32 @@ namespace sat {
     }
 
 
-    unsigned solver::get_max_lvl(literal consequent, justification js) {
+    unsigned solver::get_max_lvl(literal not_l, justification js) {
-        if (!m_ext)
+        if (!m_ext || at_base_lvl())
             return scope_lvl();
 
-        if (at_base_lvl())
-            return 0;
-
-        unsigned r = 0;
-
-        if (consequent != null_literal)
-            r = lvl(consequent);
-
         switch (js.get_kind()) {
         case justification::NONE:
-            break;
         case justification::BINARY:
-            r = std::max(r, lvl(js.get_literal()));
-            break;
         case justification::TERNARY:
-            r = std::max(r, lvl(js.get_literal1()));
-            r = std::max(r, lvl(js.get_literal2()));
-            break;
         case justification::CLAUSE: {
-            clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
+            return scope_lvl();
-            unsigned i   = 0;
-            if (consequent != null_literal) {
-                SASSERT(c[0] == consequent || c[1] == consequent);
-                if (c[0] == consequent) {
-                    i = 1;
-                }
-                else {
-                    r = std::max(r, lvl(c[0]));
-                    i = 2;
-                }
-            }
-            unsigned sz = c.size();
-            for (; i < sz; i++)
-                r = std::max(r, lvl(c[i]));
-            break;
         }
         case justification::EXT_JUSTIFICATION: {
-            fill_ext_antecedents(consequent, js);
+            unsigned r = 0;
+            if (not_l != null_literal)
+                r = lvl(~not_l);
+            fill_ext_antecedents(~not_l, js);
             literal_vector::iterator it  = m_ext_antecedents.begin();
             literal_vector::iterator end = m_ext_antecedents.end();
             for (; it != end; ++it)
                 r = std::max(r, lvl(*it));
-            break;
+            return r;
         }
         default:
             UNREACHABLE();
-            break;
+            return 0;
         }
-        return r;
     }
 
     /**

src/sat/sat_solver/inc_sat_solver.cpp

@@ -283,12 +283,9 @@ public:
                 conseq.push_back(cons);
             }
         }
-
         return r;
     }
 
-
-
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
         sat::literal_vector ls;
         u_map<expr*> lit2var;

src/shell/opt_frontend.cpp

@@ -351,6 +351,21 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
         case l_false: std::cout << "unsat\n"; break;
         case l_undef: std::cout << "unknown\n"; break;
         }
+        DEBUG_CODE(
+            if (false && r == l_true) {
+                model_ref mdl;
+                opt.get_model(mdl);
+                expr_ref_vector hard(m);
+                opt.get_hard_constraints(hard);
+                for (unsigned i = 0; i < hard.size(); ++i) {
+                    std::cout << "validate: " << i << "\n";
+                    expr_ref tmp(m);
+                    VERIFY(mdl->eval(hard[i].get(), tmp));
+                    if (!m.is_true(tmp)) {
+                        std::cout << tmp << "\n";
+                    }
+                }
+            });
     }
     catch (z3_exception & ex) {
         std::cerr << ex.msg() << "\n";