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

add missing scoped_push

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-21 18:06:28 -08:00
parent c4da5caf69
commit 3fca59ac84
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/dd/dd_bdd.cpp
View file

@ -83,13 +83,14 @@ namespace dd {
bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) {
bool first = true;
SASSERT(well_formed());
scoped_push _sp(*this);
while (true) {
try {
return apply_rec(arg1, arg2, op);
}
catch (const mem_out &) {
try_reorder();
if (!first) throw;
try_reorder();
first = false;
}
}
@ -542,13 +543,14 @@ namespace dd {
bdd bdd_manager::mk_not(bdd b) {
bool first = true;
scoped_push _sp(*this);
while (true) {
try {
return bdd(mk_not_rec(b.root), this);
}
catch (const mem_out &) {
try_reorder();
if (!first) throw;
try_reorder();
first = false;
}
}
@ -571,13 +573,14 @@ namespace dd {
bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) {
bool first = true;
scoped_push _sp(*this);
while (true) {
try {
return bdd(mk_ite_rec(c.root, t.root, e.root), this);
}
catch (const mem_out &) {
try_reorder();
if (!first) throw;
try_reorder();
first = false;
}
}

7
src/math/dd/dd_bdd.h
View file

@ -193,6 +193,13 @@ namespace dd {
void reserve_var(unsigned v);
bool well_formed();
struct scoped_push {
bdd_manager& m;
unsigned m_size;
scoped_push(bdd_manager& m) :m(m), m_size(m.m_bdd_stack.size()) {}
~scoped_push() { m.m_bdd_stack.shrink(m_size); }
};
public:
struct mem_out {};