fix uninitialized variable m_gc_burst in config, have cuber accept and receive optional vector of variables indicating splits and global autarky as output

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

examples/c++/example.cpp

@@ -707,7 +707,7 @@ void tactic_example7() {
     std::cout << s.check() << "\n";
     model m = s.get_model();
     std::cout << "model for subgoal:\n" << m << "\n";
-    std::cout << "model for original goal:\n" << r.convert_model(m) << "\n";
+    std::cout << "model for original goal:\n" << subgoal.convert_model(m) << "\n";
 }
 
 void tactic_example8() {

src/api/api_solver.cpp

@@ -553,11 +553,19 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);        
     }
 
-    Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned cutoff) {
+    Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vs, unsigned cutoff) {
         Z3_TRY;
-        LOG_Z3_solver_cube(c, s, cutoff);
+        LOG_Z3_solver_cube(c, s, vs, cutoff);
         ast_manager& m = mk_c(c)->m();
         expr_ref_vector result(m), vars(m);
+        for (ast* a : to_ast_vector_ref(vs)) {
+            if (!is_expr(a)) {
+                SET_ERROR_CODE(Z3_INVALID_USAGE);
+            }
+            else {
+                vars.push_back(to_expr(a));
+            }
+        }
         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);
@@ -580,7 +588,10 @@ extern "C" {
         for (expr* e : result) {
             v->m_ast_vector.push_back(e);
         }
-        // TBD: save return variables from vars into variable ast-vector.
+        to_ast_vector_ref(vs).reset();
+        for (expr* a : vars) {
+            to_ast_vector_ref(vs).push_back(a);
+        }
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);        
     }

src/api/c++/z3++.h

@@ -1999,18 +1999,23 @@ namespace z3 {
         param_descrs get_param_descrs() { return param_descrs(ctx(), Z3_solver_get_param_descrs(ctx(), m_solver)); }
 
 
-        expr_vector cube(unsigned cutoff) { Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, cutoff); check_error(); return expr_vector(ctx(), r); }  
+        expr_vector cube(expr_vector& vars, unsigned cutoff) { 
+            Z3_ast_vector r = Z3_solver_cube(ctx(), m_solver, vars, cutoff); 
+            check_error(); 
+            return expr_vector(ctx(), r); 
+        }  
 
         class cube_iterator {
-            solver&     m_solver;
+            solver&      m_solver;
-            unsigned&   m_cutoff;
+            unsigned&    m_cutoff;
-            expr_vector m_cube;
+            expr_vector& m_vars;
-            bool        m_end;
+            expr_vector  m_cube;
-            bool        m_empty;
+            bool         m_end;
+            bool         m_empty;
 
             void inc() {
                 assert(!m_end && !m_empty);
-                m_cube = m_solver.cube(m_cutoff);
+                m_cube = m_solver.cube(m_vars, m_cutoff);
                 m_cutoff = 0xFFFFFFFF;
                 if (m_cube.size() == 1 && m_cube[0].is_false()) {
                     m_cube = z3::expr_vector(m_solver.ctx());
@@ -2021,9 +2026,10 @@ namespace z3 {
                 }
             }
         public:
-            cube_iterator(solver& s, unsigned& cutoff, bool end):
+            cube_iterator(solver& s, expr_vector& vars, unsigned& cutoff, bool end):
                 m_solver(s),
                 m_cutoff(cutoff),
+                m_vars(vars),
                 m_cube(s.ctx()),
                 m_end(end),
                 m_empty(false) {
@@ -2056,20 +2062,32 @@ namespace z3 {
         };
 
         class cube_generator {
-            solver& m_solver;
+            solver&      m_solver;
-            unsigned m_cutoff;
+            unsigned     m_cutoff;
+            expr_vector  m_default_vars;
+            expr_vector& m_vars;
         public:
             cube_generator(solver& s):
                 m_solver(s),
-                m_cutoff(0xFFFFFFFF)
+                m_cutoff(0xFFFFFFFF),
+                m_default_vars(s.ctx()),
+                m_vars(m_default_vars)
             {}
 
-            cube_iterator begin() { return cube_iterator(m_solver, m_cutoff, false); }
+            cube_generator(solver& s, expr_vector& vars):
-            cube_iterator end() { return cube_iterator(m_solver, m_cutoff, true); }
+                m_solver(s),
+                m_cutoff(0xFFFFFFFF),
+                m_default_vars(s.ctx()),
+                m_vars(vars)
+            {}
+
+            cube_iterator begin() { return cube_iterator(m_solver, m_vars, m_cutoff, false); }
+            cube_iterator end() { return cube_iterator(m_solver, m_vars, m_cutoff, true); }
             void set_cutoff(unsigned c) { m_cutoff = c; }
         };
 
         cube_generator cubes() { return cube_generator(*this); }
+        cube_generator cubes(expr_vector& vars) { return cube_generator(*this, vars); }
 
     };
     inline std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }

src/api/dotnet/Solver.cs

@@ -404,6 +404,11 @@ namespace Microsoft.Z3
 	/// Backtrack level that can be adjusted by conquer process
 	/// </summary>
         public uint BacktrackLevel { get; set; }
+
+	/// <summary>
+	/// Variables available and returned by the cuber.
+	/// </summary>
+	public BoolExpr[] CubeVariables { get; set; }
         
 
 	/// <summary>
@@ -411,16 +416,21 @@ namespace Microsoft.Z3
 	/// </summary>
 	public IEnumerable<BoolExpr[]> Cube()
 	{
+             ASTVector cv = new ASTVector(Context);
+             if (CubeVariables != null) 
+                foreach (var b in CubeVariables) cv.Push(b);
+
 	     while (true) {
                 var lvl = BacktrackLevel;
                 BacktrackLevel = uint.MaxValue;
-                ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
+                ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
                 var v = r.ToBoolExprArray();
+                CubeVariables = cv.ToBoolExprArray();
                 if (v.Length == 1 && v[0].IsFalse) {
                    break;
                 }
                 yield return v; 
- 	            if (v.Length == 0) {
+                if (v.Length == 0) {
                    break;
                 }
 	     }

src/api/python/z3/z3.py

@@ -6313,18 +6313,25 @@ class Solver(Z3PPObject):
         consequences = [ consequences[i] for i in range(sz) ]
         return CheckSatResult(r), consequences
     
-    def cube(self):
+    def cube(self, vars = None):
         """Get set of cubes"""
+        self.cube_vs = AstVector(None, self.ctx)
+        if vars is not None:
+           for v in vars:
+               self.cube_vs.push(v)
         while True:
             lvl = self.backtrack_level
             self.backtrack_level = 4000000000
-            r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx)            
+            r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)            
             if (len(r) == 1 and is_false(r[0])):
-                return
+                return            
-            yield r            
+            yield r         
             if (len(r) == 0):                
                 return
 
+    def cube_vars(self):
+        return self.cube_vs
+
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""
         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)

src/api/z3_api.h

@@ -6230,13 +6230,20 @@ extern "C" {
        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.
        
+       The third argument is a vector of variables that may be used for cubing.
+       The contents of the vector is only used in the first call. The initial list of variables
+       is used in subsequent calls until it returns the unsatisfiable cube. 
+       The vector is modified to contain a set of Autarky variables that occor in clauses that
+       are affected by the (last literal in the) cube. These variables could be used by a different
+       cuber (on a different solver object) for further recursive cubing. 
+
        The last argument is a backtracking level. It instructs the cube process to backtrack below
        the indicated level for the next cube.
        
-       def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(UINT)))
+       def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT)))
     */
 
-    Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned backtrack_level);
+    Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level);
 
     /**
        \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions

src/sat/sat_asymm_branch.cpp

@@ -72,7 +72,7 @@ namespace sat {
             unsigned elim = m_elim_literals;
             if (big) big->init_big(s, true);
             process(big, s.m_clauses);
-            process(big, s.m_learned);
+            if (big) process(big, s.m_learned);
             s.propagate(false); 
             if (s.m_inconsistent)
                 break;

src/sat/sat_config.cpp

@@ -136,6 +136,7 @@ namespace sat {
         m_gc_increment    = p.gc_increment();
         m_gc_small_lbd    = p.gc_small_lbd();
         m_gc_k            = std::min(255u, p.gc_k());
+        m_gc_burst        = p.gc_burst();
 
         m_minimize_lemmas = p.minimize_lemmas();
         m_core_minimize   = p.core_minimize();

src/sat/sat_elim_eqs.cpp

@@ -182,8 +182,8 @@ namespace sat {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());            
-            if (m_solver.is_external(v)) {
+            bool root_ok = !m_solver.is_external(v) || m_solver.set_root(l, r);
-                m_solver.set_root(l, r);
+            if (m_solver.is_external(v) && (m_solver.is_incremental() || !root_ok)) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 m_solver.mk_bin_clause(~l, r, false);
                 m_solver.mk_bin_clause(l, ~r, false);

src/sat/sat_lookahead.cpp

@@ -338,7 +338,7 @@ namespace sat {
         } 
         TRACE("sat", display_candidates(tout << "sum: " << sum << "\n"););
         if (skip_candidates > 0) {
-            IF_VERBOSE(0, verbose_stream() << "candidates: " << m_candidates.size() << " skip: " << skip_candidates << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :candidates " << m_candidates.size() << " :skipped " << skip_candidates << ")\n";);
         }
         return sum;
     }
@@ -2049,15 +2049,15 @@ namespace sat {
         return h;
     }
 
-    lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
+    lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
         scoped_ext _scoped_ext(*this);
         lits.reset();
-        m_select_lookahead_vars.reset();
-        for (auto v : vars) {
-            m_select_lookahead_vars.insert(v);
-        }
         bool is_first = m_cube_state.m_first;
         if (is_first) {
+            m_select_lookahead_vars.reset();
+            for (auto v : vars) {
+                m_select_lookahead_vars.insert(v);
+            }
             init_search();
             m_model.reset();
             m_cube_state.m_first = false;
@@ -2109,6 +2109,8 @@ namespace sat {
 #else
                 lits.append(m_cube_state.m_cube);
 #endif
+                vars.reset();
+                for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
                 backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision);
                 return l_undef;
             }
@@ -2124,6 +2126,8 @@ namespace sat {
                 continue;
             }
             if (lit == null_literal) {
+                vars.reset();
+                for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v);
                 return l_true;
             }
             TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";);
@@ -2246,40 +2250,6 @@ namespace sat {
         return l;
     }
 
-
-    literal lookahead::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
-        IF_VERBOSE(1, verbose_stream() << "(sat-select " << vars.size() << ")\n";);
-        scoped_ext _sext(*this);
-        m_search_mode = lookahead_mode::searching;
-        scoped_level _sl(*this, c_fixed_truth);
-        init();                
-        if (inconsistent()) return null_literal;
-        inc_istamp();        
-        for (auto v : vars) {
-            m_select_lookahead_vars.insert(v);
-        }
-        
-        scoped_assumptions _sa(*this, assumptions);
-        literal l = choose();
-        m_select_lookahead_vars.reset();
-        if (inconsistent()) l = null_literal;
-
-#if 0
-        // assign unit literals that were found during search for lookahead.
-        if (assumptions.empty()) {
-            unsigned num_assigned = 0;
-            for (literal lit : m_trail) {
-                if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) {
-                    m_s.assign(lit, justification());
-                    ++num_assigned;
-                }
-            }
-            IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";);
-        }
-#endif
-        return l;
-    }
-
     /**
        \brief simplify set of clauses by extracting units from a lookahead at base level.
     */

src/sat/sat_lookahead.h

@@ -587,15 +587,14 @@ namespace sat {
         /**
            \brief create cubes to std-out in DIMACS form.
            The cubes are controlled using cut-depth and cut-fraction parameters.
-           If cut-depth != 0, then it is used to control the depth of cuts.
+           If cut-depth != 0, then it is used to control thedepth of cuts.
            Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
         */
 
-        lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
+        lbool cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
 
         void update_cube_statistics(statistics& st);
 
-        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

@@ -861,12 +861,7 @@ namespace sat {
         return r;
     }
 
-    literal solver::select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars) {
+    lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) {
-        lookahead lh(*this);
-        return lh.select_lookahead(assumptions, vars);
-    }
-
-    lbool  solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) {
         if (!m_cuber) {
             m_cuber = alloc(lookahead, *this);
         }

src/sat/sat_solver.h

@@ -355,10 +355,10 @@ namespace sat {
         bool check_clauses(model const& m) const;
         bool is_assumption(bool_var v) const;
 
-        literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
+        lbool  cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level);
-        lbool  cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
 
     protected:
+
         unsigned m_conflicts_since_init;
         unsigned m_restarts;
         unsigned m_conflicts_since_restart;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -67,12 +67,12 @@ class inc_sat_solver : public solver {
     std::string         m_unknown;
     // access formulas after they have been pre-processed and handled by the sat solver.
     // this allows to access the internal state of the SAT solver and carry on partial results.
-    bool                m_internalized;           // are formulas internalized?
     bool                m_internalized_converted; // have internalized formulas been converted back
     expr_ref_vector     m_internalized_fmls;      // formulas in internalized format
 
-
     typedef obj_map<expr, sat::literal> dep2asm_t;
+
+    bool is_internalized() const { return m_fmls_head == m_fmls.size(); }
 public:
     inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_mode):
         m(m), 
@@ -84,7 +84,6 @@ public:
         m_map(m),
         m_num_scopes(0),
         m_unknown("no reason given"),
-        m_internalized(false), 
         m_internalized_converted(false), 
         m_internalized_fmls(m) {
         updt_params(p);
@@ -94,7 +93,6 @@ public:
 
     bool override_incremental() const {
         sat_simplifier_params p(m_params);
-        std::cout << "override: " << p.override_incremental() << "\n";
         return p.override_incremental();
     }
 
@@ -124,7 +122,6 @@ public:
         if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
         //if (m_sat_mc) result->m_sat_mc = m_sat_mc->translate(tr);         MN: commenting this line removes bloat
         // copy m_bb_rewriter?
-        result->m_internalized = m_internalized;
         result->m_internalized_converted = m_internalized_converted;
         return result;
     }
@@ -188,8 +185,6 @@ public:
         if (r != l_true) return r;
         r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
         if (r != l_true) return r;
-        m_internalized = true;
-        m_internalized_converted = false;
 
         init_reason_unknown();
         try {
@@ -226,11 +221,8 @@ public:
         m_fmls_head_lim.push_back(m_fmls_head);
         if (m_bb_rewriter) m_bb_rewriter->push();
         m_map.push();
-        m_internalized = true;
-        m_internalized_converted = false;
     }
     virtual void pop(unsigned n) {
-        m_internalized = false;
         if (n > m_num_scopes) {   // allow inc_sat_solver to
             n = m_num_scopes;     // take over for another solver.
         }
@@ -264,7 +256,6 @@ public:
 
     virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr_core(expr * t) {
-        m_internalized = false;
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
@@ -306,17 +297,18 @@ public:
     }
 
     virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) {
-        if (!m_internalized) {
+        if (!is_internalized()) {
-            dep2asm_t dep2asm;
             m_model = 0;
             lbool r = internalize_formulas();
             if (r != l_true) return expr_ref_vector(m);
-            m_internalized = true;
         }
         convert_internalized();
+        obj_hashtable<expr> _vs;
+        for (expr* v : vs) _vs.insert(v);
         sat::bool_var_vector vars;
         for (auto& kv : m_map) {
-            vars.push_back(kv.m_value);
+            if (_vs.empty() || _vs.contains(kv.m_key))
+                vars.push_back(kv.m_value);
         }
         sat::literal_vector lits;
         lbool result = m_solver.cube(vars, lits, backtrack_level);
@@ -327,7 +319,7 @@ public:
         }
         if (result == l_true) {
             return expr_ref_vector(m);
-        }
+        }        
         expr_ref_vector fmls(m);
         expr_ref_vector lit2expr(m);
         lit2expr.resize(m_solver.num_vars() * 2);
@@ -335,6 +327,13 @@ public:
         for (sat::literal l : lits) {
             fmls.push_back(lit2expr[l.index()].get());
         }
+        vs.reset();
+        for (sat::bool_var v : vars) {
+            expr* x = lit2expr[sat::literal(v, false).index()].get();
+            if (x) {
+                vs.push_back(x);
+            }
+        }
         return fmls;
     }
 
@@ -419,7 +418,7 @@ public:
     }
     virtual unsigned get_num_assertions() const {
         const_cast<inc_sat_solver*>(this)->convert_internalized();
-        if (m_internalized && m_internalized_converted) {            
+        if (is_internalized() && m_internalized_converted) {            
             return m_internalized_fmls.size();
         }
         else {
@@ -427,7 +426,7 @@ public:
         }
     }
     virtual expr * get_assertion(unsigned idx) const {
-        if (m_internalized && m_internalized_converted) {
+        if (is_internalized() && m_internalized_converted) {
             return m_internalized_fmls[idx];
         }
         return m_fmls[idx];
@@ -443,7 +442,7 @@ public:
         const_cast<inc_sat_solver*>(this)->convert_internalized();
         if (m_cached_mc)
             return m_cached_mc;
-        if (m_internalized && m_internalized_converted) {            
+        if (is_internalized() && m_internalized_converted) {            
             m_cached_mc = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
             m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
             m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
@@ -455,7 +454,10 @@ public:
     }
 
     void convert_internalized() {
-        if (!m_internalized || m_internalized_converted) return;
+        if (!is_internalized() && m_fmls_head > 0) {
+            internalize_formulas();
+        }
+        if (!is_internalized() || m_internalized_converted) return;
         sat2goal s2g;
         m_cached_mc = nullptr;
         goal g(m, false, true, false);
@@ -679,6 +681,7 @@ private:
         if (res != l_undef) {
             m_fmls_head = m_fmls.size();
         }
+        m_internalized_converted = false;
         return res;
     }
 

src/solver/solver.h

@@ -47,7 +47,7 @@ class solver : public check_sat_result {
     params_ref m_params;
     bool       m_enforce_model_conversion;
 public:
-    solver(): m_enforce_model_conversion(true) {}
+    solver(): m_enforce_model_conversion(false) {}
     virtual ~solver() {}
 
     /**