fix bug in core generation in legacy core: it ignores complementary literals

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

src/opt/inc_sat_solver.cpp

@@ -356,16 +356,13 @@ private:
         }
     }
 
-    // TBD: this is super-expensive because of the
-    // bit-blasting model converter.
-
     void extract_model() {
         TRACE("sat", tout << "retrieve model\n";);
-        sat::model const & ll_m = m_solver.get_model();
+        if (!m_solver.model_is_current()) {
-        if (ll_m.empty()) {
             m_model = 0;
             return;
         }
+        sat::model const & ll_m = m_solver.get_model();
         model_ref md = alloc(model, m);
         atom2bool_var::iterator it  = m_map.begin();
         atom2bool_var::iterator end = m_map.end();

src/opt/maxres.cpp

@@ -130,6 +130,7 @@ public:
         if (m_asm2weight.find(e, weight)) {
             weight += w;
             m_asm2weight.insert(e, weight);
+            m_upper += w;
             return;
         }
         if (is_literal(e)) {
@@ -154,6 +155,7 @@ public:
     lbool mus_solver() {
         init();
         init_local();
+        trace_bounds("maxres");
         while (m_lower < m_upper) {
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
@@ -776,6 +778,7 @@ public:
             if (!m.is_true(tmp)) {
                 upper += m_weights[i];
             }
+            TRACE("opt", tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
             CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), 
                    tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
         }

src/opt/maxsmt.cpp

@@ -71,9 +71,9 @@ namespace opt {
         }
         
         TRACE("opt", 
-              tout << m_upper << ": ";
+              tout << "upper: " << m_upper << " assignments: ";
               for (unsigned i = 0; i < m_weights.size(); ++i) {
-                  tout << (m_assignment[i]?"1":"0");
+                  tout << (m_assignment[i]?"T":"F");
               }
               tout << "\n";);
     }

src/opt/opt_context.cpp

@@ -830,6 +830,7 @@ namespace opt {
 
     void context::update_bound(bool is_lower) {
         expr_ref val(m);
+        if (!m_model.get()) return;
         bool override = true;
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];

src/sat/sat_solver.cpp

@@ -948,6 +948,7 @@ namespace sat {
     }
 
     void solver::init_search() {
+        m_model_is_current        = false;
         m_phase_counter           = 0;
         m_phase_cache_on          = false;
         m_conflicts_since_restart = 0;
@@ -1036,6 +1037,7 @@ namespace sat {
 
     void solver::mk_model() {
         m_model.reset();
+        m_model_is_current = true;
         unsigned num = num_vars();
         m_model.resize(num, l_undef);
         for (bool_var v = 0; v < num; v++) {
@@ -1738,6 +1740,7 @@ namespace sat {
             m_mus(); // ignore return value on cancelation.
             m_model.reset();
             m_model.append(m_mus.get_model());            
+            m_model_is_current = true;
         }
     }
 

src/sat/sat_solver.h

@@ -76,8 +76,9 @@ namespace sat {
         random_gen              m_rand;
         clause_allocator        m_cls_allocator;
         cleaner                 m_cleaner;
-        model                   m_model;
+        model                   m_model;        
         model_converter         m_mc;
+        bool                    m_model_is_current;
         simplifier              m_simplifier;
         scc                     m_scc;
         asymm_branch            m_asymm_branch;
@@ -270,6 +271,7 @@ namespace sat {
     public:
         lbool check(unsigned num_lits = 0, literal const* lits = 0);
         model const & get_model() const { return m_model; }
+        bool model_is_current() const { return m_model_is_current; }
         literal_vector const& get_core() const { return m_core; }
         model_converter const & get_model_converter() const { return m_mc; }
 

src/smt/smt_context.cpp

@@ -2852,7 +2852,7 @@ namespace smt {
 
     void context::init_assumptions(unsigned num_assumptions, expr * const * assumptions) {
         reset_assumptions();
-        m_bool_var2assumption.reset();
+        m_literal2assumption.reset();
         m_unsat_core.reset();
         if (num_assumptions > 0) {
             // We must give a chance to the theories to propagate before we create a new scope...
@@ -2868,7 +2868,7 @@ namespace smt {
                 proof * pr = m_manager.mk_asserted(curr_assumption);
                 internalize_assertion(curr_assumption, pr, 0);
                 literal l = get_literal(curr_assumption);
-                m_bool_var2assumption.insert(l.var(), curr_assumption);
+                m_literal2assumption.insert(l.index(), curr_assumption);
                 // mark_as_relevant(l); <<< not needed
                 // internalize_assertion marked l as relevant.
                 SASSERT(is_relevant(l));
@@ -2877,7 +2877,7 @@ namespace smt {
                     assign(l, mk_justification(justification_proof_wrapper(*this, pr)));
                 else
                     assign(l, b_justification::mk_axiom());
-                m_assumptions.push_back(l.var());
+                m_assumptions.push_back(l);
                 get_bdata(l.var()).m_assumption = true;
             }
         }
@@ -2887,10 +2887,10 @@ namespace smt {
     }
 
     void context::reset_assumptions() {
-        bool_var_vector::iterator it  = m_assumptions.begin();
+        literal_vector::iterator it  = m_assumptions.begin();
-        bool_var_vector::iterator end = m_assumptions.end();
+        literal_vector::iterator end = m_assumptions.end();
         for (; it != end; ++it)
-            get_bdata(*it).m_assumption = false;
+            get_bdata(it->var()).m_assumption = false;
         m_assumptions.reset();
     }
 
@@ -2907,10 +2907,8 @@ namespace smt {
             literal l = *it;
             TRACE("unsat_core_bug", tout << "answer literal: " << l << "\n";);
             SASSERT(get_bdata(l.var()).m_assumption);
-            SASSERT(m_bool_var2assumption.contains(l.var()));
+            SASSERT(m_literal2assumption.contains(l.index()));
-            expr * a = 0;
+            expr * a = m_literal2assumption[l.index()];
-            m_bool_var2assumption.find(l.var(), a);
-            SASSERT(a);
             if (!already_found_assumptions.contains(a)) {
                 already_found_assumptions.insert(a);
                 m_unsat_core.push_back(a);

src/smt/smt_context.h

@@ -201,9 +201,9 @@ namespace smt {
         // Unsat core extraction
         //
         // -----------------------------------
-        typedef u_map<expr *>  bool_var2assumption;
+        typedef u_map<expr *>  literal2assumption;
-        bool_var_vector             m_assumptions;
+        literal_vector             m_assumptions;
-        bool_var2assumption         m_bool_var2assumption; // maps an expression associated with a literal to the original assumption
+        literal2assumption         m_literal2assumption; // maps an expression associated with a literal to the original assumption
         expr_ref_vector             m_unsat_core;
 
         // -----------------------------------