bvsls integration with opt::wmaxsmt

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/opt/weighted_maxsat.cpp

@@ -306,13 +306,13 @@ namespace opt {
             expr_dependency_ref core(m);
             goal_ref_buffer result;
             model_converter_ref model_converter;
-            (*simplify)(g, result, model_converter, pc, core); 
+            (*simplify)(g, result, model_converter, pc, core);
             SASSERT(result.size() == 1);
             goal* r = result[0];
             for (unsigned i = 0; i < r->size(); ++i) {
                 m_bvsls.assert_expr(r->form(i));
-            }        
-            
+            }
+
             m_lower = m_upper = rational::zero();
 
             for (unsigned i = 0; i < m_soft.size(); ++i) {
@@ -336,20 +336,28 @@ namespace opt {
                     objective = bv.mk_bv_add(objective, es[i].get());
                 }
             }
-            // TBD: can we set an initial model on m_bvsls?
-            bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective);
-            switch(res.is_sat) {
-            case l_true: {
-                unsigned bv_size = 0;
-                // TBD: m_bvsls.get_model(m_model);
-                VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size));
-                break;
+            lbool is_sat = s.check_sat_core(0, 0);
+            if (is_sat == l_true) {
+                updt_model(s);
+                // TBD: can we set an initial model on m_bvsls?
+                // CMW: Yes, see next line.
+                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));
+                    break;
+                }
+                case l_false:
+                case l_undef:
+                    break;
+                }
+                return res.is_sat;
             }
-            case l_false:
-            case l_undef:
-                break;
-            }
-            return res.is_sat;
+            else
+                return is_sat;
+
         }
 
         /**

src/tactic/sls/bvsls_opt_engine.cpp

@@ -16,54 +16,316 @@ Author:
 Notes:
 
 --*/
+#include "nnf.h"
 #include "bvsls_opt_engine.h"
 
 bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
-    sls_engine(m, p)
+    sls_engine(m, p),
+    m_hard_tracker(sls_engine::m_tracker),
+    m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers),
+    m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers)
 {
+    m_best_model = alloc(model, m);
 }
 
 bvsls_opt_engine::~bvsls_opt_engine()
 {    
 }
 
-bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(expr_ref const & objective)
+bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
+    expr_ref const & objective, 
+    model_ref initial_model, 
+    bool _maximize)
 {
     SASSERT(m_bv_util.is_bv(objective));
-    m_tracker.initialize(m_assertions);
-    m_restart_limit = _RESTART_LIMIT_;
+    TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
+                            mk_ismt2_pp(objective, m()) << std::endl;);
+    m_hard_tracker.initialize(m_assertions);
+    m_restart_limit = _RESTART_LIMIT_;    
+
+    if (initial_model.get() != 0) {
+        TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
+                        for (unsigned i = 0; i < initial_model->get_num_constants(); i++) {
+                            func_decl * fd = initial_model->get_constant(i);
+                            expr * val = initial_model->get_const_interp(fd);
+                            tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
+                        });
+        m_hard_tracker.set_model(initial_model);
+    }
 
     optimization_result res(m_manager);
 
-    do {
-        checkpoint();
+    res.is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
 
-        IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl; );
-        res.is_sat = search();
+    if (!res.is_sat) {
+        do {
+            checkpoint();
 
-        if (res.is_sat == l_undef)
-        {
-#if _RESTART_INIT_
-            m_tracker.randomize();
-#else
-            m_tracker.reset(m_assertions);
-#endif
-        }
-    } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ &&
-             res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts);    
+            IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
+            res.is_sat = search();
+
+            if (res.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);
+    }    
 
     if (res.is_sat)
-        res.optimum = maximize(objective);
+        res.optimum = _maximize ? maximize(objective) : minimize(objective);
+
+    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)
 {
+    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_evaluator.update_all();
+    m_obj_tracker.set_model(m_hard_tracker.get_model());
+
+    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, m_obj_tracker.get_value(obj_e));
+    m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score);
+
+    save_model(score);    
+
+    while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) &&
+           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);
+        new_const = (unsigned)-1;
+        
+        mpz score(0);
+        m_mpz_manager.set(score,
+                          find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, obj_e));        
+
+        if (new_const == static_cast<unsigned>(-1)) {
+            m_mpz_manager.set(score, old_score);
+            if (m_mpz_manager.gt(score, m_best_model_score))
+                save_model(score);            
+            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;);
+                goto bailout;
+            }
+            m_mpz_manager.set(score, top_score());            
+        }
+        else {
+            TRACE("sls_opt", tout << "New best: " << m_mpz_manager.to_string(score) << std::endl;);
+            func_decl * fd = consts[new_const];
+            incremental_score(fd, new_value);
+            m_mpz_manager.set(score, top_score());
+        }
+    }
+
+bailout:
+    m_mpz_manager.del(new_value);
+    
     expr_ref res(m_manager);
-    res = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(objective));
-
-    // TODO.
-
+    res = m_bv_util.mk_numeral(m_best_model_score, 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();
+
+    for (unsigned i = 0; i < obj_mdl->get_num_constants(); i++) {
+        func_decl * fd = obj_mdl->get_constant(i);
+        expr * val = obj_mdl->get_const_interp(fd);
+        if (mdl->has_interpretation(fd)) {
+            if (mdl->get_const_interp(fd) != val)
+                TRACE("sls_opt", tout << "model disagreement on " << fd->get_name() << ": " <<
+                mk_ismt2_pp(val, m()) << " != " << mk_ismt2_pp(mdl->get_const_interp(fd), m()) << std::endl;);
+            SASSERT(mdl->get_const_interp(fd) == val);
+        }
+        else
+            mdl->register_decl(fd, val);
+    }
+
+    m_best_model = mdl;
+    m_mpz_manager.set(m_best_model_score, score);
+}
+
+// checks whether the score outcome of a given move is better than the previous score
+bool bvsls_opt_engine::what_if(
+    func_decl * fd,
+    const unsigned & fd_inx,
+    const mpz & temp,
+    mpz & best_score,
+    unsigned & best_const,
+    mpz & best_value) 
+{
+#if _EARLY_PRUNE_
+    double r = incremental_score_prune(fd, temp);
+#else
+    double r = incremental_score(fd, temp);
+#endif
+    
+    if (r >= 1.0 && m_tracker.is_sat()) {
+        m_obj_evaluator.update(fd, temp);
+        mpz cur_best(0);
+        m_mpz_manager.set(cur_best, top_score());
+
+        TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
+              " --> " << r << "; score=" << m_mpz_manager.to_string(cur_best) << std::endl;);
+
+        if (m_mpz_manager.gt(cur_best, best_score)) {
+            m_mpz_manager.set(best_score, cur_best);
+            best_const = fd_inx;
+            m_mpz_manager.set(best_value, temp);
+            return true;
+        }
+    }
+
+    return false;
+}
+
+mpz bvsls_opt_engine::find_best_move(
+    ptr_vector<func_decl> & to_evaluate,
+    mpz score,
+    unsigned & best_const,
+    mpz & best_value,
+    unsigned & new_bit,
+    move_type & move,
+    mpz const & max_score,
+    expr * objective)
+{
+    mpz old_value, temp;
+#if _USE_MUL3_ || _USE_UNARY_MINUS_
+    mpz temp2;
+#endif
+    unsigned bv_sz;
+    mpz new_score = score;
+
+    for (unsigned i = 0; i < to_evaluate.size() && m_mpz_manager.lt(new_score, max_score); i++) {
+        func_decl * fd = to_evaluate[i];
+        sort * srt = fd->get_range();
+        bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
+        m_mpz_manager.set(old_value, m_tracker.get_value(fd));
+
+        // first try to flip every bit
+        for (unsigned j = 0; j < bv_sz && m_mpz_manager.lt(new_score, max_score); j++) {
+            // What would happen if we flipped bit #i ?                
+            mk_flip(srt, old_value, j, temp);
+
+            if (what_if(fd, i, temp, new_score, best_const, best_value)) {
+                new_bit = j;
+                move = MV_FLIP;
+            }
+        }
+
+        if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
+#if _USE_ADDSUB_
+            if (!m_mpz_manager.is_even(old_value)) {
+                // for odd values, try +1
+                mk_inc(bv_sz, old_value, temp);
+                if (what_if(fd, i, temp, new_score, best_const, best_value))
+                    move = MV_INC;
+            }
+            else {
+                // for even values, try -1
+                mk_dec(bv_sz, old_value, temp);
+                if (what_if(fd, i, temp, new_score, best_const, best_value))
+                    move = MV_DEC;
+            }
+#endif
+            // try inverting
+            mk_inv(bv_sz, old_value, temp);
+            if (what_if(fd, i, temp, new_score, best_const, best_value))
+                move = MV_INV;
+
+#if _USE_UNARY_MINUS_
+            mk_inc(bv_sz, temp, temp2);
+            if (what_if(fd, i, temp2, new_score, best_const, best_value))
+                move = MV_UMIN;
+#endif
+
+#if _USE_MUL2DIV2_
+            // try multiplication by 2
+            mk_mul2(bv_sz, old_value, temp);
+            if (what_if(fd, i, temp, new_score, best_const, best_value))
+                move = MV_MUL2;
+
+#if _USE_MUL3_
+            // try multiplication by 3
+            mk_add(bv_sz, old_value, temp, temp2);
+            if (what_if(fd, i, temp2, new_score, best_const, best_value))
+                move = MV_MUL3;
+#endif
+
+            // try division by 2
+            mk_div2(bv_sz, old_value, temp);
+            if (what_if(fd, i, temp, new_score, best_const, best_value))
+                move = MV_DIV2;
+#endif
+        }
+
+        // reset to what it was before
+        double check = incremental_score(fd, old_value);
+    }
+
+    m_mpz_manager.del(old_value);
+    m_mpz_manager.del(temp);
+#if _USE_MUL3_
+    m_mpz_manager.del(temp2);
+#endif
+
+    return new_score;    
+}
+
+bool bvsls_opt_engine::randomize_wrt_hard() {
+    ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
+    unsigned csz = consts.size();
+    unsigned retry_count = csz;
+
+    while (retry_count-- > 0)  
+    {
+        
+        unsigned ri = (m_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz;
+        func_decl * random_fd = consts[ri]; // Random constant
+        
+        mpz random_val; // random value.
+        m_mpz_manager.set(random_val, m_tracker.get_random(random_fd->get_range()));        
+        
+        mpz old_value;
+        m_mpz_manager.set(old_value, m_tracker.get_value(random_fd));
+        
+        if (!m_mpz_manager.eq(random_val, old_value)) {
+            m_evaluator.update(random_fd, random_val);
+
+            if (m_hard_tracker.is_sat()) {
+                TRACE("sls_opt", tout << "Randomizing " << random_fd->get_name() << " to " <<
+                                         m_mpz_manager.to_string(random_val) << std::endl;);
+                m_obj_evaluator.update(random_fd, random_val);
+                return true;
+            }
+            else
+                m_evaluator.update(random_fd, old_value);
+        }
+    }
+
+    return false;
 }

src/tactic/sls/bvsls_opt_engine.h

@@ -22,6 +22,12 @@ Notes:
 #include "sls_engine.h"
 
 class bvsls_opt_engine : public sls_engine {
+    sls_tracker   & m_hard_tracker;
+    sls_tracker     m_obj_tracker;
+    sls_evaluator   m_obj_evaluator;
+    model_ref       m_best_model;
+    mpz             m_best_model_score;
+    
 public:
     bvsls_opt_engine(ast_manager & m, params_ref const & p);
     ~bvsls_opt_engine();
@@ -33,10 +39,33 @@ public:
         optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {}
     };
 
-    optimization_result optimize(expr_ref const & objective);
+    optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true);
+
+    void get_model(model_ref & result) { result = m_best_model; }
 
 protected:
     expr_ref maximize(expr_ref const & objective);
+    expr_ref minimize(expr_ref const & objective);
+
+    bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, 
+                 mpz & best_score, unsigned & best_const, mpz & best_value);
+
+    mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz score,
+                       unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
+                       mpz const & max_score, expr * objective);
+
+    mpz top_score(void) {
+        mpz res(0);
+        obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
+        for (obj_hashtable<expr>::iterator it = top_exprs.begin();
+             it != top_exprs.end();
+             it++)
+             m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res);
+        return res;
+    }
+
+    void save_model(mpz const & score);
+    bool randomize_wrt_hard();
 };
 
 #endif

src/tactic/sls/sls_evaluator.h

@@ -138,6 +138,14 @@ public:
                 }
                 break;
             }
+            case OP_ITE: {
+                SASSERT(n_args = 3);
+                if (m_mpz_manager.is_one(m_tracker.get_value(args[0])))
+                    m_mpz_manager.set(result, m_tracker.get_value(args[1]));
+                else
+                    m_mpz_manager.set(result, m_tracker.get_value(args[2]));
+                break;
+            }
             default:
                 NOT_IMPLEMENTED_YET();
             }

src/tactic/sls/sls_tracker.h

@@ -133,6 +133,19 @@ public:
     }
 #endif
 
+    inline obj_hashtable<expr> const & get_top_exprs() {
+        return m_top_expr;
+    }
+
+    inline bool is_sat() {
+        for (obj_hashtable<expr>::iterator it = m_top_expr.begin();
+             it != m_top_expr.end();
+             it++)
+            if (!m_mpz_manager.is_one(get_value(*it)))
+                return false;
+        return true;
+    }
+
     inline void set_value(expr * n, const mpz & r) {
         SASSERT(m_scores.contains(n));
         m_mpz_manager.set(m_scores.find(n).value, r);
@@ -522,6 +535,28 @@ public:
         }
     }
 
+    void set_model(model_ref const & mdl) {
+        for (unsigned i = 0; i < mdl->get_num_constants(); i++) {
+            func_decl * fd = mdl->get_constant(i);
+            expr * val = mdl->get_const_interp(fd);
+            if (m_entry_points.contains(fd)) {
+                if (m_manager.is_bool(val)) {
+                    set_value(fd, m_manager.is_true(val) ? m_mpz_manager.mk_z(1) : m_mpz_manager.mk_z(0));
+                }
+                else if (m_bv_util.is_numeral(val)) {
+                    rational r_val;
+                    unsigned bv_sz;
+                    m_bv_util.is_numeral(val, r_val, bv_sz);
+                    mpq q = r_val.to_mpq();
+                    SASSERT(m_mpz_manager.is_one(q.denominator()));
+                    set_value(fd, q.numerator());
+                }
+                else
+                    NOT_IMPLEMENTED_YET();
+            }
+        }
+    }
+
     model_ref get_model() {
         model_ref res = alloc(model, m_manager);
         unsigned sz = get_num_constants();
@@ -674,6 +709,9 @@ public:
                     m_scores.find(n).has_pos_occ = 1;
             }
         }
+        else if (m_bv_util.is_bv(n)) {
+            /* CMW: I need this for optimization. Safe to ignore? */
+        }
         else
             NOT_IMPLEMENTED_YET();
     }