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