adding incremental cubing from API

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

src/api/api_solver.cpp

@@ -495,6 +495,33 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);        
     }
 
+    Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s) {
+        Z3_TRY;
+        LOG_Z3_solver_cube(c, s);
+        ast_manager& m = mk_c(c)->m();
+        expr_ref result(m);
+        unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+        api::context::set_interruptable si(*(mk_c(c)), eh);
+        {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            try {
+                result = to_solver_ref(s)->cube();
+            }
+            catch (z3_exception & ex) {
+                mk_c(c)->handle_exception(ex);
+                return 0;
+            }
+        }
+        mk_c(c)->save_ast_trail(result);
+        RETURN_Z3(of_ast(result));
+        Z3_CATCH_RETURN(0);        
+    }
+
     Z3_ast Z3_API Z3_solver_lookahead(Z3_context c,
                                       Z3_solver s,
                                       Z3_ast_vector assumptions,

src/api/z3_api.h

@@ -6183,6 +6183,16 @@ extern "C" {
 
     Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector candidates);
 
+    /**
+       \brief extract a next cube for a solver. The last cube is the constant \c true or \c false.
+       The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled
+       using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.
+       
+       def_API('Z3_solver_cube', AST, (_in(CONTEXT), _in(SOLVER)))
+    */
+
+    Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s);
+
 
     /**
        \brief retrieve lemmas from solver state. Lemmas are auxiliary unit literals, 

src/muz/spacer/spacer_itp_solver.h

@@ -119,6 +119,8 @@ public:
     {NOT_IMPLEMENTED_YET();}
     virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); }
     virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); }
+    virtual expr_ref cube() { return expr_ref(m.mk_true(), m); }
+
 
     virtual void push();
     virtual void pop(unsigned n);

src/muz/spacer/spacer_virtual_solver.h

@@ -93,10 +93,10 @@ public:
     virtual smt_params &fparams();
     virtual void reset();
 
-    virtual void set_progress_callback(progress_callback *callback)
-    {UNREACHABLE();}
+    virtual void set_progress_callback(progress_callback *callback) {UNREACHABLE();}
     virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); }
     virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); }
+    virtual expr_ref cube() { return expr_ref(m.mk_true(), m); }
 
     virtual solver *translate(ast_manager &m, params_ref const &p);
 

src/opt/maxres.cpp

@@ -368,6 +368,7 @@ public:
                 m_lower = m_upper;
                 return l_true;
             }
+            split_core(core);
             cores.push_back(core);
             if (core.size() >= m_max_core_size) {
                 break;
@@ -493,7 +494,7 @@ public:
         expr_ref fml(m);
         remove_core(core);
         SASSERT(!core.empty());
-        rational w = split_core(core);
+        rational w = core_weight(core);
         TRACE("opt", display_vec(tout << "minimized core: ", core););
         IF_VERBOSE(10, display_vec(verbose_stream() << "core: ", core););
         max_resolve(core, w);
@@ -558,19 +559,24 @@ public:
         return m_asm2weight.find(e);
     }
 
-    rational split_core(exprs const& core) {
+    rational core_weight(exprs const& core) {
         if (core.empty()) return rational(0);
         // find the minimal weight:
         rational w = get_weight(core[0]);
         for (unsigned i = 1; i < core.size(); ++i) {
             w = std::min(w, get_weight(core[i]));
         }
+        return w;
+    }
+
+    rational split_core(exprs const& core) {
+        rational w = core_weight(core);
         // add fresh soft clauses for weights that are above w.
-        for (unsigned i = 0; i < core.size(); ++i) {
-            rational w2 = get_weight(core[i]);
+        for (expr* e : core) {
+            rational w2 = get_weight(e);
             if (w2 > w) {
                 rational w3 = w2 - w;
-                new_assumption(core[i], w3);
+                new_assumption(e, w3);
             }
         }        
         return w;

src/opt/opt_solver.h

@@ -109,6 +109,7 @@ namespace opt {
         virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
         virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
         virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { return expr_ref(m.mk_true(), m); }
+        virtual expr_ref cube() { return expr_ref(m.mk_true(), m); }
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/sat/sat_lookahead.cpp

@@ -2353,6 +2353,16 @@ namespace sat {
     }
 
     lbool lookahead::cube() {
+#if 0
+        literal_vector lits;
+        while (true) {
+            lbool result = cube(lits);
+            if (lits.empty() || result != l_undef) {
+                return result;
+            }
+            display_cube(std::cout, cube);
+        }
+#endif
         lbool result = l_false;
         init_search();
         m_model.reset();
@@ -2394,6 +2404,58 @@ namespace sat {
         }
     }
 
+    lbool lookahead::cube(literal_vector& lits) {
+        lits.reset();
+        bool is_first = (m_cube_state.m_lit == null_literal);
+        if (is_first) {
+            init_search();
+            m_model.reset();
+        }        
+        scoped_level _sl(*this, c_fixed_truth);
+        m_search_mode = lookahead_mode::searching;
+        unsigned depth = 0;
+        
+        if (!is_first) {
+            goto pick_up_work;
+        }
+
+        while (true) {
+            TRACE("sat", display(tout););
+            inc_istamp();
+            checkpoint();
+            m_cube_state.m_lit = choose();
+            if (inconsistent()) {
+                TRACE("sat", tout << "inconsistent: " << cube << "\n";);
+                m_cube_state.m_freevars_threshold = m_freevars.size();                
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result;
+                continue;
+            }
+            if (m_cube_state.m_lit == null_literal) {
+                return l_true;
+            }
+            depth = m_cube_state.m_cube.size();
+            if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
+                (m_config.m_cube_cutoff == 0 && m_freevars.size() < m_cube_state.m_freevars_threshold)) {
+                m_cube_state.m_freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
+                m_cube_state.m_result = l_undef;
+                set_conflict();
+                if (!backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision)) return m_cube_state.m_result;
+                lits.append(m_cube_state.m_cube);
+                return l_undef;
+            }
+        pick_up_work:
+            TRACE("sat", tout << "choose: " << m_cube_state.m_lit << " cube: " << m_cube_state.m_cube << "\n";);
+            ++m_stats.m_decisions;
+            push(m_cube_state.m_lit, c_fixed_truth);
+            m_cube_state.m_cube.push_back(m_cube_state.m_lit);
+            m_cube_state.m_is_decision.push_back(true);
+            SASSERT(inconsistent() || !is_unsat());
+        }
+        lbool result = m_cube_state.m_result;
+        m_cube_state.reset();
+        return result;
+    }
+
     void lookahead::init_model() {
         m_model.reset();
         for (unsigned i = 0; i < m_num_vars; ++i) {

src/sat/sat_lookahead.h

@@ -139,6 +139,22 @@ namespace sat {
         };
 #endif
 
+        struct cube_state {
+            svector<bool>  m_is_decision;
+            literal_vector m_cube;
+            literal        m_lit;
+            lbool          m_result;
+            double         m_freevars_threshold;
+            cube_state() { reset(); }
+            void reset() { 
+                m_is_decision.reset(); 
+                m_cube.reset(); 
+                m_lit = null_literal; 
+                m_result = l_false; 
+                m_freevars_threshold = 0; 
+            }
+        };
+
         config                 m_config;
         double                 m_delta_trigger; 
 
@@ -202,6 +218,7 @@ namespace sat {
         lookahead_mode         m_search_mode;   // mode of search
         stats                  m_stats;
         model                  m_model; 
+        cube_state             m_cube_state;
  
         // ---------------------------------------
         // truth values
@@ -537,6 +554,8 @@ namespace sat {
         */
         lbool cube();
 
+        lbool cube(literal_vector& lits);
+
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
         /**
            \brief simplify set of clauses by extracting units from a lookahead at base level.

src/sat/sat_solver.cpp

@@ -63,6 +63,7 @@ namespace sat {
         m_next_simplify           = 0;
         m_num_checkpoints         = 0;
         m_simplifications         = 0;
+        m_cuber                   = nullptr;
     }
 
     solver::~solver() {
@@ -836,6 +837,19 @@ namespace sat {
         return lh.select_lookahead(assumptions, vars);
     }
 
+    lbool  solver::cube(literal_vector& lits) {
+        if (!m_cuber) {
+            m_cuber = alloc(lookahead, *this);
+        }
+        lbool result = m_cuber->cube(lits);
+        if (result == l_false) {
+            dealloc(m_cuber);
+            m_cuber = nullptr;
+        }
+        return result;
+    }
+
+
     // -----------------------
     //
     // Search

src/sat/sat_solver.h

@@ -156,6 +156,8 @@ namespace sat {
         unsigned                m_par_num_vars;
         bool                    m_par_syncing_clauses;
 
+        class lookahead*        m_cuber;
+
         statistics              m_aux_stats;
 
         void del_clauses(clause * const * begin, clause * const * end);
@@ -362,6 +364,7 @@ namespace sat {
         char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
 
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
+        lbool  cube(literal_vector& lits);
 
     protected:
         unsigned m_conflicts_since_init;
@@ -404,7 +407,7 @@ namespace sat {
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);
         lbool lookahead_search();
-        lbool  lookahead_cube();
+        lbool lookahead_cube();
         lbool do_local_search(unsigned num_lits, literal const* lits);
         lbool do_ccc();
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -344,6 +344,25 @@ public:
         expr_ref result(lit2expr[l.index()].get(), m);
         return result;
     }
+    virtual expr_ref cube() {
+        sat::literal_vector lits;
+        lbool result = m_solver.cube(lits);
+        if (result == l_false || lits.empty()) {
+            return expr_ref(m.mk_false(), m);
+        }
+        if (result == l_true) {
+            return expr_ref(m.mk_true(), m);
+        }
+        expr_ref_vector fmls(m);
+        expr_ref_vector lit2expr(m);
+        lit2expr.resize(m_solver.num_vars() * 2);
+        m_map.mk_inv(lit2expr);
+        for (sat::literal l : lits) {
+            fmls.push_back(lit2expr[l.index()].get());
+        }
+        return mk_and(fmls);
+    }
+
     virtual void get_lemmas(expr_ref_vector & lemmas) { 
         if (!m_internalized) return;
         sat2goal s2g;

src/smt/smt_solver.cpp

@@ -229,6 +229,11 @@ namespace smt {
             return expr_ref(m.mk_true(), m);
         }
 
+        virtual expr_ref cube() {
+            ast_manager& m = get_manager();
+            return expr_ref(m.mk_true(), m);
+        }
+
         struct collect_fds_proc {
             ast_manager & m;
             func_decl_set & m_fds;

src/solver/combined_solver.cpp

@@ -284,6 +284,10 @@ public:
         return m_solver1->lookahead(assumptions, candidates); 
     }
 
+    virtual expr_ref cube() {
+        return m_solver1->cube();
+    }
+
     virtual expr * get_assumption(unsigned idx) const {
         unsigned c1 = m_solver1->get_num_assumptions();
         if (idx < c1) return m_solver1->get_assumption(idx);

src/solver/solver.h

@@ -184,6 +184,12 @@ public:
 
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) = 0;
 
+    /**
+       \brief extract a lookahead candidates for branching.
+    */
+
+    virtual expr_ref cube() = 0;
+
     /**
        \brief extract learned lemmas.
     */

src/solver/tactic2solver.cpp

@@ -79,9 +79,13 @@ public:
 
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) {
         ast_manager& m = get_manager();
-        std::cout << "tactic2solver\n";
         return expr_ref(m.mk_true(), m);
     }
+    virtual expr_ref cube() {
+        ast_manager& m = get_manager();
+        return expr_ref(m.mk_true(), m);
+    }
+
 };
 
 ast_manager& tactic2solver::get_manager() const { return m_assertions.get_manager(); }

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -163,6 +163,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); }
+    virtual expr_ref cube() { return m_solver->cube(); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

src/tactic/portfolio/enum2bv_solver.cpp

@@ -109,6 +109,7 @@ public:
     virtual ast_manager& get_manager() const { return m;  }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { return m_solver->lookahead(assumptions, candidates); }
+    virtual expr_ref cube() { return m_solver->cube(); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { m_solver->get_lemmas(lemmas); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {

src/tactic/portfolio/pb2bv_solver.cpp

@@ -99,6 +99,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); }
+    virtual expr_ref cube() { return m_solver->cube(); }
     virtual void get_lemmas(expr_ref_vector & lemmas) { flush_assertions(); m_solver->get_lemmas(lemmas); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {