mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

integrate intblast solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-10 13:00:43 -08:00
parent 81411a5fcb
commit d72938ba9a
4 changed files with 56 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -233,6 +233,7 @@ namespace intblast {
literals.push_back(a);
}
m_core.reset();
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
expr_ref_vector es(m);
@ -241,11 +242,23 @@ namespace intblast {
translate(es);
for (auto e : es)
m_solver->assert_expr(e);
for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi;
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
lbool r = m_solver->check_sat(0, nullptr);
lbool r = m_solver->check_sat(es);
if (r == l_false) {
expr_ref_vector core(m);
m_solver->get_unsat_core(core);
obj_map<expr, unsigned> 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]]);
}
return r;
};
@ -573,6 +586,7 @@ namespace intblast {
}
break;
}
<<<<<<< HEAD
case OP_EXTRACT: {
unsigned lo, hi;
expr* old_arg;
@ -846,6 +860,10 @@ namespace intblast {
set_translated(e, e);
else
set_translated(e, m.mk_app(e->get_decl(), m_args));
=======
for (unsigned i = 0; i < es.size(); ++i)
es[i] = translated[es.get(i)];
>>>>>>> 09c2e0dd6 (integrate intblast solver)
}
rational solver::get_value(expr* e) const {