mirror of
https://github.com/Z3Prover/z3
synced 2025-04-20 23:56:37 +00:00
DoC: compact result of substract and maintain invariant
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
parent
1606359dc9
commit
8d1177bf3f
|
@ -472,15 +472,15 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
|
|||
tbv_ref t(m);
|
||||
r = allocate(A);
|
||||
t = m.allocate(B.pos());
|
||||
if (m.set_and(*t, A.pos()) && r->neg().insert(m, t.detach())) {
|
||||
result.push_back(r.detach());
|
||||
}
|
||||
else {
|
||||
result.push_back(allocate(A));
|
||||
if (m.set_and(*t, A.pos())) {
|
||||
r->neg().insert(m, t.detach());
|
||||
}
|
||||
result.push_back(r.detach());
|
||||
|
||||
for (unsigned i = 0; i < B.neg().size(); ++i) {
|
||||
r = allocate(A);
|
||||
if (set_and(*r, B.neg()[i])) {
|
||||
r->neg().intersect(m, r->pos());
|
||||
result.push_back(r.detach());
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue