From 45b0be3b37fab08911fa4a2ca7a40f8cffd309ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Dec 2023 12:53:51 -0800 Subject: [PATCH] working on model extraction Signed-off-by: Nikolaj Bjorner --- src/sat/smt/intblast_solver.cpp | 19 +++++++++++-------- src/sat/smt/polysat_internalize.cpp | 10 +++++----- 2 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 06e6f6770..3a5c316b0 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -248,18 +248,17 @@ namespace intblast { for (auto const& [src, vi] : m_vars) { auto const& [v, b] = vi; - verbose_stream() << "asserting " << mk_pp(v, m) << " < " << b << "\n"; m_solver->assert_expr(a.mk_le(a.mk_int(0), v)); m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); } - verbose_stream() << "check\n"; - m_solver->display(verbose_stream()); - verbose_stream() << es << "\n"; + IF_VERBOSE(10, verbose_stream() << "check\n"; + m_solver->display(verbose_stream()); + verbose_stream() << es << "\n"); lbool r = m_solver->check_sat(es); - verbose_stream() << "result " << r << "\n"; + IF_VERBOSE(2, verbose_stream() << "(sat.intblast :result " << r << ")\n"); if (r == l_false) { expr_ref_vector core(m); @@ -267,8 +266,13 @@ namespace intblast { obj_map e2index; for (unsigned i = 0; i < es.size(); ++i) e2index.insert(es.get(i), i); - for (auto e : core) - m_core.push_back(literals[e2index[e]]); + for (auto e : core) { + unsigned idx = e2index[e]; + if (idx < literals.size()) + m_core.push_back(literals[idx]); + else + m_core.push_back(ctx.mk_literal(e)); + } } return r; @@ -301,7 +305,6 @@ namespace intblast { sorted.push_back(arg); } } - } else if (is_quantifier(e)) { quantifier* q = to_quantifier(e); diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 4eeec3da4..46c1e293f 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -347,13 +347,13 @@ namespace polysat { unsigned sz2 = sz - arg_sz; var2pdd(expr2enode(e)->get_th_var(get_id())); if (arg_sz == sz) - add_clause(eq_internalize(e, arg), false); + add_clause(eq_internalize(e, arg), nullptr); else { sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz))); // arg < 0 ==> e = concat(arg, 1...1) // arg >= 0 ==> e = concat(arg, 0...0) - add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), false); - add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false); + add_clause(lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2))), nullptr); + add_clause(~lt0, eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr); } } @@ -364,10 +364,10 @@ namespace polysat { unsigned sz2 = sz - arg_sz; var2pdd(expr2enode(e)->get_th_var(get_id())); if (arg_sz == sz) - add_clause(eq_internalize(e, arg), false); + add_clause(eq_internalize(e, arg), nullptr); else // e = concat(arg, 0...0) - add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), false); + add_clause(eq_internalize(e, bv.mk_concat(arg, bv.mk_numeral(0, sz2))), nullptr); } void solver::internalize_div_rem(app* e, bool is_div) {