fix scope bugs per Klaus Becker's examples

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

src/opt/maxres.cpp

@@ -84,6 +84,7 @@ private:
     strategy_t       m_st;
     rational         m_max_upper;
     bool             m_hill_climb;
+    bool             m_all_cores;
 
 public:
     maxres(context& c,
@@ -95,7 +96,8 @@ public:
         m_mss(m_s, m),
         m_trail(m),
         m_st(st),
-        m_hill_climb(true)
+        m_hill_climb(true),
+        m_all_cores(false)
     {
     }
 
@@ -151,21 +153,9 @@ public:
                 return l_undef;
             }
             switch (is_sat) {
-            case l_true: {
+            case l_true: 
-                s().get_model(m_model);
+                found_optimum();
-                expr_ref tmp(m);
-                DEBUG_CODE(
-                    for (unsigned i = 0; i < m_asms.size(); ++i) {
-                        VERIFY(m_model->eval(m_asms[i].get(), tmp));                        
-                        SASSERT(m.is_true(tmp));
-                    });
-                for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    VERIFY(m_model->eval(m_soft[i].get(), tmp));
-                    m_assignment[i] = m.is_true(tmp);
-                }
-                m_upper = m_lower;
                 return l_true;
-            }
             case l_false:
                 is_sat = process_unsat();
                 if (is_sat != l_true) return is_sat;
@@ -294,22 +284,67 @@ public:
         init();
         init_local();
         sls();
+        m_all_cores = true;
         NOT_IMPLEMENTED_YET();
-        ptr_vector<expr> mcs;
         vector<ptr_vector<expr> > cores;
         return l_undef;
-#if 0
+        lbool is_sat = l_true;
-        while (m_lower < m_upper) {            
+        while (m_lower < m_upper && is_sat == l_true) {            
             TRACE("opt", 
                   display_vec(tout, m_asms.size(), m_asms.c_ptr());
                   s().display(tout);
                   tout << "\n";
                   display(tout);
                   );
+            lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
+            if (m_cancel) {
+                return l_undef;
+            }
+            switch (is_sat) {
+            case l_true: 
+                found_optimum();
+                return l_true;
+            case l_false:
+                is_sat = process_unsat(cores);
+                break;
+            default:
+                break;
+            }
+            if (is_sat == l_undef) {
+                return l_undef;
+            }
+            if (cores.empty()) {
+                SASSERT(is_sat == l_false);
+                break;
+            }
+            SASSERT(is_sat == l_true);
+            // there is some best model, 
+            // extend it to a maximal assignment
+            // extracting the mss and mcs.
+            set_mus(false);
+            ptr_vector<expr> mss, mcs;
+            is_sat = m_mss(cores, mss, mcs);
+            set_mus(true);
+            if (is_sat != l_true) return is_sat;
+            // 
         }
         m_lower = m_upper;
         return l_true;
-#endif
+    }
+
+    void found_optimum() {
+        s().get_model(m_model);
+        expr_ref tmp(m);
+        DEBUG_CODE(
+            for (unsigned i = 0; i < m_asms.size(); ++i) {
+                VERIFY(m_model->eval(m_asms[i].get(), tmp));                        
+                SASSERT(m.is_true(tmp));
+            });
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            VERIFY(m_model->eval(m_soft[i].get(), tmp));
+            m_assignment[i] = m.is_true(tmp);
+        }
+        m_upper = m_lower;
     }
 
 
@@ -341,8 +376,7 @@ public:
                 break;
             }
             cores.push_back(core);
-            // TBD: ad hoc to avoid searching for large cores..
+            if (!m_all_cores && core.size() >= 3) {
-            if (core.size() >= 3) {
                 break;
             }
             remove_soft(core, asms);
@@ -409,7 +443,7 @@ public:
         return index;
     }
 
-    lbool process_sat(ptr_vector<expr>& corr_set) {
+    lbool process_sat(ptr_vector<expr> const& corr_set) {
         expr_ref fml(m), tmp(m);
         TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
         if (corr_set.empty()) {
@@ -425,6 +459,10 @@ public:
 
     lbool process_unsat() {
         vector<ptr_vector<expr> > cores;
+        return process_unsat(cores);
+    }
+
+    lbool process_unsat(vector<ptr_vector<expr> >& cores) {
         lbool is_sat = get_cores(cores);
         if (is_sat != l_true) {
             return is_sat;
@@ -438,7 +476,7 @@ public:
         return is_sat;
     }
     
-    lbool process_unsat(ptr_vector<expr>& core) {
+    lbool process_unsat(ptr_vector<expr> const& core) {
         expr_ref fml(m);
         remove_core(core);
         rational w = split_core(core);
@@ -452,7 +490,7 @@ public:
     }
 
     lbool minimize_core(ptr_vector<expr>& core) {
-        if (m_c.sat_enabled()) {
+        if (m_c.sat_enabled() || core.empty()) {
             return l_true;
         }
         m_mus.reset();
@@ -521,7 +559,7 @@ public:
         }
     }
 
-    void max_resolve(ptr_vector<expr>& core, rational const& w) {
+    void max_resolve(ptr_vector<expr> const& core, rational const& w) {
         SASSERT(!core.empty());
         expr_ref fml(m), asum(m);
         app_ref cls(m), d(m), dd(m);
@@ -563,7 +601,7 @@ public:
     }
 
     // cs is a correction set (a complement of a (maximal) satisfying assignment).
-    void cs_max_resolve(ptr_vector<expr>& cs, rational const& w) {
+    void cs_max_resolve(ptr_vector<expr> const& cs, rational const& w) {
         TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr()););
         SASSERT(!cs.empty());
         expr_ref fml(m), asum(m);

src/opt/maxsmt.cpp

@@ -41,7 +41,7 @@ namespace opt {
         m_c(c),
         m_cancel(false), m_soft(m),
         m_assertions(m) {
-        m_s.get_model(m_model);
+        c.get_base_model(m_model);
         SASSERT(m_model);
         updt_params(c.params());
         init_soft(ws, soft);

src/opt/opt_context.cpp

@@ -215,7 +215,7 @@ namespace opt {
         case 0:
             return is_sat;
         case 1:
-            return execute(m_objectives[0], true);
+            return execute(m_objectives[0], true, false);
         default: {
             opt_params optp(m_params);
             symbol pri = optp.priority();
@@ -232,6 +232,10 @@ namespace opt {
         }
     }
 
+    void context::get_base_model(model_ref& mdl) {
+        mdl = m_model;
+    }
+
     void context::get_model(model_ref& mdl) {
         mdl = m_model;
         if (mdl) {
@@ -242,27 +246,31 @@ namespace opt {
         }
     }
 
-    lbool context::execute_min_max(unsigned index, bool committed) {
+    lbool context::execute_min_max(unsigned index, bool committed, bool scoped) {
+        if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index);
-        if (result == l_true && committed) m_optsmt.commit_assignment(index);
         if (result == l_true) m_optsmt.get_model(m_model);
+        if (scoped) get_solver().pop(1);        
+        if (result == l_true && committed) m_optsmt.commit_assignment(index);
         return result;
     }
     
-    lbool context::execute_maxsat(symbol const& id, bool committed) {
+    lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) {
         model_ref tmp;
         maxsmt& ms = *m_maxsmts.find(id);
+        if (scoped) get_solver().push();            
         lbool result = ms(m_solver.get());
-        if (result == l_true && committed) ms.commit_assignment();
         if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
+        if (scoped) get_solver().pop(1);
+        if (result == l_true && committed) ms.commit_assignment();
         return result;
     }
 
-    lbool context::execute(objective const& obj, bool committed) {
+    lbool context::execute(objective const& obj, bool committed, bool scoped) {
         switch(obj.m_type) {
-        case O_MAXIMIZE: return execute_min_max(obj.m_index, committed);
+        case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped);
-        case O_MINIMIZE: return execute_min_max(obj.m_index, committed);
+        case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped);
-        case O_MAXSMT: return execute_maxsat(obj.m_id, committed);
+        case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped);
         default: UNREACHABLE(); return l_undef;
         }
     }
@@ -271,9 +279,7 @@ namespace opt {
         lbool r = l_true;
         for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
             bool is_last = i + 1 == m_objectives.size();
-            if (!is_last) get_solver().push();            
+            r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last);
-            r = execute(m_objectives[i], i + 1 < m_objectives.size());
-            if (!is_last) get_solver().pop(1);
             if (r == l_true && !get_lower_as_num(i).is_finite()) {
                 return r;
             }
@@ -291,7 +297,7 @@ namespace opt {
             objective const& obj = m_objectives[i];
             if (obj.m_type == O_MAXSMT) {
                 solver::scoped_push _sp(get_solver());
-                r = execute(obj, false);
+                r = execute(obj, false, false);
             }
         }
         return r;
@@ -399,9 +405,6 @@ namespace opt {
         if (is_sat == l_true) {
             yield();
         }
-        else {
-            m_solver->pop(1);
-        }
         return is_sat;
     }
 

src/opt/opt_context.h

@@ -179,14 +179,15 @@ namespace opt {
         void enable_sls(expr_ref_vector const& soft, weights_t& weights);
         void set_enable_sls(bool f) { m_enable_sls = f; }
         symbol const& maxsat_engine() const { return m_maxsat_engine; }
+        void get_base_model(model_ref& m);
 
 
     private:
         void validate_feasibility(maxsmt& ms);
 
-        lbool execute(objective const& obj, bool committed);
+        lbool execute(objective const& obj, bool committed, bool scoped);
-        lbool execute_min_max(unsigned index, bool committed);
+        lbool execute_min_max(unsigned index, bool committed, bool scoped);
-        lbool execute_maxsat(symbol const& s, bool committed);
+        lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();