mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-18 16:56:53 -08:00
parent 6d23847482
commit 5d4c18dde2
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -573,6 +573,7 @@ namespace intblast {
r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1)); r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1));
break; break;
case OP_SGEQ: case OP_SGEQ:
bv_expr = e->get_arg(0);
r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1)); r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1));
break; break;
case OP_SLT: case OP_SLT:
@ -902,6 +903,12 @@ namespace intblast {
if (!is_app(n->get_expr())) if (!is_app(n->get_expr()))
return false; return false;
app* e = to_app(n->get_expr()); app* e = to_app(n->get_expr());
expr *th, * el, * c;
if (m.is_ite(e, c, th, el)) {
dep.add(n, expr2enode(th)->get_root());
dep.add(n, expr2enode(el)->get_root());
return true;
}
if (n->num_args() == 0) { if (n->num_args() == 0) {
dep.insert(n, nullptr); dep.insert(n, nullptr);
return true; return true;
@ -940,6 +947,15 @@ namespace intblast {
void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) { void solver::add_value_plugin(euf::enode* n, model& mdl, expr_ref_vector& values) {
expr_ref value(m); expr_ref value(m);
expr* e = n->get_expr(), *c, *th, *el;
while (m.is_ite(e, c, th, el)) {
auto thn = expr2enode(th);
if (thn->get_root() == n->get_root())
e = th;
else
e = el;
n = expr2enode(e);
}
if (n->interpreted()) if (n->interpreted())
value = n->get_expr(); value = n->get_expr();
else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) { else if (to_app(n->get_expr())->get_family_id() == bv.get_family_id()) {