mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

with simplification

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-03 21:10:53 -07:00
parent 05ec77cb56
commit 4f6811a6a2
1 changed files with 21 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

52
examples/python/efsmt.py
View file

@ -5,43 +5,33 @@ from z3.z3util import get_vars
Modified from the example in pysmt Modified from the example in pysmt
https://github.com/pysmt/pysmt/blob/97088bf3b0d64137c3099ef79a4e153b10ccfda7/examples/efsmt.py https://github.com/pysmt/pysmt/blob/97088bf3b0d64137c3099ef79a4e153b10ccfda7/examples/efsmt.py
''' '''
def efsmt(y, phi, maxloops=None):
"""Solving exists x. forall y. phi(x, y)""" def efsmt(ys, phi, maxloops = None):
vars = get_vars(phi) """Solving exists xs. forall ys. phi(x, y)"""
x = [item for item in vars if item not in y] xs = [x for x in get_vars(phi) if x not in ys]
esolver = Solver() E = Solver()
fsolver = Solver() F = Solver()
esolver.add(BoolVal(True)) E.add(BoolVal(True))
loops = 0 loops = 0
while maxloops is None or loops <= maxloops: while maxloops is None or loops <= maxloops:
loops += 1 loops += 1
eres = esolver.check() eres = E.check()
if eres == unsat: if eres == unsat:
return unsat return unsat
else: else:
emodel = esolver.model() emodel = E.model()
tau = [emodel.eval(var, True) for var in x] sub_phi = substitute(phi, [(x, emodel.eval(x, True)) for x in xs])
sub_phi = phi F.push()
for i in range(len(x)): F.add(Not(sub_phi))
sub_phi = simplify(substitute(sub_phi, (x[i], tau[i]))) if F.check() == sat:
fsolver.add(Not(sub_phi)) fmodel = F.model()
if fsolver.check() == sat: sub_phi = substitute(phi, [(y, fmodel.eval(y, True)) for y in ys])
fmodel = fsolver.model() E.add(sub_phi)
sigma = [fmodel.eval(v, True) for v in y]
sub_phi = phi
for j in range(len(y)):
sub_phi = simplify(substitute(sub_phi, (y[j], sigma[j])))
esolver.add(sub_phi)
else: else:
return sat return sat, [(x, emodel.eval(x, True)) for x in xs]
F.pop()
return unknown return unknown
x, y, z = Reals("x y z")
def test(): print(efsmt([y], Implies(And(y > 0, y < 10), y - 2 * x < 7)))
x, y, z = Reals("x y z") print(efsmt([y], And(y > 3, x == 1)))
fmla = Implies(And(y > 0, y < 10), y - 2 * x < 7)
fmlb = And(y > 3, x == 1)
print(efsmt([y], fmla))
print(efsmt([y], fmlb))
test()