From 305e080239a4824e13ed25ce9c8a31433d176442 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Nov 2016 17:57:28 +0100 Subject: [PATCH] enable unsat core extraction in nlsat_tactic Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 10 +++++++++- src/nlsat/nlsat_solver.h | 8 ++++++++ src/nlsat/tactic/nlsat_tactic.cpp | 15 +++++++++++++-- src/sat/tactic/sat_tactic.cpp | 7 ++++--- src/smt/tactic/smt_tactic.cpp | 9 ++------- src/solver/solver2tactic.cpp | 8 +++----- src/solver/tactic2solver.cpp | 4 +++- src/tactic/goal.cpp | 3 +++ src/test/sorting_network.cpp | 2 +- 9 files changed, 46 insertions(+), 20 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 4f9854d87..7582c8389 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1283,7 +1283,7 @@ namespace nlsat { if (r == l_false) { // collect used literals from m_lemma_assumptions vector deps; - m_asm.linearize(m_lemma_assumptions.get(), deps); + get_core(deps); for (unsigned i = 0; i < deps.size(); ++i) { literal const* lp = (literal const*)(deps[i]); if (ptr <= lp && lp < ptr + sz) { @@ -1299,6 +1299,10 @@ namespace nlsat { return r; } + void get_core(vector& deps) { + m_asm.linearize(m_lemma_assumptions.get(), deps); + } + void collect(literal_vector const& assumptions, clause_vector& clauses) { unsigned n = clauses.size(); unsigned j = 0; @@ -2712,6 +2716,10 @@ namespace nlsat { return m_imp->check(assumptions); } + void solver::get_core(vector& assumptions) { + return m_imp->get_core(assumptions); + } + void solver::reset() { m_imp->reset(); } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index eec5ba19f..3668629cd 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -195,6 +195,14 @@ namespace nlsat { lbool value(literal l) const; + // ----------------------- + // + // Core + // + // ----------------------- + + void get_core(vector& deps); + // ----------------------- // // Misc diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 14b2a6d32..b648866ef 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -147,6 +147,7 @@ class nlsat_tactic : public tactic { TRACE("nlsat", g->display(tout);); expr2var a2b(m); expr2var t2x(m); + m_g2nl(*g, m_params, m_solver, a2b, t2x); m_display_var.m_var2expr.reset(); @@ -172,9 +173,19 @@ class nlsat_tactic : public tactic { } } else { - // TODO: extract unsat core - g->assert_expr(m.mk_false(), 0, 0); + expr_dependency* lcore = 0; + if (g->unsat_core_enabled()) { + vector assumptions; + m_solver.get_core(assumptions); + for (unsigned i = 0; i < assumptions.size(); ++i) { + expr_dependency* d = static_cast(assumptions[i]); + lcore = m.mk_join(lcore, d); + } + } + g->assert_expr(m.mk_false(), 0, lcore); + core = lcore; } + g->inc_depth(); result.push_back(g.get()); TRACE("nlsat", g->display(tout);); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index da513d97b..e28f64f23 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -73,14 +73,15 @@ class sat_tactic : public tactic { if (r == l_false) { expr_dependency * lcore = 0; if (produce_core) { - sat::literal_vector const& core = m_solver.get_core(); + sat::literal_vector const& ucore = m_solver.get_core(); u_map asm2dep; mk_asm2dep(dep2asm, asm2dep); - for (unsigned i = 0; i < core.size(); ++i) { - sat::literal lit = core[i]; + for (unsigned i = 0; i < ucore.size(); ++i) { + sat::literal lit = ucore[i]; 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 2909d8848..dd0eff889 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -138,6 +138,7 @@ public: proof_converter_ref & pc, expr_dependency_ref & core) { try { + mc = 0; pc = 0; core = 0; SASSERT(in->is_well_sorted()); ast_manager & m = in->m(); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " @@ -206,8 +207,6 @@ public: mc = model2model_converter(md.get()); mc = concat(fmc.get(), mc.get()); } - pc = 0; - core = 0; return; } case l_false: { @@ -229,12 +228,10 @@ 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()); - mc = 0; - pc = 0; - core = 0; return; } case l_undef: @@ -257,8 +254,6 @@ public: m_ctx->get_model(md); mc = model2model_converter(md.get()); } - pc = 0; - core = 0; return; default: break; diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 76ebf73dd..21ecdec32 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -105,6 +105,7 @@ public: /* out */ model_converter_ref & mc, /* out */ proof_converter_ref & pc, /* out */ expr_dependency_ref & core) { + pc = 0; mc = 0; core = 0; expr_ref_vector clauses(m); expr2expr_map bool2dep; ptr_vector assumptions; @@ -123,8 +124,6 @@ public: } in->reset(); result.push_back(in.get()); - pc = 0; - core = 0; break; case l_false: { in->reset(); @@ -132,6 +131,7 @@ public: expr_dependency* lcore = 0; if (in->proofs_enabled()) { pr = local_solver->get_proof(); + pc = proof2proof_converter(m, pr); } if (in->unsat_core_enabled()) { ptr_vector core; @@ -142,9 +142,7 @@ public: } in->assert_expr(m.mk_false(), pr, lcore); result.push_back(in.get()); - mc = 0; - pc = 0; - core = 0; + core = lcore; break; } case l_undef: diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 213ba5c1c..34d2edd3c 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -137,7 +137,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass g->assert_expr(m_assertions.get(i)); } for (unsigned i = 0; i < num_assumptions; i++) { - g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i])); + proof_ref pr(m.mk_asserted(assumptions[i]), m); + expr_dependency_ref ans(m.mk_leaf(assumptions[i]), m); + g->assert_expr(assumptions[i], pr, ans); } model_ref md; diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 8897a83f8..b14d2676c 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -237,6 +237,9 @@ void goal::slow_process(expr * f, proof * pr, expr_dependency * d) { } void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) { + expr_ref _f(f, m()); + proof_ref _pr(pr, m()); + expr_dependency_ref _d(d, m()); SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr))); if (m_inconsistent) return; diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index a64d3a70f..090770d0b 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -200,7 +200,7 @@ static void test_sorting_eq(unsigned n, unsigned k) { // equality: std::cout << "eq " << k << "\n"; solver.push(); - result = sn.eq(k, in.size(), in.c_ptr()); + result = sn.eq(true, k, in.size(), in.c_ptr()); solver.assert_expr(result); for (unsigned i = 0; i < ext.m_clauses.size(); ++i) { solver.assert_expr(ext.m_clauses[i].get());