From fbd51981c302bbd3339b154b63b1e65365bc435a Mon Sep 17 00:00:00 2001 From: "Guangyu (Gary) HU" <43922980+Gy-Hu@users.noreply.github.com> Date: Fri, 10 Apr 2026 05:30:26 +0800 Subject: [PATCH] mini_quip: port to Python 3 and fix several bugs (#9246) * mini_quip: port to Python 3 and fix several bugs examples/python/mini_quip.py was Python 2 only and had several latent bugs that prevented it from running on Python 3 or producing correct results on benchmarks beyond horn1..5. Python 3 / import fixes: - Convert `print stmt` to `print(...)` calls (lines 457-458, 567, 710, 747, 765, 776). - The bare `print("Test file: %s") % file` form was applying `%` to the return value of print() (None); rewrite as `print("Test file: %s" % file)`. - Add `import sys` (used by sys.stdout.write/flush) and `import copy` (used by QReach.state2cube via copy.deepcopy); neither was previously imported. - next()/prev() passed `zip(...)` directly to z3.substitute. In Python 3 zip returns a one-shot generator; wrap with list() the same way mini_ic3 already does. Bug fixes: - is_transition(): when an init rule's body is an And without any Invariant predicate, is_body() returns (And(...), None). The function then passed inv0=None to subst_vars and crashed inside get_vars(). Add an explicit None check so the rule falls through to is_init() (same fix as mini_ic3). - generalize(): guard against an empty unsat core. Without the guard, an empty core can be returned and become cube2clause([])=Or([])=False, poisoning all frames (same class of bug as in mini_ic3). - check_reachable(): self.prev(cube) on an empty cube produced an empty list which was then added to a solver as a no-op constraint, so an empty cube would always look reachable. Only add the constraint when cube is non-empty. - quip_blocked() at f==0 for must goals contained `assert is_sat == s.check()` where `is_sat` is undefined in that scope; the intent is `assert sat == s.check()`. - Inside the lemma-pushing loop in quip_blocked(), `is_sat == unsat` was a comparison whose result was discarded; the intended assignment is `is_sat = unsat`. Verified on horn1..5 (unchanged behavior, all return same SAFE/UNSAFE result and validate). Larger benchmarks (h_CRC, h_FIFO, cache_coherence_three) now at least run without exceptions (performance is a separate matter). * mini_quip: guard against None from QReach.intersect in CEX trace loop In quip_blocked, the must-goal CEX-tracing loop calls self.reachable.intersect(self.prev(r)) and immediately uses r.children() on the result. QReach.intersect can return None when the model literals do not match any state in the partial reachable set, which crashes with AttributeError: 'NoneType' object has no attribute 'children'. Reproduces on data/h_FIFO.smt2. Fix: save the model, and when intersect returns None fall back to the raw self.project0(model) as the predecessor cube. This still gives a concrete predecessor and lets the CEX trace make progress instead of crashing. --- examples/python/mini_quip.py | 42 +++++++++++++++++++++++------------- 1 file changed, 27 insertions(+), 15 deletions(-) diff --git a/examples/python/mini_quip.py b/examples/python/mini_quip.py index a10d5a334..d25abe9af 100644 --- a/examples/python/mini_quip.py +++ b/examples/python/mini_quip.py @@ -3,6 +3,8 @@ import heapq import numpy import time import random +import sys +import copy verbose = True @@ -78,6 +80,8 @@ class Horn2Transitions: pred, inv0 = self.is_body(body) if pred is None: return False + if inv0 is None: + return False inv1 = self.is_inv(head) if inv1 is None: return False @@ -349,12 +353,12 @@ class Quip: 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, list(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, list(zip(self.xn, self.x0))) def add_solver(self): s = fd_solver() @@ -423,7 +427,8 @@ class Quip: s.push() r = self.reachable.state2cube(state) s.add(And(self.prev(r))) - s.add(self.prev(cube)) + if len(cube) > 0: + s.add(And(self.prev(list(cube)))) is_sat = s.check() s.pop() if is_sat == sat: @@ -441,7 +446,7 @@ class Quip: s = self.states[f - 1].solver if unsat == s.check(cube): core = s.unsat_core() - if self.check_reachable(core): + if len(core) > 0 and self.check_reachable(core): return core, f return cube, f @@ -454,8 +459,8 @@ class Quip: for state in self.reachable.states: s.push() s.add(And(self.next(self.reachable.state2cube(state)))) - print self.reachable.state2cube(state) - print s.check() + print(self.reachable.state2cube(state)) + print(s.check()) s.pop() def lemmas(self, level): @@ -553,7 +558,7 @@ class Quip: s.add(self.init) s.add(self.prev(g.cube)) # since init is a complete assignment, so g.cube must equal to init in sat solver - assert is_sat == s.check() + assert sat == s.check() if verbose: print("") return g @@ -564,7 +569,7 @@ class Quip: if r0 is not None: if g.must: if verbose: - print "" + print("") s = fd_solver() s.add(self.trans) # make it as a concrete reachable state @@ -573,9 +578,16 @@ class Quip: while True: is_sat = s.check(self.next(g.cube)) assert is_sat == sat - r = self.next(self.project0(s.model())) + m = s.model() + r = self.next(self.project0(m)) r = self.reachable.intersect(self.prev(r)) - child = QGoal(self.next(r.children()), g, 0, g.must, 0) + if r is None: + # reachable intersect failed: fall back to the raw + # model projection so we still get a concrete + # predecessor and avoid crashing on r.children() + child = QGoal(self.next(self.project0(m)), g, 0, g.must, 0) + else: + child = QGoal(self.next(r.children()), g, 0, g.must, 0) g = child if not check_disjoint(self.init, self.prev(g.cube)): # g is init, break the loop @@ -596,7 +608,7 @@ class Quip: for l in self.frames[f_1]: if not l.bad and len(l.cube) > 0 and set(l.cube).issubset(g.cube): cube = l.cube - is_sat == unsat + is_sat = unsat break f_1 -= 1 if cube is None: @@ -707,7 +719,7 @@ def test(file): h2t = Horn2Transitions() h2t.parse(file) if verbose: - print("Test file: %s") % file + print("Test file: %s" % file) mp = Quip(h2t.init, h2t.trans, h2t.goal, h2t.xs, h2t.inputs, h2t.xns) start_time = time.time() result = mp.run() @@ -744,7 +756,7 @@ def validate(var, result, trans): s.pop() g = g.parent if verbose: - print "--- validation succeed ----" + print("--- validation succeed ----") return if isinstance(result, ExprRef): inv = result @@ -762,7 +774,7 @@ def validate(var, result, trans): # too many steps to reach invariant if step > 1000: if verbose: - print "--- validation failed --" + print("--- validation failed --") return if not check_disjoint(var.prev(cube), var.prev(inv)): # reach invariant @@ -773,7 +785,7 @@ def validate(var, result, trans): cube = var.projectN(s.model()) s.pop() if verbose: - print "--- validation succeed ----" + print("--- validation succeed ----") return