diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2805e7e2d..9e7223aee 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -557,7 +557,7 @@ extern "C" { Z3_TRY; LOG_Z3_solver_cube(c, s, cutoff); ast_manager& m = mk_c(c)->m(); - expr_ref_vector result(m); + expr_ref_vector result(m), vars(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); @@ -568,7 +568,7 @@ extern "C" { scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { - result.append(to_solver_ref(s)->cube(cutoff)); + result.append(to_solver_ref(s)->cube(vars, cutoff)); } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); @@ -580,6 +580,7 @@ extern "C" { for (expr* e : result) { v->m_ast_vector.push_back(e); } + // TBD: save return variables from vars into variable ast-vector. RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(0); } diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 84469f490..55c1711c3 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_vector cube(unsigned) { return expr_ref_vector(m); } + virtual expr_ref_vector cube(expr_ref_vector&, 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 946df95ad..c7dfd3c11 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_vector cube(unsigned) { return expr_ref_vector(m); } + virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); } virtual solver *translate(ast_manager &m, params_ref const &p); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 117b65c5a..5fa87b3ba 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -285,10 +285,12 @@ public: m_last_index = 0; bool first = index > 0; SASSERT(index < asms.size() || asms.empty()); + IF_VERBOSE(1, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";); while (index < asms.size() && is_sat == l_true) { while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) { index = next_index(asms, index); } + IF_VERBOSE(1, verbose_stream() << "hill climb " << index << "\n";); first = false; // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";); m_last_index = index; diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 9d1eccb38..4d2f39416 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_vector cube(unsigned) { return expr_ref_vector(m); } + virtual expr_ref_vector cube(expr_ref_vector&, 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_asymm_branch.h b/src/sat/sat_asymm_branch.h index b18c549ac..6790bd963 100644 --- a/src/sat/sat_asymm_branch.h +++ b/src/sat/sat_asymm_branch.h @@ -42,7 +42,6 @@ namespace sat { unsigned m_asymm_branch_rounds; unsigned m_asymm_branch_delay; bool m_asymm_branch_sampled; - bool m_asymm_branch_propagate; bool m_asymm_branch_all; int64 m_asymm_branch_limit; diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 6b8d4cba7..32988b216 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -182,7 +182,8 @@ namespace sat { literal l(v, false); literal r = roots[v]; SASSERT(v != r.var()); - if (m_solver.is_external(v) || !m_solver.set_root(l, r)) { + if (m_solver.is_external(v)) { + m_solver.set_root(l, r); // 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); diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 379888b15..f04318a5d 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -123,13 +123,13 @@ namespace sat{ TRACE("elim_vars", tout << "eliminate " << v << "\n"; for (watched const& w : simp.get_wlist(~pos_l)) { - if (w.is_binary_unblocked_clause()) { + if (w.is_binary_non_learned_clause()) { tout << pos_l << " " << w.get_literal() << "\n"; } } m.display(tout, b1); for (watched const& w : simp.get_wlist(~neg_l)) { - if (w.is_binary_unblocked_clause()) { + if (w.is_binary_non_learned_clause()) { tout << neg_l << " " << w.get_literal() << "\n"; } } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 2af846f42..3984ec324 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -305,7 +305,7 @@ public: return 0; } - virtual expr_ref_vector cube(unsigned backtrack_level) { + virtual expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) { if (!m_internalized) { dep2asm_t dep2asm; m_model = 0; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 01ea61fd9..3449ad480 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -222,7 +222,7 @@ namespace smt { return expr_ref(m.mk_true(), m); } - virtual expr_ref_vector cube(unsigned) { + virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(get_manager()); } diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 29f6a32f1..713009cd6 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -275,8 +275,8 @@ public: return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions(); } - virtual expr_ref_vector cube(unsigned backtrack_level) { - return m_solver1->cube(backtrack_level); + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { + return m_solver1->cube(vars, backtrack_level); } virtual expr * get_assumption(unsigned idx) const { diff --git a/src/solver/solver.h b/src/solver/solver.h index 7a51725a2..7634a346e 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -190,7 +190,7 @@ public: \brief extract a lookahead candidates for branching. */ - virtual expr_ref_vector cube(unsigned backtrack_level) = 0; + virtual expr_ref_vector cube(expr_ref_vector& vars, 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 1b7203351..2f6a22580 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_vector cube(unsigned ) { return expr_ref_vector(m); } + virtual expr_ref_vector cube(expr_ref_vector& vars, 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 4585af65e..cbe6b34a9 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_vector cube(unsigned ) { + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned ) { return expr_ref_vector(get_manager()); } diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index b8a8f6704..c81d413b8 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -162,7 +162,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_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); } + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, 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 ffb51fe2e..bfe057f82 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -103,7 +103,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_vector cube(unsigned backtrack_level) { return m_solver->cube(backtrack_level); } + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { return m_solver->cube(vars, 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 8e14d77e2..f4982c2c2 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -414,7 +414,8 @@ private: cubes.reset(); s.set_cube_params(); while (true) { - expr_ref_vector c = s.get_solver().cube(UINT_MAX); // TBD tune this + expr_ref_vector vars(m); + expr_ref_vector c = s.get_solver().cube(vars, UINT_MAX); // TBD tune this if (c.empty()) { report_undef(s); return; diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index cb5327443..eba10cbd1 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -100,7 +100,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_vector cube(unsigned backtrack_level) { flush_assertions(); return m_solver->cube(backtrack_level); } + virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { flush_assertions(); return m_solver->cube(vars, 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();