From 0242566792d858275b39175936ad35e1faa22c63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Dec 2021 11:54:05 -0800 Subject: [PATCH] remove --- .../smt_tactic_core.cpp | 474 ------------------ 1 file changed, 474 deletions(-) delete mode 100644 enc_temp_folder/fe6ce1b742e2a086b6bab9a9a6a6456b/smt_tactic_core.cpp diff --git a/enc_temp_folder/fe6ce1b742e2a086b6bab9a9a6a6456b/smt_tactic_core.cpp b/enc_temp_folder/fe6ce1b742e2a086b6bab9a9a6a6456b/smt_tactic_core.cpp deleted file mode 100644 index 8aae7a19749..00000000000 --- a/enc_temp_folder/fe6ce1b742e2a086b6bab9a9a6a6456b/smt_tactic_core.cpp +++ /dev/null @@ -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 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 assumptions; - ref 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 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 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); -} -