allow adding constraints during on_model

Author: NikolajBjorner

src/opt/maxres.cpp

@@ -791,11 +791,10 @@ class maxres : public maxsmt_solver_base {
         improve_model(mdl);
         mdl->set_model_completion(true);
         unsigned correction_set_size = 0;
-        for (expr* a : m_asms) {
-            if (mdl->is_false(a)) {
+        for (expr* a : m_asms) 
+            if (mdl->is_false(a)) 
                 ++correction_set_size;
-            }
-        }
+
         if (!m_csmodel.get() || correction_set_size < m_correction_set_size) {
             m_csmodel = mdl;
             m_correction_set_size = correction_set_size;
@@ -810,22 +809,22 @@ class maxres : public maxsmt_solver_base {
             return;
         }
 
-        if (!m_c.verify_model(m_index, mdl.get(), upper)) {
+        if (!m_c.verify_model(m_index, mdl.get(), upper)) 
             return;
-        }
 
+        unsigned num_assertions = s().get_num_assertions();
         m_model = mdl;
         m_c.model_updated(mdl.get());
 
         TRACE("opt", tout << "updated upper: " << upper << "\n";);
 
-        for (soft& s : m_soft) {
+        for (soft& s : m_soft) 
             s.set_value(m_model->is_true(s.s));
-        }
 
         verify_assignment();
 
-        m_upper = upper;
+        if (num_assertions == s().get_num_assertions())
+            m_upper = upper;
 
         trace();
 

src/opt/maxsmt.cpp

@@ -50,7 +50,13 @@ namespace opt {
 
     void maxsmt_solver_base::updt_params(params_ref& p) {
         m_params.copy(p);
-    }       
+    }
+
+    void maxsmt_solver_base::reset_upper() {
+        m_upper = m_lower;
+        for (soft& s : m_soft) 
+            m_upper += s.weight;
+    }
 
     solver& maxsmt_solver_base::s() {
         return m_c.get_solver(); 
@@ -289,6 +295,12 @@ namespace opt {
         }
     }
 
+    void maxsmt::reset_upper() {
+        if (m_msolver) {
+            m_msolver->reset_upper();
+            m_upper = m_msolver->get_upper();
+        }
+    }
 
     void maxsmt::verify_assignment() {
         // TBD: have to use a different solver 

src/opt/maxsmt.h

@@ -103,6 +103,8 @@ namespace opt {
         };
 
         lbool find_mutexes(obj_map<expr, rational>& new_soft);
+
+        void reset_upper();
 
 
     protected:
@@ -153,6 +155,7 @@ namespace opt {
         void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;
         void model_updated(model* mdl);
+        void reset_upper();
     private:
         bool is_maxsat_problem(weights_t& ws) const;        
         void verify_assignment();

src/opt/opt_context.cpp

@@ -195,13 +195,22 @@ namespace opt {
     }
 
     void context::add_hard_constraint(expr* f) {
-        if (m_calling_on_model) 
+        if (m_calling_on_model) {
             get_solver().assert_expr(f);
+            for (auto const& [k, v] : m_maxsmts)
+                v->reset_upper();
+            for (unsigned i = 0; i < num_objectives(); ++i) {
+                auto const& o = m_scoped_state.m_objectives[i]; 
+                if (o.m_type != O_MAXSMT)
+                    m_optsmt.update_upper(o.m_index, inf_eps::infinity());
+            }
+        }
         else {
             m_scoped_state.add(f);
             clear_state();
         }
     }
+    
 
     void context::add_hard_constraint(expr* f, expr* t) {
         if (m_calling_on_model) 

src/sat/sat_solver.cpp

@@ -3818,6 +3818,8 @@ namespace sat {
     void solver::move_to_front(bool_var b) {
         if (b >= num_vars())
             return;
+        if (m_case_split_queue.empty())
+            return;
         bool_var next = m_case_split_queue.min_var();
         auto next_act = m_activity[next];
         set_activity(b, next_act + 1);