mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

share subst node

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-23 10:39:42 +01:00
parent cbbf1381f7
commit 5e1ad37533
1 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/math/dd/dd_pdd.cpp
View file

@ -261,9 +261,6 @@ namespace dd {
if (is_one(p)) return q;
SASSERT(!is_val(p));
SASSERT(!is_val(q));
if (level(p) < level(q))
// p*hi(q) + lo(q)
return make_node(level(q), lo(q), p);
break;
default:
UNREACHABLE();
@ -425,10 +422,16 @@ namespace dd {
case pdd_subst_add_op:
SASSERT(!is_val(p));
SASSERT(!is_val(q));
SASSERT(level_p > level_q);
push(apply_rec(hi(p), q, pdd_subst_add_op)); // hi := add_subst(hi(p), q)
r = make_node(level_p, lo(p), read(1)); // r := hi*var(p) + lo(p)
npop = 1;
SASSERT(level_p != level_q);
if (level_p < level_q) {
r = make_node(level_q, lo(q), p); // p*hi(q) + lo(q)
npop = 0;
}
else {
push(apply_rec(hi(p), q, pdd_subst_add_op)); // hi := add_subst(hi(p), q)
r = make_node(level_p, lo(p), read(1)); // r := hi*var(p) + lo(p)
npop = 1;
}
break;
default:
r = null_pdd;