diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 0c94c0b4e..9f13ce3c1 100644
--- a/src/api/api_solver.cpp
+++ b/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);
}
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 24a0bbc61..4b8ff4cf6 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -362,20 +362,19 @@ namespace Microsoft.Z3
///
/// Return a set of cubes.
///
- public IEnumerable Cube()
+ public IEnumerable 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;
}
}
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 1402d1ce7..e281a1273 100644
--- a/src/api/python/z3/z3.py
+++ b/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."""
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b17e2a531..67fc0c903 100644
--- a/src/api/z3_api.h
+++ b/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
diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h
index c61dba13c..ab3b94894 100644
--- a/src/muz/spacer/spacer_itp_solver.h
+++ b/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();
diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h
index 4818600a9..3b256f297 100644
--- a/src/muz/spacer/spacer_virtual_solver.h
+++ b/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);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index f695bae28..61947e768 100644
--- a/src/opt/opt_solver.h
+++ b/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& mutexes);
virtual lbool preferred_sat(expr_ref_vector const& asms, 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);
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 98c42ed19..b5efe57da 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/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) {
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 1a0e6facd..850621e67 100644
--- a/src/smt/smt_solver.cpp
+++ b/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 {
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index 7d41a8685..cc52c90cb 100644
--- a/src/solver/combined_solver.cpp
+++ b/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);
}
diff --git a/src/solver/solver.h b/src/solver/solver.h
index a3454a798..713434d7c 100644
--- a/src/solver/solver.h
+++ b/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.
diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index afefd8433..3c7837ad5 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -223,7 +223,7 @@ public:
virtual void get_labels(svector & 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(); }
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 607f0994f..dd2f42e7a 100644
--- a/src/solver/tactic2solver.cpp
+++ b/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; }
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index da031171d..c0e5e0a46 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/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 & 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& 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();
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 474084650..4722f9289 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -113,7 +113,7 @@ public:
virtual void get_labels(svector & r) { m_solver->get_labels(r); }
virtual ast_manager& get_manager() const { return m; }
virtual lbool find_mutexes(expr_ref_vector const& vars, 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);
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index 7d25f0f7e..8a6c6fa15 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/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";);
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index 4f4c044b8..f6a7b1622 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/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 & 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& 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();