mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

updated mini

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-26 15:44:49 -08:00
parent c6539deb61
commit 53f72d9cbe
1 changed files with 5 additions and 2 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()