def z3py.And | ( | args | ) |
Create a Z3 and-expression or and-probe. >>> p, q, r = Bools('p q r') >>> And(p, q, r) And(p, q, r) >>> P = BoolVector('p', 5) >>> And(P) And(p__0, p__1, p__2, p__3, p__4)
Definition at line 1468 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Bool(), Bools(), BoolVector(), Fixedpoint.query(), tree_interpolant(), and Fixedpoint.update_rule().
01468 01469 def And(*args): 01470 """Create a Z3 and-expression or and-probe. 01471 01472 >>> p, q, r = Bools('p q r') 01473 >>> And(p, q, r) 01474 And(p, q, r) 01475 >>> P = BoolVector('p', 5) 01476 >>> And(P) 01477 And(p__0, p__1, p__2, p__3, p__4) 01478 """ 01479 last_arg = None 01480 if len(args) > 0: 01481 last_arg = args[len(args)-1] 01482 if isinstance(last_arg, Context): 01483 ctx = args[len(args)-1] 01484 args = args[:len(args)-1] 01485 else: 01486 ctx = main_ctx() 01487 args = _get_args(args) 01488 ctx_args = _ctx_from_ast_arg_list(args, ctx) 01489 if __debug__: 01490 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") 01491 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") 01492 if _has_probe(args): 01493 return _probe_and(args, ctx) 01494 else: 01495 args = _coerce_expr_list(args, ctx) 01496 _args, sz = _to_ast_array(args) 01497 return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
def z3py.AndThen | ( | ts, | |
ks | |||
) |
Return a tactic that applies the tactics in `*ts` in sequence. >>> x, y = Ints('x y') >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 6537 of file z3py.py.
Referenced by Context.Then(), and Then().
06537 06538 def AndThen(*ts, **ks): 06539 """Return a tactic that applies the tactics in `*ts` in sequence. 06540 06541 >>> x, y = Ints('x y') 06542 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) 06543 >>> t(And(x == 0, y > x + 1)) 06544 [[Not(y <= 1)]] 06545 >>> t(And(x == 0, y > x + 1)).as_expr() 06546 Not(y <= 1) 06547 """ 06548 if __debug__: 06549 _z3_assert(len(ts) >= 2, "At least two arguments expected") 06550 ctx = ks.get('ctx', None) 06551 num = len(ts) 06552 r = ts[0] 06553 for i in range(num - 1): 06554 r = _and_then(r, ts[i+1], ctx) 06555 return r
def z3py.append_log | ( | s | ) |
Append user-defined string to interaction log.
Definition at line 90 of file z3py.py.
00090 00091 def append_log(s): 00092 """Append user-defined string to interaction log. """ 00093 Z3_append_log(s)
def z3py.args2params | ( | arguments, | |
keywords, | |||
ctx = None |
|||
) |
Convert python arguments into a Z3_params object. A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true)
Definition at line 4467 of file z3py.py.
Referenced by Tactic.apply(), Fixedpoint.set(), simplify(), and With().
04467 04468 def args2params(arguments, keywords, ctx=None): 04469 """Convert python arguments into a Z3_params object. 04470 A ':' is added to the keywords, and '_' is replaced with '-' 04471 04472 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) 04473 (params model true relevancy 2 elim_and true) 04474 """ 04475 if __debug__: 04476 _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") 04477 prev = None 04478 r = ParamsRef(ctx) 04479 for a in arguments: 04480 if prev == None: 04481 prev = a 04482 else: 04483 r.set(prev, a) 04484 prev = None 04485 for k in keywords: 04486 v = keywords[k] 04487 r.set(k, v) 04488 return r
def z3py.Array | ( | name, | |
dom, | |||
rng | |||
) |
Return an array constant named `name` with the given domain and range sorts. >>> a = Array('a', IntSort(), IntSort()) >>> a.sort() Array(Int, Int) >>> a[0] a[0]
Definition at line 3976 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), Store(), and Update().
03976 03977 def Array(name, dom, rng): 03978 """Return an array constant named `name` with the given domain and range sorts. 03979 03980 >>> a = Array('a', IntSort(), IntSort()) 03981 >>> a.sort() 03982 Array(Int, Int) 03983 >>> a[0] 03984 a[0] 03985 """ 03986 s = ArraySort(dom, rng) 03987 ctx = s.ctx 03988 return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
def z3py.ArraySort | ( | d, | |
r | |||
) |
Return the Z3 array sort with the given domain and range sorts. >>> A = ArraySort(IntSort(), BoolSort()) >>> A Array(Int, Bool) >>> A.domain() Int >>> A.range() Bool >>> AA = ArraySort(IntSort(), A) >>> AA Array(Int, Array(Int, Bool))
Definition at line 3955 of file z3py.py.
Referenced by Array(), Sort.create(), ArraySortRef.domain(), Context.mkArraySort(), Context.MkArraySort(), and ArraySortRef.range().
03955 03956 def ArraySort(d, r): 03957 """Return the Z3 array sort with the given domain and range sorts. 03958 03959 >>> A = ArraySort(IntSort(), BoolSort()) 03960 >>> A 03961 Array(Int, Bool) 03962 >>> A.domain() 03963 Int 03964 >>> A.range() 03965 Bool 03966 >>> AA = ArraySort(IntSort(), A) 03967 >>> AA 03968 Array(Int, Array(Int, Bool)) 03969 """ 03970 if __debug__: 03971 _z3_assert(is_sort(d), "Z3 sort expected") 03972 _z3_assert(is_sort(r), "Z3 sort expected") 03973 _z3_assert(d.ctx == r.ctx, "Context mismatch") 03974 ctx = d.ctx 03975 return ArraySortRef(Z3_mk_array_sort(ctx.ref(), d.ast, r.ast), ctx)
def z3py.binary_interpolant | ( | a, | |
b, | |||
p = None , |
|||
ctx = None |
|||
) |
Compute an interpolant for a binary conjunction. If a & b is unsatisfiable, returns an interpolant for a & b. This is a formula phi such that 1) a implies phi 2) b implies not phi 3) All the uninterpreted symbols of phi occur in both a and b. If a & b is satisfiable, raises an object of class ModelRef that represents a model of a &b. If parameters p are supplied, these are used in creating the solver that determines satisfiability. x = Int('x') print binary_interpolant(x<0,x>2) Not(x >= 0)
Definition at line 7368 of file z3py.py.
07368 07369 def binary_interpolant(a,b,p=None,ctx=None): 07370 """Compute an interpolant for a binary conjunction. 07371 07372 If a & b is unsatisfiable, returns an interpolant for a & b. 07373 This is a formula phi such that 07374 07375 1) a implies phi 07376 2) b implies not phi 07377 3) All the uninterpreted symbols of phi occur in both a and b. 07378 07379 If a & b is satisfiable, raises an object of class ModelRef 07380 that represents a model of a &b. 07381 07382 If parameters p are supplied, these are used in creating the 07383 solver that determines satisfiability. 07384 07385 x = Int('x') 07386 print binary_interpolant(x<0,x>2) 07387 Not(x >= 0) 07388 """ 07389 f = And(Interpolant(a),b) 07390 return tree_interpolant(f,p,ctx)[0]
def z3py.BitVec | ( | name, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. If `ctx=None`, then the global context is used. >>> x = BitVec('x', 16) >>> is_bv(x) True >>> x.size() 16 >>> x.sort() BitVec(16) >>> word = BitVecSort(16) >>> x2 = BitVec('x', word) >>> eq(x, x2) True
Definition at line 3465 of file z3py.py.
Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().
03465 03466 def BitVec(name, bv, ctx=None): 03467 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. 03468 If `ctx=None`, then the global context is used. 03469 03470 >>> x = BitVec('x', 16) 03471 >>> is_bv(x) 03472 True 03473 >>> x.size() 03474 16 03475 >>> x.sort() 03476 BitVec(16) 03477 >>> word = BitVecSort(16) 03478 >>> x2 = BitVec('x', word) 03479 >>> eq(x, x2) 03480 True 03481 """ 03482 if isinstance(bv, BitVecSortRef): 03483 ctx = bv.ctx 03484 else: 03485 ctx = _get_ctx(ctx) 03486 bv = BitVecSort(bv, ctx) 03487 return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
def z3py.BitVecs | ( | names, | |
bv, | |||
ctx = None |
|||
) |
Return a tuple of bit-vector constants of size bv. >>> x, y, z = BitVecs('x y z', 16) >>> x.size() 16 >>> x.sort() BitVec(16) >>> Sum(x, y, z) 0 + x + y + z >>> Product(x, y, z) 1*x*y*z >>> simplify(Product(x, y, z)) x*y*z
Definition at line 3488 of file z3py.py.
Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().
03488 03489 def BitVecs(names, bv, ctx=None): 03490 """Return a tuple of bit-vector constants of size bv. 03491 03492 >>> x, y, z = BitVecs('x y z', 16) 03493 >>> x.size() 03494 16 03495 >>> x.sort() 03496 BitVec(16) 03497 >>> Sum(x, y, z) 03498 0 + x + y + z 03499 >>> Product(x, y, z) 03500 1*x*y*z 03501 >>> simplify(Product(x, y, z)) 03502 x*y*z 03503 """ 03504 ctx = _get_ctx(ctx) 03505 if isinstance(names, str): 03506 names = names.split(" ") 03507 return [BitVec(name, bv, ctx) for name in names]
def z3py.BitVecSort | ( | sz, | |
ctx = None |
|||
) |
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. >>> Byte = BitVecSort(8) >>> Word = BitVecSort(16) >>> Byte BitVec(8) >>> x = Const('x', Byte) >>> eq(x, BitVec('x', 8)) True
Definition at line 3435 of file z3py.py.
Referenced by BitVec(), BitVecSortRef.cast(), Sort.create(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), and BitVecRef.sort().
03435 03436 def BitVecSort(sz, ctx=None): 03437 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. 03438 03439 >>> Byte = BitVecSort(8) 03440 >>> Word = BitVecSort(16) 03441 >>> Byte 03442 BitVec(8) 03443 >>> x = Const('x', Byte) 03444 >>> eq(x, BitVec('x', 8)) 03445 True 03446 """ 03447 ctx = _get_ctx(ctx) 03448 return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
def z3py.BitVecVal | ( | val, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. >>> v = BitVecVal(10, 32) >>> v 10 >>> print("0x%.8x" % v.as_long()) 0x0000000a
Definition at line 3449 of file z3py.py.
Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().
03449 03450 def BitVecVal(val, bv, ctx=None): 03451 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. 03452 03453 >>> v = BitVecVal(10, 32) 03454 >>> v 03455 10 03456 >>> print("0x%.8x" % v.as_long()) 03457 0x0000000a 03458 """ 03459 if is_bv_sort(bv): 03460 ctx = bv.ctx 03461 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx) 03462 else: 03463 ctx = _get_ctx(ctx) 03464 return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
def z3py.Bool | ( | name, | |
ctx = None |
|||
) |
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. >>> p = Bool('p') >>> q = Bool('q') >>> And(p, q) And(p, q)
Definition at line 1360 of file z3py.py.
Referenced by Solver.assert_and_track(), and Not().
01360 01361 def Bool(name, ctx=None): 01362 """Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. 01363 01364 >>> p = Bool('p') 01365 >>> q = Bool('q') 01366 >>> And(p, q) 01367 And(p, q) 01368 """ 01369 ctx = _get_ctx(ctx) 01370 return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
def z3py.Bools | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Boolean constants. `names` is a single string containing all names separated by blank spaces. If `ctx=None`, then the global context is used. >>> p, q, r = Bools('p q r') >>> And(p, Or(q, r)) And(p, Or(q, r))
Definition at line 1371 of file z3py.py.
Referenced by And(), Implies(), Or(), Solver.unsat_core(), and Xor().
01371 01372 def Bools(names, ctx=None): 01373 """Return a tuple of Boolean constants. 01374 01375 `names` is a single string containing all names separated by blank spaces. 01376 If `ctx=None`, then the global context is used. 01377 01378 >>> p, q, r = Bools('p q r') 01379 >>> And(p, Or(q, r)) 01380 And(p, Or(q, r)) 01381 """ 01382 ctx = _get_ctx(ctx) 01383 if isinstance(names, str): 01384 names = names.split(" ") 01385 return [Bool(name, ctx) for name in names]
def z3py.BoolSort | ( | ctx = None | ) |
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. >>> BoolSort() Bool >>> p = Const('p', BoolSort()) >>> is_bool(p) True >>> r = Function('r', IntSort(), IntSort(), BoolSort()) >>> r(0, 1) r(0, 1) >>> is_bool(r(0, 1)) True
Definition at line 1325 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Bool(), Sort.create(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.MkBoolConst(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().
01325 01326 def BoolSort(ctx=None): 01327 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. 01328 01329 >>> BoolSort() 01330 Bool 01331 >>> p = Const('p', BoolSort()) 01332 >>> is_bool(p) 01333 True 01334 >>> r = Function('r', IntSort(), IntSort(), BoolSort()) 01335 >>> r(0, 1) 01336 r(0, 1) 01337 >>> is_bool(r(0, 1)) 01338 True 01339 """ 01340 ctx = _get_ctx(ctx) 01341 return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
def z3py.BoolVal | ( | val, | |
ctx = None |
|||
) |
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. >>> BoolVal(True) True >>> is_true(BoolVal(True)) True >>> is_true(True) False >>> is_false(BoolVal(False)) True
Definition at line 1342 of file z3py.py.
Referenced by ApplyResult.as_expr(), BoolSortRef.cast(), and Solver.to_smt2().
01342 01343 def BoolVal(val, ctx=None): 01344 """Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. 01345 01346 >>> BoolVal(True) 01347 True 01348 >>> is_true(BoolVal(True)) 01349 True 01350 >>> is_true(True) 01351 False 01352 >>> is_false(BoolVal(False)) 01353 True 01354 """ 01355 ctx = _get_ctx(ctx) 01356 if val == False: 01357 return BoolRef(Z3_mk_false(ctx.ref()), ctx) 01358 else: 01359 return BoolRef(Z3_mk_true(ctx.ref()), ctx)
def z3py.BoolVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of Boolean constants of size `sz`. The constants are named using the given prefix. If `ctx=None`, then the global context is used. >>> P = BoolVector('p', 3) >>> P [p__0, p__1, p__2] >>> And(P) And(p__0, p__1, p__2)
Definition at line 1386 of file z3py.py.
Referenced by And(), and Or().
01386 01387 def BoolVector(prefix, sz, ctx=None): 01388 """Return a list of Boolean constants of size `sz`. 01389 01390 The constants are named using the given prefix. 01391 If `ctx=None`, then the global context is used. 01392 01393 >>> P = BoolVector('p', 3) 01394 >>> P 01395 [p__0, p__1, p__2] 01396 >>> And(P) 01397 And(p__0, p__1, p__2) 01398 """ 01399 return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
def z3py.BV2Int | ( | a | ) |
Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) >>> BV2Int(b).sort() Int >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2]
Definition at line 3417 of file z3py.py.
03417 03418 def BV2Int(a): 03419 """Return the Z3 expression BV2Int(a). 03420 03421 >>> b = BitVec('b', 3) 03422 >>> BV2Int(b).sort() 03423 Int 03424 >>> x = Int('x') 03425 >>> x > BV2Int(b) 03426 x > BV2Int(b) 03427 >>> solve(x > BV2Int(b), b == 1, x < 3) 03428 [b = 1, x = 2] 03429 """ 03430 if __debug__: 03431 _z3_assert(is_bv(a), "Z3 bit-vector expression expected") 03432 ctx = a.ctx 03433 ## investigate problem with bv2int 03434 return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx)
def z3py.Cbrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the cubic root of a. >>> x = Real('x') >>> Cbrt(x) x**(1/3)
def z3py.Concat | ( | args | ) |
Create a Z3 bit-vector concatenation expression. >>> v = BitVecVal(1, 4) >>> Concat(v, v+1, v) Concat(Concat(1, 1 + 1), 1) >>> simplify(Concat(v, v+1, v)) 289 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 121
Definition at line 3508 of file z3py.py.
Referenced by BitVecRef.size().
03508 03509 def Concat(*args): 03510 """Create a Z3 bit-vector concatenation expression. 03511 03512 >>> v = BitVecVal(1, 4) 03513 >>> Concat(v, v+1, v) 03514 Concat(Concat(1, 1 + 1), 1) 03515 >>> simplify(Concat(v, v+1, v)) 03516 289 03517 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 03518 121 03519 """ 03520 args = _get_args(args) 03521 if __debug__: 03522 _z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.") 03523 _z3_assert(len(args) >= 2, "At least two arguments expected.") 03524 ctx = args[0].ctx 03525 r = args[0] 03526 for i in range(len(args) - 1): 03527 r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx) 03528 return r
def z3py.Cond | ( | p, | |
t1, | |||
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
Definition at line 6940 of file z3py.py.
Referenced by If().
06940 06941 def Cond(p, t1, t2, ctx=None): 06942 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. 06943 06944 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt')) 06945 """ 06946 p = _to_probe(p, ctx) 06947 t1 = _to_tactic(t1, ctx) 06948 t2 = _to_tactic(t2, ctx) 06949 return Tactic(Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
def z3py.Const | ( | name, | |
sort | |||
) |
Create a constant of the given sort. >>> Const('x', IntSort()) x
Definition at line 1134 of file z3py.py.
Referenced by BitVecSort(), Consts(), IntSort(), RealSort(), and DatatypeSortRef.recognizer().
01134 01135 def Const(name, sort): 01136 """Create a constant of the given sort. 01137 01138 >>> Const('x', IntSort()) 01139 x 01140 """ 01141 if __debug__: 01142 _z3_assert(isinstance(sort, SortRef), "Z3 sort expected") 01143 ctx = sort.ctx 01144 return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
def z3py.Consts | ( | names, | |
sort | |||
) |
Create a several constants of the given sort. `names` is a string containing the names of all constants to be created. Blank spaces separate the names of different constants. >>> x, y, z = Consts('x y z', IntSort()) >>> x + y + z x + y + z
Definition at line 1145 of file z3py.py.
Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
01145 01146 def Consts(names, sort): 01147 """Create a several constants of the given sort. 01148 01149 `names` is a string containing the names of all constants to be created. 01150 Blank spaces separate the names of different constants. 01151 01152 >>> x, y, z = Consts('x y z', IntSort()) 01153 >>> x + y + z 01154 x + y + z 01155 """ 01156 if isinstance(names, str): 01157 names = names.split(" ") 01158 return [Const(name, sort) for name in names]
def z3py.CreateDatatypes | ( | ds | ) |
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. In the following example we define a Tree-List using two mutually recursive datatypes. >>> TreeList = Datatype('TreeList') >>> Tree = Datatype('Tree') >>> # Tree has two constructors: leaf and node >>> Tree.declare('leaf', ('val', IntSort())) >>> # a node contains a list of trees >>> Tree.declare('node', ('children', TreeList)) >>> TreeList.declare('nil') >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) >>> Tree.val(Tree.leaf(10)) val(leaf(10)) >>> simplify(Tree.val(Tree.leaf(10))) 10 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) >>> n1 node(cons(leaf(10), cons(leaf(20), nil))) >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) >>> simplify(n2 == n1) False >>> simplify(TreeList.car(Tree.children(n2)) == n1) True
Definition at line 4209 of file z3py.py.
Referenced by Datatype.create().
04209 04210 def CreateDatatypes(*ds): 04211 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. 04212 04213 In the following example we define a Tree-List using two mutually recursive datatypes. 04214 04215 >>> TreeList = Datatype('TreeList') 04216 >>> Tree = Datatype('Tree') 04217 >>> # Tree has two constructors: leaf and node 04218 >>> Tree.declare('leaf', ('val', IntSort())) 04219 >>> # a node contains a list of trees 04220 >>> Tree.declare('node', ('children', TreeList)) 04221 >>> TreeList.declare('nil') 04222 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) 04223 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) 04224 >>> Tree.val(Tree.leaf(10)) 04225 val(leaf(10)) 04226 >>> simplify(Tree.val(Tree.leaf(10))) 04227 10 04228 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) 04229 >>> n1 04230 node(cons(leaf(10), cons(leaf(20), nil))) 04231 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) 04232 >>> simplify(n2 == n1) 04233 False 04234 >>> simplify(TreeList.car(Tree.children(n2)) == n1) 04235 True 04236 """ 04237 ds = _get_args(ds) 04238 if __debug__: 04239 _z3_assert(len(ds) > 0, "At least one Datatype must be specified") 04240 _z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes") 04241 _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch") 04242 _z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected") 04243 ctx = ds[0].ctx 04244 num = len(ds) 04245 names = (Symbol * num)() 04246 out = (Sort * num)() 04247 clists = (ConstructorList * num)() 04248 to_delete = [] 04249 for i in range(num): 04250 d = ds[i] 04251 names[i] = to_symbol(d.name, ctx) 04252 num_cs = len(d.constructors) 04253 cs = (Constructor * num_cs)() 04254 for j in range(num_cs): 04255 c = d.constructors[j] 04256 cname = to_symbol(c[0], ctx) 04257 rname = to_symbol(c[1], ctx) 04258 fs = c[2] 04259 num_fs = len(fs) 04260 fnames = (Symbol * num_fs)() 04261 sorts = (Sort * num_fs)() 04262 refs = (ctypes.c_uint * num_fs)() 04263 for k in range(num_fs): 04264 fname = fs[k][0] 04265 ftype = fs[k][1] 04266 fnames[k] = to_symbol(fname, ctx) 04267 if isinstance(ftype, Datatype): 04268 if __debug__: 04269 _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected") 04270 sorts[k] = None 04271 refs[k] = ds.index(ftype) 04272 else: 04273 if __debug__: 04274 _z3_assert(is_sort(ftype), "Z3 sort expected") 04275 sorts[k] = ftype.ast 04276 refs[k] = 0 04277 cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs) 04278 to_delete.append(ScopedConstructor(cs[j], ctx)) 04279 clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs) 04280 to_delete.append(ScopedConstructorList(clists[i], ctx)) 04281 Z3_mk_datatypes(ctx.ref(), num, names, out, clists) 04282 result = [] 04283 ## Create a field for every constructor, recognizer and accessor 04284 for i in range(num): 04285 dref = DatatypeSortRef(out[i], ctx) 04286 num_cs = dref.num_constructors() 04287 for j in range(num_cs): 04288 cref = dref.constructor(j) 04289 cref_name = cref.name() 04290 cref_arity = cref.arity() 04291 if cref.arity() == 0: 04292 cref = cref() 04293 setattr(dref, cref_name, cref) 04294 rref = dref.recognizer(j) 04295 setattr(dref, rref.name(), rref) 04296 for k in range(cref_arity): 04297 aref = dref.accessor(j, k) 04298 setattr(dref, aref.name(), aref) 04299 result.append(dref) 04300 return tuple(result)
def z3py.DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpred sort named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context. >>> A = DeclareSort('A') >>> a = Const('a', A) >>> b = Const('b', A) >>> a.sort() == A True >>> b.sort() == A True >>> a == b a == b
Definition at line 563 of file z3py.py.
Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
00563 00564 def DeclareSort(name, ctx=None): 00565 """Create a new uninterpred sort named `name`. 00566 00567 If `ctx=None`, then the new sort is declared in the global Z3Py context. 00568 00569 >>> A = DeclareSort('A') 00570 >>> a = Const('a', A) 00571 >>> b = Const('b', A) 00572 >>> a.sort() == A 00573 True 00574 >>> b.sort() == A 00575 True 00576 >>> a == b 00577 a == b 00578 """ 00579 ctx = _get_ctx(ctx) 00580 return SortRef(Z3_mk_uninterpreted_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
def z3py.describe_probes | ( | ) |
Display a (tabular) description of all available probes in Z3.
Definition at line 6870 of file z3py.py.
06870 06871 def describe_probes(): 06872 """Display a (tabular) description of all available probes in Z3.""" 06873 if in_html_mode(): 06874 even = True 06875 print('<table border="1" cellpadding="2" cellspacing="0">') 06876 for p in probes(): 06877 if even: 06878 print('<tr style="background-color:#CFCFCF">') 06879 even = False 06880 else: 06881 print('<tr>') 06882 even = True 06883 print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40))) 06884 print('</table>') 06885 else: 06886 for p in probes(): 06887 print('%s : %s' % (p, probe_description(p)))
def z3py.describe_tactics | ( | ) |
Display a (tabular) description of all available tactics in Z3.
Definition at line 6682 of file z3py.py.
06682 06683 def describe_tactics(): 06684 """Display a (tabular) description of all available tactics in Z3.""" 06685 if in_html_mode(): 06686 even = True 06687 print('<table border="1" cellpadding="2" cellspacing="0">') 06688 for t in tactics(): 06689 if even: 06690 print('<tr style="background-color:#CFCFCF">') 06691 even = False 06692 else: 06693 print('<tr>') 06694 even = True 06695 print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40))) 06696 print('</table>') 06697 else: 06698 for t in tactics(): 06699 print('%s : %s' % (t, tactic_description(t)))
def z3py.disable_trace | ( | msg | ) |
Definition at line 61 of file z3py.py.
00061 00062 def disable_trace(msg): 00063 Z3_disable_trace(msg)
def z3py.Distinct | ( | args | ) |
Create a Z3 distinct expression. >>> x = Int('x') >>> y = Int('y') >>> Distinct(x, y) x != y >>> z = Int('z') >>> Distinct(x, y, z) Distinct(x, y, z) >>> simplify(Distinct(x, y, z)) Distinct(x, y, z) >>> simplify(Distinct(x, y, z), blast_distinct=True) And(Not(x == y), Not(x == z), Not(y == z))
Definition at line 1103 of file z3py.py.
01103 01104 def Distinct(*args): 01105 """Create a Z3 distinct expression. 01106 01107 >>> x = Int('x') 01108 >>> y = Int('y') 01109 >>> Distinct(x, y) 01110 x != y 01111 >>> z = Int('z') 01112 >>> Distinct(x, y, z) 01113 Distinct(x, y, z) 01114 >>> simplify(Distinct(x, y, z)) 01115 Distinct(x, y, z) 01116 >>> simplify(Distinct(x, y, z), blast_distinct=True) 01117 And(Not(x == y), Not(x == z), Not(y == z)) 01118 """ 01119 args = _get_args(args) 01120 ctx = _ctx_from_ast_arg_list(args) 01121 if __debug__: 01122 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression") 01123 args = _coerce_expr_list(args, ctx) 01124 _args, sz = _to_ast_array(args) 01125 return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
def z3py.enable_trace | ( | msg | ) |
Definition at line 58 of file z3py.py.
00058 00059 def enable_trace(msg): 00060 Z3_enable_trace(msg)
def z3py.EnumSort | ( | name, | |
values, | |||
ctx = None |
|||
) |
Return a new enumeration sort named `name` containing the given values. The result is a pair (sort, list of constants). Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Definition at line 4398 of file z3py.py.
Referenced by Context.mkEnumSort(), and Context.MkEnumSort().
04398 04399 def EnumSort(name, values, ctx=None): 04400 """Return a new enumeration sort named `name` containing the given values. 04401 04402 The result is a pair (sort, list of constants). 04403 Example: 04404 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue']) 04405 """ 04406 if __debug__: 04407 _z3_assert(isinstance(name, str), "Name must be a string") 04408 _z3_assert(all([isinstance(v, str) for v in values]), "Eumeration sort values must be strings") 04409 _z3_assert(len(values) > 0, "At least one value expected") 04410 ctx = _get_ctx(ctx) 04411 num = len(values) 04412 _val_names = (Symbol * num)() 04413 for i in range(num): 04414 _val_names[i] = to_symbol(values[i]) 04415 _values = (FuncDecl * num)() 04416 _testers = (FuncDecl * num)() 04417 name = to_symbol(name) 04418 S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx) 04419 V = [] 04420 for i in range(num): 04421 V.append(FuncDeclRef(_values[i], ctx)) 04422 V = [a() for a in V] 04423 return S, V
def z3py.eq | ( | a, | |
b | |||
) |
Return `True` if `a` and `b` are structurally identical AST nodes. >>> x = Int('x') >>> y = Int('y') >>> eq(x, y) False >>> eq(x + 1, x + 1) True >>> eq(x + 1, 1 + x) False >>> eq(simplify(x + 1), simplify(1 + x)) True
Definition at line 372 of file z3py.py.
Referenced by BitVec(), BitVecSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), Select(), and substitute().
00372 00373 def eq(a, b): 00374 """Return `True` if `a` and `b` are structurally identical AST nodes. 00375 00376 >>> x = Int('x') 00377 >>> y = Int('y') 00378 >>> eq(x, y) 00379 False 00380 >>> eq(x + 1, x + 1) 00381 True 00382 >>> eq(x + 1, 1 + x) 00383 False 00384 >>> eq(simplify(x + 1), simplify(1 + x)) 00385 True 00386 """ 00387 if __debug__: 00388 _z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected") 00389 return a.eq(b)
def z3py.Exists | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 exists formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> q = Exists([x, y], f(x, y) >= x, skid="foo") >>> q Exists([x, y], f(x, y) >= x) >>> is_quantifier(q) True >>> r = Tactic('nnf')(q).as_expr() >>> is_quantifier(r) False
Definition at line 1808 of file z3py.py.
Referenced by Fixedpoint.abstract(), and QuantifierRef.is_forall().
01808 01809 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 01810 """Create a Z3 exists formula. 01811 01812 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 01813 01814 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 01815 01816 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 01817 >>> x = Int('x') 01818 >>> y = Int('y') 01819 >>> q = Exists([x, y], f(x, y) >= x, skid="foo") 01820 >>> q 01821 Exists([x, y], f(x, y) >= x) 01822 >>> is_quantifier(q) 01823 True 01824 >>> r = Tactic('nnf')(q).as_expr() 01825 >>> is_quantifier(r) 01826 False 01827 """ 01828 return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
def z3py.Extract | ( | high, | |
low, | |||
a | |||
) |
Create a Z3 bit-vector extraction expression. >>> x = BitVec('x', 8) >>> Extract(6, 2, x) Extract(6, 2, x) >>> Extract(6, 2, x).sort() BitVec(5)
Definition at line 3529 of file z3py.py.
03529 03530 def Extract(high, low, a): 03531 """Create a Z3 bit-vector extraction expression. 03532 03533 >>> x = BitVec('x', 8) 03534 >>> Extract(6, 2, x) 03535 Extract(6, 2, x) 03536 >>> Extract(6, 2, x).sort() 03537 BitVec(5) 03538 """ 03539 if __debug__: 03540 _z3_assert(low <= high, "First argument must be greater than or equal to second argument") 03541 _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers") 03542 _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression") 03543 return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
def z3py.FailIf | ( | p, | |
ctx = None |
|||
) |
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 6903 of file z3py.py.
06903 06904 def FailIf(p, ctx=None): 06905 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 06906 06907 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. 06908 06909 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) 06910 >>> x, y = Ints('x y') 06911 >>> g = Goal() 06912 >>> g.add(x > 0) 06913 >>> g.add(y > 0) 06914 >>> t(g) 06915 [[x > 0, y > 0]] 06916 >>> g.add(x == y + 1) 06917 >>> t(g) 06918 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 06919 """ 06920 p = _to_probe(p, ctx) 06921 return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
def z3py.ForAll | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 forall formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> ForAll([x, y], f(x, y) >= x) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, weight=10) ForAll([x, y], f(x, y) >= x)
Definition at line 1789 of file z3py.py.
Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
01789 01790 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): 01791 """Create a Z3 forall formula. 01792 01793 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. 01794 01795 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 01796 01797 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 01798 >>> x = Int('x') 01799 >>> y = Int('y') 01800 >>> ForAll([x, y], f(x, y) >= x) 01801 ForAll([x, y], f(x, y) >= x) 01802 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) 01803 ForAll([x, y], f(x, y) >= x) 01804 >>> ForAll([x, y], f(x, y) >= x, weight=10) 01805 ForAll([x, y], f(x, y) >= x) 01806 """ 01807 return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
def z3py.FreshBool | ( | prefix = 'b' , |
|
ctx = None |
|||
) |
Return a fresh Boolean constant in the given context using the given prefix. If `ctx=None`, then the global context is used. >>> b1 = FreshBool() >>> b2 = FreshBool() >>> eq(b1, b2) False
Definition at line 1400 of file z3py.py.
01400 01401 def FreshBool(prefix='b', ctx=None): 01402 """Return a fresh Boolean constant in the given context using the given prefix. 01403 01404 If `ctx=None`, then the global context is used. 01405 01406 >>> b1 = FreshBool() 01407 >>> b2 = FreshBool() 01408 >>> eq(b1, b2) 01409 False 01410 """ 01411 ctx = _get_ctx(ctx) 01412 return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
def z3py.FreshInt | ( | prefix = 'x' , |
|
ctx = None |
|||
) |
Return a fresh integer constant in the given context using the given prefix. >>> x = FreshInt() >>> y = FreshInt() >>> eq(x, y) False >>> x.sort() Int
Definition at line 2752 of file z3py.py.
02752 02753 def FreshInt(prefix='x', ctx=None): 02754 """Return a fresh integer constant in the given context using the given prefix. 02755 02756 >>> x = FreshInt() 02757 >>> y = FreshInt() 02758 >>> eq(x, y) 02759 False 02760 >>> x.sort() 02761 Int 02762 """ 02763 ctx = _get_ctx(ctx) 02764 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
def z3py.FreshReal | ( | prefix = 'b' , |
|
ctx = None |
|||
) |
Return a fresh real constant in the given context using the given prefix. >>> x = FreshReal() >>> y = FreshReal() >>> eq(x, y) False >>> x.sort() Real
Definition at line 2804 of file z3py.py.
02804 02805 def FreshReal(prefix='b', ctx=None): 02806 """Return a fresh real constant in the given context using the given prefix. 02807 02808 >>> x = FreshReal() 02809 >>> y = FreshReal() 02810 >>> eq(x, y) 02811 False 02812 >>> x.sort() 02813 Real 02814 """ 02815 ctx = _get_ctx(ctx) 02816 return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
def z3py.Function | ( | name, | |
sig | |||
) |
Create a new Z3 uninterpreted function with the given sorts. >>> f = Function('f', IntSort(), IntSort()) >>> f(f(0)) f(f(0))
Definition at line 701 of file z3py.py.
Referenced by ModelRef.__getitem__(), ModelRef.__len__(), FuncEntry.arg_value(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), QuantifierRef.children(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), QuantifierRef.is_forall(), is_map(), is_pattern(), is_quantifier(), Map(), MultiPattern(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
00701 00702 def Function(name, *sig): 00703 """Create a new Z3 uninterpreted function with the given sorts. 00704 00705 >>> f = Function('f', IntSort(), IntSort()) 00706 >>> f(f(0)) 00707 f(f(0)) 00708 """ 00709 sig = _get_args(sig) 00710 if __debug__: 00711 _z3_assert(len(sig) > 0, "At least two arguments expected") 00712 arity = len(sig) - 1 00713 rng = sig[arity] 00714 if __debug__: 00715 _z3_assert(is_sort(rng), "Z3 sort expected") 00716 dom = (Sort * arity)() 00717 for i in range(arity): 00718 if __debug__: 00719 _z3_assert(is_sort(sig[i]), "Z3 sort expected") 00720 dom[i] = sig[i].ast 00721 ctx = rng.ctx 00722 return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
def z3py.get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
Definition at line 5533 of file z3py.py.
05533 05534 def get_as_array_func(n): 05535 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f).""" 05536 if __debug__: 05537 _z3_assert(is_as_array(n), "as-array Z3 expression expected.") 05538 return FuncDeclRef(Z3_get_as_array_func_decl(n.ctx.ref(), n.as_ast()), n.ctx)
def z3py.get_map_func | ( | a | ) |
Return the function declaration associated with a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> eq(f, get_map_func(a)) True >>> get_map_func(a) f >>> get_map_func(a)(0) f(0)
Definition at line 3938 of file z3py.py.
03938 03939 def get_map_func(a): 03940 """Return the function declaration associated with a Z3 map array expression. 03941 03942 >>> f = Function('f', IntSort(), IntSort()) 03943 >>> b = Array('b', IntSort(), IntSort()) 03944 >>> a = Map(f, b) 03945 >>> eq(f, get_map_func(a)) 03946 True 03947 >>> get_map_func(a) 03948 f 03949 >>> get_map_func(a)(0) 03950 f(0) 03951 """ 03952 if __debug__: 03953 _z3_assert(is_map(a), "Z3 array map expression expected.") 03954 return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
def z3py.get_param | ( | name | ) |
Return the value of a Z3 global (or module) parameter >>> get_param('nlsat.reorder') 'true'
Definition at line 247 of file z3py.py.
00247 00248 def get_param(name): 00249 """Return the value of a Z3 global (or module) parameter 00250 00251 >>> get_param('nlsat.reorder') 00252 'true' 00253 """ 00254 ptr = (ctypes.c_char_p * 1)() 00255 if Z3_global_param_get(str(name), ptr): 00256 r = z3core._to_pystr(ptr[0]) 00257 return r 00258 raise Z3Exception("failed to retrieve value for '%s'" % name)
def z3py.get_var_index | ( | a | ) |
Return the de-Bruijn index of the Z3 bounded variable `a`. >>> x = Int('x') >>> y = Int('y') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # Z3 replaces x and y with bound variables when ForAll is executed. >>> q = ForAll([x, y], f(x, y) == x + y) >>> q.body() f(Var(1), Var(0)) == Var(1) + Var(0) >>> b = q.body() >>> b.arg(0) f(Var(1), Var(0)) >>> v1 = b.arg(0).arg(0) >>> v2 = b.arg(0).arg(1) >>> v1 Var(1) >>> v2 Var(0) >>> get_var_index(v1) 1 >>> get_var_index(v2) 0
Definition at line 1037 of file z3py.py.
01037 01038 def get_var_index(a): 01039 """Return the de-Bruijn index of the Z3 bounded variable `a`. 01040 01041 >>> x = Int('x') 01042 >>> y = Int('y') 01043 >>> is_var(x) 01044 False 01045 >>> is_const(x) 01046 True 01047 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 01048 >>> # Z3 replaces x and y with bound variables when ForAll is executed. 01049 >>> q = ForAll([x, y], f(x, y) == x + y) 01050 >>> q.body() 01051 f(Var(1), Var(0)) == Var(1) + Var(0) 01052 >>> b = q.body() 01053 >>> b.arg(0) 01054 f(Var(1), Var(0)) 01055 >>> v1 = b.arg(0).arg(0) 01056 >>> v2 = b.arg(0).arg(1) 01057 >>> v1 01058 Var(1) 01059 >>> v2 01060 Var(0) 01061 >>> get_var_index(v1) 01062 1 01063 >>> get_var_index(v2) 01064 0 01065 """ 01066 if __debug__: 01067 _z3_assert(is_var(a), "Z3 bound variable expected") 01068 return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
def z3py.get_version | ( | ) |
Definition at line 72 of file z3py.py.
00072 00073 def get_version(): 00074 major = ctypes.c_uint(0) 00075 minor = ctypes.c_uint(0) 00076 build = ctypes.c_uint(0) 00077 rev = ctypes.c_uint(0) 00078 Z3_get_version(major, minor, build, rev) 00079 return (major.value, minor.value, build.value, rev.value) 00080 00081 # We use _z3_assert instead of the assert command because we want to # produce nice error messages in Z3Py at rise4fun.com
def z3py.get_version_string | ( | ) |
Definition at line 64 of file z3py.py.
00064 00065 def get_version_string(): 00066 major = ctypes.c_uint(0) 00067 minor = ctypes.c_uint(0) 00068 build = ctypes.c_uint(0) 00069 rev = ctypes.c_uint(0) 00070 Z3_get_version(major, minor, build, rev) 00071 return "%s.%s.%s" % (major.value, minor.value, build.value)
def z3py.help_simplify | ( | ) |
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 6980 of file z3py.py.
06980 06981 def help_simplify(): 06982 """Return a string describing all options available for Z3 `simplify` procedure.""" 06983 print(Z3_simplify_get_help(main_ctx().ref()))
def z3py.If | ( | a, | |
b, | |||
c, | |||
ctx = None |
|||
) |
Create a Z3 if-then-else expression. >>> x = Int('x') >>> y = Int('y') >>> max = If(x > y, x, y) >>> max If(x > y, x, y) >>> simplify(max) If(x <= y, y, x)
Definition at line 1081 of file z3py.py.
01081 01082 def If(a, b, c, ctx=None): 01083 """Create a Z3 if-then-else expression. 01084 01085 >>> x = Int('x') 01086 >>> y = Int('y') 01087 >>> max = If(x > y, x, y) 01088 >>> max 01089 If(x > y, x, y) 01090 >>> simplify(max) 01091 If(x <= y, y, x) 01092 """ 01093 if isinstance(a, Probe) or isinstance(b, Tactic) or isinstance(c, Tactic): 01094 return Cond(a, b, c, ctx) 01095 else: 01096 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx)) 01097 s = BoolSort(ctx) 01098 a = s.cast(a) 01099 b, c = _coerce_exprs(b, c, ctx) 01100 if __debug__: 01101 _z3_assert(a.ctx == b.ctx, "Context mismatch") 01102 return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
def z3py.Implies | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 implies expression. >>> p, q = Bools('p q') >>> Implies(p, q) Implies(p, q) >>> simplify(Implies(p, q)) Or(Not(p), q)
Definition at line 1413 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().
01413 01414 def Implies(a, b, ctx=None): 01415 """Create a Z3 implies expression. 01416 01417 >>> p, q = Bools('p q') 01418 >>> Implies(p, q) 01419 Implies(p, q) 01420 >>> simplify(Implies(p, q)) 01421 Or(Not(p), q) 01422 """ 01423 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 01424 s = BoolSort(ctx) 01425 a = s.cast(a) 01426 b = s.cast(b) 01427 return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
def z3py.Int | ( | name, | |
ctx = None |
|||
) |
Return an integer constant named `name`. If `ctx=None`, then the global context is used. >>> x = Int('x') >>> is_int(x) True >>> is_int(x + 1) True
Definition at line 2717 of file z3py.py.
Referenced by ArithRef.__add__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), binary_interpolant(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), Interpolant(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_forall(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), is_pattern(), is_quantifier(), ArithSortRef.is_real(), is_real(), is_select(), is_to_real(), K(), AstMap.keys(), Statistics.keys(), Solver.model(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), Solver.pop(), AstVector.push(), Solver.push(), Solver.reason_unknown(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), sequence_interpolant(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), tree_interpolant(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
02717 02718 def Int(name, ctx=None): 02719 """Return an integer constant named `name`. If `ctx=None`, then the global context is used. 02720 02721 >>> x = Int('x') 02722 >>> is_int(x) 02723 True 02724 >>> is_int(x + 1) 02725 True 02726 """ 02727 ctx = _get_ctx(ctx) 02728 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
def z3py.Interpolant | ( | a, | |
ctx = None |
|||
) |
Create an interpolation operator. The argument is an interpolation pattern (see tree_interpolant). >>> x = Int('x') >>> print Interpolant(x>0) interp(x > 0)
Definition at line 7295 of file z3py.py.
Referenced by binary_interpolant(), and tree_interpolant().
07295 07296 def Interpolant(a,ctx=None): 07297 """Create an interpolation operator. 07298 07299 The argument is an interpolation pattern (see tree_interpolant). 07300 07301 >>> x = Int('x') 07302 >>> print Interpolant(x>0) 07303 interp(x > 0) 07304 """ 07305 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 07306 s = BoolSort(ctx) 07307 a = s.cast(a) 07308 return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
def z3py.Ints | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Integer constants. >>> x, y, z = Ints('x y z') >>> Sum(x, y, z) x + y + z
Definition at line 2729 of file z3py.py.
Referenced by ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.depth(), Goal.get(), Goal.inconsistent(), is_add(), is_div(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().
02729 02730 def Ints(names, ctx=None): 02731 """Return a tuple of Integer constants. 02732 02733 >>> x, y, z = Ints('x y z') 02734 >>> Sum(x, y, z) 02735 x + y + z 02736 """ 02737 ctx = _get_ctx(ctx) 02738 if isinstance(names, str): 02739 names = names.split(" ") 02740 return [Int(name, ctx) for name in names]
def z3py.IntSort | ( | ctx = None | ) |
Return the interger sort in the given context. If `ctx=None`, then the global context is used. >>> IntSort() Int >>> x = Const('x', IntSort()) >>> is_int(x) True >>> x.sort() == IntSort() True >>> x.sort() == BoolSort() False
Definition at line 2614 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Sort.create(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), FreshInt(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), Int(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), QuantifierRef.is_forall(), is_K(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), K(), Map(), Context.MkInt(), Context.MkIntConst(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), ArrayRef.sort(), Store(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
02614 02615 def IntSort(ctx=None): 02616 """Return the interger sort in the given context. If `ctx=None`, then the global context is used. 02617 02618 >>> IntSort() 02619 Int 02620 >>> x = Const('x', IntSort()) 02621 >>> is_int(x) 02622 True 02623 >>> x.sort() == IntSort() 02624 True 02625 >>> x.sort() == BoolSort() 02626 False 02627 """ 02628 ctx = _get_ctx(ctx) 02629 return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
def z3py.IntVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 integer value. If `ctx=None`, then the global context is used. >>> IntVal(1) 1 >>> IntVal("100") 100
Definition at line 2661 of file z3py.py.
Referenced by AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_long(), IntNumRef.as_string(), is_arith(), is_int(), is_int_value(), is_rational_value(), AstMap.keys(), and AstMap.reset().
02661 02662 def IntVal(val, ctx=None): 02663 """Return a Z3 integer value. If `ctx=None`, then the global context is used. 02664 02665 >>> IntVal(1) 02666 1 02667 >>> IntVal("100") 02668 100 02669 """ 02670 ctx = _get_ctx(ctx) 02671 return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
def z3py.IntVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of integer constants of size `sz`. >>> X = IntVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2
def z3py.is_add | ( | a | ) |
Return `True` if `a` is an expression of the form b + c. >>> x, y = Ints('x y') >>> is_add(x + y) True >>> is_add(x - y) False
def z3py.is_algebraic_value | ( | a | ) |
Return `True` if `a` is an algerbraic value of sort Real. >>> is_algebraic_value(RealVal("3/5")) False >>> n = simplify(Sqrt(2)) >>> n 1.4142135623? >>> is_algebraic_value(n) True
Definition at line 2305 of file z3py.py.
02305 02306 def is_algebraic_value(a): 02307 """Return `True` if `a` is an algerbraic value of sort Real. 02308 02309 >>> is_algebraic_value(RealVal("3/5")) 02310 False 02311 >>> n = simplify(Sqrt(2)) 02312 >>> n 02313 1.4142135623? 02314 >>> is_algebraic_value(n) 02315 True 02316 """ 02317 return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
def z3py.is_and | ( | a | ) |
Return `True` if `a` is a Z3 and expression. >>> p, q = Bools('p q') >>> is_and(And(p, q)) True >>> is_and(Or(p, q)) False
def z3py.is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application. Note that, constants are function applications with 0 arguments. >>> a = Int('a') >>> is_app(a) True >>> is_app(a + 1) True >>> is_app(IntSort()) False >>> is_app(1) False >>> is_app(IntVal(1)) True >>> x = Int('x') >>> is_app(ForAll(x, x >= 0)) False
Definition at line 970 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), and ExprRef.num_args().
00970 00971 def is_app(a): 00972 """Return `True` if `a` is a Z3 function application. 00973 00974 Note that, constants are function applications with 0 arguments. 00975 00976 >>> a = Int('a') 00977 >>> is_app(a) 00978 True 00979 >>> is_app(a + 1) 00980 True 00981 >>> is_app(IntSort()) 00982 False 00983 >>> is_app(1) 00984 False 00985 >>> is_app(IntVal(1)) 00986 True 00987 >>> x = Int('x') 00988 >>> is_app(ForAll(x, x >= 0)) 00989 False 00990 """ 00991 if not isinstance(a, ExprRef): 00992 return False 00993 k = _ast_kind(a.ctx, a) 00994 return k == Z3_NUMERAL_AST or k == Z3_APP_AST
def z3py.is_app_of | ( | a, | |
k | |||
) |
Return `True` if `a` is an application of the given kind `k`. >>> x = Int('x') >>> n = x + 1 >>> is_app_of(n, Z3_OP_ADD) True >>> is_app_of(n, Z3_OP_MUL) False
Definition at line 1069 of file z3py.py.
Referenced by is_add(), is_and(), is_distinct(), is_eq(), is_false(), is_not(), is_or(), and is_true().
01069 01070 def is_app_of(a, k): 01071 """Return `True` if `a` is an application of the given kind `k`. 01072 01073 >>> x = Int('x') 01074 >>> n = x + 1 01075 >>> is_app_of(n, Z3_OP_ADD) 01076 True 01077 >>> is_app_of(n, Z3_OP_MUL) 01078 False 01079 """ 01080 return is_app(a) and a.decl().kind() == k
def z3py.is_arith | ( | a | ) |
Return `True` if `a` is an arithmetical expression. >>> x = Int('x') >>> is_arith(x) True >>> is_arith(x + 1) True >>> is_arith(1) False >>> is_arith(IntVal(1)) True >>> y = Real('y') >>> is_arith(y) True >>> is_arith(y + 1) True
Definition at line 2199 of file z3py.py.
Referenced by is_algebraic_value().
02199 02200 def is_arith(a): 02201 """Return `True` if `a` is an arithmetical expression. 02202 02203 >>> x = Int('x') 02204 >>> is_arith(x) 02205 True 02206 >>> is_arith(x + 1) 02207 True 02208 >>> is_arith(1) 02209 False 02210 >>> is_arith(IntVal(1)) 02211 True 02212 >>> y = Real('y') 02213 >>> is_arith(y) 02214 True 02215 >>> is_arith(y + 1) 02216 True 02217 """ 02218 return isinstance(a, ArithRef)
def z3py.is_arith_sort | ( | s | ) |
Return `True` if s is an arithmetical sort (type). >>> is_arith_sort(IntSort()) True >>> is_arith_sort(RealSort()) True >>> is_arith_sort(BoolSort()) False >>> n = Int('x') + 1 >>> is_arith_sort(n.sort()) True
Definition at line 1902 of file z3py.py.
01902 01903 def is_arith_sort(s): 01904 """Return `True` if s is an arithmetical sort (type). 01905 01906 >>> is_arith_sort(IntSort()) 01907 True 01908 >>> is_arith_sort(RealSort()) 01909 True 01910 >>> is_arith_sort(BoolSort()) 01911 False 01912 >>> n = Int('x') + 1 01913 >>> is_arith_sort(n.sort()) 01914 True 01915 """ 01916 return isinstance(s, ArithSortRef)
def z3py.is_array | ( | a | ) |
Return `True` if `a` is a Z3 array expression. >>> a = Array('a', IntSort(), IntSort()) >>> is_array(a) True >>> is_array(Store(a, 0, 1)) True >>> is_array(a[0]) False
Definition at line 3886 of file z3py.py.
03886 03887 def is_array(a): 03888 """Return `True` if `a` is a Z3 array expression. 03889 03890 >>> a = Array('a', IntSort(), IntSort()) 03891 >>> is_array(a) 03892 True 03893 >>> is_array(Store(a, 0, 1)) 03894 True 03895 >>> is_array(a[0]) 03896 False 03897 """ 03898 return isinstance(a, ArrayRef)
def z3py.is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 5529 of file z3py.py.
Referenced by get_as_array_func().
05529 05530 def is_as_array(n): 05531 """Return true if n is a Z3 expression of the form (_ as-array f).""" 05532 return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
def z3py.is_ast | ( | a | ) |
Return `True` if `a` is an AST node. >>> is_ast(10) False >>> is_ast(IntVal(10)) True >>> is_ast(Int('x')) True >>> is_ast(BoolSort()) True >>> is_ast(Function('f', IntSort(), IntSort())) True >>> is_ast("x") False >>> is_ast(Solver()) False
Definition at line 352 of file z3py.py.
Referenced by AstRef.eq(), and eq().
00352 00353 def is_ast(a): 00354 """Return `True` if `a` is an AST node. 00355 00356 >>> is_ast(10) 00357 False 00358 >>> is_ast(IntVal(10)) 00359 True 00360 >>> is_ast(Int('x')) 00361 True 00362 >>> is_ast(BoolSort()) 00363 True 00364 >>> is_ast(Function('f', IntSort(), IntSort())) 00365 True 00366 >>> is_ast("x") 00367 False 00368 >>> is_ast(Solver()) 00369 False 00370 """ 00371 return isinstance(a, AstRef)
def z3py.is_bool | ( | a | ) |
Return `True` if `a` is a Z3 Boolean expression. >>> p = Bool('p') >>> is_bool(p) True >>> q = Bool('q') >>> is_bool(And(p, q)) True >>> x = Real('x') >>> is_bool(x) False >>> is_bool(x == 0) True
Definition at line 1225 of file z3py.py.
Referenced by BoolSort(), and prove().
01225 01226 def is_bool(a): 01227 """Return `True` if `a` is a Z3 Boolean expression. 01228 01229 >>> p = Bool('p') 01230 >>> is_bool(p) 01231 True 01232 >>> q = Bool('q') 01233 >>> is_bool(And(p, q)) 01234 True 01235 >>> x = Real('x') 01236 >>> is_bool(x) 01237 False 01238 >>> is_bool(x == 0) 01239 True 01240 """ 01241 return isinstance(a, BoolRef)
def z3py.is_bv | ( | a | ) |
def z3py.is_bv_sort | ( | s | ) |
Return True if `s` is a Z3 bit-vector sort. >>> is_bv_sort(BitVecSort(32)) True >>> is_bv_sort(IntSort()) False
Definition at line 2929 of file z3py.py.
Referenced by BitVecVal().
02929 02930 def is_bv_sort(s): 02931 """Return True if `s` is a Z3 bit-vector sort. 02932 02933 >>> is_bv_sort(BitVecSort(32)) 02934 True 02935 >>> is_bv_sort(IntSort()) 02936 False 02937 """ 02938 return isinstance(s, BitVecSortRef)
def z3py.is_bv_value | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector numeral value. >>> b = BitVec('b', 32) >>> is_bv_value(b) False >>> b = BitVecVal(10, 32) >>> b 10 >>> is_bv_value(b) True
Definition at line 3403 of file z3py.py.
03403 03404 def is_bv_value(a): 03405 """Return `True` if `a` is a Z3 bit-vector numeral value. 03406 03407 >>> b = BitVec('b', 32) 03408 >>> is_bv_value(b) 03409 False 03410 >>> b = BitVecVal(10, 32) 03411 >>> b 03412 10 03413 >>> is_bv_value(b) 03414 True 03415 """ 03416 return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
def z3py.is_const | ( | a | ) |
Return `True` if `a` is Z3 constant/variable expression. >>> a = Int('a') >>> is_const(a) True >>> is_const(a + 1) False >>> is_const(1) False >>> is_const(IntVal(1)) True >>> x = Int('x') >>> is_const(ForAll(x, x >= 0)) False
Definition at line 995 of file z3py.py.
Referenced by prove().
00995 00996 def is_const(a): 00997 """Return `True` if `a` is Z3 constant/variable expression. 00998 00999 >>> a = Int('a') 01000 >>> is_const(a) 01001 True 01002 >>> is_const(a + 1) 01003 False 01004 >>> is_const(1) 01005 False 01006 >>> is_const(IntVal(1)) 01007 True 01008 >>> x = Int('x') 01009 >>> is_const(ForAll(x, x >= 0)) 01010 False 01011 """ 01012 return is_app(a) and a.num_args() == 0
def z3py.is_const_array | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_const_array(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_const_array(a) False
Definition at line 3899 of file z3py.py.
03899 03900 def is_const_array(a): 03901 """Return `True` if `a` is a Z3 constant array. 03902 03903 >>> a = K(IntSort(), 10) 03904 >>> is_const_array(a) 03905 True 03906 >>> a = Array('a', IntSort(), IntSort()) 03907 >>> is_const_array(a) 03908 False 03909 """ 03910 return is_app_of(a, Z3_OP_CONST_ARRAY)
def z3py.is_distinct | ( | a | ) |
Return `True` if `a` is a Z3 distinct expression. >>> x, y, z = Ints('x y z') >>> is_distinct(x == y) False >>> is_distinct(Distinct(x, y, z)) True
Definition at line 1314 of file z3py.py.
01314 01315 def is_distinct(a): 01316 """Return `True` if `a` is a Z3 distinct expression. 01317 01318 >>> x, y, z = Ints('x y z') 01319 >>> is_distinct(x == y) 01320 False 01321 >>> is_distinct(Distinct(x, y, z)) 01322 True 01323 """ 01324 return is_app_of(a, Z3_OP_DISTINCT)
def z3py.is_div | ( | a | ) |
Return `True` if `a` is an expression of the form b / c. >>> x, y = Reals('x y') >>> is_div(x / y) True >>> is_div(x + y) False >>> x, y = Ints('x y') >>> is_div(x / y) False >>> is_idiv(x / y) True
Definition at line 2351 of file z3py.py.
02351 02352 def is_div(a): 02353 """Return `True` if `a` is an expression of the form b / c. 02354 02355 >>> x, y = Reals('x y') 02356 >>> is_div(x / y) 02357 True 02358 >>> is_div(x + y) 02359 False 02360 >>> x, y = Ints('x y') 02361 >>> is_div(x / y) 02362 False 02363 >>> is_idiv(x / y) 02364 True 02365 """ 02366 return is_app_of(a, Z3_OP_DIV)
def z3py.is_eq | ( | a | ) |
Return `True` if `a` is a Z3 equality expression. >>> x, y = Ints('x y') >>> is_eq(x == y) True
def z3py.is_expr | ( | a | ) |
Return `True` if `a` is a Z3 expression. >>> a = Int('a') >>> is_expr(a) True >>> is_expr(a + 1) True >>> is_expr(IntSort()) False >>> is_expr(1) False >>> is_expr(IntVal(1)) True >>> x = Int('x') >>> is_expr(ForAll(x, x >= 0)) True
Definition at line 950 of file z3py.py.
Referenced by SortRef.cast(), BoolSortRef.cast(), Cbrt(), ExprRef.children(), is_var(), simplify(), substitute(), and substitute_vars().
00950 00951 def is_expr(a): 00952 """Return `True` if `a` is a Z3 expression. 00953 00954 >>> a = Int('a') 00955 >>> is_expr(a) 00956 True 00957 >>> is_expr(a + 1) 00958 True 00959 >>> is_expr(IntSort()) 00960 False 00961 >>> is_expr(1) 00962 False 00963 >>> is_expr(IntVal(1)) 00964 True 00965 >>> x = Int('x') 00966 >>> is_expr(ForAll(x, x >= 0)) 00967 True 00968 """ 00969 return isinstance(a, ExprRef)
def z3py.is_false | ( | a | ) |
def z3py.is_func_decl | ( | a | ) |
Return `True` if `a` is a Z3 function declaration. >>> f = Function('f', IntSort(), IntSort()) >>> is_func_decl(f) True >>> x = Real('x') >>> is_func_decl(x) False
Definition at line 689 of file z3py.py.
Referenced by prove().
00689 00690 def is_func_decl(a): 00691 """Return `True` if `a` is a Z3 function declaration. 00692 00693 >>> f = Function('f', IntSort(), IntSort()) 00694 >>> is_func_decl(f) 00695 True 00696 >>> x = Real('x') 00697 >>> is_func_decl(x) 00698 False 00699 """ 00700 return isinstance(a, FuncDeclRef)
def z3py.is_ge | ( | a | ) |
Return `True` if `a` is an expression of the form b >= c. >>> x, y = Ints('x y') >>> is_ge(x >= y) True >>> is_ge(x == y) False
def z3py.is_gt | ( | a | ) |
Return `True` if `a` is an expression of the form b > c. >>> x, y = Ints('x y') >>> is_gt(x > y) True >>> is_gt(x == y) False
def z3py.is_idiv | ( | a | ) |
def z3py.is_int | ( | a | ) |
Return `True` if `a` is an integer expression. >>> x = Int('x') >>> is_int(x + 1) True >>> is_int(1) False >>> is_int(IntVal(1)) True >>> y = Real('y') >>> is_int(y) False >>> is_int(y + 1) False
Definition at line 2219 of file z3py.py.
Referenced by Int(), IntSort(), and RealSort().
02219 02220 def is_int(a): 02221 """Return `True` if `a` is an integer expression. 02222 02223 >>> x = Int('x') 02224 >>> is_int(x + 1) 02225 True 02226 >>> is_int(1) 02227 False 02228 >>> is_int(IntVal(1)) 02229 True 02230 >>> y = Real('y') 02231 >>> is_int(y) 02232 False 02233 >>> is_int(y + 1) 02234 False 02235 """ 02236 return is_arith(a) and a.is_int()
def z3py.is_int_value | ( | a | ) |
Return `True` if `a` is an integer value of sort Int. >>> is_int_value(IntVal(1)) True >>> is_int_value(1) False >>> is_int_value(Int('x')) False >>> n = Int('x') + 1 >>> n x + 1 >>> n.arg(1) 1 >>> is_int_value(n.arg(1)) True >>> is_int_value(RealVal("1/3")) False >>> is_int_value(RealVal(1)) False
Definition at line 2261 of file z3py.py.
02261 02262 def is_int_value(a): 02263 """Return `True` if `a` is an integer value of sort Int. 02264 02265 >>> is_int_value(IntVal(1)) 02266 True 02267 >>> is_int_value(1) 02268 False 02269 >>> is_int_value(Int('x')) 02270 False 02271 >>> n = Int('x') + 1 02272 >>> n 02273 x + 1 02274 >>> n.arg(1) 02275 1 02276 >>> is_int_value(n.arg(1)) 02277 True 02278 >>> is_int_value(RealVal("1/3")) 02279 False 02280 >>> is_int_value(RealVal(1)) 02281 False 02282 """ 02283 return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
def z3py.is_is_int | ( | a | ) |
Return `True` if `a` is an expression of the form IsInt(b). >>> x = Real('x') >>> is_is_int(IsInt(x)) True >>> is_is_int(x) False
def z3py.is_K | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_K(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_K(a) False
def z3py.is_le | ( | a | ) |
Return `True` if `a` is an expression of the form b <= c. >>> x, y = Ints('x y') >>> is_le(x <= y) True >>> is_le(x < y) False
def z3py.is_lt | ( | a | ) |
Return `True` if `a` is an expression of the form b < c. >>> x, y = Ints('x y') >>> is_lt(x < y) True >>> is_lt(x == y) False
def z3py.is_map | ( | a | ) |
Return `True` if `a` is a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> a Map(f, b) >>> is_map(a) True >>> is_map(b) False
Definition at line 3923 of file z3py.py.
Referenced by get_map_func().
03923 03924 def is_map(a): 03925 """Return `True` if `a` is a Z3 map array expression. 03926 03927 >>> f = Function('f', IntSort(), IntSort()) 03928 >>> b = Array('b', IntSort(), IntSort()) 03929 >>> a = Map(f, b) 03930 >>> a 03931 Map(f, b) 03932 >>> is_map(a) 03933 True 03934 >>> is_map(b) 03935 False 03936 """ 03937 return is_app_of(a, Z3_OP_ARRAY_MAP)
def z3py.is_mod | ( | a | ) |
Return `True` if `a` is an expression of the form b % c. >>> x, y = Ints('x y') >>> is_mod(x % y) True >>> is_mod(x + y) False
def z3py.is_mul | ( | a | ) |
Return `True` if `a` is an expression of the form b * c. >>> x, y = Ints('x y') >>> is_mul(x * y) True >>> is_mul(x - y) False
def z3py.is_not | ( | a | ) |
Return `True` if `a` is a Z3 not expression. >>> p = Bool('p') >>> is_not(p) False >>> is_not(Not(p)) True
def z3py.is_or | ( | a | ) |
Return `True` if `a` is a Z3 or expression. >>> p, q = Bools('p q') >>> is_or(Or(p, q)) True >>> is_or(And(p, q)) False
def z3py.is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) >>> q ForAll(x, f(x) == 0) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) f(Var(0))
Definition at line 1545 of file z3py.py.
Referenced by MultiPattern().
01545 01546 def is_pattern(a): 01547 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. 01548 01549 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 01550 01551 >>> f = Function('f', IntSort(), IntSort()) 01552 >>> x = Int('x') 01553 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) 01554 >>> q 01555 ForAll(x, f(x) == 0) 01556 >>> q.num_patterns() 01557 1 01558 >>> is_pattern(q.pattern(0)) 01559 True 01560 >>> q.pattern(0) 01561 f(Var(0)) 01562 """ 01563 return isinstance(a, PatternRef)
def z3py.is_probe | ( | p | ) |
def z3py.is_quantifier | ( | a | ) |
Return `True` if `a` is a Z3 quantifier. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> is_quantifier(q) True >>> is_quantifier(f(x)) False
Definition at line 1748 of file z3py.py.
Referenced by Exists().
01748 01749 def is_quantifier(a): 01750 """Return `True` if `a` is a Z3 quantifier. 01751 01752 >>> f = Function('f', IntSort(), IntSort()) 01753 >>> x = Int('x') 01754 >>> q = ForAll(x, f(x) == 0) 01755 >>> is_quantifier(q) 01756 True 01757 >>> is_quantifier(f(x)) 01758 False 01759 """ 01760 return isinstance(a, QuantifierRef)
def z3py.is_rational_value | ( | a | ) |
Return `True` if `a` is rational value of sort Real. >>> is_rational_value(RealVal(1)) True >>> is_rational_value(RealVal("3/5")) True >>> is_rational_value(IntVal(1)) False >>> is_rational_value(1) False >>> n = Real('x') + 1 >>> n.arg(1) 1 >>> is_rational_value(n.arg(1)) True >>> is_rational_value(Real('x')) False
Definition at line 2284 of file z3py.py.
Referenced by RatNumRef.denominator(), and RatNumRef.numerator().
02284 02285 def is_rational_value(a): 02286 """Return `True` if `a` is rational value of sort Real. 02287 02288 >>> is_rational_value(RealVal(1)) 02289 True 02290 >>> is_rational_value(RealVal("3/5")) 02291 True 02292 >>> is_rational_value(IntVal(1)) 02293 False 02294 >>> is_rational_value(1) 02295 False 02296 >>> n = Real('x') + 1 02297 >>> n.arg(1) 02298 1 02299 >>> is_rational_value(n.arg(1)) 02300 True 02301 >>> is_rational_value(Real('x')) 02302 False 02303 """ 02304 return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
def z3py.is_real | ( | a | ) |
Return `True` if `a` is a real expression. >>> x = Int('x') >>> is_real(x + 1) False >>> y = Real('y') >>> is_real(y) True >>> is_real(y + 1) True >>> is_real(1) False >>> is_real(RealVal(1)) True
Definition at line 2237 of file z3py.py.
Referenced by Real(), and RealSort().
02237 02238 def is_real(a): 02239 """Return `True` if `a` is a real expression. 02240 02241 >>> x = Int('x') 02242 >>> is_real(x + 1) 02243 False 02244 >>> y = Real('y') 02245 >>> is_real(y) 02246 True 02247 >>> is_real(y + 1) 02248 True 02249 >>> is_real(1) 02250 False 02251 >>> is_real(RealVal(1)) 02252 True 02253 """ 02254 return is_arith(a) and a.is_real()
def z3py.is_select | ( | a | ) |
Return `True` if `a` is a Z3 array select application. >>> a = Array('a', IntSort(), IntSort()) >>> is_select(a) False >>> i = Int('i') >>> is_select(a[i]) True
def z3py.is_sort | ( | s | ) |
Return `True` if `s` is a Z3 sort. >>> is_sort(IntSort()) True >>> is_sort(Int('x')) False >>> is_expr(Int('x')) True
Definition at line 532 of file z3py.py.
Referenced by ArraySort(), CreateDatatypes(), Function(), prove(), and Var().
def z3py.is_store | ( | a | ) |
Return `True` if `a` is a Z3 array store application. >>> a = Array('a', IntSort(), IntSort()) >>> is_store(a) False >>> is_store(Store(a, 0, 1)) True
def z3py.is_sub | ( | a | ) |
Return `True` if `a` is an expression of the form b - c. >>> x, y = Ints('x y') >>> is_sub(x - y) True >>> is_sub(x + y) False
def z3py.is_to_int | ( | a | ) |
Return `True` if `a` is an expression of the form ToInt(b). >>> x = Real('x') >>> n = ToInt(x) >>> n ToInt(x) >>> is_to_int(n) True >>> is_to_int(x) False
def z3py.is_to_real | ( | a | ) |
Return `True` if `a` is an expression of the form ToReal(b). >>> x = Int('x') >>> n = ToReal(x) >>> n ToReal(x) >>> is_to_real(n) True >>> is_to_real(x) False
Definition at line 2444 of file z3py.py.
02444 02445 def is_to_real(a): 02446 """Return `True` if `a` is an expression of the form ToReal(b). 02447 02448 >>> x = Int('x') 02449 >>> n = ToReal(x) 02450 >>> n 02451 ToReal(x) 02452 >>> is_to_real(n) 02453 True 02454 >>> is_to_real(x) 02455 False 02456 """ 02457 return is_app_of(a, Z3_OP_TO_REAL)
def z3py.is_true | ( | a | ) |
Return `True` if `a` is the Z3 true expression. >>> p = Bool('p') >>> is_true(p) False >>> is_true(simplify(p == p)) True >>> x = Real('x') >>> is_true(x == 0) False >>> # True is a Python Boolean expression >>> is_true(True) False
Definition at line 1242 of file z3py.py.
Referenced by BoolVal().
01242 01243 def is_true(a): 01244 """Return `True` if `a` is the Z3 true expression. 01245 01246 >>> p = Bool('p') 01247 >>> is_true(p) 01248 False 01249 >>> is_true(simplify(p == p)) 01250 True 01251 >>> x = Real('x') 01252 >>> is_true(x == 0) 01253 False 01254 >>> # True is a Python Boolean expression 01255 >>> is_true(True) 01256 False 01257 """ 01258 return is_app_of(a, Z3_OP_TRUE)
def z3py.is_var | ( | a | ) |
Return `True` if `a` is variable. Z3 uses de-Bruijn indices for representing bound variables in quantifiers. >>> x = Int('x') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort()) >>> # Z3 replaces x with bound variables when ForAll is executed. >>> q = ForAll(x, f(x) == x) >>> b = q.body() >>> b f(Var(0)) == Var(0) >>> b.arg(1) Var(0) >>> is_var(b.arg(1)) True
Definition at line 1013 of file z3py.py.
Referenced by get_var_index().
01013 01014 def is_var(a): 01015 """Return `True` if `a` is variable. 01016 01017 Z3 uses de-Bruijn indices for representing bound variables in 01018 quantifiers. 01019 01020 >>> x = Int('x') 01021 >>> is_var(x) 01022 False 01023 >>> is_const(x) 01024 True 01025 >>> f = Function('f', IntSort(), IntSort()) 01026 >>> # Z3 replaces x with bound variables when ForAll is executed. 01027 >>> q = ForAll(x, f(x) == x) 01028 >>> b = q.body() 01029 >>> b 01030 f(Var(0)) == Var(0) 01031 >>> b.arg(1) 01032 Var(0) 01033 >>> is_var(b.arg(1)) 01034 True 01035 """ 01036 return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
def z3py.IsInt | ( | a | ) |
Return the Z3 predicate IsInt(a). >>> x = Real('x') >>> IsInt(x + "1/2") IsInt(x + 1/2) >>> solve(IsInt(x + "1/2"), x > 0, x < 1) [x = 1/2] >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") no solution
Definition at line 2851 of file z3py.py.
Referenced by is_is_int().
02851 02852 def IsInt(a): 02853 """ Return the Z3 predicate IsInt(a). 02854 02855 >>> x = Real('x') 02856 >>> IsInt(x + "1/2") 02857 IsInt(x + 1/2) 02858 >>> solve(IsInt(x + "1/2"), x > 0, x < 1) 02859 [x = 1/2] 02860 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") 02861 no solution 02862 """ 02863 if __debug__: 02864 _z3_assert(a.is_real(), "Z3 real expression expected.") 02865 ctx = a.ctx 02866 return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
def z3py.K | ( | dom, | |
v | |||
) |
Return a Z3 constant array expression. >>> a = K(IntSort(), 10) >>> a K(Int, 10) >>> a.sort() Array(Int, Int) >>> i = Int('i') >>> a[i] K(Int, 10)[i] >>> simplify(a[i]) 10
Definition at line 4062 of file z3py.py.
Referenced by is_const_array(), and is_K().
04062 04063 def K(dom, v): 04064 """Return a Z3 constant array expression. 04065 04066 >>> a = K(IntSort(), 10) 04067 >>> a 04068 K(Int, 10) 04069 >>> a.sort() 04070 Array(Int, Int) 04071 >>> i = Int('i') 04072 >>> a[i] 04073 K(Int, 10)[i] 04074 >>> simplify(a[i]) 04075 10 04076 """ 04077 if __debug__: 04078 _z3_assert(is_sort(dom), "Z3 sort expected") 04079 ctx = dom.ctx 04080 if not is_expr(v): 04081 v = _py2expr(v, ctx) 04082 return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
def z3py.LShR | ( | a, | |
b | |||
) |
Create the Z3 expression logical right shift. Use the operator >> for the arithmetical right shift. >>> x, y = BitVecs('x y', 32) >>> LShR(x, y) LShR(x, y) >>> (x >> y).sexpr() '(bvashr x y)' >>> LShR(x, y).sexpr() '(bvlshr x y)' >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() -4 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() -2 >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) 2 >>> simplify(BitVecVal(2, 3) >> 1) 1 >>> simplify(LShR(BitVecVal(2, 3), 1)) 1
Definition at line 3676 of file z3py.py.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), and BitVecRef.__rshift__().
03676 03677 def LShR(a, b): 03678 """Create the Z3 expression logical right shift. 03679 03680 Use the operator >> for the arithmetical right shift. 03681 03682 >>> x, y = BitVecs('x y', 32) 03683 >>> LShR(x, y) 03684 LShR(x, y) 03685 >>> (x >> y).sexpr() 03686 '(bvashr x y)' 03687 >>> LShR(x, y).sexpr() 03688 '(bvlshr x y)' 03689 >>> BitVecVal(4, 3) 03690 4 03691 >>> BitVecVal(4, 3).as_signed_long() 03692 -4 03693 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() 03694 -2 03695 >>> simplify(BitVecVal(4, 3) >> 1) 03696 6 03697 >>> simplify(LShR(BitVecVal(4, 3), 1)) 03698 2 03699 >>> simplify(BitVecVal(2, 3) >> 1) 03700 1 03701 >>> simplify(LShR(BitVecVal(2, 3), 1)) 03702 1 03703 """ 03704 _check_bv_args(a, b) 03705 a, b = _coerce_exprs(a, b) 03706 return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.main_ctx | ( | ) |
Return a reference to the global Z3 context. >>> x = Real('x') >>> x.ctx == main_ctx() True >>> c = Context() >>> c == main_ctx() False >>> x2 = Real('x', c) >>> x2.ctx == c True >>> eq(x, x2) False
Definition at line 188 of file z3py.py.
Referenced by And(), help_simplify(), simplify_param_descrs(), and Goal.translate().
00188 00189 def main_ctx(): 00190 """Return a reference to the global Z3 context. 00191 00192 >>> x = Real('x') 00193 >>> x.ctx == main_ctx() 00194 True 00195 >>> c = Context() 00196 >>> c == main_ctx() 00197 False 00198 >>> x2 = Real('x', c) 00199 >>> x2.ctx == c 00200 True 00201 >>> eq(x, x2) 00202 False 00203 """ 00204 global _main_ctx 00205 if _main_ctx == None: 00206 _main_ctx = Context() 00207 return _main_ctx
def z3py.Map | ( | f, | |
args | |||
) |
Return a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> a1 = Array('a1', IntSort(), IntSort()) >>> a2 = Array('a2', IntSort(), IntSort()) >>> b = Map(f, a1, a2) >>> b Map(f, a1, a2) >>> prove(b[0] == f(a1[0], a2[0])) proved
Definition at line 4040 of file z3py.py.
Referenced by Context.Context(), get_map_func(), InterpolationContext.InterpolationContext(), and is_map().
04040 04041 def Map(f, *args): 04042 """Return a Z3 map array expression. 04043 04044 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 04045 >>> a1 = Array('a1', IntSort(), IntSort()) 04046 >>> a2 = Array('a2', IntSort(), IntSort()) 04047 >>> b = Map(f, a1, a2) 04048 >>> b 04049 Map(f, a1, a2) 04050 >>> prove(b[0] == f(a1[0], a2[0])) 04051 proved 04052 """ 04053 args = _get_args(args) 04054 if __debug__: 04055 _z3_assert(len(args) > 0, "At least one Z3 array expression expected") 04056 _z3_assert(is_func_decl(f), "First argument must be a Z3 function declaration") 04057 _z3_assert(all([is_array(a) for a in args]), "Z3 array expected expected") 04058 _z3_assert(len(args) == f.arity(), "Number of arguments mismatch") 04059 _args, sz = _to_ast_array(args) 04060 ctx = f.ctx 04061 return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
def z3py.MultiPattern | ( | args | ) |
Create a Z3 multi-pattern using the given expressions `*args` See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) >>> q ForAll(x, f(x) != g(x)) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) MultiPattern(f(Var(0)), g(Var(0)))
Definition at line 1564 of file z3py.py.
01564 01565 def MultiPattern(*args): 01566 """Create a Z3 multi-pattern using the given expressions `*args` 01567 01568 See http://rise4fun.com/Z3Py/tutorial/advanced for more details. 01569 01570 >>> f = Function('f', IntSort(), IntSort()) 01571 >>> g = Function('g', IntSort(), IntSort()) 01572 >>> x = Int('x') 01573 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) 01574 >>> q 01575 ForAll(x, f(x) != g(x)) 01576 >>> q.num_patterns() 01577 1 01578 >>> is_pattern(q.pattern(0)) 01579 True 01580 >>> q.pattern(0) 01581 MultiPattern(f(Var(0)), g(Var(0))) 01582 """ 01583 if __debug__: 01584 _z3_assert(len(args) > 0, "At least one argument expected") 01585 _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected") 01586 ctx = args[0].ctx 01587 args, sz = _to_ast_array(args) 01588 return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
def z3py.Not | ( | a, | |
ctx = None |
|||
) |
Create a Z3 not expression or probe. >>> p = Bool('p') >>> Not(Not(p)) Not(Not(p)) >>> simplify(Not(Not(p))) p
Definition at line 1443 of file z3py.py.
Referenced by binary_interpolant(), Implies(), prove(), sequence_interpolant(), tree_interpolant(), and Xor().
01443 01444 def Not(a, ctx=None): 01445 """Create a Z3 not expression or probe. 01446 01447 >>> p = Bool('p') 01448 >>> Not(Not(p)) 01449 Not(Not(p)) 01450 >>> simplify(Not(Not(p))) 01451 p 01452 """ 01453 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx)) 01454 if is_probe(a): 01455 # Not is also used to build probes 01456 return Probe(Z3_probe_not(ctx.ref(), a.probe), ctx) 01457 else: 01458 s = BoolSort(ctx) 01459 a = s.cast(a) 01460 return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
def z3py.open_log | ( | fname | ) |
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 86 of file z3py.py.
00086 00087 def open_log(fname): 00088 """Log interaction to a file. This function must be invoked immediately after init(). """ 00089 Z3_open_log(fname)
def z3py.Or | ( | args | ) |
Create a Z3 or-expression or or-probe. >>> p, q, r = Bools('p q r') >>> Or(p, q, r) Or(p, q, r) >>> P = BoolVector('p', 5) >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 1498 of file z3py.py.
Referenced by ApplyResult.as_expr(), Bools(), and Implies().
01498 01499 def Or(*args): 01500 """Create a Z3 or-expression or or-probe. 01501 01502 >>> p, q, r = Bools('p q r') 01503 >>> Or(p, q, r) 01504 Or(p, q, r) 01505 >>> P = BoolVector('p', 5) 01506 >>> Or(P) 01507 Or(p__0, p__1, p__2, p__3, p__4) 01508 """ 01509 last_arg = None 01510 if len(args) > 0: 01511 last_arg = args[len(args)-1] 01512 if isinstance(last_arg, Context): 01513 ctx = args[len(args)-1] 01514 args = args[:len(args)-1] 01515 else: 01516 ctx = main_ctx() 01517 args = _get_args(args) 01518 ctx_args = _ctx_from_ast_arg_list(args, ctx) 01519 if __debug__: 01520 _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") 01521 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") 01522 if _has_probe(args): 01523 return _probe_or(args, ctx) 01524 else: 01525 args = _coerce_expr_list(args, ctx) 01526 _args, sz = _to_ast_array(args) 01527 return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
def z3py.OrElse | ( | ts, | |
ks | |||
) |
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) >>> # Tactic split-clause fails if there is no clause in the given goal. >>> t(x == 0) [[x == 0]] >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]]
Definition at line 6568 of file z3py.py.
06568 06569 def OrElse(*ts, **ks): 06570 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). 06571 06572 >>> x = Int('x') 06573 >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) 06574 >>> # Tactic split-clause fails if there is no clause in the given goal. 06575 >>> t(x == 0) 06576 [[x == 0]] 06577 >>> t(Or(x == 0, x == 1)) 06578 [[x == 0], [x == 1]] 06579 """ 06580 if __debug__: 06581 _z3_assert(len(ts) >= 2, "At least two arguments expected") 06582 ctx = ks.get('ctx', None) 06583 num = len(ts) 06584 r = ts[0] 06585 for i in range(num - 1): 06586 r = _or_else(r, ts[i+1], ctx) 06587 return r
def z3py.ParAndThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
Alias for ParThen(t1, t2, ctx).
Definition at line 6620 of file z3py.py.
06620 06621 def ParAndThen(t1, t2, ctx=None): 06622 """Alias for ParThen(t1, t2, ctx).""" 06623 return ParThen(t1, t2, ctx)
def z3py.ParOr | ( | ts, | |
ks | |||
) |
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = ParOr(Tactic('simplify'), Tactic('fail')) >>> t(x + 1 == 2) [[x == 1]]
Definition at line 6588 of file z3py.py.
06588 06589 def ParOr(*ts, **ks): 06590 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). 06591 06592 >>> x = Int('x') 06593 >>> t = ParOr(Tactic('simplify'), Tactic('fail')) 06594 >>> t(x + 1 == 2) 06595 [[x == 1]] 06596 """ 06597 if __debug__: 06598 _z3_assert(len(ts) >= 2, "At least two arguments expected") 06599 ctx = _get_ctx(ks.get('ctx', None)) 06600 ts = [ _to_tactic(t, ctx) for t in ts ] 06601 sz = len(ts) 06602 _args = (TacticObj * sz)() 06603 for i in range(sz): 06604 _args[i] = ts[i].tactic 06605 return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
def z3py.parse_smt2_file | ( | f, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a file in SMT 2.0 format using the given sorts and decls. This function is similar to parse_smt2_string().
Definition at line 7285 of file z3py.py.
07285 07286 def parse_smt2_file(f, sorts={}, decls={}, ctx=None): 07287 """Parse a file in SMT 2.0 format using the given sorts and decls. 07288 07289 This function is similar to parse_smt2_string(). 07290 """ 07291 ctx = _get_ctx(ctx) 07292 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 07293 dsz, dnames, ddecls = _dict2darray(decls, ctx) 07294 return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
def z3py.parse_smt2_string | ( | s, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a string in SMT 2.0 format using the given sorts and decls. The arguments sorts and decls are Python dictionaries used to initialize the symbol table used for the SMT 2.0 parser. >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') And(x > 0, x < 10) >>> x, y = Ints('x y') >>> f = Function('f', IntSort(), IntSort()) >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) x + f(y) > 0 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) a > 0
Definition at line 7265 of file z3py.py.
Referenced by parse_smt2_file().
07265 07266 def parse_smt2_string(s, sorts={}, decls={}, ctx=None): 07267 """Parse a string in SMT 2.0 format using the given sorts and decls. 07268 07269 The arguments sorts and decls are Python dictionaries used to initialize 07270 the symbol table used for the SMT 2.0 parser. 07271 07272 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') 07273 And(x > 0, x < 10) 07274 >>> x, y = Ints('x y') 07275 >>> f = Function('f', IntSort(), IntSort()) 07276 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) 07277 x + f(y) > 0 07278 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) 07279 a > 0 07280 """ 07281 ctx = _get_ctx(ctx) 07282 ssz, snames, ssorts = _dict2sarray(sorts, ctx) 07283 dsz, dnames, ddecls = _dict2darray(decls, ctx) 07284 return _to_expr_ref(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
def z3py.ParThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. >>> x, y = Ints('x y') >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) >>> t(And(Or(x == 1, x == 2), y == x + 1)) [[x == 1, y == 2], [x == 2, y == 3]]
Definition at line 6606 of file z3py.py.
Referenced by ParAndThen().
06606 06607 def ParThen(t1, t2, ctx=None): 06608 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. 06609 06610 >>> x, y = Ints('x y') 06611 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) 06612 >>> t(And(Or(x == 1, x == 2), y == x + 1)) 06613 [[x == 1, y == 2], [x == 2, y == 3]] 06614 """ 06615 t1 = _to_tactic(t1, ctx) 06616 t2 = _to_tactic(t2, ctx) 06617 if __debug__: 06618 _z3_assert(t1.ctx == t2.ctx, "Context mismatch") 06619 return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
def z3py.probe_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the probe named `name`. >>> d = probe_description('memory')
Definition at line 6862 of file z3py.py.
Referenced by describe_probes().
06862 06863 def probe_description(name, ctx=None): 06864 """Return a short description for the probe named `name`. 06865 06866 >>> d = probe_description('memory') 06867 """ 06868 ctx = _get_ctx(ctx) 06869 return Z3_probe_get_descr(ctx.ref(), name)
def z3py.probes | ( | ctx = None | ) |
Return a list of all available probes in Z3. >>> l = probes() >>> l.count('memory') == 1 True
Definition at line 6852 of file z3py.py.
Referenced by describe_probes().
06852 06853 def probes(ctx=None): 06854 """Return a list of all available probes in Z3. 06855 06856 >>> l = probes() 06857 >>> l.count('memory') == 1 06858 True 06859 """ 06860 ctx = _get_ctx(ctx) 06861 return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
def z3py.Product | ( | args | ) |
Create the product of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Product(a, b, c) a*b*c >>> Product([a, b, c]) a*b*c >>> A = IntVector('a', 5) >>> Product(A) a__0*a__1*a__2*a__3*a__4
Definition at line 7059 of file z3py.py.
Referenced by BitVecs().
07059 07060 def Product(*args): 07061 """Create the product of the Z3 expressions. 07062 07063 >>> a, b, c = Ints('a b c') 07064 >>> Product(a, b, c) 07065 a*b*c 07066 >>> Product([a, b, c]) 07067 a*b*c 07068 >>> A = IntVector('a', 5) 07069 >>> Product(A) 07070 a__0*a__1*a__2*a__3*a__4 07071 """ 07072 args = _get_args(args) 07073 if __debug__: 07074 _z3_assert(len(args) > 0, "Non empty list of arguments expected") 07075 ctx = _ctx_from_ast_arg_list(args) 07076 if __debug__: 07077 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression") 07078 args = _coerce_expr_list(args, ctx) 07079 if is_bv(args[0]): 07080 return _reduce(lambda a, b: a * b, args, 1) 07081 else: 07082 _args, sz = _to_ast_array(args) 07083 return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
def z3py.prove | ( | claim, | |
keywords | |||
) |
Try to prove the given claim. This is a simple function for creating demonstrations. It tries to prove `claim` by showing the negation is unsatisfiable. >>> p, q = Bools('p q') >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) proved
Definition at line 7141 of file z3py.py.
Referenced by Map(), Store(), and Update().
07141 07142 def prove(claim, **keywords): 07143 """Try to prove the given claim. 07144 07145 This is a simple function for creating demonstrations. It tries to prove 07146 `claim` by showing the negation is unsatisfiable. 07147 07148 >>> p, q = Bools('p q') 07149 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q))) 07150 proved 07151 """ 07152 if __debug__: 07153 _z3_assert(is_bool(claim), "Z3 Boolean expression expected") 07154 s = Solver() 07155 s.set(**keywords) 07156 s.add(Not(claim)) 07157 if keywords.get('show', False): 07158 print(s) 07159 r = s.check() 07160 if r == unsat: 07161 print("proved") 07162 elif r == unknown: 07163 print("failed to prove") 07164 print(s.model()) 07165 else: 07166 print("counterexample") 07167 print(s.model())
def z3py.Q | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> Q(3,5) 3/5 >>> Q(3,5).sort() Real
Definition at line 2705 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), and RatNumRef.numerator().
def z3py.RatVal | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 2690 of file z3py.py.
Referenced by Q().
02690 02691 def RatVal(a, b, ctx=None): 02692 """Return a Z3 rational a/b. 02693 02694 If `ctx=None`, then the global context is used. 02695 02696 >>> RatVal(3,5) 02697 3/5 02698 >>> RatVal(3,5).sort() 02699 Real 02700 """ 02701 if __debug__: 02702 _z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer") 02703 _z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer") 02704 return simplify(RealVal(a, ctx)/RealVal(b, ctx))
def z3py.Real | ( | name, | |
ctx = None |
|||
) |
Return a real constant named `name`. If `ctx=None`, then the global context is used. >>> x = Real('x') >>> is_real(x) True >>> is_real(x + 1) True
Definition at line 2765 of file z3py.py.
Referenced by ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_is_int(), is_rational_value(), ArithSortRef.is_real(), ArithRef.is_real(), is_real(), is_to_int(), IsInt(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
02765 02766 def Real(name, ctx=None): 02767 """Return a real constant named `name`. If `ctx=None`, then the global context is used. 02768 02769 >>> x = Real('x') 02770 >>> is_real(x) 02771 True 02772 >>> is_real(x + 1) 02773 True 02774 """ 02775 ctx = _get_ctx(ctx) 02776 return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
def z3py.Reals | ( | names, | |
ctx = None |
|||
) |
Return a tuple of real constants. >>> x, y, z = Reals('x y z') >>> Sum(x, y, z) x + y + z >>> Sum(x, y, z).sort() Real
Definition at line 2777 of file z3py.py.
Referenced by is_div().
02777 02778 def Reals(names, ctx=None): 02779 """Return a tuple of real constants. 02780 02781 >>> x, y, z = Reals('x y z') 02782 >>> Sum(x, y, z) 02783 x + y + z 02784 >>> Sum(x, y, z).sort() 02785 Real 02786 """ 02787 ctx = _get_ctx(ctx) 02788 if isinstance(names, str): 02789 names = names.split(" ") 02790 return [Real(name, ctx) for name in names]
def z3py.RealSort | ( | ctx = None | ) |
Return the real sort in the given context. If `ctx=None`, then the global context is used. >>> RealSort() Real >>> x = Const('x', RealSort()) >>> is_real(x) True >>> is_int(x) False >>> x.sort() == RealSort() True
Definition at line 2630 of file z3py.py.
Referenced by ArithSortRef.cast(), Sort.create(), FreshReal(), Context.getRealSort(), is_arith_sort(), Context.MkReal(), Context.MkRealConst(), Context.mkRealSort(), Context.MkRealSort(), Real(), RealVar(), and QuantifierRef.var_sort().
02630 02631 def RealSort(ctx=None): 02632 """Return the real sort in the given context. If `ctx=None`, then the global context is used. 02633 02634 >>> RealSort() 02635 Real 02636 >>> x = Const('x', RealSort()) 02637 >>> is_real(x) 02638 True 02639 >>> is_int(x) 02640 False 02641 >>> x.sort() == RealSort() 02642 True 02643 """ 02644 ctx = _get_ctx(ctx) 02645 return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
def z3py.RealVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 real value. `val` may be a Python int, long, float or string representing a number in decimal or rational notation. If `ctx=None`, then the global context is used. >>> RealVal(1) 1 >>> RealVal(1).sort() Real >>> RealVal("3/5") 3/5 >>> RealVal("1.5") 3/2
Definition at line 2672 of file z3py.py.
Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), and RatVal().
02672 02673 def RealVal(val, ctx=None): 02674 """Return a Z3 real value. 02675 02676 `val` may be a Python int, long, float or string representing a number in decimal or rational notation. 02677 If `ctx=None`, then the global context is used. 02678 02679 >>> RealVal(1) 02680 1 02681 >>> RealVal(1).sort() 02682 Real 02683 >>> RealVal("3/5") 02684 3/5 02685 >>> RealVal("1.5") 02686 3/2 02687 """ 02688 ctx = _get_ctx(ctx) 02689 return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
def z3py.RealVar | ( | idx, | |
ctx = None |
|||
) |
Create a real free variable. Free variables are used to create quantified formulas. They are also used to create polynomials. >>> RealVar(0) Var(0)
Definition at line 1171 of file z3py.py.
Referenced by RealVarVector().
def z3py.RealVarVector | ( | n, | |
ctx = None |
|||
) |
Create a list of Real free variables. The variables have ids: 0, 1, ..., n-1 >>> x0, x1, x2, x3 = RealVarVector(4) >>> x2 Var(2)
Definition at line 1181 of file z3py.py.
01181 01182 def RealVarVector(n, ctx=None): 01183 """ 01184 Create a list of Real free variables. 01185 The variables have ids: 0, 1, ..., n-1 01186 01187 >>> x0, x1, x2, x3 = RealVarVector(4) 01188 >>> x2 01189 Var(2) 01190 """ 01191 return [ RealVar(i, ctx) for i in range(n) ]
def z3py.RealVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of real constants of size `sz`. >>> X = RealVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2 >>> Sum(X).sort() Real
Definition at line 2791 of file z3py.py.
02791 02792 def RealVector(prefix, sz, ctx=None): 02793 """Return a list of real constants of size `sz`. 02794 02795 >>> X = RealVector('x', 3) 02796 >>> X 02797 [x__0, x__1, x__2] 02798 >>> Sum(X) 02799 x__0 + x__1 + x__2 02800 >>> Sum(X).sort() 02801 Real 02802 """ 02803 return [ Real('%s__%s' % (prefix, i)) for i in range(sz) ]
def z3py.Repeat | ( | t, | |
max = 4294967295 , |
|||
ctx = None |
|||
) |
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. >>> x, y = Ints('x y') >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) >>> r = t(c) >>> for subgoal in r: print(subgoal) [x == 0, y == 0, x > y] [x == 0, y == 1, x > y] [x == 1, y == 0, x > y] [x == 1, y == 1, x > y] >>> t = Then(t, Tactic('propagate-values')) >>> t(c) [[x == 1, y == 0]]
Definition at line 6637 of file z3py.py.
06637 06638 def Repeat(t, max=4294967295, ctx=None): 06639 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. 06640 06641 >>> x, y = Ints('x y') 06642 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) 06643 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) 06644 >>> r = t(c) 06645 >>> for subgoal in r: print(subgoal) 06646 [x == 0, y == 0, x > y] 06647 [x == 0, y == 1, x > y] 06648 [x == 1, y == 0, x > y] 06649 [x == 1, y == 1, x > y] 06650 >>> t = Then(t, Tactic('propagate-values')) 06651 >>> t(c) 06652 [[x == 1, y == 0]] 06653 """ 06654 t = _to_tactic(t, ctx) 06655 return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
def z3py.RepeatBitVec | ( | n, | |
a | |||
) |
Return an expression representing `n` copies of `a`. >>> x = BitVec('x', 8) >>> n = RepeatBitVec(4, x) >>> n RepeatBitVec(4, x) >>> n.size() 32 >>> v0 = BitVecVal(10, 4) >>> print("%.x" % v0.as_long()) a >>> v = simplify(RepeatBitVec(4, v0)) >>> v.size() 16 >>> print("%.x" % v.as_long()) aaaa
Definition at line 3793 of file z3py.py.
03793 03794 def RepeatBitVec(n, a): 03795 """Return an expression representing `n` copies of `a`. 03796 03797 >>> x = BitVec('x', 8) 03798 >>> n = RepeatBitVec(4, x) 03799 >>> n 03800 RepeatBitVec(4, x) 03801 >>> n.size() 03802 32 03803 >>> v0 = BitVecVal(10, 4) 03804 >>> print("%.x" % v0.as_long()) 03805 a 03806 >>> v = simplify(RepeatBitVec(4, v0)) 03807 >>> v.size() 03808 16 03809 >>> print("%.x" % v.as_long()) 03810 aaaa 03811 """ 03812 if __debug__: 03813 _z3_assert(isinstance(n, int), "First argument must be an integer") 03814 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 03815 return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
def z3py.reset_params | ( | ) |
Reset all global (or module) parameters.
Definition at line 237 of file z3py.py.
00237 00238 def reset_params(): 00239 """Reset all global (or module) parameters. 00240 """ 00241 Z3_global_param_reset_all()
def z3py.RotateLeft | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the left `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateLeft(a, b) RotateLeft(a, b) >>> simplify(RotateLeft(a, 0)) a >>> simplify(RotateLeft(a, 16)) a
Definition at line 3707 of file z3py.py.
03707 03708 def RotateLeft(a, b): 03709 """Return an expression representing `a` rotated to the left `b` times. 03710 03711 >>> a, b = BitVecs('a b', 16) 03712 >>> RotateLeft(a, b) 03713 RotateLeft(a, b) 03714 >>> simplify(RotateLeft(a, 0)) 03715 a 03716 >>> simplify(RotateLeft(a, 16)) 03717 a 03718 """ 03719 _check_bv_args(a, b) 03720 a, b = _coerce_exprs(a, b) 03721 return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.RotateRight | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the right `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateRight(a, b) RotateRight(a, b) >>> simplify(RotateRight(a, 0)) a >>> simplify(RotateRight(a, 16)) a
Definition at line 3722 of file z3py.py.
03722 03723 def RotateRight(a, b): 03724 """Return an expression representing `a` rotated to the right `b` times. 03725 03726 >>> a, b = BitVecs('a b', 16) 03727 >>> RotateRight(a, b) 03728 RotateRight(a, b) 03729 >>> simplify(RotateRight(a, 0)) 03730 a 03731 >>> simplify(RotateRight(a, 16)) 03732 a 03733 """ 03734 _check_bv_args(a, b) 03735 a, b = _coerce_exprs(a, b) 03736 return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.Select | ( | a, | |
i | |||
) |
Return a Z3 select array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i = Int('i') >>> Select(a, i) a[i] >>> eq(Select(a, i), a[i]) True
Definition at line 4026 of file z3py.py.
04026 04027 def Select(a, i): 04028 """Return a Z3 select array expression. 04029 04030 >>> a = Array('a', IntSort(), IntSort()) 04031 >>> i = Int('i') 04032 >>> Select(a, i) 04033 a[i] 04034 >>> eq(Select(a, i), a[i]) 04035 True 04036 """ 04037 if __debug__: 04038 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 04039 return a[i]
def z3py.sequence_interpolant | ( | v, | |
p = None , |
|||
ctx = None |
|||
) |
Compute interpolant for a sequence of formulas. If len(v) == N, and if the conjunction of the formulas in v is unsatisfiable, the interpolant is a sequence of formulas w such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1: 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N) 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i] and v[i+1]..v[n] Requires len(v) >= 1. If a & b is satisfiable, raises an object of class ModelRef that represents a model of a & b. If parameters p are supplied, these are used in creating the solver that determines satisfiability. >>> x = Int('x') >>> y = Int('y') >>> print sequence_interpolant([x < 0, y == x , y > 2]) [Not(x >= 0), Not(y >= 0)]
Definition at line 7391 of file z3py.py.
07391 07392 def sequence_interpolant(v,p=None,ctx=None): 07393 """Compute interpolant for a sequence of formulas. 07394 07395 If len(v) == N, and if the conjunction of the formulas in v is 07396 unsatisfiable, the interpolant is a sequence of formulas w 07397 such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1: 07398 07399 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N) 07400 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i] 07401 and v[i+1]..v[n] 07402 07403 Requires len(v) >= 1. 07404 07405 If a & b is satisfiable, raises an object of class ModelRef 07406 that represents a model of a & b. 07407 07408 If parameters p are supplied, these are used in creating the 07409 solver that determines satisfiability. 07410 07411 >>> x = Int('x') 07412 >>> y = Int('y') 07413 >>> print sequence_interpolant([x < 0, y == x , y > 2]) 07414 [Not(x >= 0), Not(y >= 0)] 07415 """ 07416 f = v[0] 07417 for i in range(1,len(v)): 07418 f = And(Interpolant(f),v[i]) 07419 return tree_interpolant(f,p,ctx) 07420
def z3py.set_option | ( | args, | |
kws | |||
) |
Alias for 'set_param' for backward compatibility.
Definition at line 242 of file z3py.py.
00242 00243 def set_option(*args, **kws): 00244 """Alias for 'set_param' for backward compatibility. 00245 """ 00246 return set_param(*args, **kws)
def z3py.set_param | ( | args, | |
kws | |||
) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 214 of file z3py.py.
Referenced by set_option().
00214 00215 def set_param(*args, **kws): 00216 """Set Z3 global (or module) parameters. 00217 00218 >>> set_param(precision=10) 00219 """ 00220 if __debug__: 00221 _z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.") 00222 new_kws = {} 00223 for k in kws: 00224 v = kws[k] 00225 if not set_pp_option(k, v): 00226 new_kws[k] = v 00227 for key in new_kws: 00228 value = new_kws[key] 00229 Z3_global_param_set(str(key).upper(), _to_param_value(value)) 00230 prev = None 00231 for a in args: 00232 if prev == None: 00233 prev = a 00234 else: 00235 Z3_global_param_set(str(prev), _to_param_value(a)) 00236 prev = None
def z3py.SignExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra sign-bits. >>> x = BitVec('x', 16) >>> n = SignExt(8, x) >>> n.size() 24 >>> n SignExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(SignExt(6, v0)) >>> v 254 >>> v.size() 8 >>> print("%.x" % v.as_long()) fe
Definition at line 3737 of file z3py.py.
03737 03738 def SignExt(n, a): 03739 """Return a bit-vector expression with `n` extra sign-bits. 03740 03741 >>> x = BitVec('x', 16) 03742 >>> n = SignExt(8, x) 03743 >>> n.size() 03744 24 03745 >>> n 03746 SignExt(8, x) 03747 >>> n.sort() 03748 BitVec(24) 03749 >>> v0 = BitVecVal(2, 2) 03750 >>> v0 03751 2 03752 >>> v0.size() 03753 2 03754 >>> v = simplify(SignExt(6, v0)) 03755 >>> v 03756 254 03757 >>> v.size() 03758 8 03759 >>> print("%.x" % v.as_long()) 03760 fe 03761 """ 03762 if __debug__: 03763 _z3_assert(isinstance(n, int), "First argument must be an integer") 03764 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 03765 return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
def z3py.SimpleSolver | ( | ctx = None | ) |
Return a simple general purpose solver with limited amount of preprocessing. >>> s = SimpleSolver() >>> x = Int('x') >>> s.add(x > 0) >>> s.check() sat
Definition at line 6073 of file z3py.py.
Referenced by Solver.reason_unknown(), and Solver.statistics().
06073 06074 def SimpleSolver(ctx=None): 06075 """Return a simple general purpose solver with limited amount of preprocessing. 06076 06077 >>> s = SimpleSolver() 06078 >>> x = Int('x') 06079 >>> s.add(x > 0) 06080 >>> s.check() 06081 sat 06082 """ 06083 ctx = _get_ctx(ctx) 06084 return Solver(Z3_mk_simple_solver(ctx.ref()), ctx)
def z3py.simplify | ( | a, | |
arguments, | |||
keywords | |||
) |
Utils.
Simplify the expression `a` using the given options. This function has many options. Use `help_simplify` to obtain the complete list. >>> x = Int('x') >>> y = Int('y') >>> simplify(x + 1 + y + x + 1) 2 + 2*x + y >>> simplify((x + 1)*(y + 1), som=True) 1 + x + y + x*y >>> simplify(Distinct(x, y, 1), blast_distinct=True) And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1)))
Definition at line 6956 of file z3py.py.
Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), CreateDatatypes(), Implies(), is_algebraic_value(), K(), LShR(), Not(), Q(), RatVal(), DatatypeSortRef.recognizer(), RepeatBitVec(), RotateLeft(), RotateRight(), SignExt(), Xor(), and ZeroExt().
06956 06957 def simplify(a, *arguments, **keywords): 06958 """Simplify the expression `a` using the given options. 06959 06960 This function has many options. Use `help_simplify` to obtain the complete list. 06961 06962 >>> x = Int('x') 06963 >>> y = Int('y') 06964 >>> simplify(x + 1 + y + x + 1) 06965 2 + 2*x + y 06966 >>> simplify((x + 1)*(y + 1), som=True) 06967 1 + x + y + x*y 06968 >>> simplify(Distinct(x, y, 1), blast_distinct=True) 06969 And(Not(x == y), Not(x == 1), Not(y == 1)) 06970 >>> simplify(And(x == 0, y == 1), elim_and=True) 06971 Not(Or(Not(x == 0), Not(y == 1))) 06972 """ 06973 if __debug__: 06974 _z3_assert(is_expr(a), "Z3 expression expected") 06975 if len(arguments) > 0 or len(keywords) > 0: 06976 p = args2params(arguments, keywords, a.ctx) 06977 return _to_expr_ref(Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx) 06978 else: 06979 return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
def z3py.simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 6984 of file z3py.py.
06984 06985 def simplify_param_descrs(): 06986 """Return the set of parameter descriptions for Z3 `simplify` procedure.""" 06987 return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())
def z3py.solve | ( | args, | |
keywords | |||
) |
Solve the constraints `*args`. This is a simple function for creating demonstrations. It creates a solver, configure it using the options in `keywords`, adds the constraints in `args`, and invokes check. >>> a = Int('a') >>> solve(a > 0, a < 2) [a = 1]
Definition at line 7084 of file z3py.py.
Referenced by BV2Int(), and IsInt().
07084 07085 def solve(*args, **keywords): 07086 """Solve the constraints `*args`. 07087 07088 This is a simple function for creating demonstrations. It creates a solver, 07089 configure it using the options in `keywords`, adds the constraints 07090 in `args`, and invokes check. 07091 07092 >>> a = Int('a') 07093 >>> solve(a > 0, a < 2) 07094 [a = 1] 07095 """ 07096 s = Solver() 07097 s.set(**keywords) 07098 s.add(*args) 07099 if keywords.get('show', False): 07100 print(s) 07101 r = s.check() 07102 if r == unsat: 07103 print("no solution") 07104 elif r == unknown: 07105 print("failed to solve") 07106 try: 07107 print(s.model()) 07108 except Z3Exception: 07109 return 07110 else: 07111 print(s.model())
def z3py.solve_using | ( | s, | |
args, | |||
keywords | |||
) |
Solve the constraints `*args` using solver `s`. This is a simple function for creating demonstrations. It is similar to `solve`, but it uses the given solver `s`. It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check.
Definition at line 7112 of file z3py.py.
07112 07113 def solve_using(s, *args, **keywords): 07114 """Solve the constraints `*args` using solver `s`. 07115 07116 This is a simple function for creating demonstrations. It is similar to `solve`, 07117 but it uses the given solver `s`. 07118 It configures solver `s` using the options in `keywords`, adds the constraints 07119 in `args`, and invokes check. 07120 """ 07121 if __debug__: 07122 _z3_assert(isinstance(s, Solver), "Solver object expected") 07123 s.set(**keywords) 07124 s.add(*args) 07125 if keywords.get('show', False): 07126 print("Problem:") 07127 print(s) 07128 r = s.check() 07129 if r == unsat: 07130 print("no solution") 07131 elif r == unknown: 07132 print("failed to solve") 07133 try: 07134 print(s.model()) 07135 except Z3Exception: 07136 return 07137 else: 07138 if keywords.get('show', False): 07139 print("Solution:") 07140 print(s.model())
def z3py.SolverFor | ( | logic, | |
ctx = None |
|||
) |
Create a solver customized for the given logic. The parameter `logic` is a string. It should be contains the name of a SMT-LIB logic. See http://www.smtlib.org/ for the name of all available logics. >>> s = SolverFor("QF_LIA") >>> x = Int('x') >>> s.add(x > 0) >>> s.add(x < 2) >>> s.check() sat >>> s.model() [x = 1]
Definition at line 6053 of file z3py.py.
06053 06054 def SolverFor(logic, ctx=None): 06055 """Create a solver customized for the given logic. 06056 06057 The parameter `logic` is a string. It should be contains 06058 the name of a SMT-LIB logic. 06059 See http://www.smtlib.org/ for the name of all available logics. 06060 06061 >>> s = SolverFor("QF_LIA") 06062 >>> x = Int('x') 06063 >>> s.add(x > 0) 06064 >>> s.add(x < 2) 06065 >>> s.check() 06066 sat 06067 >>> s.model() 06068 [x = 1] 06069 """ 06070 ctx = _get_ctx(ctx) 06071 logic = to_symbol(logic) 06072 return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx)
def z3py.Sqrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the square root of a. >>> x = Real('x') >>> Sqrt(x) x**(1/2)
Definition at line 2867 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().
def z3py.SRem | ( | a, | |
b | |||
) |
Create the Z3 expression signed remainder. Use the operator % for signed modulus, and URem() for unsigned remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> SRem(x, y) SRem(x, y) >>> SRem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)'
Definition at line 3656 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and URem().
03656 03657 def SRem(a, b): 03658 """Create the Z3 expression signed remainder. 03659 03660 Use the operator % for signed modulus, and URem() for unsigned remainder. 03661 03662 >>> x = BitVec('x', 32) 03663 >>> y = BitVec('y', 32) 03664 >>> SRem(x, y) 03665 SRem(x, y) 03666 >>> SRem(x, y).sort() 03667 BitVec(32) 03668 >>> (x % y).sexpr() 03669 '(bvsmod x y)' 03670 >>> SRem(x, y).sexpr() 03671 '(bvsrem x y)' 03672 """ 03673 _check_bv_args(a, b) 03674 a, b = _coerce_exprs(a, b) 03675 return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.Store | ( | a, | |
i, | |||
v | |||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Store(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 4010 of file z3py.py.
Referenced by is_array(), and is_store().
04010 04011 def Store(a, i, v): 04012 """Return a Z3 store array expression. 04013 04014 >>> a = Array('a', IntSort(), IntSort()) 04015 >>> i, v = Ints('i v') 04016 >>> s = Store(a, i, v) 04017 >>> s.sort() 04018 Array(Int, Int) 04019 >>> prove(s[i] == v) 04020 proved 04021 >>> j = Int('j') 04022 >>> prove(Implies(i != j, s[j] == a[j])) 04023 proved 04024 """ 04025 return Update(a, i, v)
def z3py.substitute | ( | t, | |
m | |||
) |
Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to. >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 1 + 1
Definition at line 6988 of file z3py.py.
06988 06989 def substitute(t, *m): 06990 """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to. 06991 06992 >>> x = Int('x') 06993 >>> y = Int('y') 06994 >>> substitute(x + 1, (x, y + 1)) 06995 y + 1 + 1 06996 >>> f = Function('f', IntSort(), IntSort()) 06997 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 06998 1 + 1 06999 """ 07000 if isinstance(m, tuple): 07001 m1 = _get_args(m) 07002 if isinstance(m1, list): 07003 m = m1 07004 if __debug__: 07005 _z3_assert(is_expr(t), "Z3 expression expected") 07006 _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.") 07007 num = len(m) 07008 _from = (Ast * num)() 07009 _to = (Ast * num)() 07010 for i in range(num): 07011 _from[i] = m[i][0].as_ast() 07012 _to[i] = m[i][1].as_ast() 07013 return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
def z3py.substitute_vars | ( | t, | |
m | |||
) |
Substitute the free variables in t with the expression in m. >>> v0 = Var(0, IntSort()) >>> v1 = Var(1, IntSort()) >>> x = Int('x') >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # replace v0 with x+1 and v1 with x >>> substitute_vars(f(v0, v1), x + 1, x) f(x + 1, x)
Definition at line 7014 of file z3py.py.
07014 07015 def substitute_vars(t, *m): 07016 """Substitute the free variables in t with the expression in m. 07017 07018 >>> v0 = Var(0, IntSort()) 07019 >>> v1 = Var(1, IntSort()) 07020 >>> x = Int('x') 07021 >>> f = Function('f', IntSort(), IntSort(), IntSort()) 07022 >>> # replace v0 with x+1 and v1 with x 07023 >>> substitute_vars(f(v0, v1), x + 1, x) 07024 f(x + 1, x) 07025 """ 07026 if __debug__: 07027 _z3_assert(is_expr(t), "Z3 expression expected") 07028 _z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.") 07029 num = len(m) 07030 _to = (Ast * num)() 07031 for i in range(num): 07032 _to[i] = m[i].as_ast() 07033 return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
def z3py.Sum | ( | args | ) |
Create the sum of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Sum(a, b, c) a + b + c >>> Sum([a, b, c]) a + b + c >>> A = IntVector('a', 5) >>> Sum(A) a__0 + a__1 + a__2 + a__3 + a__4
Definition at line 7034 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().
07034 07035 def Sum(*args): 07036 """Create the sum of the Z3 expressions. 07037 07038 >>> a, b, c = Ints('a b c') 07039 >>> Sum(a, b, c) 07040 a + b + c 07041 >>> Sum([a, b, c]) 07042 a + b + c 07043 >>> A = IntVector('a', 5) 07044 >>> Sum(A) 07045 a__0 + a__1 + a__2 + a__3 + a__4 07046 """ 07047 args = _get_args(args) 07048 if __debug__: 07049 _z3_assert(len(args) > 0, "Non empty list of arguments expected") 07050 ctx = _ctx_from_ast_arg_list(args) 07051 if __debug__: 07052 _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression") 07053 args = _coerce_expr_list(args, ctx) 07054 if is_bv(args[0]): 07055 return _reduce(lambda a, b: a + b, args, 0) 07056 else: 07057 _args, sz = _to_ast_array(args) 07058 return ArithRef(Z3_mk_add(ctx.ref(), sz, _args), ctx)
def z3py.tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 6674 of file z3py.py.
Referenced by describe_tactics().
06674 06675 def tactic_description(name, ctx=None): 06676 """Return a short description for the tactic named `name`. 06677 06678 >>> d = tactic_description('simplify') 06679 """ 06680 ctx = _get_ctx(ctx) 06681 return Z3_tactic_get_descr(ctx.ref(), name)
def z3py.tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3. >>> l = tactics() >>> l.count('simplify') == 1 True
Definition at line 6664 of file z3py.py.
Referenced by describe_tactics().
06664 06665 def tactics(ctx=None): 06666 """Return a list of all available tactics in Z3. 06667 06668 >>> l = tactics() 06669 >>> l.count('simplify') == 1 06670 True 06671 """ 06672 ctx = _get_ctx(ctx) 06673 return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
def z3py.Then | ( | ts, | |
ks | |||
) |
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). >>> x, y = Ints('x y') >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 6556 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().
06556 06557 def Then(*ts, **ks): 06558 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). 06559 06560 >>> x, y = Ints('x y') 06561 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) 06562 >>> t(And(x == 0, y > x + 1)) 06563 [[Not(y <= 1)]] 06564 >>> t(And(x == 0, y > x + 1)).as_expr() 06565 Not(y <= 1) 06566 """ 06567 return AndThen(*ts, **ks)
def z3py.to_symbol | ( | s, | |
ctx = None |
|||
) |
Convert an integer or string into a Z3 symbol.
Definition at line 94 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), Function(), Int(), prove(), Real(), Fixedpoint.set_predicate_representation(), SolverFor(), and Fixedpoint.update_rule().
00094 00095 def to_symbol(s, ctx=None): 00096 """Convert an integer or string into a Z3 symbol.""" 00097 if isinstance(s, int): 00098 return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s) 00099 else: 00100 return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
def z3py.ToInt | ( | a | ) |
Return the Z3 expression ToInt(a). >>> x = Real('x') >>> x.sort() Real >>> n = ToInt(x) >>> n ToInt(x) >>> n.sort() Int
Definition at line 2834 of file z3py.py.
Referenced by is_to_int().
02834 02835 def ToInt(a): 02836 """ Return the Z3 expression ToInt(a). 02837 02838 >>> x = Real('x') 02839 >>> x.sort() 02840 Real 02841 >>> n = ToInt(x) 02842 >>> n 02843 ToInt(x) 02844 >>> n.sort() 02845 Int 02846 """ 02847 if __debug__: 02848 _z3_assert(a.is_real(), "Z3 real expression expected.") 02849 ctx = a.ctx 02850 return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
def z3py.ToReal | ( | a | ) |
Return the Z3 expression ToReal(a). >>> x = Int('x') >>> x.sort() Int >>> n = ToReal(x) >>> n ToReal(x) >>> n.sort() Real
Definition at line 2817 of file z3py.py.
Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().
02817 02818 def ToReal(a): 02819 """ Return the Z3 expression ToReal(a). 02820 02821 >>> x = Int('x') 02822 >>> x.sort() 02823 Int 02824 >>> n = ToReal(x) 02825 >>> n 02826 ToReal(x) 02827 >>> n.sort() 02828 Real 02829 """ 02830 if __debug__: 02831 _z3_assert(a.is_int(), "Z3 integer expression expected.") 02832 ctx = a.ctx 02833 return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
def z3py.tree_interpolant | ( | pat, | |
p = None , |
|||
ctx = None |
|||
) |
Compute interpolant for a tree of formulas. The input is an interpolation pattern over a set of formulas C. The pattern pat is a formula combining the formulas in C using logical conjunction and the "interp" operator (see Interp). This interp operator is logically the identity operator. It marks the sub-formulas of the pattern for which interpolants should be computed. The interpolant is a map sigma from marked subformulas to formulas, such that, for each marked subformula phi of pat (where phi sigma is phi with sigma(psi) substituted for each subformula psi of phi such that psi in dom(sigma)): 1) phi sigma implies sigma(phi), and 2) sigma(phi) is in the common uninterpreted vocabulary between the formulas of C occurring in phi and those not occurring in phi and moreover pat sigma implies false. In the simplest case an interpolant for the pattern "(and (interp A) B)" maps A to an interpolant for A /\ B. The return value is a vector of formulas representing sigma. This vector contains sigma(phi) for each marked subformula of pat, in pre-order traversal. This means that subformulas of phi occur before phi in the vector. Also, subformulas that occur multiply in pat will occur multiply in the result vector. If pat is satisfiable, raises an object of class ModelRef that represents a model of pat. If parameters p are supplied, these are used in creating the solver that determines satisfiability. >>> x = Int('x') >>> y = Int('y') >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)) [Not(x >= 0), Not(y <= 2)] >>> g = And(Interpolant(x<0),x<2) >>> try: ... print tree_interpolant(g).sexpr() ... except ModelRef as m: ... print m.sexpr() (define-fun x () Int (- 1))
Definition at line 7309 of file z3py.py.
Referenced by binary_interpolant(), and sequence_interpolant().
07309 07310 def tree_interpolant(pat,p=None,ctx=None): 07311 """Compute interpolant for a tree of formulas. 07312 07313 The input is an interpolation pattern over a set of formulas C. 07314 The pattern pat is a formula combining the formulas in C using 07315 logical conjunction and the "interp" operator (see Interp). This 07316 interp operator is logically the identity operator. It marks the 07317 sub-formulas of the pattern for which interpolants should be 07318 computed. The interpolant is a map sigma from marked subformulas 07319 to formulas, such that, for each marked subformula phi of pat 07320 (where phi sigma is phi with sigma(psi) substituted for each 07321 subformula psi of phi such that psi in dom(sigma)): 07322 07323 1) phi sigma implies sigma(phi), and 07324 07325 2) sigma(phi) is in the common uninterpreted vocabulary between 07326 the formulas of C occurring in phi and those not occurring in 07327 phi 07328 07329 and moreover pat sigma implies false. In the simplest case 07330 an interpolant for the pattern "(and (interp A) B)" maps A 07331 to an interpolant for A /\ B. 07332 07333 The return value is a vector of formulas representing sigma. This 07334 vector contains sigma(phi) for each marked subformula of pat, in 07335 pre-order traversal. This means that subformulas of phi occur before phi 07336 in the vector. Also, subformulas that occur multiply in pat will 07337 occur multiply in the result vector. 07338 07339 If pat is satisfiable, raises an object of class ModelRef 07340 that represents a model of pat. 07341 07342 If parameters p are supplied, these are used in creating the 07343 solver that determines satisfiability. 07344 07345 >>> x = Int('x') 07346 >>> y = Int('y') 07347 >>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)) 07348 [Not(x >= 0), Not(y <= 2)] 07349 07350 >>> g = And(Interpolant(x<0),x<2) 07351 >>> try: 07352 ... print tree_interpolant(g).sexpr() 07353 ... except ModelRef as m: 07354 ... print m.sexpr() 07355 (define-fun x () Int 07356 (- 1)) 07357 """ 07358 f = pat 07359 ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx)) 07360 ptr = (AstVectorObj * 1)() 07361 mptr = (Model * 1)() 07362 if p == None: 07363 p = ParamsRef(ctx) 07364 res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) 07365 if res == Z3_L_FALSE: 07366 return AstVector(ptr[0],ctx) 07367 raise ModelRef(mptr[0], ctx)
def z3py.TryFor | ( | t, | |
ms, | |||
ctx = None |
|||
) |
Return a tactic that applies `t` to a given goal for `ms` milliseconds. If `t` does not terminate in `ms` milliseconds, then it fails.
Definition at line 6656 of file z3py.py.
06656 06657 def TryFor(t, ms, ctx=None): 06658 """Return a tactic that applies `t` to a given goal for `ms` milliseconds. 06659 06660 If `t` does not terminate in `ms` milliseconds, then it fails. 06661 """ 06662 t = _to_tactic(t, ctx) 06663 return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
def z3py.UDiv | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) division `self / other`. Use the operator / for signed division. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> UDiv(x, y) UDiv(x, y) >>> UDiv(x, y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)'
Definition at line 3616 of file z3py.py.
Referenced by BitVecRef.__div__(), and BitVecRef.__rdiv__().
03616 03617 def UDiv(a, b): 03618 """Create the Z3 expression (unsigned) division `self / other`. 03619 03620 Use the operator / for signed division. 03621 03622 >>> x = BitVec('x', 32) 03623 >>> y = BitVec('y', 32) 03624 >>> UDiv(x, y) 03625 UDiv(x, y) 03626 >>> UDiv(x, y).sort() 03627 BitVec(32) 03628 >>> (x / y).sexpr() 03629 '(bvsdiv x y)' 03630 >>> UDiv(x, y).sexpr() 03631 '(bvudiv x y)' 03632 """ 03633 _check_bv_args(a, b) 03634 a, b = _coerce_exprs(a, b) 03635 return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.UGE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other >= self`. Use the operator >= for signed greater than or equal to. >>> x, y = BitVecs('x y', 32) >>> UGE(x, y) UGE(x, y) >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)'
Definition at line 3582 of file z3py.py.
Referenced by BitVecRef.__ge__().
03582 03583 def UGE(a, b): 03584 """Create the Z3 expression (unsigned) `other >= self`. 03585 03586 Use the operator >= for signed greater than or equal to. 03587 03588 >>> x, y = BitVecs('x y', 32) 03589 >>> UGE(x, y) 03590 UGE(x, y) 03591 >>> (x >= y).sexpr() 03592 '(bvsge x y)' 03593 >>> UGE(x, y).sexpr() 03594 '(bvuge x y)' 03595 """ 03596 _check_bv_args(a, b) 03597 a, b = _coerce_exprs(a, b) 03598 return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.UGT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other > self`. Use the operator > for signed greater than. >>> x, y = BitVecs('x y', 32) >>> UGT(x, y) UGT(x, y) >>> (x > y).sexpr() '(bvsgt x y)' >>> UGT(x, y).sexpr() '(bvugt x y)'
Definition at line 3599 of file z3py.py.
Referenced by BitVecRef.__gt__().
03599 03600 def UGT(a, b): 03601 """Create the Z3 expression (unsigned) `other > self`. 03602 03603 Use the operator > for signed greater than. 03604 03605 >>> x, y = BitVecs('x y', 32) 03606 >>> UGT(x, y) 03607 UGT(x, y) 03608 >>> (x > y).sexpr() 03609 '(bvsgt x y)' 03610 >>> UGT(x, y).sexpr() 03611 '(bvugt x y)' 03612 """ 03613 _check_bv_args(a, b) 03614 a, b = _coerce_exprs(a, b) 03615 return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.ULE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other <= self`. Use the operator <= for signed less than or equal to. >>> x, y = BitVecs('x y', 32) >>> ULE(x, y) ULE(x, y) >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)'
Definition at line 3548 of file z3py.py.
Referenced by BitVecRef.__le__().
03548 03549 def ULE(a, b): 03550 """Create the Z3 expression (unsigned) `other <= self`. 03551 03552 Use the operator <= for signed less than or equal to. 03553 03554 >>> x, y = BitVecs('x y', 32) 03555 >>> ULE(x, y) 03556 ULE(x, y) 03557 >>> (x <= y).sexpr() 03558 '(bvsle x y)' 03559 >>> ULE(x, y).sexpr() 03560 '(bvule x y)' 03561 """ 03562 _check_bv_args(a, b) 03563 a, b = _coerce_exprs(a, b) 03564 return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.ULT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other < self`. Use the operator < for signed less than. >>> x, y = BitVecs('x y', 32) >>> ULT(x, y) ULT(x, y) >>> (x < y).sexpr() '(bvslt x y)' >>> ULT(x, y).sexpr() '(bvult x y)'
Definition at line 3565 of file z3py.py.
Referenced by BitVecRef.__lt__().
03565 03566 def ULT(a, b): 03567 """Create the Z3 expression (unsigned) `other < self`. 03568 03569 Use the operator < for signed less than. 03570 03571 >>> x, y = BitVecs('x y', 32) 03572 >>> ULT(x, y) 03573 ULT(x, y) 03574 >>> (x < y).sexpr() 03575 '(bvslt x y)' 03576 >>> ULT(x, y).sexpr() 03577 '(bvult x y)' 03578 """ 03579 _check_bv_args(a, b) 03580 a, b = _coerce_exprs(a, b) 03581 return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.Update | ( | a, | |
i, | |||
v | |||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Update(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 3989 of file z3py.py.
Referenced by Store().
03989 03990 def Update(a, i, v): 03991 """Return a Z3 store array expression. 03992 03993 >>> a = Array('a', IntSort(), IntSort()) 03994 >>> i, v = Ints('i v') 03995 >>> s = Update(a, i, v) 03996 >>> s.sort() 03997 Array(Int, Int) 03998 >>> prove(s[i] == v) 03999 proved 04000 >>> j = Int('j') 04001 >>> prove(Implies(i != j, s[j] == a[j])) 04002 proved 04003 """ 04004 if __debug__: 04005 _z3_assert(is_array(a), "First argument must be a Z3 array expression") 04006 i = a.domain().cast(i) 04007 v = a.range().cast(v) 04008 ctx = a.ctx 04009 return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
def z3py.URem | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) remainder `self % other`. Use the operator % for signed modulus, and SRem() for signed remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> URem(x, y) URem(x, y) >>> URem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> URem(x, y).sexpr() '(bvurem x y)'
Definition at line 3636 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().
03636 03637 def URem(a, b): 03638 """Create the Z3 expression (unsigned) remainder `self % other`. 03639 03640 Use the operator % for signed modulus, and SRem() for signed remainder. 03641 03642 >>> x = BitVec('x', 32) 03643 >>> y = BitVec('y', 32) 03644 >>> URem(x, y) 03645 URem(x, y) 03646 >>> URem(x, y).sort() 03647 BitVec(32) 03648 >>> (x % y).sexpr() 03649 '(bvsmod x y)' 03650 >>> URem(x, y).sexpr() 03651 '(bvurem x y)' 03652 """ 03653 _check_bv_args(a, b) 03654 a, b = _coerce_exprs(a, b) 03655 return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
def z3py.Var | ( | idx, | |
s | |||
) |
Create a Z3 free variable. Free variables are used to create quantified formulas. >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False
Definition at line 1159 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().
01159 01160 def Var(idx, s): 01161 """Create a Z3 free variable. Free variables are used to create quantified formulas. 01162 01163 >>> Var(0, IntSort()) 01164 Var(0) 01165 >>> eq(Var(0, IntSort()), Var(0, BoolSort())) 01166 False 01167 """ 01168 if __debug__: 01169 _z3_assert(is_sort(s), "Z3 sort expected") 01170 return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
def z3py.When | ( | p, | |
t, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. >>> t = When(Probe('size') > 2, Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 6922 of file z3py.py.
06922 06923 def When(p, t, ctx=None): 06924 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. 06925 06926 >>> t = When(Probe('size') > 2, Tactic('simplify')) 06927 >>> x, y = Ints('x y') 06928 >>> g = Goal() 06929 >>> g.add(x > 0) 06930 >>> g.add(y > 0) 06931 >>> t(g) 06932 [[x > 0, y > 0]] 06933 >>> g.add(x == y + 1) 06934 >>> t(g) 06935 [[Not(x <= 0), Not(y <= 0), x == 1 + y]] 06936 """ 06937 p = _to_probe(p, ctx) 06938 t = _to_tactic(t, ctx) 06939 return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
def z3py.With | ( | t, | |
args, | |||
keys | |||
) |
Return a tactic that applies tactic `t` using the given configuration options. >>> x, y = Ints('x y') >>> t = With(Tactic('simplify'), som=True) >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]]
Definition at line 6624 of file z3py.py.
Referenced by Goal.prec().
06624 06625 def With(t, *args, **keys): 06626 """Return a tactic that applies tactic `t` using the given configuration options. 06627 06628 >>> x, y = Ints('x y') 06629 >>> t = With(Tactic('simplify'), som=True) 06630 >>> t((x + 1)*(y + 2) == 0) 06631 [[2*x + y + x*y == -2]] 06632 """ 06633 ctx = keys.get('ctx', None) 06634 t = _to_tactic(t, ctx) 06635 p = args2params(args, keys, t.ctx) 06636 return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
def z3py.Xor | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 Xor expression. >>> p, q = Bools('p q') >>> Xor(p, q) Xor(p, q) >>> simplify(Xor(p, q)) Not(p) == q
Definition at line 1428 of file z3py.py.
01428 01429 def Xor(a, b, ctx=None): 01430 """Create a Z3 Xor expression. 01431 01432 >>> p, q = Bools('p q') 01433 >>> Xor(p, q) 01434 Xor(p, q) 01435 >>> simplify(Xor(p, q)) 01436 Not(p) == q 01437 """ 01438 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) 01439 s = BoolSort(ctx) 01440 a = s.cast(a) 01441 b = s.cast(b) 01442 return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
def z3py.ZeroExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra zero-bits. >>> x = BitVec('x', 16) >>> n = ZeroExt(8, x) >>> n.size() 24 >>> n ZeroExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(ZeroExt(6, v0)) >>> v 2 >>> v.size() 8
Definition at line 3766 of file z3py.py.
03766 03767 def ZeroExt(n, a): 03768 """Return a bit-vector expression with `n` extra zero-bits. 03769 03770 >>> x = BitVec('x', 16) 03771 >>> n = ZeroExt(8, x) 03772 >>> n.size() 03773 24 03774 >>> n 03775 ZeroExt(8, x) 03776 >>> n.sort() 03777 BitVec(24) 03778 >>> v0 = BitVecVal(2, 2) 03779 >>> v0 03780 2 03781 >>> v0.size() 03782 2 03783 >>> v = simplify(ZeroExt(6, v0)) 03784 >>> v 03785 2 03786 >>> v.size() 03787 8 03788 """ 03789 if __debug__: 03790 _z3_assert(isinstance(n, int), "First argument must be an integer") 03791 _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression") 03792 return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
tuple _error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) |
tuple _Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core) |
tuple sat = CheckSatResult(Z3_L_TRUE) |
tuple unknown = CheckSatResult(Z3_L_UNDEF) |
tuple unsat = CheckSatResult(Z3_L_FALSE) |