mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

address some of the ugliness pointed out by abandoned pull request #5008

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-09 11:23:16 -08:00
parent 8b5094fe73
commit e722589810
1 changed files with 29 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/api/python/z3/z3util.py
View file

@ -11,6 +11,7 @@ Usage:
import common_z3 as CM_Z3 import common_z3 as CM_Z3
""" """
import ctypes
from .z3 import * from .z3 import *
def vset(seq, idfun=None, as_list=True): def vset(seq, idfun=None, as_list=True):
@ -140,7 +141,7 @@ def is_expr_val(v):
def get_vars(f,rs=[]): def get_vars(f, rs = None):
""" """
>>> x,y = Ints('x y') >>> x,y = Ints('x y')
>>> a,b = Bools('a b') >>> a,b = Bools('a b')
@ -148,6 +149,9 @@ def get_vars(f,rs=[]):
[x, y, a, b] [x, y, a, b]
""" """
if rs is None:
rs = []
if z3_debug(): if z3_debug():
assert is_expr(f) assert is_expr(f)
@ -174,11 +178,8 @@ def mk_var(name,vsort):
v = Bool(name) v = Bool(name)
elif vsort.kind() == Z3_DATATYPE_SORT: elif vsort.kind() == Z3_DATATYPE_SORT:
v = Const(name, vsort) v = Const(name, vsort)
else: else:
assert False, 'Cannot handle this sort (s: %sid: %d)'\ raise TypeError(f"Cannot handle this sort (s: {vsort}id: {vsort.kind()})")
%(vsort,vsort.kind())
return v return v
@ -231,7 +232,6 @@ def prove(claim,assume=None,verbose=0):
if z3_debug(): if z3_debug():
assert not assume or is_expr(assume) assert not assume or is_expr(assume)
to_prove = claim to_prove = claim
if assume: if assume:
if z3_debug(): if z3_debug():
@ -247,8 +247,6 @@ def prove(claim,assume=None,verbose=0):
to_prove = Implies(assume,to_prove) to_prove = Implies(assume,to_prove)
if verbose >= 2: if verbose >= 2:
print('assume: ') print('assume: ')
print(assume) print(assume)
@ -316,8 +314,6 @@ def get_models(f,k):
assert is_expr(f) assert is_expr(f)
assert k >= 1 assert k >= 1
s = Solver() s = Solver()
s.add(f) s.add(f)
@ -325,12 +321,9 @@ def get_models(f,k):
i = 0 i = 0
while s.check() == sat and i < k: while s.check() == sat and i < k:
i = i + 1 i = i + 1
m = s.model() m = s.model()
if not m: #if m == [] if not m: #if m == []
break break
models.append(m) models.append(m)
@ -461,27 +454,27 @@ def myBinOp(op,*L):
if L: if L:
if len(L)==1: if len(L)==1:
return L[0] return L[0]
else:
if op == Z3_OP_OR: if op == Z3_OP_OR:
return Or(L) return Or(L)
elif op == Z3_OP_AND: if op == Z3_OP_AND:
return And(L) return And(L)
else: #IMPLIES
return Implies(L[0],L[1]) return Implies(L[0],L[1])
else: else:
return None return None
def myAnd(*L): return myBinOp(Z3_OP_AND,*L) def myAnd(*L):
def myOr(*L): return myBinOp(Z3_OP_OR,*L) return myBinOp(Z3_OP_AND,*L)
def myImplies(a,b):return myBinOp(Z3_OP_IMPLIES,[a,b])
def myOr(*L):
return myBinOp(Z3_OP_OR,*L)
def myImplies(a,b):
return myBinOp(Z3_OP_IMPLIES,[a,b])
Iff = lambda f: And(Implies(f[0],f[1]),Implies(f[1],f[0])) Iff = lambda f: And(Implies(f[0],f[1]),Implies(f[1],f[0]))
def model_str(m,as_str=True): def model_str(m,as_str=True):
""" """
Returned a 'sorted' model (so that it's easier to see) Returned a 'sorted' model (so that it's easier to see)