mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

reorg if-then-else structure

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-08 10:00:45 -07:00
parent 72a6384353
commit 6a1193eebd
1 changed files with 12 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_user_propagator.cpp
View file

@ -183,11 +183,13 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
} }
} }
if (!th && v == null_theory_var) if (v == null_theory_var && !th)
return;
if (v == null_theory_var && th->get_family_id() != bv.get_fid())
return; return;
if (v == null_theory_var) { if (v == null_theory_var) {
if (th->get_family_id() == bv.get_fid()) {
// it is not a registered boolean value but it is a bitvector // it is not a registered boolean value but it is a bitvector
auto registered_bv = ((theory_bv*)th)->get_bv_with_theory(var, get_family_id()); auto registered_bv = ((theory_bv*)th)->get_bv_with_theory(var, get_family_id());
if (!registered_bv.first) if (!registered_bv.first)
@ -197,9 +199,6 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
original_bit = registered_bv.second; original_bit = registered_bv.second;
v = original_enode->get_th_var(get_family_id()); v = original_enode->get_th_var(get_family_id());
} }
else
return;
}
// call the registered callback // call the registered callback
unsigned new_bit = original_bit; unsigned new_bit = original_bit;
@ -228,11 +227,9 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
// expression was set to a bit-vector // expression was set to a bit-vector
auto th_bv = (theory_bv*)ctx.get_theory(bv.get_fid()); auto th_bv = (theory_bv*)ctx.get_theory(bv.get_fid());
bool_var new_var = th_bv->get_first_unassigned(new_bit, new_enode); bool_var new_var = th_bv->get_first_unassigned(new_bit, new_enode);
if (new_var != null_bool_var)
if (new_var != null_bool_var) {
var = new_var; var = new_var;
} }
}
// in case the callback did not decide on a truth value -> let Z3 decide // in case the callback did not decide on a truth value -> let Z3 decide
is_pos = ctx.guess(var, phase); is_pos = ctx.guess(var, phase);