update to vector format

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

src/api/api_solver.cpp

@@ -529,11 +529,11 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);        
     }
 
-    Z3_ast 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, unsigned cutoff) {
         Z3_TRY;
         LOG_Z3_solver_cube(c, s, cutoff);
         ast_manager& m = mk_c(c)->m();
-        expr_ref result(m);
+        expr_ref_vector 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);
@@ -544,15 +544,19 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
-                result = to_solver_ref(s)->cube(cutoff);
+                result.append(to_solver_ref(s)->cube(cutoff));
             }
             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_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        for (expr* e : result) {
+            v->m_ast_vector.push_back(e);
+        }
+        RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);        
     }
 

src/api/dotnet/Solver.cs

@@ -362,20 +362,19 @@ namespace Microsoft.Z3
 	/// <summary>
 	/// Return a set of cubes.
 	/// </summary>
-	public IEnumerable<BoolExpr> Cube()
+	public IEnumerable<BoolExpr[]> Cube()
 	{
 	     while (true) {
                 var lvl = BacktrackLevel;
                 BacktrackLevel = uint.MaxValue;
-		BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
-                if (r.IsFalse) {
+                ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
+                if (r.Size == 1 && ((Expr)r[0]).IsFalse) {
                    break;
                 }
-	        if (r.IsTrue) {
-                     yield return r;
-                     break;
+                yield return r.ToBoolExprArray();
+	        if (r.Size == 0) {
+                   break;
                 }
-                yield return r;
 	     }
 	}
 

src/api/python/z3/z3.py

@@ -6289,13 +6289,12 @@ class Solver(Z3PPObject):
         while True:
             lvl = self.backtrack_level
             self.backtrack_level = 4000000000
-            r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx)            
-            if (is_false(r)):
+            r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, lvl), self.ctx)            
+            if (len(r) == 1 and is_false(r[0])):
                 return
-            if (is_true(r)):
-                yield r
+            yield r            
+            if (len(r) == 0):                
                 return
-            yield r
 
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""

src/api/z3_api.h

@@ -6235,10 +6235,10 @@ extern "C" {
        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, (_in(CONTEXT), _in(SOLVER), _in(UINT)))
+       def_API('Z3_solver_cube', AST_VECTOR, (_in(CONTEXT), _in(SOLVER), _in(UINT)))
     */
 
-    Z3_ast 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, unsigned backtrack_level);
 
     /**
        \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions

src/muz/spacer/spacer_itp_solver.h

@@ -119,7 +119,7 @@ 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(unsigned) { return expr_ref(m.mk_true(), m); }
+    virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
 
 
     virtual void push();

src/muz/spacer/spacer_virtual_solver.h

@@ -94,7 +94,7 @@ public:
     virtual void reset();
 
     virtual void set_progress_callback(progress_callback *callback) {UNREACHABLE();}
-    virtual expr_ref cube(unsigned) { return expr_ref(m.mk_true(), m); }
+    virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
 
     virtual solver *translate(ast_manager &m, params_ref const &p);
 

src/opt/opt_solver.h

@@ -108,7 +108,7 @@ namespace opt {
         virtual ast_manager& get_manager() const { return m; } 
         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 cube(unsigned) { return expr_ref(m.mk_true(), m); }
+        virtual expr_ref_vector cube(unsigned) { return expr_ref_vector(m); }
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/sat/sat_solver/inc_sat_solver.cpp

@@ -301,12 +301,12 @@ public:
         return 0;
     }
 
-    virtual expr_ref cube(unsigned backtrack_level) {
+    virtual expr_ref_vector cube(unsigned backtrack_level) {
         if (!m_internalized) {
             dep2asm_t dep2asm;
             m_model = 0;
             lbool r = internalize_formulas();
-            if (r != l_true) return expr_ref(m.mk_true(), m);
+            if (r != l_true) return expr_ref_vector(m);
             m_internalized = true;
         }
         convert_internalized();
@@ -317,10 +317,12 @@ public:
         sat::literal_vector lits;
         lbool result = m_solver.cube(vars, lits, backtrack_level);
         if (result == l_false || lits.empty()) {
-            return expr_ref(m.mk_false(), m);
+            expr_ref_vector result(m);
+            result.push_back(m.mk_false());
+            return result;
         }
         if (result == l_true) {
-            return expr_ref(m.mk_true(), m);
+            return expr_ref_vector(m);
         }
         expr_ref_vector fmls(m);
         expr_ref_vector lit2expr(m);
@@ -329,7 +331,7 @@ public:
         for (sat::literal l : lits) {
             fmls.push_back(lit2expr[l.index()].get());
         }
-        return mk_and(fmls);
+        return fmls;
     }
 
     virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {

src/smt/smt_solver.cpp

@@ -226,9 +226,8 @@ namespace smt {
             return expr_ref(m.mk_true(), m);
         }
 
-        virtual expr_ref cube(unsigned) {
-            ast_manager& m = get_manager();
-            return expr_ref(m.mk_true(), m);
+        virtual expr_ref_vector cube(unsigned) {
+            return expr_ref_vector(get_manager());
         }
 
         struct collect_fds_proc {

src/solver/combined_solver.cpp

@@ -281,7 +281,7 @@ public:
         return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions();
     }
 
-    virtual expr_ref cube(unsigned backtrack_level) {
+    virtual expr_ref_vector cube(unsigned backtrack_level) {
         return m_solver1->cube(backtrack_level);
     }
 

src/solver/solver.h

@@ -189,7 +189,7 @@ public:
        \brief extract a lookahead candidates for branching.
     */
 
-    virtual expr_ref cube(unsigned backtrack_level) = 0;
+    virtual expr_ref_vector cube(unsigned backtrack_level) = 0;
 
     /**
        \brief Display the content of this solver.

src/solver/solver_pool.cpp

@@ -223,7 +223,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { return m_base->get_labels(r); }
     virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); }
 
-    virtual expr_ref cube(unsigned ) { return expr_ref(m.mk_true(), m); }
+    virtual expr_ref_vector cube(unsigned ) { return expr_ref_vector(m); }
 
     virtual ast_manager& get_manager() const { return m_base->get_manager(); } 
 

src/solver/tactic2solver.cpp

@@ -77,9 +77,8 @@ public:
 
     virtual ast_manager& get_manager() const; 
 
-    virtual expr_ref cube(unsigned ) {
-        ast_manager& m = get_manager();
-        return expr_ref(m.mk_true(), m);
+    virtual expr_ref_vector cube(unsigned ) {
+        return expr_ref_vector(get_manager());
     }
 
     virtual model_converter_ref get_model_converter() const { return m_mc; }

src/tactic/portfolio/bounded_int2bv_solver.cpp

@@ -163,7 +163,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    virtual expr_ref cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
     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) {
         flush_assertions();

src/tactic/portfolio/enum2bv_solver.cpp

@@ -113,7 +113,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     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 cube(unsigned backtrack_level) { return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(unsigned backtrack_level) { return m_solver->cube(backtrack_level); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         datatype_util dt(m);

src/tactic/portfolio/parallel_tactic.cpp

@@ -414,16 +414,15 @@ private:
         cubes.reset();
         s.set_cube_params();
         while (true) {
-            expr_ref c = s.get_solver().cube(UINT_MAX); // TBD tune this
-            VERIFY(c);
-            if (m.is_false(c)) {                
-                break;
-            }
-            if (m.is_true(c)) {
+            expr_ref_vector c = s.get_solver().cube(UINT_MAX); // TBD tune this
+            if (c.empty()) {
                 report_undef(s);
                 return;
             }
-            cubes.push_back(c);            
+            if (m.is_false(c.back())) {                
+                break;
+            }
+            cubes.push_back(mk_and(c));            
         }
 
         IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << ")\n";);

src/tactic/portfolio/pb2bv_solver.cpp

@@ -103,7 +103,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
-    virtual expr_ref cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
+    virtual expr_ref_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); }
     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) {
         flush_assertions();