1from z3 import * 2from z3.z3util import get_vars 3 4''' 5Modified from the example in pysmt 6https://github.com/pysmt/pysmt/blob/97088bf3b0d64137c3099ef79a4e153b10ccfda7/examples/efsmt.py 7''' 8def efsmt(y, phi, maxloops=None): 9 """Solving exists x. forall y. phi(x, y)""" 10 vars = get_vars(phi) 11 x = [item for item in vars if item not in y] 12 esolver = Solver() 13 fsolver = Solver() 14 esolver.add(BoolVal(True)) 15 loops = 0 16 while maxloops is None or loops <= maxloops: 17 loops += 1 18 eres = esolver.check() 19 if eres == unsat: 20 return unsat 21 else: 22 emodel = esolver.model() 23 tau = [emodel.eval(var, True) for var in x] 24 sub_phi = phi 25 for i in range(len(x)): 26 sub_phi = simplify(substitute(sub_phi, (x[i], tau[i]))) 27 fsolver.add(Not(sub_phi)) 28 if fsolver.check() == sat: 29 fmodel = fsolver.model() 30 sigma = [fmodel.eval(v, True) for v in y] 31 sub_phi = phi 32 for j in range(len(y)): 33 sub_phi = simplify(substitute(sub_phi, (y[j], sigma[j]))) 34 esolver.add(sub_phi) 35 else: 36 return sat 37 return unknown 38 39 40def test(): 41 x, y, z = Reals("x y z") 42 fmla = Implies(And(y > 0, y < 10), y - 2 * x < 7) 43 fmlb = And(y > 3, x == 1) 44 print(efsmt([y], fmla)) 45 print(efsmt([y], fmlb)) 46 47test() 48