refactor weighted maxsmt

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

src/opt/weighted_maxsat.cpp

@@ -722,12 +722,20 @@ namespace opt {
             lbool is_sat = s().check_sat(0, 0);
             if (is_sat == l_true) {
                 s().get_model(m_model);
+                params_ref p;
+                p.set_uint("restarts", 20);
+                m_bvsls.updt_params(p);
                 bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective, m_model, true);
                 switch (res.is_sat) {
                 case l_true: {
                     unsigned bv_size = 0;
                     m_bvsls.get_model(m_model);
                     VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size));
+                    for (unsigned i = 0; i < m_soft.size(); ++i) {
+                        expr_ref tmp(m);
+                        m_model->eval(m_soft[i].get(), tmp, true);
+                        m_assignment[i] = m.is_true(tmp);
+                    }
                     break;
                 }
                 case l_false:

src/tactic/sls/bvsls_opt_engine.cpp

@@ -16,6 +16,7 @@ Author:
 Notes:
 
 --*/
+#include "sls_compilation_settings.h"
 #include "nnf.h"
 #include "bvsls_opt_engine.h"
 
@@ -42,6 +43,7 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
                             mk_ismt2_pp(objective, m()) << std::endl;);
     m_hard_tracker.initialize(m_assertions);
     m_restart_limit = _RESTART_LIMIT_;
+    setup_opt_tracker(objective, _maximize);
 
     if (initial_model.get() != 0) {
         TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
@@ -54,57 +56,85 @@ bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
     }    
    
     optimization_result res(m_manager);
+    lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;    
 
-    res.is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
+    for (m_stats.m_restarts = 0;
+         m_stats.m_restarts < m_max_restarts;
+         m_stats.m_restarts++)
+    {
+        mpz old_best;
+        m_mpz_manager.set(old_best, m_best_model_score);
 
-    if (!res.is_sat) {
+        if (!is_sat) {
             do {
                 checkpoint();
 
                 IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
-            res.is_sat = search();
+                is_sat = search();
 
-            if (res.is_sat == l_undef)
+                if (is_sat == l_undef)
                     m_hard_tracker.randomize(m_assertions);
-        } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ &&
+            } 
-                 res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts);
+            while (is_sat != l_true && 
+                   m_stats.m_restarts++ < m_max_restarts);
         }
 
-    if (res.is_sat)
+        if (is_sat == l_true) {
-        res.optimum = _maximize ? maximize(objective) : minimize(objective);
+            IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
+            res.is_sat = l_true;
+            m_obj_tracker.set_model(m_hard_tracker.get_model());
+            m_obj_evaluator.update_all();
+            expr_ref local_best = maximize();
+            if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) ||
+                (!_maximize && m_mpz_manager.lt(m_best_model_score, old_best))) 
+            {
+                res.optimum = local_best;
+            }
+        }
+        
+        m_hard_tracker.randomize(m_assertions);
+        m_evaluator.update_all();
+        is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
+    }    
 
     TRACE("sls_opt", tout << "sat: " << res.is_sat << "; optimum: " << mk_ismt2_pp(res.optimum, m()) << std::endl;);
 
     return res;
 }
 
-expr_ref bvsls_opt_engine::maximize(expr_ref const & objective)
+void bvsls_opt_engine::setup_opt_tracker(expr_ref const & objective, bool _max) 
+{
+    expr_ref obj(m_manager);
+    obj = objective;
+    if (!_max)
+        obj = m_bv_util.mk_bv_neg(objective);
+
+    m_obj_e = obj.get();
+    m_obj_bv_sz = m_bv_util.get_bv_size(m_obj_e);
+    ptr_vector<expr> objs;
+    objs.push_back(m_obj_e);
+    m_obj_tracker.initialize(objs);    
+}
+
+expr_ref bvsls_opt_engine::maximize()
 {
     SASSERT(m_hard_tracker.is_sat());
 
-    expr * obj_e = objective.get();
-    unsigned obj_bv_sz = m_bv_util.get_bv_size(obj_e);        
-    ptr_vector<expr> objs;
-    objs.push_back(obj_e);
-    m_obj_tracker.initialize(objs);
-    m_obj_tracker.set_model(m_hard_tracker.get_model());
-    m_obj_evaluator.update_all();
-
     TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout););    
-    IF_VERBOSE(1, verbose_stream() << "Maximizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);    
 
     mpz score, old_score, max_score, new_value;
     unsigned new_const = (unsigned)-1, new_bit = 0;
     ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
     move_type move;
     m_mpz_manager.set(score, top_score());
-    m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score);
+    m_mpz_manager.set(max_score, m_powers(m_obj_bv_sz)); m_mpz_manager.dec(max_score);
+
+    IF_VERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;);
 
     save_model(score);
 
-    while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) &&
+    while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves))
-           m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ &&
+    {
-           m_mpz_manager.lt(score, max_score)) {
         checkpoint();
         m_stats.m_moves++;
         m_mpz_manager.set(old_score, score);
@@ -112,7 +142,7 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective)
         
         mpz score(0);
         m_mpz_manager.set(score,
-                          find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, obj_e));        
+                          find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, m_obj_e));
 
         if (new_const == static_cast<unsigned>(-1)) {
             m_mpz_manager.set(score, old_score);
@@ -121,12 +151,15 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective)
             if (!randomize_wrt_hard()) {
                 // Can't improve and can't randomize; can't do anything other than bail out.
                 TRACE("sls_opt", tout << "Got stuck; bailing out." << std::endl;);
+                IF_VERBOSE(10, verbose_stream() << "No local improvements possible." << std::endl;);
                 goto bailout;
             }            
             m_mpz_manager.set(score, top_score());
         }
         else {
-            TRACE("sls_opt", tout << "New best: " << m_mpz_manager.to_string(score) << std::endl;);
+            m_stats.m_moves++;
+            TRACE("sls_opt", tout << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
+            IF_VERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
             func_decl * fd = consts[new_const];
             incremental_score(fd, new_value);
             m_obj_evaluator.update(fd, new_value);
@@ -138,17 +171,10 @@ bailout:
     m_mpz_manager.del(new_value);
     
     expr_ref res(m_manager);
-    res = m_bv_util.mk_numeral(m_best_model_score, obj_bv_sz);
+    res = m_bv_util.mk_numeral(m_best_model_score, m_obj_bv_sz);
     return res;
 }
 
-expr_ref bvsls_opt_engine::minimize(expr_ref const & objective)
-{
-    expr_ref n_obj(m_manager);
-    n_obj = m_bv_util.mk_bv_neg(objective);
-    return maximize(n_obj);
-}
-
 void bvsls_opt_engine::save_model(mpz const & score) {
     model_ref mdl = m_hard_tracker.get_model();
     model_ref obj_mdl = m_obj_tracker.get_model();

src/tactic/sls/bvsls_opt_engine.h

@@ -27,6 +27,8 @@ class bvsls_opt_engine : public sls_engine {
     sls_evaluator   m_obj_evaluator;
     model_ref       m_best_model;
     mpz             m_best_model_score;
+    unsigned        m_obj_bv_sz;
+    expr          * m_obj_e;
 
 public:
     bvsls_opt_engine(ast_manager & m, params_ref const & p);
@@ -44,8 +46,8 @@ public:
     void get_model(model_ref & result) { result = m_best_model; }
 
 protected:
-    expr_ref maximize(expr_ref const & objective);
+    void setup_opt_tracker(expr_ref const & objective, bool _max);
-    expr_ref minimize(expr_ref const & objective);
+    expr_ref maximize();    
 
     bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
                  mpz & best_score, unsigned & best_const, mpz & best_value);

src/tactic/sls/sls_compilation_settings.h

@@ -38,7 +38,7 @@ Notes:
 
 // do we use restarts?
 // 0 = no, 1 = use #moves, 2 = use #plateaus, 3 = use time
-#define _RESTARTS_ 3
+#define _RESTARTS_ 1
 // limit of moves/plateaus/seconds until first restart occurs
 #define _RESTART_LIMIT_ 10
 // 0 = initialize with all zero, 1 initialize with random value