z3.z3util
index
/home/vsts/work/1/s/build/python/z3/z3util.py

Usage:
import common_z3 as CM_Z3

 
Modules
       
codecs
copy
ctypes
io
math
os
pkg_resources
sys
z3.z3
z3.z3core

 
Functions
       
Iff(f)
POINTER(...)
addressof(...)
addressof(C instance) -> integer
Return the address of the C instance internal buffer
alignment(...)
alignment(C type) -> integer
alignment(C instance) -> integer
Return the alignment requirements of a C instance
byref(...)
byref(C instance[, offset=0]) -> byref-object
Return a pointer lookalike to a C instance, only usable
as function argument
ehash(v)
Returns a 'stronger' hash value than the default hash() method.
The result from hash() is not enough to distinguish between 2
z3 expressions in some cases.
 
Note: the following doctests will fail with Python 2.x as the
default formatting doesn't match that of 3.x.
>>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
>>> print(x1.hash(), x2.hash(), x3.hash()) #BAD: all same hash values
783810685 783810685 783810685
>>> print(ehash(x1), ehash(x2), ehash(x3))
x_783810685_1 x_783810685_1 x_783810685_2
exact_one_model(f)
return True if f has exactly 1 model, False otherwise.
 
EXAMPLES:
 
>>> x, y = Ints('x y')
>>> exact_one_model(And(0<=x**y,x <= 0))
False
 
>>> exact_one_model(And(0<=x,x <= 0))
True
 
>>> exact_one_model(And(0<=x,x <= 1))
False
 
>>> exact_one_model(And(0<=x,x <= -1))
False
get_errno(...)
get_models(f, k)
Returns the first k models satisfiying f.
If f is not satisfiable, returns False.
If f cannot be solved, returns None
If f is satisfiable, returns the first k models
Note that if f is a tautology, e.g.\ True, then the result is []
 
Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
 
EXAMPLES:
>>> x, y = Ints('x y')
>>> len(get_models(And(0<=x,x <= 4),k=11))
5
>>> get_models(And(0<=x**y,x <= 1),k=2) is None
True
>>> get_models(And(0<=x,x <= -1),k=2)
False
>>> len(get_models(x+y==7,5))
5
>>> len(get_models(And(x<=5,x>=1),7))
5
>>> get_models(And(x<=0,x>=5),7)
False
 
>>> x = Bool('x')
>>> get_models(And(x,Not(x)),k=1)
False
>>> get_models(Implies(x,x),k=1)
[]
>>> get_models(BoolVal(True),k=1)
[]
get_vars(f, rs=None)
>>> x,y = Ints('x y')
>>> a,b = Bools('a b')
>>> get_vars(Implies(And(x+y==0,x*2==10),Or(a,Implies(a,b==False))))
[x, y, a, b]
get_z3_version(as_str=False)
is_contradiction(claim, verbose=0)
>>> x,y=Bools('x y')
>>> is_contradiction(BoolVal(False))
True
 
>>> is_contradiction(BoolVal(True))
False
 
>>> is_contradiction(x)
False
 
>>> is_contradiction(Implies(x,y))
False
 
>>> is_contradiction(Implies(x,x))
False
 
>>> is_contradiction(And(x,Not(x)))
True
is_expr_val(v)
EXAMPLES:
 
>>> is_expr_val(Int('7'))
False
>>> is_expr_val(IntVal('7'))
True
>>> is_expr_val(Bool('y'))
False
>>> is_expr_val(Int('x') + 7 == Int('y'))
False
>>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
>>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
>>> is_expr_val(LOnOff)
False
>>> is_expr_val(On)
True
>>> is_expr_val(Block)
False
>>> is_expr_val(SafetyInjection)
False
is_expr_var(v)
EXAMPLES:
 
>>> is_expr_var(Int('7'))
True
>>> is_expr_var(IntVal('7'))
False
>>> is_expr_var(Bool('y'))
True
>>> is_expr_var(Int('x') + 7 == Int('y'))
False
>>> LOnOff, (On,Off) = EnumSort("LOnOff",['On','Off'])
>>> Block,Reset,SafetyInjection=Consts("Block Reset SafetyInjection",LOnOff)
>>> is_expr_var(LOnOff)
False
>>> is_expr_var(On)
False
>>> is_expr_var(Block)
True
>>> is_expr_var(SafetyInjection)
True
is_tautology(claim, verbose=0)
>>> is_tautology(Implies(Bool('x'),Bool('x')))
True
 
>>> is_tautology(Implies(Bool('x'),Bool('y')))
False
 
>>> is_tautology(BoolVal(True))
True
 
>>> is_tautology(BoolVal(False))
False
mk_var(name, vsort)
model_str(m, as_str=True)
Returned a 'sorted' model (so that it's easier to see)
The model is sorted by its key,
e.g. if the model is y = 3 , x = 10, then the result is
x = 10, y = 3
 
EXAMPLES:
see doctest exampels from function prove()
myAnd(*L)
myBinOp(op, *L)
>>> myAnd(*[Bool('x'),Bool('y')])
And(x, y)
 
>>> myAnd(*[Bool('x'),None])
x
 
>>> myAnd(*[Bool('x')])
x
 
>>> myAnd(*[])
 
>>> myAnd(Bool('x'),Bool('y'))
And(x, y)
 
>>> myAnd(*[Bool('x'),Bool('y')])
And(x, y)
 
>>> myAnd([Bool('x'),Bool('y')])
And(x, y)
 
>>> myAnd((Bool('x'),Bool('y')))
And(x, y)
 
>>> myAnd(*[Bool('x'),Bool('y'),True])
Traceback (most recent call last):
...
AssertionError
myImplies(a, b)
myOr(*L)
pointer(...)
prove(claim, assume=None, verbose=0)
>>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False)
(True, None)
 
#infinite counter example when proving contradiction
>>> r,m = prove(BoolVal(False)); r,model_str(m,as_str=False)
(False, [])
 
>>> x,y,z=Bools('x y z')
>>> r,m = prove(And(x,Not(x))); r,model_str(m,as_str=True)
(False, '[]')
 
>>> r,m = prove(True,assume=And(x,Not(x)),verbose=0)
Traceback (most recent call last):
...
AssertionError: Assumption is always False!
 
>>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False)
assume:
y
claim:
Implies(x, x)
to_prove:
Implies(y, Implies(x, x))
(True, None)
 
>>> r,m = prove(And(x,True),assume=y,verbose=0); r,model_str(m,as_str=False)
(False, [(x, False), (y, True)])
 
>>> r,m = prove(And(x,y),assume=y,verbose=0)
>>> print(r)
False
>>> print(model_str(m,as_str=True))
x = False
y = True
 
>>> a,b = Ints('a b')
>>> r,m = prove(a**b == b**a,assume=None,verbose=0)
E: cannot solve !
>>> r is None and m is None
True
resize(...)
Resize the memory buffer of a ctypes instance
set_conversion_mode(...)
set_conversion_mode(encoding, errors) -> (previous-encoding, previous-errors)
 
Set the encoding and error handling ctypes uses when converting
between unicode and strings.  Returns the previous values.
set_errno(...)
sizeof(...)
sizeof(C type) -> integer
sizeof(C instance) -> integer
Return the size in bytes of a C instance
vset(seq, idfun=None, as_list=True)
order preserving
 
>>> vset([[11,2],1, [10,['9',1]],2, 1, [11,2],[3,3],[10,99],1,[10,['9',1]]],idfun=repr)
[[11, 2], 1, [10, ['9', 1]], 2, [3, 3], [10, 99]]

 
Data
        DEFAULT_MODE = 0
RTLD_GLOBAL = 256
RTLD_LOCAL = 0
Z3_APP_AST = 1
Z3_ARRAY_SORT = 5
Z3_BOOL_SORT = 1
Z3_BV_SORT = 4
Z3_DATATYPE_SORT = 6
Z3_DEBUG = True
Z3_DEC_REF_ERROR = 11
Z3_EXCEPTION = 12
Z3_FILE_ACCESS_ERROR = 8
Z3_FINITE_DOMAIN_SORT = 8
Z3_FLOATING_POINT_SORT = 9
Z3_FUNC_DECL_AST = 5
Z3_GOAL_OVER = 2
Z3_GOAL_PRECISE = 0
Z3_GOAL_UNDER = 1
Z3_GOAL_UNDER_OVER = 3
Z3_INTERNAL_FATAL = 9
Z3_INT_SORT = 2
Z3_INT_SYMBOL = 0
Z3_INVALID_ARG = 3
Z3_INVALID_PATTERN = 6
Z3_INVALID_USAGE = 10
Z3_IOB = 2
Z3_L_FALSE = -1
Z3_L_TRUE = 1
Z3_L_UNDEF = 0
Z3_MEMOUT_FAIL = 7
Z3_NO_PARSER = 5
Z3_NUMERAL_AST = 0
Z3_OK = 0
Z3_OP_ADD = 518
Z3_OP_AGNUM = 513
Z3_OP_AND = 261
Z3_OP_ANUM = 512
Z3_OP_ARRAY_DEFAULT = 772
Z3_OP_ARRAY_EXT = 779
Z3_OP_ARRAY_MAP = 771
Z3_OP_AS_ARRAY = 778
Z3_OP_BADD = 1028
Z3_OP_BAND = 1049
Z3_OP_BASHR = 1066
Z3_OP_BCOMP = 1063
Z3_OP_BIT0 = 1026
Z3_OP_BIT1 = 1025
Z3_OP_BIT2BOOL = 1071
Z3_OP_BLSHR = 1065
Z3_OP_BMUL = 1030
Z3_OP_BNAND = 1053
Z3_OP_BNEG = 1027
Z3_OP_BNOR = 1054
Z3_OP_BNOT = 1051
Z3_OP_BNUM = 1024
Z3_OP_BOR = 1050
Z3_OP_BREDAND = 1062
Z3_OP_BREDOR = 1061
Z3_OP_BSDIV = 1031
Z3_OP_BSDIV0 = 1036
Z3_OP_BSDIV_I = 1079
Z3_OP_BSHL = 1064
Z3_OP_BSMOD = 1035
Z3_OP_BSMOD0 = 1040
Z3_OP_BSMOD_I = 1083
Z3_OP_BSMUL_NO_OVFL = 1076
Z3_OP_BSMUL_NO_UDFL = 1078
Z3_OP_BSREM = 1033
Z3_OP_BSREM0 = 1038
Z3_OP_BSREM_I = 1081
Z3_OP_BSUB = 1029
Z3_OP_BUDIV = 1032
Z3_OP_BUDIV0 = 1037
Z3_OP_BUDIV_I = 1080
Z3_OP_BUMUL_NO_OVFL = 1077
Z3_OP_BUREM = 1034
Z3_OP_BUREM0 = 1039
Z3_OP_BUREM_I = 1082
Z3_OP_BV2INT = 1073
Z3_OP_BXNOR = 1055
Z3_OP_BXOR = 1052
Z3_OP_CARRY = 1074
Z3_OP_CONCAT = 1056
Z3_OP_CONST_ARRAY = 770
Z3_OP_DISTINCT = 259
Z3_OP_DIV = 522
Z3_OP_DT_ACCESSOR = 2051
Z3_OP_DT_CONSTRUCTOR = 2048
Z3_OP_DT_IS = 2050
Z3_OP_DT_RECOGNISER = 2049
Z3_OP_DT_UPDATE_FIELD = 2052
Z3_OP_EQ = 258
Z3_OP_EXTRACT = 1059
Z3_OP_EXT_ROTATE_LEFT = 1069
Z3_OP_EXT_ROTATE_RIGHT = 1070
Z3_OP_FALSE = 257
Z3_OP_FD_CONSTANT = 1549
Z3_OP_FD_LT = 1550
Z3_OP_FPA_ABS = 45073
Z3_OP_FPA_ADD = 45067
Z3_OP_FPA_BV2RM = 45099
Z3_OP_FPA_BVWRAP = 45098
Z3_OP_FPA_DIV = 45071
Z3_OP_FPA_EQ = 45079
Z3_OP_FPA_FMA = 45076
Z3_OP_FPA_FP = 45091
Z3_OP_FPA_GE = 45083
Z3_OP_FPA_GT = 45081
Z3_OP_FPA_IS_INF = 45085
Z3_OP_FPA_IS_NAN = 45084
Z3_OP_FPA_IS_NEGATIVE = 45089
Z3_OP_FPA_IS_NORMAL = 45087
Z3_OP_FPA_IS_POSITIVE = 45090
Z3_OP_FPA_IS_SUBNORMAL = 45088
Z3_OP_FPA_IS_ZERO = 45086
Z3_OP_FPA_LE = 45082
Z3_OP_FPA_LT = 45080
Z3_OP_FPA_MAX = 45075
Z3_OP_FPA_MIN = 45074
Z3_OP_FPA_MINUS_INF = 45063
Z3_OP_FPA_MINUS_ZERO = 45066
Z3_OP_FPA_MUL = 45070
Z3_OP_FPA_NAN = 45064
Z3_OP_FPA_NEG = 45069
Z3_OP_FPA_NUM = 45061
Z3_OP_FPA_PLUS_INF = 45062
Z3_OP_FPA_PLUS_ZERO = 45065
Z3_OP_FPA_REM = 45072
Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY = 45057
Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 45056
Z3_OP_FPA_RM_TOWARD_NEGATIVE = 45059
Z3_OP_FPA_RM_TOWARD_POSITIVE = 45058
Z3_OP_FPA_RM_TOWARD_ZERO = 45060
Z3_OP_FPA_ROUND_TO_INTEGRAL = 45078
Z3_OP_FPA_SQRT = 45077
Z3_OP_FPA_SUB = 45068
Z3_OP_FPA_TO_FP = 45092
Z3_OP_FPA_TO_FP_UNSIGNED = 45093
Z3_OP_FPA_TO_IEEE_BV = 45097
Z3_OP_FPA_TO_REAL = 45096
Z3_OP_FPA_TO_SBV = 45095
Z3_OP_FPA_TO_UBV = 45094
Z3_OP_GE = 515
Z3_OP_GT = 517
Z3_OP_IDIV = 523
Z3_OP_IFF = 263
Z3_OP_IMPLIES = 266
Z3_OP_INT2BV = 1072
Z3_OP_INTERNAL = 45100
Z3_OP_INT_TO_STR = 1567
Z3_OP_IS_INT = 528
Z3_OP_ITE = 260
Z3_OP_LABEL = 1792
Z3_OP_LABEL_LIT = 1793
Z3_OP_LE = 514
Z3_OP_LT = 516
Z3_OP_MOD = 525
Z3_OP_MUL = 521
Z3_OP_NOT = 265
Z3_OP_OEQ = 267
Z3_OP_OR = 262
Z3_OP_PB_AT_LEAST = 2305
Z3_OP_PB_AT_MOST = 2304
Z3_OP_PB_EQ = 2308
Z3_OP_PB_GE = 2307
Z3_OP_PB_LE = 2306
Z3_OP_POWER = 529
Z3_OP_PR_AND_ELIM = 1293
Z3_OP_PR_APPLY_DEF = 1314
Z3_OP_PR_ASSERTED = 1282
Z3_OP_PR_ASSUMPTION_ADD = 1309
Z3_OP_PR_BIND = 1291
Z3_OP_PR_CLAUSE_TRAIL = 1312
Z3_OP_PR_COMMUTATIVITY = 1307
Z3_OP_PR_DEF_AXIOM = 1308
Z3_OP_PR_DEF_INTRO = 1313
Z3_OP_PR_DER = 1300
Z3_OP_PR_DISTRIBUTIVITY = 1292
Z3_OP_PR_ELIM_UNUSED_VARS = 1299
Z3_OP_PR_GOAL = 1283
Z3_OP_PR_HYPER_RESOLVE = 1321
Z3_OP_PR_HYPOTHESIS = 1302
Z3_OP_PR_IFF_FALSE = 1306
Z3_OP_PR_IFF_OEQ = 1315
Z3_OP_PR_IFF_TRUE = 1305
Z3_OP_PR_LEMMA = 1303
Z3_OP_PR_LEMMA_ADD = 1310
Z3_OP_PR_MODUS_PONENS = 1284
Z3_OP_PR_MODUS_PONENS_OEQ = 1319
Z3_OP_PR_MONOTONICITY = 1289
Z3_OP_PR_NNF_NEG = 1317
Z3_OP_PR_NNF_POS = 1316
Z3_OP_PR_NOT_OR_ELIM = 1294
Z3_OP_PR_PULL_QUANT = 1297
Z3_OP_PR_PUSH_QUANT = 1298
Z3_OP_PR_QUANT_INST = 1301
Z3_OP_PR_QUANT_INTRO = 1290
Z3_OP_PR_REDUNDANT_DEL = 1311
Z3_OP_PR_REFLEXIVITY = 1285
Z3_OP_PR_REWRITE = 1295
Z3_OP_PR_REWRITE_STAR = 1296
Z3_OP_PR_SKOLEMIZE = 1318
Z3_OP_PR_SYMMETRY = 1286
Z3_OP_PR_TH_LEMMA = 1320
Z3_OP_PR_TRANSITIVITY = 1287
Z3_OP_PR_TRANSITIVITY_STAR = 1288
Z3_OP_PR_TRUE = 1281
Z3_OP_PR_UNDEF = 1280
Z3_OP_PR_UNIT_RESOLUTION = 1304
Z3_OP_RA_CLONE = 1548
Z3_OP_RA_COMPLEMENT = 1546
Z3_OP_RA_EMPTY = 1537
Z3_OP_RA_FILTER = 1543
Z3_OP_RA_IS_EMPTY = 1538
Z3_OP_RA_JOIN = 1539
Z3_OP_RA_NEGATION_FILTER = 1544
Z3_OP_RA_PROJECT = 1542
Z3_OP_RA_RENAME = 1545
Z3_OP_RA_SELECT = 1547
Z3_OP_RA_STORE = 1536
Z3_OP_RA_UNION = 1540
Z3_OP_RA_WIDEN = 1541
Z3_OP_REM = 524
Z3_OP_REPEAT = 1060
Z3_OP_RE_COMPLEMENT = 1580
Z3_OP_RE_CONCAT = 1573
Z3_OP_RE_EMPTY_SET = 1578
Z3_OP_RE_FULL_SET = 1579
Z3_OP_RE_INTERSECT = 1577
Z3_OP_RE_LOOP = 1576
Z3_OP_RE_OPTION = 1572
Z3_OP_RE_PLUS = 1570
Z3_OP_RE_RANGE = 1575
Z3_OP_RE_STAR = 1571
Z3_OP_RE_UNION = 1574
Z3_OP_ROTATE_LEFT = 1067
Z3_OP_ROTATE_RIGHT = 1068
Z3_OP_SELECT = 769
Z3_OP_SEQ_AT = 1559
Z3_OP_SEQ_CONCAT = 1553
Z3_OP_SEQ_CONTAINS = 1556
Z3_OP_SEQ_EMPTY = 1552
Z3_OP_SEQ_EXTRACT = 1557
Z3_OP_SEQ_INDEX = 1562
Z3_OP_SEQ_IN_RE = 1565
Z3_OP_SEQ_LAST_INDEX = 1563
Z3_OP_SEQ_LENGTH = 1561
Z3_OP_SEQ_NTH = 1560
Z3_OP_SEQ_PREFIX = 1554
Z3_OP_SEQ_REPLACE = 1558
Z3_OP_SEQ_SUFFIX = 1555
Z3_OP_SEQ_TO_RE = 1564
Z3_OP_SEQ_UNIT = 1551
Z3_OP_SET_CARD = 781
Z3_OP_SET_COMPLEMENT = 776
Z3_OP_SET_DIFFERENCE = 775
Z3_OP_SET_HAS_SIZE = 780
Z3_OP_SET_INTERSECT = 774
Z3_OP_SET_SUBSET = 777
Z3_OP_SET_UNION = 773
Z3_OP_SGEQ = 1044
Z3_OP_SGT = 1048
Z3_OP_SIGN_EXT = 1057
Z3_OP_SLEQ = 1042
Z3_OP_SLT = 1046
Z3_OP_SPECIAL_RELATION_LO = 40960
Z3_OP_SPECIAL_RELATION_PLO = 40962
Z3_OP_SPECIAL_RELATION_PO = 40961
Z3_OP_SPECIAL_RELATION_TC = 40964
Z3_OP_SPECIAL_RELATION_TO = 40963
Z3_OP_SPECIAL_RELATION_TRC = 40965
Z3_OP_STORE = 768
Z3_OP_STRING_LE = 1569
Z3_OP_STRING_LT = 1568
Z3_OP_STR_TO_INT = 1566
Z3_OP_SUB = 519
Z3_OP_TO_INT = 527
Z3_OP_TO_REAL = 526
Z3_OP_TRUE = 256
Z3_OP_UGEQ = 1043
Z3_OP_UGT = 1047
Z3_OP_ULEQ = 1041
Z3_OP_ULT = 1045
Z3_OP_UMINUS = 520
Z3_OP_UNINTERPRETED = 45101
Z3_OP_XOR = 264
Z3_OP_XOR3 = 1075
Z3_OP_ZERO_EXT = 1058
Z3_PARAMETER_AST = 5
Z3_PARAMETER_DOUBLE = 1
Z3_PARAMETER_FUNC_DECL = 6
Z3_PARAMETER_INT = 0
Z3_PARAMETER_RATIONAL = 2
Z3_PARAMETER_SORT = 4
Z3_PARAMETER_SYMBOL = 3
Z3_PARSER_ERROR = 4
Z3_PK_BOOL = 1
Z3_PK_DOUBLE = 2
Z3_PK_INVALID = 6
Z3_PK_OTHER = 5
Z3_PK_STRING = 4
Z3_PK_SYMBOL = 3
Z3_PK_UINT = 0
Z3_PRINT_LOW_LEVEL = 1
Z3_PRINT_SMTLIB2_COMPLIANT = 2
Z3_PRINT_SMTLIB_FULL = 0
Z3_QUANTIFIER_AST = 3
Z3_REAL_SORT = 3
Z3_RELATION_SORT = 7
Z3_RE_SORT = 12
Z3_ROUNDING_MODE_SORT = 10
Z3_SEQ_SORT = 11
Z3_SORT_AST = 4
Z3_SORT_ERROR = 1
Z3_STRING_SYMBOL = 1
Z3_UNINTERPRETED_SORT = 0
Z3_UNKNOWN_AST = 1000
Z3_UNKNOWN_SORT = 1000
Z3_VAR_AST = 2
cdll = <ctypes.LibraryLoader object>
d = '/home/vsts/work/1/s/build/libz3.so'
lds = ['/home/vsts/.opam/system/bin', '/home/linuxbrew/.linuxbrew/bin', '/home/linuxbrew/.linuxbrew/sbin', '/home/vsts/.local/bin', '/opt/pipx_bin', '/usr/share/rust/.cargo/bin', '/home/vsts/.config/composer/vendor/bin', '/usr/local/.ghcup/bin', '/home/vsts/.dotnet/tools', '/snap/bin', '/usr/local/sbin', '/usr/local/bin', '/usr/sbin', '/usr/bin', '/sbin', '/bin', '/usr/games', '/usr/local/games', '/snap/bin']
lp = '/home/vsts/.opam/system/bin:/home/linuxbrew/.lin...:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin'
memmove = <CFunctionType object>
memset = <CFunctionType object>
pydll = <ctypes.LibraryLoader object>
pythonapi = <PyDLL 'None', handle 7f0c212f5170 at 7f0c1f47a9d0>
sat = sat
unknown = unknown
unsat = unsat
v = 'PYTHONPATH'