reworking pd-maxres

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

src/opt/maxres.cpp

@@ -104,6 +104,7 @@ private:
     bool             m_wmax;                   // Block upper bound using wmax
                                                // this option is disabled if SAT core is used.
 
+    std::string      m_trace_id;
     typedef ptr_vector<expr> exprs;
 
 public:
@@ -125,6 +126,14 @@ public:
         m_maximize_assignment(false),
         m_max_correction_set_size(3)
     {
+        switch(st) {
+        case s_primal:
+            m_trace_id = "maxres";
+            break;
+        case s_primal_dual:
+            m_trace_id = "pd-maxres";
+            break;
+        }        
     }
 
     virtual ~maxres() {}
@@ -168,10 +177,14 @@ public:
         m_trail.push_back(e);        
     }
 
+    void trace() {
+        trace_bounds(m_trace_id.c_str());
+    }
+
     lbool mus_solver() {
         init();
         init_local();
-        trace_bounds("maxres");
+        trace();
         while (m_lower < m_upper) {
             TRACE("opt", 
                   display_vec(tout, m_asms);
@@ -197,16 +210,15 @@ public:
                 break;
             }
         }
-        trace_bounds("maxres");
+        trace();
         return l_true;
     }
 
     lbool primal_dual_solver() {
         init();
         init_local();
-        set_soft_assumptions();
         lbool is_sat = l_true;
-        trace_bounds("maxres");
+        trace();
         exprs cs;
         while (m_lower < m_upper) {
             is_sat = check_sat_hill_climb(m_asms);
@@ -235,7 +247,7 @@ public:
                 break;
             }
         }
-        trace_bounds("maxres");
+        trace();
         return l_true;
     }
 
@@ -456,7 +468,7 @@ public:
         fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
         s().assert_expr(fml);
         m_lower += w;
-        trace_bounds("maxres");
+        trace();
     }
 
     bool get_mus_model(model_ref& mdl) {
@@ -652,7 +664,7 @@ public:
         }
         m_upper = upper;
         DEBUG_CODE(verify_assignment(););
-        trace_bounds("maxres");
+        trace();
 
         add_upper_bound_block();
     }

src/opt/maxsmt.cpp

@@ -101,10 +101,6 @@ namespace opt {
         m_c.enable_sls(force);
     }
 
-    void maxsmt_solver_base::set_soft_assumptions() {
-        m_c.set_soft_assumptions();
-    }
-
     app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
         app* result = m.mk_fresh_const(name, m.mk_bool_sort());
         m_c.fm().insert(result->get_decl());

src/opt/maxsmt.h

@@ -101,7 +101,6 @@ namespace opt {
 
     protected:
         void enable_sls(bool force);
-        void set_soft_assumptions();
         void trace_bounds(char const* solver);
 
     };

src/opt/opt_context.cpp

@@ -530,10 +530,6 @@ namespace opt {
         }
     }
 
-    void context::set_soft_assumptions() {
-        // TBD no-op
-    }
-
     void context::enable_sls(bool force) {
         if ((force || m_enable_sls) && m_sat_solver.get()) {
             m_params.set_bool("optimize_model", true);

src/opt/opt_context.h

@@ -51,7 +51,6 @@ namespace opt {
         virtual ast_manager& get_manager() = 0;      
         virtual params_ref& params() = 0;
         virtual void enable_sls(bool force) = 0;              // stochastic local search 
-        virtual void set_soft_assumptions() = 0;    // configure SAT solver to skip assumptions assigned by unit-propagation  
         virtual symbol const& maxsat_engine() const = 0; // retrieve maxsat engine configuration parameter.
         virtual void get_base_model(model_ref& _m) = 0;  // retrieve model from initial satisfiability call.
         virtual smt::context& smt_context() = 0;    // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
@@ -216,7 +215,6 @@ namespace opt {
         virtual ast_manager& get_manager() { return this->m; }
         virtual params_ref& params() { return m_params; }
         virtual void enable_sls(bool force);
-        virtual void set_soft_assumptions();
         virtual symbol const& maxsat_engine() const { return m_maxsat_engine; }
         virtual void get_base_model(model_ref& _m);
 

src/sat/sat_solver.cpp

@@ -925,6 +925,7 @@ namespace sat {
             else {
                 svector<literal> blocker;
                 if (!init_weighted_assumptions(num_lits, lits, weights, max_weight, blocker)) {
+                    ++m_stats.m_blocked_corr_sets;
                     pop_to_base_level();
                     mk_clause(blocker.size(), blocker.c_ptr());
                     goto retry_init_assumptions;
@@ -2811,6 +2812,7 @@ namespace sat {
         st.update("restarts", m_restart);
         st.update("minimized lits", m_minimized_lits);
         st.update("dyn subsumption resolution", m_dyn_sub_res);
+        st.update("blocked correction sets", m_blocked_corr_sets);
     }
 
     void stats::reset() {
@@ -2829,6 +2831,7 @@ namespace sat {
         m_minimized_lits = 0;
         m_dyn_sub_res = 0;
         m_non_learned_generation = 0;
+        m_blocked_corr_sets = 0;
     }
 
     void mk_stat::display(std::ostream & out) const {

src/sat/sat_solver.h

@@ -60,6 +60,7 @@ namespace sat {
         unsigned m_minimized_lits;
         unsigned m_dyn_sub_res;
         unsigned m_non_learned_generation;
+        unsigned m_blocked_corr_sets;
         stats() { reset(); }
         void reset();
         void collect_statistics(statistics & st) const;