From 53f72d9cbe310f2d2fbc509127fb369de957058b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Jan 2022 15:44:49 -0800 Subject: [PATCH] updated mini Signed-off-by: Nikolaj Bjorner --- examples/python/mini_ic3.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 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()