mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
remove
This commit is contained in:
Nikolaj Bjorner
parent
f0e9363e78
commit
0242566792
|
|
@ -1,474 +0,0 @@
|
||||||
/*++
|
|
||||||
Copyright (c) 2011 Microsoft Corporation
|
|
||||||
|
|
||||||
Module Name:
|
|
||||||
|
|
||||||
smt_tactic.h
|
|
||||||
|
|
||||||
Abstract:
|
|
||||||
|
|
||||||
smt::context as a tactic.
|
|
||||||
|
|
||||||
Author:
|
|
||||||
|
|
||||||
Leonardo (leonardo) 2011-10-18
|
|
||||||
|
|
||||||
Notes:
|
|
||||||
|
|
||||||
--*/
|
|
||||||
#include "util/debug.h"
|
|
||||||
#include "ast/rewriter/rewriter_types.h"
|
|
||||||
#include "ast/ast_util.h"
|
|
||||||
#include "ast/ast_ll_pp.h"
|
|
||||||
#include "smt/smt_kernel.h"
|
|
||||||
#include "smt/params/smt_params.h"
|
|
||||||
#include "smt/params/smt_params_helper.hpp"
|
|
||||||
#include "smt/smt_solver.h"
|
|
||||||
#include "tactic/tactic.h"
|
|
||||||
#include "tactic/tactical.h"
|
|
||||||
#include "tactic/generic_model_converter.h"
|
|
||||||
#include "solver/solver2tactic.h"
|
|
||||||
#include "solver/solver.h"
|
|
||||||
#include "solver/mus.h"
|
|
||||||
#include "solver/parallel_tactic.h"
|
|
||||||
#include "solver/parallel_params.hpp"
|
|
||||||
|
|
||||||
typedef obj_map<expr, expr *> expr2expr_map;
|
|
||||||
|
|
||||||
|
|
||||||
class smt_tactic : public tactic {
|
|
||||||
ast_manager& m;
|
|
||||||
smt_params m_params;
|
|
||||||
params_ref m_params_ref;
|
|
||||||
statistics m_stats;
|
|
||||||
smt::kernel * m_ctx;
|
|
||||||
symbol m_logic;
|
|
||||||
progress_callback * m_callback;
|
|
||||||
bool m_candidate_models;
|
|
||||||
bool m_fail_if_inconclusive;
|
|
||||||
|
|
||||||
public:
|
|
||||||
smt_tactic(ast_manager& m, params_ref const & p):
|
|
||||||
m(m),
|
|
||||||
m_params_ref(p),
|
|
||||||
m_ctx(nullptr),
|
|
||||||
m_callback(nullptr),
|
|
||||||
m_vars(m) {
|
|
||||||
updt_params_core(p);
|
|
||||||
TRACE("smt_tactic", tout << "p: " << p << "\n";);
|
|
||||||
}
|
|
||||||
|
|
||||||
tactic * translate(ast_manager & m) override {
|
|
||||||
return alloc(smt_tactic, m, m_params_ref);
|
|
||||||
}
|
|
||||||
|
|
||||||
~smt_tactic() override {
|
|
||||||
SASSERT(m_ctx == nullptr);
|
|
||||||
}
|
|
||||||
|
|
||||||
smt_params & fparams() {
|
|
||||||
return m_params;
|
|
||||||
}
|
|
||||||
|
|
||||||
params_ref & params() {
|
|
||||||
return m_params_ref;
|
|
||||||
}
|
|
||||||
|
|
||||||
void updt_params_core(params_ref const & p) {
|
|
||||||
smt_params_helper _p(p);
|
|
||||||
m_candidate_models = _p.candidate_models();
|
|
||||||
m_fail_if_inconclusive = p.get_bool("fail_if_inconclusive", true);
|
|
||||||
}
|
|
||||||
|
|
||||||
void updt_params(params_ref const & p) override {
|
|
||||||
TRACE("smt_tactic", tout << "updt_params: " << p << "\n";);
|
|
||||||
updt_params_core(p);
|
|
||||||
fparams().updt_params(p);
|
|
||||||
m_params_ref.copy(p);
|
|
||||||
m_logic = p.get_sym(symbol("logic"), m_logic);
|
|
||||||
if (m_logic != symbol::null && m_ctx) {
|
|
||||||
m_ctx->set_logic(m_logic);
|
|
||||||
}
|
|
||||||
SASSERT(p.get_bool("auto_config", fparams().m_auto_config) == fparams().m_auto_config);
|
|
||||||
}
|
|
||||||
|
|
||||||
void collect_param_descrs(param_descrs & r) override {
|
|
||||||
r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
|
|
||||||
smt_params_helper::collect_param_descrs(r);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void collect_statistics(statistics & st) const override {
|
|
||||||
if (m_ctx)
|
|
||||||
m_ctx->collect_statistics(st); // ctx is still running...
|
|
||||||
else
|
|
||||||
st.copy(m_stats);
|
|
||||||
}
|
|
||||||
|
|
||||||
void cleanup() override {
|
|
||||||
}
|
|
||||||
|
|
||||||
void reset_statistics() override {
|
|
||||||
m_stats.reset();
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_logic(symbol const & l) override {
|
|
||||||
m_logic = l;
|
|
||||||
}
|
|
||||||
|
|
||||||
void set_progress_callback(progress_callback * callback) override {
|
|
||||||
m_callback = callback;
|
|
||||||
}
|
|
||||||
|
|
||||||
struct scoped_init_ctx {
|
|
||||||
smt_tactic & m_owner;
|
|
||||||
smt_params m_params; // smt-setup overwrites parameters depending on the current assertions.
|
|
||||||
params_ref m_params_ref;
|
|
||||||
|
|
||||||
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
|
|
||||||
m_params = o.fparams();
|
|
||||||
m_params_ref = o.params();
|
|
||||||
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
|
|
||||||
TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
|
|
||||||
new_ctx->set_logic(o.m_logic);
|
|
||||||
if (o.m_callback) {
|
|
||||||
new_ctx->set_progress_callback(o.m_callback);
|
|
||||||
}
|
|
||||||
o.m_ctx = new_ctx;
|
|
||||||
}
|
|
||||||
|
|
||||||
~scoped_init_ctx() {
|
|
||||||
smt::kernel * d = m_owner.m_ctx;
|
|
||||||
m_owner.m_ctx = nullptr;
|
|
||||||
m_owner.m_user_ctx = nullptr;
|
|
||||||
|
|
||||||
if (d)
|
|
||||||
dealloc(d);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
void handle_canceled(goal_ref const & in,
|
|
||||||
goal_ref_buffer & result) {
|
|
||||||
}
|
|
||||||
|
|
||||||
void operator()(goal_ref const & in,
|
|
||||||
goal_ref_buffer & result) override {
|
|
||||||
try {
|
|
||||||
IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
|
|
||||||
tactic_report report("smt", *in);
|
|
||||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
|
||||||
<< " PREPROCESS: " << fparams().m_preprocess << "\n";
|
|
||||||
tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n";
|
|
||||||
tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n";
|
|
||||||
tout << "params_ref: " << m_params_ref << "\n";
|
|
||||||
tout << "nnf: " << fparams().m_nnf_cnf << "\n";);
|
|
||||||
TRACE("smt_tactic_params", m_params.display(tout););
|
|
||||||
TRACE("smt_tactic_detail", in->display(tout););
|
|
||||||
TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
|
|
||||||
scoped_init_ctx init(*this, m);
|
|
||||||
SASSERT(m_ctx);
|
|
||||||
|
|
||||||
expr_ref_vector clauses(m);
|
|
||||||
expr2expr_map bool2dep;
|
|
||||||
ptr_vector<expr> assumptions;
|
|
||||||
ref<generic_model_converter> fmc;
|
|
||||||
if (in->unsat_core_enabled()) {
|
|
||||||
extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
|
|
||||||
TRACE("mus", in->display_with_dependencies(tout);
|
|
||||||
tout << clauses << "\n";);
|
|
||||||
if (in->proofs_enabled() && !assumptions.empty())
|
|
||||||
throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
|
|
||||||
for (unsigned i = 0; i < clauses.size(); ++i) {
|
|
||||||
m_ctx->assert_expr(clauses[i].get());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if (in->proofs_enabled()) {
|
|
||||||
unsigned sz = in->size();
|
|
||||||
for (unsigned i = 0; i < sz; i++) {
|
|
||||||
m_ctx->assert_expr(in->form(i), in->pr(i));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
unsigned sz = in->size();
|
|
||||||
for (unsigned i = 0; i < sz; i++) {
|
|
||||||
m_ctx->assert_expr(in->form(i));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (m_ctx->canceled()) {
|
|
||||||
throw tactic_exception(Z3_CANCELED_MSG);
|
|
||||||
}
|
|
||||||
user_propagate_delay_init();
|
|
||||||
|
|
||||||
lbool r;
|
|
||||||
try {
|
|
||||||
if (assumptions.empty() && !m_user_ctx)
|
|
||||||
r = m_ctx->setup_and_check();
|
|
||||||
else
|
|
||||||
r = m_ctx->check(assumptions.size(), assumptions.data());
|
|
||||||
}
|
|
||||||
catch(...) {
|
|
||||||
TRACE("smt_tactic", tout << "exception\n";);
|
|
||||||
m_ctx->collect_statistics(m_stats);
|
|
||||||
throw;
|
|
||||||
}
|
|
||||||
SASSERT(m_ctx);
|
|
||||||
m_ctx->collect_statistics(m_stats);
|
|
||||||
proof_ref pr(m_ctx->get_proof(), m);
|
|
||||||
TRACE("smt_tactic", tout << r << " " << pr << "\n";);
|
|
||||||
switch (r) {
|
|
||||||
case l_true: {
|
|
||||||
if (m_fail_if_inconclusive && !in->sat_preserved())
|
|
||||||
throw tactic_exception("over-approximated goal found to be sat");
|
|
||||||
// the empty assertion set is trivially satifiable.
|
|
||||||
in->reset();
|
|
||||||
result.push_back(in.get());
|
|
||||||
// store the model in a no-op model converter, and filter fresh Booleans
|
|
||||||
if (in->models_enabled()) {
|
|
||||||
model_ref md;
|
|
||||||
m_ctx->get_model(md);
|
|
||||||
buffer<symbol> r;
|
|
||||||
m_ctx->get_relevant_labels(nullptr, r);
|
|
||||||
labels_vec rv;
|
|
||||||
rv.append(r.size(), r.data());
|
|
||||||
model_converter_ref mc;
|
|
||||||
mc = model_and_labels2model_converter(md.get(), rv);
|
|
||||||
mc = concat(fmc.get(), mc.get());
|
|
||||||
in->add(mc.get());
|
|
||||||
}
|
|
||||||
if (m_ctx->canceled())
|
|
||||||
throw tactic_exception(Z3_CANCELED_MSG);
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
case l_false: {
|
|
||||||
if (m_fail_if_inconclusive && !in->unsat_preserved()) {
|
|
||||||
TRACE("smt_tactic", tout << "failed to show to be unsat...\n";);
|
|
||||||
throw tactic_exception("under-approximated goal found to be unsat");
|
|
||||||
}
|
|
||||||
// formula is unsat, reset the goal, and store false there.
|
|
||||||
in->reset();
|
|
||||||
expr_dependency * lcore = nullptr;
|
|
||||||
if (in->unsat_core_enabled()) {
|
|
||||||
unsigned sz = m_ctx->get_unsat_core_size();
|
|
||||||
for (unsigned i = 0; i < sz; i++) {
|
|
||||||
expr * b = m_ctx->get_unsat_core_expr(i);
|
|
||||||
SASSERT(is_uninterp_const(b) && m.is_bool(b));
|
|
||||||
expr * d = bool2dep.find(b);
|
|
||||||
lcore = m.mk_join(lcore, m.mk_leaf(d));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
if (m.proofs_enabled() && !pr) pr = m.mk_asserted(m.mk_false()); // bail out
|
|
||||||
if (pr && m.get_fact(pr) != m.mk_false()) pr = m.mk_asserted(m.mk_false()); // could happen in clause_proof mode
|
|
||||||
in->assert_expr(m.mk_false(), pr, lcore);
|
|
||||||
|
|
||||||
result.push_back(in.get());
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
case l_undef:
|
|
||||||
|
|
||||||
if (m_ctx->canceled() && !pr) {
|
|
||||||
throw tactic_exception(Z3_CANCELED_MSG);
|
|
||||||
}
|
|
||||||
|
|
||||||
if (m_fail_if_inconclusive && !m_candidate_models && !pr) {
|
|
||||||
std::stringstream strm;
|
|
||||||
strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string();
|
|
||||||
throw tactic_exception(strm.str());
|
|
||||||
}
|
|
||||||
result.push_back(in.get());
|
|
||||||
if (pr) {
|
|
||||||
in->reset();
|
|
||||||
in->assert_expr(m.get_fact(pr), pr, nullptr);
|
|
||||||
in->updt_prec(goal::UNDER_OVER);
|
|
||||||
}
|
|
||||||
if (m_candidate_models) {
|
|
||||||
switch (m_ctx->last_failure()) {
|
|
||||||
case smt::NUM_CONFLICTS:
|
|
||||||
case smt::THEORY:
|
|
||||||
case smt::QUANTIFIERS:
|
|
||||||
if (in->models_enabled()) {
|
|
||||||
model_ref md;
|
|
||||||
m_ctx->get_model(md);
|
|
||||||
buffer<symbol> r;
|
|
||||||
m_ctx->get_relevant_labels(nullptr, r);
|
|
||||||
labels_vec rv;
|
|
||||||
rv.append(r.size(), r.data());
|
|
||||||
in->add(model_and_labels2model_converter(md.get(), rv));
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
default:
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (pr) {
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
throw tactic_exception(m_ctx->last_failure_as_string());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
catch (rewriter_exception & ex) {
|
|
||||||
throw tactic_exception(ex.msg());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void* m_user_ctx = nullptr;
|
|
||||||
user_propagator::push_eh_t m_push_eh;
|
|
||||||
user_propagator::pop_eh_t m_pop_eh;
|
|
||||||
user_propagator::fresh_eh_t m_fresh_eh;
|
|
||||||
user_propagator::fixed_eh_t m_fixed_eh;
|
|
||||||
user_propagator::final_eh_t m_final_eh;
|
|
||||||
user_propagator::eq_eh_t m_eq_eh;
|
|
||||||
user_propagator::eq_eh_t m_diseq_eh;
|
|
||||||
expr_ref_vector m_vars;
|
|
||||||
unsigned_vector m_var2internal;
|
|
||||||
unsigned_vector m_internal2var;
|
|
||||||
|
|
||||||
user_propagator::fixed_eh_t i_fixed_eh;
|
|
||||||
user_propagator::final_eh_t i_final_eh;
|
|
||||||
user_propagator::eq_eh_t i_eq_eh;
|
|
||||||
user_propagator::eq_eh_t i_diseq_eh;
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
struct callback : public user_propagator::callback {
|
|
||||||
smt_tactic* t = nullptr;
|
|
||||||
user_propagator::callback* cb = nullptr;
|
|
||||||
unsigned_vector fixed, lhs, rhs;
|
|
||||||
void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) override {
|
|
||||||
fixed.reset();
|
|
||||||
lhs.reset();
|
|
||||||
rhs.reset();
|
|
||||||
for (unsigned i = 0; i < num_fixed; ++i)
|
|
||||||
fixed.push_back(t->m_var2internal[i]);
|
|
||||||
for (unsigned i = 0; i < num_eqs; ++i) {
|
|
||||||
lhs.push_back(t->m_var2internal[eq_lhs[i]]);
|
|
||||||
rhs.push_back(t->m_var2internal[eq_rhs[i]]);
|
|
||||||
}
|
|
||||||
cb->propagate_cb(num_fixed, fixed.data(), num_eqs, lhs.data(), rhs.data(), conseq);
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
callback i_cb;
|
|
||||||
|
|
||||||
void init_i_fixed_eh() {
|
|
||||||
if (!m_fixed_eh)
|
|
||||||
return;
|
|
||||||
i_fixed_eh = [this](void* ctx, user_propagator::callback* cb, unsigned id, expr* value) {
|
|
||||||
i_cb.t = this;
|
|
||||||
i_cb.cb = cb;
|
|
||||||
m_fixed_eh(ctx, &i_cb, m_internal2var[id], value);
|
|
||||||
};
|
|
||||||
m_ctx->user_propagate_register_fixed(i_fixed_eh);
|
|
||||||
}
|
|
||||||
|
|
||||||
void init_i_final_eh() {
|
|
||||||
if (!m_final_eh)
|
|
||||||
return;
|
|
||||||
i_final_eh = [this](void* ctx, user_propagator::callback* cb) {
|
|
||||||
i_cb.t = this;
|
|
||||||
i_cb.cb = cb;
|
|
||||||
m_final_eh(ctx, &i_cb);
|
|
||||||
};
|
|
||||||
m_ctx->user_propagate_register_final(i_final_eh);
|
|
||||||
}
|
|
||||||
|
|
||||||
void init_i_eq_eh() {
|
|
||||||
if (!m_eq_eh)
|
|
||||||
return;
|
|
||||||
i_eq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) {
|
|
||||||
i_cb.t = this;
|
|
||||||
i_cb.cb = cb;
|
|
||||||
m_eq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]);
|
|
||||||
};
|
|
||||||
m_ctx->user_propagate_register_eq(i_eq_eh);
|
|
||||||
}
|
|
||||||
|
|
||||||
void init_i_diseq_eh() {
|
|
||||||
if (!m_diseq_eh)
|
|
||||||
return;
|
|
||||||
i_diseq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) {
|
|
||||||
i_cb.t = this;
|
|
||||||
i_cb.cb = cb;
|
|
||||||
m_diseq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]);
|
|
||||||
};
|
|
||||||
m_ctx->user_propagate_register_diseq(i_diseq_eh);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
void user_propagate_delay_init() {
|
|
||||||
if (!m_user_ctx)
|
|
||||||
return;
|
|
||||||
m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh);
|
|
||||||
init_i_fixed_eh();
|
|
||||||
init_i_final_eh();
|
|
||||||
init_i_eq_eh();
|
|
||||||
init_i_diseq_eh();
|
|
||||||
|
|
||||||
unsigned i = 0;
|
|
||||||
for (expr* v : m_vars) {
|
|
||||||
unsigned j = m_ctx->user_propagate_register(v);
|
|
||||||
m_var2internal.setx(i, j, 0);
|
|
||||||
m_internal2var.setx(j, i, 0);
|
|
||||||
++i;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void user_propagate_init(
|
|
||||||
void* ctx,
|
|
||||||
user_propagator::push_eh_t& push_eh,
|
|
||||||
user_propagator::pop_eh_t& pop_eh,
|
|
||||||
user_propagator::fresh_eh_t& fresh_eh) override {
|
|
||||||
m_vars.reset();
|
|
||||||
m_fixed_eh = nullptr;
|
|
||||||
m_final_eh = nullptr;
|
|
||||||
m_eq_eh = nullptr;
|
|
||||||
m_diseq_eh = nullptr;
|
|
||||||
m_user_ctx = ctx;
|
|
||||||
m_push_eh = push_eh;
|
|
||||||
m_pop_eh = pop_eh;
|
|
||||||
m_fresh_eh = fresh_eh;
|
|
||||||
}
|
|
||||||
|
|
||||||
void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override {
|
|
||||||
m_fixed_eh = fixed_eh;
|
|
||||||
}
|
|
||||||
|
|
||||||
void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override {
|
|
||||||
m_final_eh = final_eh;
|
|
||||||
}
|
|
||||||
|
|
||||||
void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override {
|
|
||||||
m_eq_eh = eq_eh;
|
|
||||||
}
|
|
||||||
|
|
||||||
void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override {
|
|
||||||
m_diseq_eh = diseq_eh;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned user_propagate_register(expr* e) override {
|
|
||||||
m_vars.push_back(e);
|
|
||||||
return m_vars.size() - 1;
|
|
||||||
}
|
|
||||||
};
|
|
||||||
|
|
||||||
static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) {
|
|
||||||
return alloc(smt_tactic, m, p);
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
|
|
||||||
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
|
|
||||||
}
|
|
||||||
|
|
||||||
tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) {
|
|
||||||
parallel_params pp(p);
|
|
||||||
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(m, p);
|
|
||||||
}
|
|
||||||
|
|
||||||
tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) {
|
|
||||||
parallel_params pp(_p);
|
|
||||||
params_ref p = _p;
|
|
||||||
p.set_bool("auto_config", auto_config);
|
|
||||||
return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(m, p), p);
|
|
||||||
}
|
|
||||||
|
|
||||||
Loading…
Reference in a new issue