Merge branch 'master' of https://github.com/Z3Prover/z3

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]);
@@ -742,6 +749,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/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_solver.cpp

@@ -192,7 +192,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";);
@@ -502,7 +502,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 (scope_lvl() == 0)
             j = justification(); // erase justification for level 0
         m_assignment[l.index()]    = l_true;
@@ -1070,9 +1070,7 @@ namespace sat {
         }
 
         TRACE("sat",
-              for (unsigned i = 0; i < num_lits; ++i)
-                  tout << lits[i] << " ";
-              tout << "\n";
+              tout << literal_vector(num_lits, lits) << "\n";
               if (!m_user_scope_literals.empty()) {
                   tout << "user literals: " << m_user_scope_literals << "\n";
               }
@@ -2039,7 +2037,7 @@ namespace sat {
             }
         }
 
-        literal consequent = m_not_l;
+        literal consequent = m_not_l; 
         justification js   = m_conflict;
 
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -273,12 +273,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";