From e507a6ccd1113067366d9fd2726ba3bcef80e3f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Sep 2017 09:06:17 -0700 Subject: [PATCH] adding incremental cubing from API Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 27 ++++++++ src/api/z3_api.h | 10 +++ src/muz/spacer/spacer_itp_solver.h | 2 + src/muz/spacer/spacer_virtual_solver.h | 4 +- src/opt/maxres.cpp | 16 +++-- src/opt/opt_solver.h | 1 + src/sat/sat_lookahead.cpp | 62 +++++++++++++++++++ src/sat/sat_lookahead.h | 19 ++++++ src/sat/sat_solver.cpp | 14 +++++ src/sat/sat_solver.h | 5 +- src/sat/sat_solver/inc_sat_solver.cpp | 19 ++++++ src/smt/smt_solver.cpp | 5 ++ src/solver/combined_solver.cpp | 4 ++ src/solver/solver.h | 6 ++ src/solver/tactic2solver.cpp | 6 +- .../portfolio/bounded_int2bv_solver.cpp | 1 + src/tactic/portfolio/enum2bv_solver.cpp | 1 + src/tactic/portfolio/pb2bv_solver.cpp | 1 + 18 files changed, 194 insertions(+), 9 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index e7c5c979d..73ba5e082 100644 --- a/src/api/api_solver.cpp +++ b/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 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, diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 77ea9bed0..8615cd7cb 100644 --- a/src/api/z3_api.h +++ b/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, diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 07764745f..ec878af00 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/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); diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h index 2c338ad2e..fafaf2020 100644 --- a/src/muz/spacer/spacer_virtual_solver.h +++ b/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); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index d77eff902..52972fef1 100644 --- a/src/opt/maxres.cpp +++ b/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; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 5455e2b11..a3107057a 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -109,6 +109,7 @@ namespace opt { 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 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); diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index f3a0c9d9c..f4bfb14e2 100644 --- a/src/sat/sat_lookahead.cpp +++ b/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) { diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index be6070014..3fcf3e18b 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -139,6 +139,22 @@ namespace sat { }; #endif + struct cube_state { + svector 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. diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e15cddbd6..cbbb6b13d 100644 --- a/src/sat/sat_solver.cpp +++ b/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 diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 53e8e12dc..c115b71bb 100644 --- a/src/sat/sat_solver.h +++ b/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(); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7c3c9643e..da8f22e86 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/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; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index ae7bd95fd..9f411b0e6 100644 --- a/src/smt/smt_solver.cpp +++ b/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; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index a556570f8..a67fd724d 100644 --- a/src/solver/combined_solver.cpp +++ b/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); diff --git a/src/solver/solver.h b/src/solver/solver.h index c44b049b1..abd9b01f2 100644 --- a/src/solver/solver.h +++ b/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. */ diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 722326dfe..b165304bf 100644 --- a/src/solver/tactic2solver.cpp +++ b/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(); } diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 9fcce9360..09791f7c9 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -163,6 +163,7 @@ public: virtual void get_labels(svector & 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& 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) { diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index a9e91bfe6..6288223fa 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/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& 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) { diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 80e135ca7..d76260e0d 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -99,6 +99,7 @@ public: virtual void get_labels(svector & 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& 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) {