fix #5254

src/opt/opt_context.cpp

@@ -1714,23 +1714,8 @@ namespace opt {
             objective const& obj = m_objectives[i];
             switch(obj.m_type) {
             case O_MINIMIZE:
-            case O_MAXIMIZE: {
+            case O_MAXIMIZE: 
-                inf_eps n = m_optsmt.get_lower(obj.m_index);
-                if (false && // theory_lra doesn't produce infinitesimals
-                    m_optsmt.objective_is_model_valid(obj.m_index) && 
-                    n.get_infinity().is_zero() &&
-                    n.get_infinitesimal().is_zero() &&
-                    is_numeral((*m_model)(obj.m_term), r1)) {
-                    rational r2 = n.get_rational();
-                    if (obj.m_type == O_MINIMIZE) {
-                        r1.neg();
-                    }
-                    CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";);
-                    CTRACE("opt", r1 != r2, tout << *m_model;);
-                    SASSERT(r1 == r2);
-                }
                 break;
-            }
             case O_MAXSMT: {
                 rational value(0);
                 for (unsigned i = 0; i < obj.m_terms.size(); ++i) {

src/opt/opt_solver.cpp

@@ -244,23 +244,46 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         m_last_model = nullptr;
+        //
+        // compute an optimization hint.
+        // The hint is valid if there are no shared symbols (a pure LP).
+        // Generally, the hint is not necessarily valid and has to be checked
+        // relative to other theories.
+        // 
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
         m_context.get_model(m_last_model);
         inf_eps val2;
-        m_valid_objectives[i] = true;
         has_shared = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";
               if (m_last_model) tout << *m_last_model << "\n";);
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
+
+        //
+        // retrieve value of objective from current model and update 
+        // current optimal.
+        // 
+        auto update_objective = [&]() {
+            rational r;
+            expr_ref value = (*m_last_model)(m_objective_terms.get(i));
+            if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i])
+                m_objective_values[i] = inf_eps(r);            
+        };
+
+        update_objective();
                         
-        auto decrement = [&]() {
+
+        // 
+        // check that "val" obtained from optimization hint is a valid bound.
+        // 
+        auto check_bound = [&]() {
             SASSERT(has_shared);
-            decrement_value(i, val);
+            bool ok = bound_value(i, val);
             if (l_true != m_context.check(0, nullptr))  
                 return false;
-            m_context.get_model(m_last_model);      
+            m_context.get_model(m_last_model);   
-            return true;
+            update_objective();
+            return ok;
         };
 
         if (!val.is_finite()) {
@@ -270,19 +293,16 @@ namespace opt {
             TRACE("opt", tout << "updated\n";);
             m_last_model = nullptr;
             m_context.get_model(m_last_model);
-            if (has_shared && val != current_objective_value(i)) {
+            if (!has_shared || val == current_objective_value(i))
-                if (!decrement())
-                    return false;
-            }
-            else {
                 m_models.set(i, m_last_model.get());
-            }
+            else if (!check_bound())
+                return false;
         }
-        else if (!decrement())
+        else if (!check_bound())
             return false;
         m_objective_values[i] = val;
         TRACE("opt", { 
-                tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
+                tout << "objective:     " << mk_pp(m_objective_terms.get(i), m) << "\n";
                 tout << "maximal value: " << val << "\n"; 
                 tout << "new condition: " << blocker << "\n";
                 if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); 
@@ -291,10 +311,9 @@ namespace opt {
         return true;
     }
 
-    lbool opt_solver::decrement_value(unsigned i, inf_eps& val) {
+    bool opt_solver::bound_value(unsigned i, inf_eps& val) {
         push_core();
         expr_ref ge = mk_ge(i, val);
-        TRACE("opt", tout << ge << "\n";);
         assert_expr(ge);
         lbool is_sat = m_context.check(0, nullptr);
         is_sat = adjust_result(is_sat);
@@ -303,19 +322,7 @@ namespace opt {
             m_models.set(i, m_last_model.get());
         }
         pop_core(1);
-        TRACE("opt", tout << is_sat << "\n";);
+        return is_sat == l_true;
-        if (is_sat != l_true) {
-            // cop-out approximation
-            if (arith_util(m).is_real(m_objective_terms.get(i))) {
-                val -= inf_eps(inf_rational(rational(0), true));
-            }
-            else {
-                val -= inf_eps(inf_rational(rational(1)));
-            }
-            m_valid_objectives[i] = false;
-        }
-        return is_sat;
-
     }
 
     lbool opt_solver::adjust_result(lbool r) {
@@ -338,10 +345,12 @@ namespace opt {
         for (unsigned i = m_models.size(); i-- > 0; ) {
             auto* mdl = m_models[i];
             if (mdl) {
+                TRACE("opt", tout << "get " << i << "\n" << *mdl << "\n";);
                 m = mdl;
                 return;
             }
         }        
+        TRACE("opt", tout << "get last\n";);
         m = m_last_model.get();
     }
     
@@ -384,7 +393,6 @@ namespace opt {
         m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational::minus_one(), inf_rational()));
         m_objective_terms.push_back(term);
-        m_valid_objectives.push_back(true);
         m_models.push_back(nullptr);
         return v;
     }
@@ -486,7 +494,6 @@ namespace opt {
         m_objective_vars.reset();
         m_objective_values.reset();
         m_objective_terms.reset();
-        m_valid_objectives.reset();
     }
 
     opt_solver& opt_solver::to_opt(solver& s) {

src/opt/opt_solver.h

@@ -77,7 +77,6 @@ namespace opt {
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;
         expr_ref_vector     m_objective_terms;
-        bool_vector       m_valid_objectives;
         bool                m_dump_benchmarks;
         static unsigned     m_dump_count;
         statistics          m_stats;
@@ -124,9 +123,6 @@ namespace opt {
         inf_eps const & saved_objective_value(unsigned obj_index);
         inf_eps current_objective_value(unsigned obj_index);
         model* get_model_idx(unsigned obj_index) { return m_models[obj_index]; }
-        bool objective_is_model_valid(unsigned obj_index) const {
-            return m_valid_objectives[obj_index];
-        }
 
         bool was_unknown() const { return m_was_unknown; }
 
@@ -147,7 +143,7 @@ namespace opt {
                                symbol const& logic = symbol::null, char const * status = "unknown", char const * attributes = "");
 
     private:
-        lbool decrement_value(unsigned i, inf_eps& val);
+        bool bound_value(unsigned i, inf_eps& val);
         void set_model(unsigned i);
         lbool adjust_result(lbool r);
     };

src/opt/optsmt.cpp

@@ -195,24 +195,25 @@ namespace opt {
     lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
         TRACE("opt", tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";);
         arith_util arith(m);
-        bool is_int = arith.is_int(m_objs[obj_index].get());
+        bool is_int = arith.is_int(m_objs.get(obj_index));
         lbool is_sat = l_true;
         expr_ref bound(m), last_bound(m);
 
-        for (unsigned i = 0; i < obj_index; ++i) {
+        for (unsigned i = 0; i < obj_index; ++i) 
             commit_assignment(i);
-        }
 
         unsigned steps = 0;
         unsigned step_incs = 0;
         rational delta_per_step(1);
         unsigned num_scopes = 0;
+        inf_eps last_objective = inf_eps(rational(-1), inf_rational(0));
 
         while (m.inc()) {
             SASSERT(delta_per_step.is_int());
             SASSERT(delta_per_step.is_pos());
             is_sat = m_s->check_sat(0, nullptr);
             TRACE("opt", tout << "check " << is_sat << "\n";
+                  tout << "last bound: " << last_bound << "\n";
                   tout << "lower: " << m_lower[obj_index] << "\n";
                   tout << "upper: " << m_upper[obj_index] << "\n";
                   );
@@ -221,6 +222,7 @@ namespace opt {
                 m_s->get_model(m_model);
                 SASSERT(m_model);
                 inf_eps obj = m_s->saved_objective_value(obj_index);
+                TRACE("opt", tout << "saved objective: " << obj << "\n";);
                 update_lower_lex(obj_index, obj, is_maximize);
                 if (!is_int || !m_lower[obj_index].is_finite()) {
                     delta_per_step = rational(1);
@@ -233,12 +235,12 @@ namespace opt {
                 else {
                     ++steps;
                 }
-                if (delta_per_step > rational::one()) {
+                if (delta_per_step > rational::one() || obj == last_objective) {
                     m_s->push();
                     ++num_scopes;
                     bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
                 }
-                TRACE("opt", tout << "delta: " << delta_per_step << " " << bound << "\n";);
+                last_objective = obj;
                 if (bound == last_bound) {
                     break;
                 }
@@ -357,6 +359,7 @@ namespace opt {
     }
 
     void optsmt::update_lower_lex(unsigned idx, inf_eps const& v, bool is_maximize) {
+        TRACE("opt", tout << v << " lower: " << m_lower[idx] << "\n";);
         if (v > m_lower[idx]) {
             m_lower[idx] = v;                
             IF_VERBOSE(1, 
@@ -368,6 +371,7 @@ namespace opt {
             for (unsigned i = idx+1; i < m_vars.size(); ++i) {
                 m_lower[i] = m_s->saved_objective_value(i);
             }
+            TRACE("opt", tout << "update best model " << *m_model << "\n";);
             m_best_model = m_model;
             m_s->get_labels(m_labels);
             m_context.set_model(m_model);
@@ -532,10 +536,6 @@ namespace opt {
         return m_lower[i];
     }
 
-    bool optsmt::objective_is_model_valid(unsigned index) const {
-        return m_s->objective_is_model_valid(index);
-    }
-
     inf_eps optsmt::get_upper(unsigned i) const {
         if (i >= m_upper.size()) return inf_eps();
         return m_upper[i];
@@ -543,6 +543,7 @@ namespace opt {
 
     void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {        
         mdl = m_best_model.get();
+        TRACE("opt", tout << *mdl << "\n";);
         labels = m_labels;
     }
 

src/opt/optsmt.h

@@ -61,7 +61,6 @@ namespace opt {
         void commit_assignment(unsigned index);
         inf_eps get_lower(unsigned index) const;
         inf_eps get_upper(unsigned index) const;
-        bool objective_is_model_valid(unsigned index) const;
         void    get_model(model_ref& mdl, svector<symbol>& labels);
         model*  get_model(unsigned index) const { return m_models[index]; }