From 0eaf5a85103f4eb47d8c2037a02a65bd61df34db Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Jan 2022 16:18:18 -0800 Subject: [PATCH] factor cache pointers are invalid if the table is resized Signed-off-by: Nikolaj Bjorner --- examples/python/mini_ic3.py | 7 +++++-- src/math/dd/dd_pdd.cpp | 8 ++------ 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/examples/python/mini_ic3.py b/examples/python/mini_ic3.py index b7b732459..31d3c595b 100644 --- a/examples/python/mini_ic3.py +++ b/examples/python/mini_ic3.py @@ -162,6 +162,9 @@ class Goal: self.cube = cube self.parent = parent + def __lt__(self, other): + return self.level < other.level + def is_seq(f): return isinstance(f, list) or isinstance(f, tuple) or isinstance(f, AstVector) @@ -210,12 +213,12 @@ class MiniIC3: def next(self, f): if is_seq(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): if is_seq(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): s = fd_solver() diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 421441af9..63a38be36 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -890,12 +890,8 @@ namespace dd { rest = p; } } - if (gc_generation != m_gc_generation) { - // Cache was reset while factoring (due to GC), - // 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(); - } + et = m_factor_cache.insert_if_not_there2({p.root, v, degree}); + e = &et->get_data(); e->m_lc = lc.root; e->m_rest = rest.root; }