disable propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 11, 2022 · ac55e29 · ac55e29
1 parent eb2dd92
commit ac55e29
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 11 deletions.
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
@@ -91,12 +91,15 @@ namespace opt {
                 m_upper += s.weight;
         }
 
+        return true;
+
         preprocess pp(s());
         rational lower(0);
         bool r = pp(m_soft, lower);
 
+
         if (lower != 0)
-            m_adjust_value.set_offset(lower + m_adjust_value.get_offset());
+            m_adjust_value->set_offset(lower + m_adjust_value->get_offset());
 
         TRACE("opt", 
               tout << "upper: " << m_upper << " assignments: ";
@@ -166,8 +169,8 @@ namespace opt {
 
     void maxsmt_solver_base::trace_bounds(char const * solver) {
         IF_VERBOSE(1, 
-                   rational l = m_adjust_value(m_lower);
-                   rational u = m_adjust_value(m_upper);
+                   rational l = (*m_adjust_value)(m_lower);
+                   rational u = (*m_adjust_value)(m_upper);
                    if (l > u) std::swap(l, u);
                    verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);                
     }
@@ -206,7 +209,7 @@ namespace opt {
 
         if (m_msolver) {
             m_msolver->updt_params(m_params);
-            m_msolver->set_adjust_value(m_adjust_value);
+            m_msolver->set_adjust_value(*m_adjust_value);
             is_sat = l_undef;
             try {
                 is_sat = (*m_msolver)();
@@ -231,9 +234,9 @@ namespace opt {
     }
 
     void maxsmt::set_adjust_value(adjust_value& adj) { 
-        m_adjust_value = adj; 
+        m_adjust_value = &adj; 
         if (m_msolver) {
-            m_msolver->set_adjust_value(m_adjust_value);
+            m_msolver->set_adjust_value(adj);            
         }
     }
 
@@ -265,7 +268,7 @@ namespace opt {
             rational q = m_msolver->get_lower();
             if (q > r) r = q;
         }
-        return m_adjust_value(r);
+        return (*m_adjust_value)(r);
     }
 
     rational maxsmt::get_upper() const {
@@ -274,7 +277,7 @@ namespace opt {
             rational q = m_msolver->get_upper();
             if (q < r) r = q; 
         }
-        return m_adjust_value(r);
+        return (*m_adjust_value)(r);
     }
 
     void maxsmt::update_lower(rational const& r) {

diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h
@@ -35,7 +35,7 @@ namespace opt {
 
     class maxsmt_solver {
     protected:
-        adjust_value m_adjust_value;
+        adjust_value* m_adjust_value = nullptr;
     public:        
         virtual ~maxsmt_solver() {}
         virtual lbool operator()() = 0;
@@ -45,7 +45,7 @@ namespace opt {
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
         virtual void updt_params(params_ref& p) = 0;
-        void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
+        void set_adjust_value(adjust_value& adj) { m_adjust_value = &adj; }
 
     };
 
@@ -128,7 +128,7 @@ namespace opt {
         expr_ref_vector  m_answer;
         rational         m_lower;
         rational         m_upper;
-        adjust_value     m_adjust_value;
+        adjust_value*    m_adjust_value = nullptr;
         model_ref        m_model;
         svector<symbol>  m_labels;
         params_ref       m_params;