1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
from z3 import *
from z3.z3util import get_vars
'''
Modified from the example in pysmt
https://github.com/pysmt/pysmt/blob/97088bf3b0d64137c3099ef79a4e153b10ccfda7/examples/efsmt.py
'''
def efsmt(ys, phi, maxloops = None):
"""Solving exists xs. forall ys. phi(x, y)"""
xs = [x for x in get_vars(phi) if x not in ys]
E = Solver()
F = Solver()
E.add(BoolVal(True))
loops = 0
while maxloops is None or loops <= maxloops:
loops += 1
eres = E.check()
if eres == sat:
emodel = E.model()
sub_phi = substitute(phi, [(x, emodel.eval(x, True)) for x in xs])
F.push()
F.add(Not(sub_phi))
fres = F.check()
if fres == sat:
fmodel = F.model()
sub_phi = substitute(phi, [(y, fmodel.eval(y, True)) for y in ys])
E.add(sub_phi)
else:
return fres, [(x, emodel.eval(x, True)) for x in xs]
F.pop()
else:
return eres
return unknown
x, y, z = Reals("x y z")
print(efsmt([y], Implies(And(y > 0, y < 10), y - 2 * x < 7)))
print(efsmt([y], And(y > 3, x == 1)))
|
