mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
adding Cube method to .NET API, removing lookahead and get-lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2774d6896b
commit
92b5301b7f
|
@ -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<reslimit> 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);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -275,31 +275,6 @@ namespace Microsoft.Z3
|
|||
return lboolToStatus(r);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Select a lookahead literal from the set of supplied candidates.
|
||||
/// </summary>
|
||||
public BoolExpr Lookahead(IEnumerable<BoolExpr> assumptions, IEnumerable<BoolExpr> 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));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieve set of lemmas that have been inferred by solver.
|
||||
/// </summary>
|
||||
public BoolExpr[] Lemmas
|
||||
{
|
||||
get
|
||||
{
|
||||
var r = Native.Z3_solver_get_lemmas(Context.nCtx, NativeObject);
|
||||
var v = new ASTVector(Context, r);
|
||||
return v.ToBoolExprArray();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The model of the last <c>Check</c>.
|
||||
/// </summary>
|
||||
|
@ -370,6 +345,28 @@ namespace Microsoft.Z3
|
|||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Return a set of cubes.
|
||||
/// </summary>
|
||||
public IEnumerable<BoolExpr> 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;
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create a clone of the current solver with respect to <c>ctx</c>.
|
||||
/// </summary>
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -108,7 +108,6 @@ namespace opt {
|
|||
virtual ast_manager& get_manager() const { return m; }
|
||||
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
|
||||
virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_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);
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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";);
|
||||
|
|
|
@ -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();
|
||||
}
|
||||
|
|
|
@ -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> solver_ref;
|
||||
|
||||
#endif
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -162,9 +162,7 @@ public:
|
|||
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
|
||||
virtual void get_labels(svector<symbol> & 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<expr_ref_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();
|
||||
|
|
|
@ -108,9 +108,7 @@ public:
|
|||
virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
|
||||
virtual ast_manager& get_manager() const { return m; }
|
||||
virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_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);
|
||||
|
|
|
@ -98,9 +98,7 @@ public:
|
|||
virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
|
||||
virtual void get_labels(svector<symbol> & 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<expr_ref_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();
|
||||
|
|
Loading…
Reference in a new issue