From f61600d1d833fff241376ad340244068fe7ece21 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Nov 2016 14:14:55 +0000 Subject: [PATCH] fixing unsat core extraction for tactics Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tactic_cmds.cpp | 2 -- src/nlsat/tactic/nlsat_tactic.cpp | 1 - src/sat/tactic/sat_tactic.cpp | 1 - src/smt/tactic/smt_tactic.cpp | 1 - src/solver/combined_solver.cpp | 8 ++--- src/tactic/core/cofactor_term_ite_tactic.cpp | 2 +- src/tactic/core/pb_preprocess_tactic.cpp | 30 +++++++++++-------- src/tactic/smtlogics/qfuf_tactic.cpp | 2 +- src/tactic/tactical.cpp | 5 ++-- src/tactic/ufbv/ufbv_tactic.cpp | 31 ++++++++++---------- 10 files changed, 42 insertions(+), 41 deletions(-) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 86900e175..91963fa0d 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -288,9 +288,7 @@ public: #endif p.insert("print_model_converter", CPK_BOOL, "(default: false) print model converter."); p.insert("print_benchmark", CPK_BOOL, "(default: false) display resultant goals as a SMT2 benchmark."); -#ifndef _EXTERNAL_RELEASE p.insert("print_dependencies", CPK_BOOL, "(default: false) print dependencies when displaying the resultant set of goals."); -#endif exec_given_tactic_cmd::init_pdescrs(ctx, p); } diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index b648866ef..4ecdade38 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -183,7 +183,6 @@ class nlsat_tactic : public tactic { } } g->assert_expr(m.mk_false(), 0, lcore); - core = lcore; } g->inc_depth(); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index e28f64f23..f99e46851 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -81,7 +81,6 @@ class sat_tactic : public tactic { expr* dep = asm2dep.find(lit.index()); lcore = m.mk_join(lcore, m.mk_leaf(dep)); } - core = lcore; } g->assert_expr(m.mk_false(), 0, lcore); } diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index dd0eff889..c9e0ddc69 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -228,7 +228,6 @@ public: expr * d = bool2dep.find(b); lcore = m.mk_join(lcore, m.mk_leaf(d)); } - core = lcore; } in->assert_expr(m.mk_false(), pr, lcore); result.push_back(in.get()); diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 7f5f6872e..1eb6be08e 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -217,7 +217,7 @@ public: m_use_solver1_results = false; if (get_num_assumptions() != 0 || - num_assumptions > 0 || // assumptions were provided + num_assumptions > 0 || // assumptions were provided m_ignore_solver1) { // must use incremental solver switch_inc_mode(); @@ -227,7 +227,7 @@ public: if (m_inc_mode) { if (m_inc_timeout == UINT_MAX) { IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";); - lbool r = m_solver2->check_sat(0, 0); + lbool r = m_solver2->check_sat(num_assumptions, assumptions); if (r != l_undef || !use_solver1_when_undef()) { return r; } @@ -238,7 +238,7 @@ public: lbool r = l_undef; try { scoped_timer timer(m_inc_timeout, &eh); - r = m_solver2->check_sat(0, 0); + r = m_solver2->check_sat(num_assumptions, assumptions); } catch (z3_exception&) { if (!eh.m_canceled) { @@ -254,7 +254,7 @@ public: IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";); m_use_solver1_results = true; - return m_solver1->check_sat(0, 0); + return m_solver1->check_sat(num_assumptions, assumptions); } virtual void set_progress_callback(progress_callback * callback) { diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 24b381476..2286281f4 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -36,7 +36,7 @@ class cofactor_term_ite_tactic : public tactic { expr * f = g.form(i); expr_ref new_f(m); m_elim_ite(f, new_f); - g.update(i, new_f); + g.update(i, new_f, 0, g.dep(i)); } } diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index b4f335db5..a7e381576 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -151,9 +151,6 @@ public: SASSERT(g->is_well_sorted()); pc = 0; core = 0; - if (g->unsat_core_enabled()) { - throw tactic_exception("pb-preprocess does not support cores"); - } if (g->proofs_enabled()) { throw tactic_exception("pb-preprocess does not support proofs"); } @@ -202,6 +199,7 @@ public: while (it != m_vars.end()) { app * e = it->m_key; rec const& r = it->m_value; + TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";); if (r.pos.empty()) { replace(r.neg, e, m.mk_false(), g); mc.set_value(e, false); @@ -249,11 +247,11 @@ public: unsigned_vector const& pos = neg?r.neg:r.pos; for (unsigned j = 0; j < pos.size(); ++j) { unsigned k = pos[j]; - if (k == i) continue; + if (k == m_ge[i]) continue; if (!to_ge(g->form(k), args2, coeffs2, k2)) continue; if (subsumes(args1, coeffs1, k1, args2, coeffs2, k2)) { IF_VERBOSE(3, verbose_stream() << "replace " << mk_pp(g->form(k), m) << "\n";); - g->update(k, m.mk_true()); + g->update(k, m.mk_true(), 0, m.mk_join(g->dep(m_ge[i]), g->dep(k))); m_progress = true; } } @@ -299,7 +297,7 @@ private: args.push_back(negate(to_app(r)->get_arg(j))); } tmp = pb.mk_ge(args.size(), coeffs.c_ptr(), args.c_ptr(), sum - k + rational::one()); - g->update(i, tmp); + g->update(i, tmp, g->pr(i), g->dep(i)); } } } @@ -331,12 +329,12 @@ private: for (unsigned j = 0; j < cuts.size(); ++j) { unsigned end = cuts[j]; fml1 = decompose_cut(a, start, end, cut_args, cut_coeffs); - g->assert_expr(fml1); + g->assert_expr(fml1, 0, g->dep(i)); start = end; TRACE("pb", tout << fml1 << "\n";); } fml2 = pb.mk_ge(cut_args.size(), cut_coeffs.c_ptr(), cut_args.c_ptr(), pb.get_k(e)); - g->update(i, fml2); + g->update(i, fml2, 0, g->dep(i)); TRACE("pb", tout << fml2 << "\n";); } } @@ -577,8 +575,12 @@ private: verbose_stream() << "resolve: " << mk_pp(fml1, m) << "\n" << mk_pp(fml2, m) << "\n" << tmp1 << "\n"; verbose_stream() << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";); - g->update(idx1, m.mk_true()); // proof & dependencies - g->update(idx2, tmp2); // proof & dependencies + TRACE("pb", + tout << "resolve: " << mk_pp(fml1, m) << "\n" << mk_pp(fml2, m) << "\n" << tmp1 << "\n"; + tout << "to\n" << mk_pp(fml2, m) << " -> " << tmp2 << "\n";); + + g->update(idx2, tmp2, 0, m.mk_join(g->dep(idx1), g->dep(idx2))); + g->update(idx1, m.mk_true(), 0, 0); m_progress = true; //IF_VERBOSE(0, if (!g->inconsistent()) display_annotation(verbose_stream(), g);); } @@ -634,14 +636,18 @@ private: for (unsigned i = 0; i < positions.size(); ++i) { unsigned idx = positions[i]; expr_ref f(m); + proof_ref new_pr(m); f = g->form(idx); if (!m.is_true(f)) { - m_r(f, tmp); + m_r(f, tmp, new_pr); if (tmp != f) { TRACE("pb", tout << mk_pp(f, m) << " -> " << tmp << " by " << mk_pp(e, m) << " |-> " << mk_pp(v, m) << "\n";); IF_VERBOSE(3, verbose_stream() << "replace " << mk_pp(f, m) << " -> " << tmp << "\n";); - g->update(idx, tmp); // proof & dependencies. + if (g->proofs_enabled()) { + new_pr = m.mk_modus_ponens(g->pr(idx), new_pr); + } + g->update(idx, tmp, new_pr, g->dep(idx)); m_progress = true; } } diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index 567325f6a..7648e20fe 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -33,7 +33,7 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) { mk_propagate_values_tactic(m, p), mk_solve_eqs_tactic(m, p), using_params(mk_simplify_tactic(m, p), s2_p), - mk_symmetry_reduce_tactic(m, p), + if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))), mk_smt_tactic(p)); } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 0d276ba72..4cb212265 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -132,8 +132,7 @@ public: if (r1_size == 1) { if (r1[0]->is_decided()) { result.push_back(r1[0]); - if (models_enabled) mc = mc1; - SASSERT(!pc); SASSERT(!core); + if (models_enabled) mc = mc1; return; } goal_ref r1_0 = r1[0]; @@ -964,7 +963,7 @@ class repeat_tactical : public unary_tactical { pc = 0; core = 0; { - goal orig_in(in->m()); + goal orig_in(in->m(), proofs_enabled, models_enabled, cores_enabled); orig_in.copy_from(*(in.get())); m_t->operator()(in, r1, mc1, pc1, core1); if (is_equal(orig_in, *(in.get()))) { diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index b5a4ca3a3..7a185c854 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -41,21 +41,22 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_trace_tactic("ufbv_pre"), - and_then(mk_simplify_tactic(m, p), - mk_propagate_values_tactic(m, p), - and_then(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and), - mk_simplify_tactic(m, p)), - and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), - mk_elim_and_tactic(m, p), - mk_solve_eqs_tactic(m, p), - and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_distribute_forall_tactic(m, p), mk_simplify_tactic(m, p))), - and_then(and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), - mk_simplify_tactic(m, p)), + and_then(mk_simplify_tactic(m, p), + mk_propagate_values_tactic(m, p), + and_then(if_no_proofs(if_no_unsat_cores(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and))), + mk_simplify_tactic(m, p)), + and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), + mk_elim_and_tactic(m, p), + mk_solve_eqs_tactic(m, p), + and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_distribute_forall_tactic(m, p), mk_simplify_tactic(m, p))), + if_no_unsat_cores( + and_then(and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)))), + and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), + mk_simplify_tactic(m, p), mk_trace_tactic("ufbv_post")); }