mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 07:15:26 +00:00
Code Activity

working on model extraction

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-11 12:53:51 -08:00
parent fbecbd7d70
commit 45b0be3b37
2 changed files with 16 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/sat/smt/intblast_solver.cpp
View file

@ -248,18 +248,17 @@ namespace intblast {
for (auto const& [src, vi] : m_vars) { for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi; 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_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b))); m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
} }
verbose_stream() << "check\n"; IF_VERBOSE(10, verbose_stream() << "check\n";
m_solver->display(verbose_stream()); m_solver->display(verbose_stream());
verbose_stream() << es << "\n"; verbose_stream() << es << "\n");
lbool r = m_solver->check_sat(es); 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) { if (r == l_false) {
expr_ref_vector core(m); expr_ref_vector core(m);
@ -267,8 +266,13 @@ namespace intblast {
obj_map<expr, unsigned> e2index; obj_map<expr, unsigned> e2index;
for (unsigned i = 0; i < es.size(); ++i) for (unsigned i = 0; i < es.size(); ++i)
e2index.insert(es.get(i), i); e2index.insert(es.get(i), i);
for (auto e : core) for (auto e : core) {
m_core.push_back(literals[e2index[e]]); 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; return r;
@ -301,7 +305,6 @@ namespace intblast {
sorted.push_back(arg); sorted.push_back(arg);
} }
} }
} }
else if (is_quantifier(e)) { else if (is_quantifier(e)) {
quantifier* q = to_quantifier(e); quantifier* q = to_quantifier(e);

10
src/sat/smt/polysat_internalize.cpp
View file

@ -347,13 +347,13 @@ namespace polysat {
unsigned sz2 = sz - arg_sz; unsigned sz2 = sz - arg_sz;
var2pdd(expr2enode(e)->get_th_var(get_id())); var2pdd(expr2enode(e)->get_th_var(get_id()));
if (arg_sz == sz) if (arg_sz == sz)
add_clause(eq_internalize(e, arg), false); add_clause(eq_internalize(e, arg), nullptr);
else { else {
sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz))); 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, 1...1)
// arg >= 0 ==> e = concat(arg, 0...0) // 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(rational::power_of_two(sz2) - 1, sz2))), nullptr);
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(0, sz2))), nullptr);
} }
} }
@ -364,10 +364,10 @@ namespace polysat {
unsigned sz2 = sz - arg_sz; unsigned sz2 = sz - arg_sz;
var2pdd(expr2enode(e)->get_th_var(get_id())); var2pdd(expr2enode(e)->get_th_var(get_id()));
if (arg_sz == sz) if (arg_sz == sz)
add_clause(eq_internalize(e, arg), false); add_clause(eq_internalize(e, arg), nullptr);
else else
// e = concat(arg, 0...0) // 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) { void solver::internalize_div_rem(app* e, bool is_div) {