fix lower/upper bound updates

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

src/opt/fu_malik.cpp

@@ -43,28 +43,31 @@ namespace opt {
 
     struct fu_malik::imp {
         ast_manager& m;        
+        solver &        m_original_solver;
+        ref<solver>     m_s;
         expr_ref_vector m_soft;
         expr_ref_vector m_orig_soft;
         expr_ref_vector m_aux;
         expr_ref_vector m_assignment;
-        unsigned        m_upper_size;
+        unsigned        m_upper;
+        unsigned        m_lower;
         model_ref       m_model;
 
-        ref<solver>     m_s;
-        solver &        m_original_solver;
         bool            m_use_new_bv_solver; 
 
         imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
             m(m),
+            m_original_solver(s),
             m_s(&s),
             m_soft(soft),
             m_orig_soft(soft),
             m_aux(m),
             m_assignment(m),
-            m_original_solver(s),
+            m_upper(0),
+            m_lower(0),
             m_use_new_bv_solver(false)
         {
-            m_upper_size = m_soft.size() + 1;
+            m_upper = m_soft.size() + 1;
         }
 
         solver& s() { return *m_s; }
@@ -156,7 +159,7 @@ namespace opt {
         }
 
         lbool step() {
-            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
+            IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper << ")\n";);
             expr_ref_vector assumptions(m), block_vars(m);
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 assumptions.push_back(m.mk_not(m_aux[i].get()));
@@ -295,14 +298,14 @@ namespace opt {
                 lbool is_sat = l_true;                
                 do {
                     is_sat = step();
-                    --m_upper_size;
+                    --m_upper;
                 }
                 while (is_sat == l_false);
                 
                 if (is_sat == l_true) {
                     // Get a list of satisfying m_soft
                     s().get_model(m_model);
-
+                    m_lower = m_upper;
                     m_assignment.reset();                    
                     for (unsigned i = 0; i < m_orig_soft.size(); ++i) {
                         expr_ref val(m);
@@ -335,10 +338,10 @@ namespace opt {
         return (*m_imp)();
     }
     rational fu_malik::get_lower() const {
-        return rational(0);
+        return rational(m_imp->m_lower);
     }
     rational fu_malik::get_upper() const {
-        return rational(m_imp->m_upper_size);
+        return rational(m_imp->m_upper);
     }
     rational fu_malik::get_value() const {
         return rational(m_imp->m_assignment.size());

src/opt/opt_context.cpp

@@ -381,12 +381,10 @@ namespace opt {
             objective & obj = m_objectives[i];
             switch(obj.m_type) {
             case O_MINIMIZE:
-                obj.m_index = m_optsmt.get_num_objectives();
+                obj.m_index = m_optsmt.add(obj.m_term, false);
-                m_optsmt.add(obj.m_term, false);
                 break;
             case O_MAXIMIZE:
-                obj.m_index = m_optsmt.get_num_objectives();
+                obj.m_index = m_optsmt.add(obj.m_term, true);
-                m_optsmt.add(obj.m_term, true);
                 break;
             case O_MAXSMT: {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);

src/opt/optsmt.cpp

@@ -349,7 +349,7 @@ namespace opt {
         }        
     }
 
-    void optsmt::add(app* t, bool is_max) {
+    unsigned optsmt::add(app* t, bool is_max) {
         expr_ref t1(t, m), t2(m);
         th_rewriter rw(m);
         if (!is_max) {
@@ -362,6 +362,7 @@ namespace opt {
         m_is_max.push_back(is_max);
         m_lower.push_back(inf_eps(rational(-1),inf_rational(0)));
         m_upper.push_back(inf_eps(rational(1), inf_rational(0)));
+        return m_objs.size()-1;
     }
 
     void optsmt::updt_params(params_ref& p) {

src/opt/optsmt.h

@@ -47,7 +47,7 @@ namespace opt {
 
         lbool lex(unsigned obj_index);
 
-        void add(app* t, bool is_max);
+        unsigned add(app* t, bool is_max);
 
         void set_cancel(bool f);
 

src/opt/weighted_maxsat.cpp

@@ -291,6 +291,7 @@ namespace opt {
         expr_ref_vector  m_assignment;
         vector<rational> m_weights;
         rational         m_upper;
+        rational         m_lower;
         model_ref        m_model;
 
         imp(ast_manager& m, opt_solver& s, expr_ref_vector& soft_constraints, vector<rational> const& weights):
@@ -345,6 +346,9 @@ namespace opt {
                 }
             }
             m_upper = wth.get_min_cost();
+            if (result == l_true) {
+                m_lower = m_upper;
+            }
             wth.get_model(m_model);
             TRACE("opt", tout << "min cost: " << m_upper << "\n";);
             wth.reset();
@@ -352,7 +356,7 @@ namespace opt {
         }        
 
         rational get_lower() const {
-            return rational(0);
+            return m_lower;
         }
 
         rational get_upper() const {