mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 02:46:16 +00:00
Code Activity

factor cache pointers are invalid if the table is resized

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-26 16:18:18 -08:00
parent d1fcc41c7f
commit 0eaf5a8510
2 changed files with 7 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
examples/python/mini_ic3.py
View file

@ -162,6 +162,9 @@ class Goal:
self.cube = cube self.cube = cube
self.parent = parent self.parent = parent
def __lt__(self, other):
return self.level < other.level
def is_seq(f): def is_seq(f):
return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector) return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector)
@ -210,12 +213,12 @@ class MiniIC3:
def next(self, f): def next(self, f):
if is_seq(f): if is_seq(f):
return [self.next(f1) for f1 in f] return [self.next(f1) for f1 in f]
return substitute(f, zip(self.x0, self.xn)) return substitute(f, [p for p in zip(self.x0, self.xn)])
def prev(self, f): def prev(self, f):
if is_seq(f): if is_seq(f):
return [self.prev(f1) for f1 in f] return [self.prev(f1) for f1 in f]
return substitute(f, zip(self.xn, self.x0)) return substitute(f, [p for p in zip(self.xn, self.x0)])
def add_solver(self): def add_solver(self):
s = fd_solver() s = fd_solver()

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

@ -890,12 +890,8 @@ namespace dd {
rest = p; rest = p;
} }
} }
if (gc_generation != m_gc_generation) { et = m_factor_cache.insert_if_not_there2({p.root, v, degree});
// Cache was reset while factoring (due to GC), e = &et->get_data();
// which means the old entry has been removed and we need to insert it again.
auto* et = m_factor_cache.insert_if_not_there2({p.root, v, degree});
e = &et->get_data();
}
e->m_lc = lc.root; e->m_lc = lc.root;
e->m_rest = rest.root; e->m_rest = rest.root;
} }