diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 73ba5e082..f0a8c47f6 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -522,69 +522,5 @@ extern "C" { Z3_CATCH_RETURN(0); } - Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, - Z3_solver s, - Z3_ast_vector assumptions, - Z3_ast_vector candidates) { - Z3_TRY; - LOG_Z3_solver_lookahead(c, s, assumptions, candidates); - ast_manager& m = mk_c(c)->m(); - expr_ref_vector _candidates(m), _assumptions(m); - ast_ref_vector const& __candidates = to_ast_vector_ref(candidates); - ast_ref_vector const& __assumptions = to_ast_vector_ref(assumptions); - for (auto & e : __candidates) { - if (!is_expr(e)) { - SET_ERROR_CODE(Z3_INVALID_USAGE); - return 0; - } - _candidates.push_back(to_expr(e)); - } - for (auto & e : __assumptions) { - if (!is_expr(e)) { - SET_ERROR_CODE(Z3_INVALID_USAGE); - return 0; - } - _assumptions.push_back(to_expr(e)); - } - - 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)->lookahead(_assumptions, _candidates); - } - 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_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s) { - Z3_TRY; - LOG_Z3_solver_get_lemmas(c, s); - RESET_ERROR_CODE(); - ast_manager& m = mk_c(c)->m(); - init_solver(c, s); - Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); - mk_c(c)->save_object(v); - expr_ref_vector lemmas(m); - to_solver_ref(s)->get_lemmas(lemmas); - for (expr* e : lemmas) { - 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 40da086ce..c18556d0c 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -275,31 +275,6 @@ namespace Microsoft.Z3 return lboolToStatus(r); } - /// - /// Select a lookahead literal from the set of supplied candidates. - /// - public BoolExpr Lookahead(IEnumerable assumptions, IEnumerable candidates) - { - ASTVector cands = new ASTVector(Context); - foreach (var c in candidates) cands.Push(c); - ASTVector assums = new ASTVector(Context); - foreach (var c in assumptions) assums.Push(c); - return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, assums.NativeObject, cands.NativeObject)); - } - - /// - /// Retrieve set of lemmas that have been inferred by solver. - /// - public BoolExpr[] Lemmas - { - get - { - var r = Native.Z3_solver_get_lemmas(Context.nCtx, NativeObject); - var v = new ASTVector(Context, r); - return v.ToBoolExprArray(); - } - } - /// /// The model of the last Check. /// @@ -370,6 +345,28 @@ namespace Microsoft.Z3 } } + /// + /// Return a set of cubes. + /// + public IEnumerable Cube() + { + int rounds = 0; + while (true) { + BoolExpr r = (BoolExpr)Expr.Create(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject)); + if (r.IsFalse) { + if (rounds == 0) + yield return r; + break; + } + if (r.IsTrue) { + yield return r; + break; + } + ++rounds; + yield return r; + } + } + /// /// Create a clone of the current solver with respect to ctx. /// diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 8615cd7cb..f0085f2ed 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6174,14 +6174,6 @@ extern "C" { Z3_ast_vector variables, Z3_ast_vector consequences); - /** - \brief select a literal from the list of candidate propositional variables to split on. - If the candidate list is empty, then the solver chooses a formula based on its internal state. - - def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR))) - */ - - 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. @@ -6193,18 +6185,6 @@ extern "C" { Z3_ast Z3_API Z3_solver_cube(Z3_context c, Z3_solver s); - - /** - \brief retrieve lemmas from solver state. Lemmas are auxiliary unit literals, - binary clauses and other learned clauses that are below a minimal glue level. - Lemmas that have been retrieved in a previous call may be suppressed from subsequent - calls. - - def_API('Z3_solver_get_lemmas', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) - */ - - Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s); - /** \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index a3107057a..46b52e387 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -108,7 +108,6 @@ 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 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); diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 3942f96db..820000b4c 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -90,6 +90,8 @@ namespace sat { inline void simplifier::checkpoint() { s.checkpoint(); } + bool simplifier::single_threaded() const { return s.m_config.m_num_threads == 1; } + void simplifier::register_clauses(clause_vector & cs) { std::stable_sort(cs.begin(), cs.end(), size_lt()); for (clause* c : cs) { @@ -230,7 +232,7 @@ namespace sat { subsume(); if (s.inconsistent()) return; - if (!learned && elim_vars_enabled() && s.m_config.m_num_threads == 1) + if (!learned && elim_vars_enabled()) elim_vars(); if (s.inconsistent()) return; diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 6e120796f..54f8c59dd 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -75,7 +75,7 @@ namespace sat { bool m_cce; // covered clause elimination bool m_acce; // cce with asymetric literal addition bool m_bca; // blocked (binary) clause addition. - unsigned m_bce_delay; + unsigned m_bce_delay; bool m_elim_blocked_clauses; unsigned m_elim_blocked_clauses_at; bool m_retain_blocked_clauses; @@ -171,13 +171,14 @@ namespace sat { struct blocked_clause_elim; void elim_blocked_clauses(); + bool single_threaded() const; // { return s.m_config.m_num_threads == 1; } bool bce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls || cce_enabled()); } bool acce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_acce; } - bool cce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); } + bool cce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && (m_cce || acce_enabled()); } bool abce_enabled() const { return !m_learned_in_use_lists && m_num_calls >= m_bce_delay && m_abce; } - bool bca_enabled() const { return m_bca && m_learned_in_use_lists; } - bool elim_vars_bdd_enabled() const { return m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay; } - bool elim_vars_enabled() const { return m_elim_vars; } + bool bca_enabled() const { return m_bca && m_learned_in_use_lists && single_threaded(); } + bool elim_vars_bdd_enabled() const { return m_elim_vars_bdd && m_num_calls >= m_elim_vars_bdd_delay && single_threaded(); } + bool elim_vars_enabled() const { return m_elim_vars && single_threaded(); } unsigned get_num_unblocked_bin(literal l) const; unsigned get_to_elim_cost(bool_var v) const; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5cf16ccc7..44dc414af 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -310,51 +310,6 @@ public: return 0; } - virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { - IF_VERBOSE(1, verbose_stream() << "(sat-lookahead " << candidates.size() << ")\n";); - sat::bool_var_vector vars; - sat::literal_vector lits; - expr_ref_vector lit2expr(m); - lit2expr.resize(m_solver.num_vars() * 2); - m_map.mk_inv(lit2expr); - for (auto c : candidates) { - sat::bool_var v = m_map.to_bool_var(c); - if (v != sat::null_bool_var) { - vars.push_back(v); - } - } - for (auto c : assumptions) { - SASSERT(is_literal(c)); - sat::bool_var v = sat::null_bool_var; - bool sign = false; - expr* e = c; - while (m.is_not(e, e)) { - sign = !sign; - } - if (is_uninterp_const(e)) { - v = m_map.to_bool_var(e); - } - if (v != sat::null_bool_var) { - lits.push_back(sat::literal(v, sign)); - } - else { - IF_VERBOSE(0, verbose_stream() << "WARNING: could not handle " << mk_pp(c, m) << "\n";); - } - } - if (vars.empty()) { - return expr_ref(m.mk_true(), m); - } - sat::literal l = m_solver.select_lookahead(lits, vars); - if (m_solver.inconsistent()) { - IF_VERBOSE(1, verbose_stream() << "(sat-lookahead inconsistent)\n";); - return expr_ref(m.mk_false(), m); - } - if (l == sat::null_literal) { - return expr_ref(m.mk_true(), m); - } - expr_ref result(lit2expr[l.index()].get(), m); - return result; - } virtual expr_ref cube() { if (!m_internalized) { dep2asm_t dep2asm; @@ -386,16 +341,6 @@ public: return mk_and(fmls); } - virtual void get_lemmas(expr_ref_vector & lemmas) { - if (!m_internalized) return; - sat2goal s2g; - goal g(m, false, false, false); - s2g.get_learned(m_solver, m_map, m_params, lemmas); - IF_VERBOSE(1, verbose_stream() << "(sat :lemmas " << lemmas.size() << ")\n";); - // TBD: handle externals properly. - } - - virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { init_preprocess(); TRACE("sat", tout << assumptions << "\n" << vars << "\n";); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index a67fd724d..9a685d5b3 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -280,10 +280,6 @@ public: return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions(); } - virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { - return m_solver1->lookahead(assumptions, candidates); - } - virtual expr_ref cube() { return m_solver1->cube(); } diff --git a/src/solver/solver.h b/src/solver/solver.h index abd9b01f2..6171f111f 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -182,18 +182,21 @@ public: \brief extract a lookahead candidates for branching. */ - virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) = 0; + virtual expr_ref cube() = 0; +#if 0 /** \brief extract a lookahead candidates for branching. */ - virtual expr_ref cube() = 0; + virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) = 0; + /** \brief extract learned lemmas. */ virtual void get_lemmas(expr_ref_vector& lemmas) {} +#endif /** \brief Display the content of this solver. @@ -217,4 +220,6 @@ protected: }; +typedef ref solver_ref; + #endif diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 7d9388f50..0286197fa 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -77,10 +77,6 @@ public: virtual ast_manager& get_manager() const; - virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { - ast_manager& m = get_manager(); - return expr_ref(m.mk_true(), m); - } virtual expr_ref cube() { 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 ec83766a0..db8a1fe53 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -162,9 +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 lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); } virtual expr_ref cube() { flush_assertions(); 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) { flush_assertions(); diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 6288223fa..c5c7e3028 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -108,9 +108,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 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) { datatype_util dt(m); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index ee4b14178..4ff7251be 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -98,9 +98,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 lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) { flush_assertions(); return m_solver->lookahead(assumptions, candidates); } virtual expr_ref cube() { flush_assertions(); 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) { flush_assertions();