From 405a26c5856ba726c31582eaf51103d01f1b51a7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 9 Apr 2022 09:55:02 +0200
Subject: [PATCH] allow adding constraints during on_model

---
 src/opt/maxres.cpp      | 17 ++++++++---------
 src/opt/maxsmt.cpp      | 14 +++++++++++++-
 src/opt/maxsmt.h        |  3 +++
 src/opt/opt_context.cpp | 11 ++++++++++-
 src/sat/sat_solver.cpp  |  2 ++
 5 files changed, 36 insertions(+), 11 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 27b3b7260..1b4348105 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -791,11 +791,10 @@ public:
         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 @@ public:
             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();
 
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 6a8a2ee35..bf25f3f95 100644
--- a/src/opt/maxsmt.cpp
+++ b/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 
diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
index ad355cc9e..5bf637dde 100644
--- a/src/opt/maxsmt.h
+++ b/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();
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 02cd90113..8848b61c9 100644
--- a/src/opt/opt_context.cpp
+++ b/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) 
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5505cfa70..4a254ac06 100644
--- a/src/sat/sat_solver.cpp
+++ b/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);