From 75b8d10f48ce59b6770e24f223eaf522565c7f54 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Nov 2017 21:44:21 -0800 Subject: [PATCH 1/2] add backtrack level to cuber interface Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 6 +++--- src/api/dotnet/Solver.cs | 11 ++++++++--- src/api/python/z3/z3.py | 9 +++------ src/api/z3_api.h | 7 +++++-- src/muz/spacer/spacer_itp_solver.h | 2 +- src/muz/spacer/spacer_virtual_solver.h | 2 +- src/opt/opt_solver.h | 2 +- src/sat/ba_solver.cpp | 10 +++++----- src/sat/sat_lookahead.cpp | 12 ++++++++++-- src/sat/sat_lookahead.h | 2 +- src/sat/sat_solver.cpp | 4 ++-- src/sat/sat_solver.h | 2 +- src/sat/sat_solver/inc_sat_solver.cpp | 4 ++-- src/smt/smt_solver.cpp | 2 +- src/solver/combined_solver.cpp | 4 ++-- src/solver/solver.h | 2 +- src/solver/solver_pool.cpp | 2 +- src/solver/tactic2solver.cpp | 2 +- src/tactic/portfolio/bounded_int2bv_solver.cpp | 2 +- src/tactic/portfolio/enum2bv_solver.cpp | 2 +- src/tactic/portfolio/parallel_tactic.cpp | 2 +- src/tactic/portfolio/pb2bv_solver.cpp | 2 +- 22 files changed, 53 insertions(+), 40 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 53ce36720..0c94c0b4e 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -529,9 +529,9 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } - Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s) { + Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, unsigned cutoff) { Z3_TRY; - LOG_Z3_solver_cube(c, s); + LOG_Z3_solver_cube(c, s, cutoff); 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()); @@ -544,7 +544,7 @@ extern "C" { scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { - result = to_solver_ref(s)->cube(); + result = to_solver_ref(s)->cube(cutoff); } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 9154117ce..4a779e91b 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -353,6 +353,12 @@ namespace Microsoft.Z3 } } + /// + /// Backtrack level that can be adjusted by conquer process + /// + public uint BacktrackLevel { get; set; } + + /// /// Return a set of cubes. /// @@ -360,10 +366,8 @@ namespace Microsoft.Z3 { int rounds = 0; while (true) { - BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject)); + BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, BacktrackLevel)); if (r.IsFalse) { - if (rounds == 0) - yield return r; break; } if (r.IsTrue) { @@ -412,6 +416,7 @@ namespace Microsoft.Z3 : base(ctx, obj) { Contract.Requires(ctx != null); + this.BacktrackLevel = uint.MaxValue; } internal class DecRefQueue : IDecRefQueue diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6b6c90019..45fedc674 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6283,19 +6283,16 @@ class Solver(Z3PPObject): consequences = [ consequences[i] for i in range(sz) ] return CheckSatResult(r), consequences - def cube(self): + def cube(self, level_ref): """Get set of cubes""" - rounds = 0 while True: - r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver), self.ctx) + backtrack_level = level_ref.backtrack_level + r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, backtrack_level), self.ctx) if (is_false(r)): - if (rounds == 0): - yield r return if (is_true(r)): yield r return - rounds += 1 yield r def proof(self): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ffda1ecbd..b17e2a531 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6232,10 +6232,13 @@ 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. - def_API('Z3_solver_cube', AST, (_in(CONTEXT), _in(SOLVER))) + 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))) */ - Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s); + Z3_ast 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 6fc67a243..c61dba13c 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() { return expr_ref(m.mk_true(), m); } + virtual expr_ref cube(unsigned) { return expr_ref(m.mk_true(), m); } virtual void push(); diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h index 4e1f43bfc..4818600a9 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() { return expr_ref(m.mk_true(), m); } + virtual expr_ref cube(unsigned) { return expr_ref(m.mk_true(), 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 1f0a518b2..f695bae28 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() { return expr_ref(m.mk_true(), m); } + virtual expr_ref cube(unsigned) { return expr_ref(m.mk_true(), m); } void set_logic(symbol const& logic); smt::theory_var add_objective(app* term); diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 2a880f918..a1a80df97 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -349,7 +349,7 @@ namespace sat { } bool nullify = p.lit() != null_literal && value(p.lit()) == l_true; if (nullify) { - IF_VERBOSE(10, display(verbose_stream() << "nullify tracking literal\n", p, true);); + IF_VERBOSE(100, display(verbose_stream() << "nullify tracking literal\n", p, true);); SASSERT(lvl(p.lit()) == 0); nullify_tracking_literal(p); init_watch(p, true); @@ -374,7 +374,7 @@ namespace sat { if (p.k() == 1 && p.lit() == null_literal) { literal_vector lits(p.literals()); s().mk_clause(lits.size(), lits.c_ptr(), p.learned()); - IF_VERBOSE(10, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); + IF_VERBOSE(100, display(verbose_stream() << "add clause: " << lits << "\n", p, true);); remove_constraint(p, "implies clause"); } else if (true_val == 0 && num_false == 0) { @@ -384,14 +384,14 @@ namespace sat { } else if (true_val >= p.k()) { if (p.lit() != null_literal) { - IF_VERBOSE(10, display(verbose_stream() << "assign true literal ", p, true);); + IF_VERBOSE(100, display(verbose_stream() << "assign true literal ", p, true);); s().assign(p.lit(), justification()); } remove_constraint(p, "is true"); } else if (slack + true_val < p.k()) { if (p.lit() != null_literal) { - IF_VERBOSE(10, display(verbose_stream() << "assign false literal ", p, true);); + IF_VERBOSE(100, display(verbose_stream() << "assign false literal ", p, true);); s().assign(~p.lit(), justification()); } else { @@ -2877,7 +2877,7 @@ namespace sat { bool ba_solver::elim_pure(literal lit) { if (value(lit) == l_undef && !m_cnstr_use_list[lit.index()].empty() && use_count(~lit) == 0 && get_num_unblocked_bin(~lit) == 0) { - IF_VERBOSE(10, verbose_stream() << "pure literal: " << lit << "\n";); + IF_VERBOSE(100, verbose_stream() << "pure literal: " << lit << "\n";); s().assign(lit, justification()); return true; } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index a41468936..e4878df42 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1964,7 +1964,7 @@ namespace sat { bool_var_vector vars; for (bool_var v : m_freevars) vars.push_back(v); while (true) { - lbool result = cube(vars, lits); + lbool result = cube(vars, lits, UINT_MAX); if (lits.empty() || result != l_undef) { return l_undef; } @@ -1973,7 +1973,7 @@ namespace sat { return l_undef; } - lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits) { + lbool lookahead::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); m_select_lookahead_vars.reset(); @@ -2006,6 +2006,14 @@ namespace sat { continue; } pick_up_work: + if (m_cube_state.m_cube.size() >= backtrack_level) { + IF_VERBOSE(10, verbose_stream() << "(sat-cube :cube: " << m_cube_state.m_cube.size() << " :backtrack_level " << backtrack_level << ")\n";); + while (m_cube_state.m_cube.size() >= backtrack_level) { + set_conflict(); + backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); + } + backtrack_level = UINT_MAX; + } 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)) { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index baf3ed660..6cf75937f 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -567,7 +567,7 @@ namespace sat { lbool cube(); - lbool cube(bool_var_vector const& vars, literal_vector& lits); + lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); /** diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ba6e63680..61dc1f6c2 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -837,11 +837,11 @@ namespace sat { return lh.select_lookahead(assumptions, vars); } - lbool solver::cube(bool_var_vector const& vars, literal_vector& lits) { + lbool solver::cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level) { if (!m_cuber) { m_cuber = alloc(lookahead, *this); } - lbool result = m_cuber->cube(vars, lits); + lbool result = m_cuber->cube(vars, lits, backtrack_level); if (result == l_false) { dealloc(m_cuber); m_cuber = nullptr; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index bf5f0975b..cb8c2b763 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -352,7 +352,7 @@ namespace sat { bool check_clauses(model const& m) const; literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars); - lbool cube(bool_var_vector const& vars, literal_vector& lits); + lbool cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level); protected: unsigned m_conflicts_since_init; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b9bc81e3d..98c42ed19 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -301,7 +301,7 @@ public: return 0; } - virtual expr_ref cube() { + virtual expr_ref cube(unsigned backtrack_level) { if (!m_internalized) { dep2asm_t dep2asm; m_model = 0; @@ -315,7 +315,7 @@ public: vars.push_back(kv.m_value); } sat::literal_vector lits; - lbool result = m_solver.cube(vars, lits); + lbool result = m_solver.cube(vars, lits, backtrack_level); if (result == l_false || lits.empty()) { return expr_ref(m.mk_false(), m); } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index b37d004f4..1a0e6facd 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -226,7 +226,7 @@ namespace smt { return expr_ref(m.mk_true(), m); } - virtual expr_ref cube() { + virtual expr_ref cube(unsigned) { ast_manager& m = get_manager(); return expr_ref(m.mk_true(), m); } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 05e75a9a4..7d41a8685 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -281,8 +281,8 @@ public: return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions(); } - virtual expr_ref cube() { - return m_solver1->cube(); + virtual expr_ref cube(unsigned backtrack_level) { + return m_solver1->cube(backtrack_level); } virtual expr * get_assumption(unsigned idx) const { diff --git a/src/solver/solver.h b/src/solver/solver.h index 3719b5a6a..8d9488c48 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() = 0; + virtual expr_ref 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 b2da00bfa..afefd8433 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() { return expr_ref(m.mk_true(), m); } + virtual expr_ref cube(unsigned ) { return expr_ref(m.mk_true(), 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 dc9f1b25f..607f0994f 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -77,7 +77,7 @@ public: virtual ast_manager& get_manager() const; - virtual expr_ref cube() { + virtual expr_ref cube(unsigned ) { ast_manager& m = get_manager(); return expr_ref(m.mk_true(), m); } diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 195a16fbf..da031171d 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() { flush_assertions(); return m_solver->cube(); } + virtual expr_ref 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 b16ba2443..474084650 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() { return m_solver->cube(); } + virtual expr_ref 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 7651ace16..7d25f0f7e 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -414,7 +414,7 @@ private: cubes.reset(); s.set_cube_params(); while (true) { - expr_ref c = s.get_solver().cube(); + expr_ref c = s.get_solver().cube(UINT_MAX); // TBD tune this VERIFY(c); if (m.is_false(c)) { break; diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 33a8fcd46..7d2e1f322 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() { flush_assertions(); return m_solver->cube(); } + virtual expr_ref 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(); From bc8681a0ea5441a7741b29380b118e59ad656d28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Nov 2017 22:14:59 -0800 Subject: [PATCH 2/2] reset backtrack level after first backtrack Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 6 +++--- src/sat/sat_lookahead.cpp | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 45fedc674..2ae7e6ced 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5988,6 +5988,7 @@ class Solver(Z3PPObject): def __init__(self, solver=None, ctx=None): assert solver is None or ctx is not None self.ctx = _get_ctx(ctx) + self.backtrack_level = 4000000000 self.solver = None if solver is None: self.solver = Z3_mk_solver(self.ctx.ref()) @@ -6283,11 +6284,10 @@ class Solver(Z3PPObject): consequences = [ consequences[i] for i in range(sz) ] return CheckSatResult(r), consequences - def cube(self, level_ref): + def cube(self): """Get set of cubes""" while True: - backtrack_level = level_ref.backtrack_level - r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, backtrack_level), self.ctx) + r = _to_expr_ref(Z3_solver_cube(self.ctx.ref(), self.solver, self.backtrack_level), self.ctx) if (is_false(r)): return if (is_true(r)): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index e4878df42..27d174653 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2012,8 +2012,8 @@ namespace sat { set_conflict(); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); } - backtrack_level = UINT_MAX; } + backtrack_level = UINT_MAX; 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)) {