Functions | |
def | z3_debug () |
def | enable_trace (msg) |
def | disable_trace (msg) |
def | get_version_string () |
def | get_version () |
def | get_full_version () |
def | open_log (fname) |
def | append_log (s) |
def | to_symbol (s, ctx=None) |
def | z3_error_handler (c, e) |
def | main_ctx () |
def | get_ctx (ctx) |
def | set_param (*args, **kws) |
def | reset_params () |
def | set_option (*args, **kws) |
def | get_param (name) |
def | is_ast (a) |
def | eq (a, b) |
def | is_sort (s) |
def | DeclareSort (name, ctx=None) |
def | is_func_decl (a) |
def | Function (name, *sig) |
def | FreshFunction (*sig) |
def | RecFunction (name, *sig) |
def | RecAddDefinition (f, args, body) |
def | is_expr (a) |
def | is_app (a) |
def | is_const (a) |
def | is_var (a) |
def | get_var_index (a) |
def | is_app_of (a, k) |
def | If (a, b, c, ctx=None) |
def | Distinct (*args) |
def | Const (name, sort) |
def | Consts (names, sort) |
def | FreshConst (sort, prefix="c") |
def | Var (idx, s) |
def | RealVar (idx, ctx=None) |
def | RealVarVector (n, ctx=None) |
def | is_bool (a) |
def | is_true (a) |
def | is_false (a) |
def | is_and (a) |
def | is_or (a) |
def | is_implies (a) |
def | is_not (a) |
def | is_eq (a) |
def | is_distinct (a) |
def | BoolSort (ctx=None) |
def | BoolVal (val, ctx=None) |
def | Bool (name, ctx=None) |
def | Bools (names, ctx=None) |
def | BoolVector (prefix, sz, ctx=None) |
def | FreshBool (prefix="b", ctx=None) |
def | Implies (a, b, ctx=None) |
def | Xor (a, b, ctx=None) |
def | Not (a, ctx=None) |
def | mk_not (a) |
def | And (*args) |
def | Or (*args) |
def | is_pattern (a) |
def | MultiPattern (*args) |
def | is_quantifier (a) |
def | ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
def | Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
def | Lambda (vs, body) |
def | is_arith_sort (s) |
def | is_arith (a) |
def | is_int (a) |
def | is_real (a) |
def | is_int_value (a) |
def | is_rational_value (a) |
def | is_algebraic_value (a) |
def | is_add (a) |
def | is_mul (a) |
def | is_sub (a) |
def | is_div (a) |
def | is_idiv (a) |
def | is_mod (a) |
def | is_le (a) |
def | is_lt (a) |
def | is_ge (a) |
def | is_gt (a) |
def | is_is_int (a) |
def | is_to_real (a) |
def | is_to_int (a) |
def | IntSort (ctx=None) |
def | RealSort (ctx=None) |
def | IntVal (val, ctx=None) |
def | RealVal (val, ctx=None) |
def | RatVal (a, b, ctx=None) |
def | Q (a, b, ctx=None) |
def | Int (name, ctx=None) |
def | Ints (names, ctx=None) |
def | IntVector (prefix, sz, ctx=None) |
def | FreshInt (prefix="x", ctx=None) |
def | Real (name, ctx=None) |
def | Reals (names, ctx=None) |
def | RealVector (prefix, sz, ctx=None) |
def | FreshReal (prefix="b", ctx=None) |
def | ToReal (a) |
def | ToInt (a) |
def | IsInt (a) |
def | Sqrt (a, ctx=None) |
def | Cbrt (a, ctx=None) |
def | is_bv_sort (s) |
def | is_bv (a) |
def | is_bv_value (a) |
def | BV2Int (a, is_signed=False) |
def | Int2BV (a, num_bits) |
def | BitVecSort (sz, ctx=None) |
def | BitVecVal (val, bv, ctx=None) |
def | BitVec (name, bv, ctx=None) |
def | BitVecs (names, bv, ctx=None) |
def | Concat (*args) |
def | Extract (high, low, a) |
def | ULE (a, b) |
def | ULT (a, b) |
def | UGE (a, b) |
def | UGT (a, b) |
def | UDiv (a, b) |
def | URem (a, b) |
def | SRem (a, b) |
def | LShR (a, b) |
def | RotateLeft (a, b) |
def | RotateRight (a, b) |
def | SignExt (n, a) |
def | ZeroExt (n, a) |
def | RepeatBitVec (n, a) |
def | BVRedAnd (a) |
def | BVRedOr (a) |
def | BVAddNoOverflow (a, b, signed) |
def | BVAddNoUnderflow (a, b) |
def | BVSubNoOverflow (a, b) |
def | BVSubNoUnderflow (a, b, signed) |
def | BVSDivNoOverflow (a, b) |
def | BVSNegNoOverflow (a) |
def | BVMulNoOverflow (a, b, signed) |
def | BVMulNoUnderflow (a, b) |
def | is_array_sort (a) |
def | is_array (a) |
def | is_const_array (a) |
def | is_K (a) |
def | is_map (a) |
def | is_default (a) |
def | get_map_func (a) |
def | ArraySort (*sig) |
def | Array (name, dom, rng) |
def | Update (a, i, v) |
def | Default (a) |
def | Store (a, i, v) |
def | Select (a, i) |
def | Map (f, *args) |
def | K (dom, v) |
def | Ext (a, b) |
def | SetHasSize (a, k) |
def | is_select (a) |
def | is_store (a) |
def | SetSort (s) |
Sets. More... | |
def | EmptySet (s) |
def | FullSet (s) |
def | SetUnion (*args) |
def | SetIntersect (*args) |
def | SetAdd (s, e) |
def | SetDel (s, e) |
def | SetComplement (s) |
def | SetDifference (a, b) |
def | IsMember (e, s) |
def | IsSubset (a, b) |
def | CreateDatatypes (*ds) |
def | TupleSort (name, sorts, ctx=None) |
def | DisjointSum (name, sorts, ctx=None) |
def | EnumSort (name, values, ctx=None) |
def | args2params (arguments, keywords, ctx=None) |
def | Model (ctx=None) |
def | is_as_array (n) |
def | get_as_array_func (n) |
def | SolverFor (logic, ctx=None, logFile=None) |
def | SimpleSolver (ctx=None, logFile=None) |
def | FiniteDomainSort (name, sz, ctx=None) |
def | is_finite_domain_sort (s) |
def | is_finite_domain (a) |
def | FiniteDomainVal (val, sort, ctx=None) |
def | is_finite_domain_value (a) |
def | AndThen (*ts, **ks) |
def | Then (*ts, **ks) |
def | OrElse (*ts, **ks) |
def | ParOr (*ts, **ks) |
def | ParThen (t1, t2, ctx=None) |
def | ParAndThen (t1, t2, ctx=None) |
def | With (t, *args, **keys) |
def | WithParams (t, p) |
def | Repeat (t, max=4294967295, ctx=None) |
def | TryFor (t, ms, ctx=None) |
def | tactics (ctx=None) |
def | tactic_description (name, ctx=None) |
def | describe_tactics () |
def | is_probe (p) |
def | probes (ctx=None) |
def | probe_description (name, ctx=None) |
def | describe_probes () |
def | FailIf (p, ctx=None) |
def | When (p, t, ctx=None) |
def | Cond (p, t1, t2, ctx=None) |
def | simplify (a, *arguments, **keywords) |
Utils. More... | |
def | help_simplify () |
def | simplify_param_descrs () |
def | substitute (t, *m) |
def | substitute_vars (t, *m) |
def | Sum (*args) |
def | Product (*args) |
def | AtMost (*args) |
def | AtLeast (*args) |
def | PbLe (args, k) |
def | PbGe (args, k) |
def | PbEq (args, k, ctx=None) |
def | solve (*args, **keywords) |
def | solve_using (s, *args, **keywords) |
def | prove (claim, show=False, **keywords) |
def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
def | get_default_rounding_mode (ctx=None) |
def | set_default_rounding_mode (rm, ctx=None) |
def | get_default_fp_sort (ctx=None) |
def | set_default_fp_sort (ebits, sbits, ctx=None) |
def | Float16 (ctx=None) |
def | FloatHalf (ctx=None) |
def | Float32 (ctx=None) |
def | FloatSingle (ctx=None) |
def | Float64 (ctx=None) |
def | FloatDouble (ctx=None) |
def | Float128 (ctx=None) |
def | FloatQuadruple (ctx=None) |
def | is_fp_sort (s) |
def | is_fprm_sort (s) |
def | RoundNearestTiesToEven (ctx=None) |
def | RNE (ctx=None) |
def | RoundNearestTiesToAway (ctx=None) |
def | RNA (ctx=None) |
def | RoundTowardPositive (ctx=None) |
def | RTP (ctx=None) |
def | RoundTowardNegative (ctx=None) |
def | RTN (ctx=None) |
def | RoundTowardZero (ctx=None) |
def | RTZ (ctx=None) |
def | is_fprm (a) |
def | is_fprm_value (a) |
def | is_fp (a) |
def | is_fp_value (a) |
def | FPSort (ebits, sbits, ctx=None) |
def | fpNaN (s) |
def | fpPlusInfinity (s) |
def | fpMinusInfinity (s) |
def | fpInfinity (s, negative) |
def | fpPlusZero (s) |
def | fpMinusZero (s) |
def | fpZero (s, negative) |
def | FPVal (sig, exp=None, fps=None, ctx=None) |
def | FP (name, fpsort, ctx=None) |
def | FPs (names, fpsort, ctx=None) |
def | fpAbs (a, ctx=None) |
def | fpNeg (a, ctx=None) |
def | fpAdd (rm, a, b, ctx=None) |
def | fpSub (rm, a, b, ctx=None) |
def | fpMul (rm, a, b, ctx=None) |
def | fpDiv (rm, a, b, ctx=None) |
def | fpRem (a, b, ctx=None) |
def | fpMin (a, b, ctx=None) |
def | fpMax (a, b, ctx=None) |
def | fpFMA (rm, a, b, c, ctx=None) |
def | fpSqrt (rm, a, ctx=None) |
def | fpRoundToIntegral (rm, a, ctx=None) |
def | fpIsNaN (a, ctx=None) |
def | fpIsInf (a, ctx=None) |
def | fpIsZero (a, ctx=None) |
def | fpIsNormal (a, ctx=None) |
def | fpIsSubnormal (a, ctx=None) |
def | fpIsNegative (a, ctx=None) |
def | fpIsPositive (a, ctx=None) |
def | fpLT (a, b, ctx=None) |
def | fpLEQ (a, b, ctx=None) |
def | fpGT (a, b, ctx=None) |
def | fpGEQ (a, b, ctx=None) |
def | fpEQ (a, b, ctx=None) |
def | fpNEQ (a, b, ctx=None) |
def | fpFP (sgn, exp, sig, ctx=None) |
def | fpToFP (a1, a2=None, a3=None, ctx=None) |
def | fpBVToFP (v, sort, ctx=None) |
def | fpFPToFP (rm, v, sort, ctx=None) |
def | fpRealToFP (rm, v, sort, ctx=None) |
def | fpSignedToFP (rm, v, sort, ctx=None) |
def | fpUnsignedToFP (rm, v, sort, ctx=None) |
def | fpToFPUnsigned (rm, x, s, ctx=None) |
def | fpToSBV (rm, x, s, ctx=None) |
def | fpToUBV (rm, x, s, ctx=None) |
def | fpToReal (x, ctx=None) |
def | fpToIEEEBV (x, ctx=None) |
def | StringSort (ctx=None) |
def | SeqSort (s) |
def | is_seq (a) |
def | is_string (a) |
def | is_string_value (a) |
def | StringVal (s, ctx=None) |
def | String (name, ctx=None) |
def | Strings (names, ctx=None) |
def | SubString (s, offset, length) |
def | SubSeq (s, offset, length) |
def | Empty (s) |
def | Full (s) |
def | Unit (a) |
def | PrefixOf (a, b) |
def | SuffixOf (a, b) |
def | Contains (a, b) |
def | Replace (s, src, dst) |
def | IndexOf (s, substr, offset=None) |
def | LastIndexOf (s, substr) |
def | Length (s) |
def | StrToInt (s) |
def | IntToStr (s) |
def | Re (s, ctx=None) |
def | ReSort (s) |
def | is_re (s) |
def | InRe (s, re) |
def | Union (*args) |
def | Intersect (*args) |
def | Plus (re) |
def | Option (re) |
def | Complement (re) |
def | Star (re) |
def | Loop (re, lo, hi=0) |
def | Range (lo, hi, ctx=None) |
def | PartialOrder (a, index) |
def | LinearOrder (a, index) |
def | TreeOrder (a, index) |
def | PiecewiseLinearOrder (a, index) |
def | TransitiveClosure (f) |
def | ensure_prop_closures () |
def | user_prop_push (ctx) |
def | user_prop_pop (ctx, num_scopes) |
def | user_prop_fresh (id, ctx) |
def | user_prop_fixed (ctx, cb, id, value) |
def | user_prop_final (ctx, cb) |
def | user_prop_eq (ctx, cb, x, y) |
def | user_prop_diseq (ctx, cb, x, y) |
Variables | |
Z3_DEBUG = __debug__ | |
sat = CheckSatResult(Z3_L_TRUE) | |
unsat = CheckSatResult(Z3_L_FALSE) | |
unknown = CheckSatResult(Z3_L_UNDEF) | |
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 1813 of file z3py.py.
Referenced by Tactic.__call__(), Fixedpoint.add_rule(), And(), AndThen(), Tactic.apply(), Goal.as_expr(), ApplyResult.as_expr(), Bool(), Bools(), BoolVector(), Distinct(), is_and(), is_bool(), is_implies(), is_or(), Lambda(), ParThen(), prove(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Repeat(), simplify(), Then(), and Fixedpoint.update_rule().
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 8171 of file z3py.py.
def z3py.append_log | ( | s | ) |
Append user-defined string to interaction log.
Definition at line 124 of file z3py.py.
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 5396 of file z3py.py.
Referenced by Tactic.apply(), args2params(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), and With().
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 4678 of file z3py.py.
Referenced by ArrayRef.__getitem__(), Array(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Lambda(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), and Update().
def z3py.ArraySort | ( | * | sig | ) |
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 4645 of file z3py.py.
Referenced by Array(), ArraySort(), ArraySortRef.domain(), SortRef.kind(), Context.MkArraySort(), SortRef.name(), ArraySortRef.range(), and SetSort().
def z3py.AtLeast | ( | * | args | ) |
Create an at-most Pseudo-Boolean k constraint. >>> a, b, c = Bools('a b c') >>> f = AtLeast(a, b, c, 2)
Definition at line 8800 of file z3py.py.
Referenced by AtLeast().
def z3py.AtMost | ( | * | args | ) |
Create an at-most Pseudo-Boolean k constraint. >>> a, b, c = Bools('a b c') >>> f = AtMost(a, b, c, 2)
Definition at line 8782 of file z3py.py.
Referenced by AtMost().
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 3999 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__(), BitVec(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().
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 4023 of file z3py.py.
Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), BitVecs(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().
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 3967 of file z3py.py.
Referenced by BitVec(), BitVecSort(), BitVecVal(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), and BitVecRef.sort().
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 3982 of file z3py.py.
Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), BitVecVal(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().
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 1692 of file z3py.py.
Referenced by SortRef.__eq__(), SortRef.__ne__(), Fixedpoint.add_rule(), Solver.assert_and_track(), Optimize.assert_and_track(), Bool(), Bools(), BoolVector(), is_bool(), is_false(), is_not(), is_true(), and Not().
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 1704 of file z3py.py.
Referenced by And(), AtLeast(), AtMost(), Bools(), Solver.consequences(), Implies(), is_and(), is_implies(), is_or(), Or(), PbEq(), PbGe(), PbLe(), prove(), Solver.unsat_core(), and Xor().
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 1655 of file z3py.py.
Referenced by FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), SortRef.__ne__(), FuncDeclRef.arity(), ArraySort(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), BoolSort(), BoolSortRef.cast(), Solver.check(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FreshBool(), Context.getBoolSort(), If(), Implies(), IntSort(), is_arith_sort(), is_ast(), SortRef.kind(), Context.mkBoolSort(), SortRef.name(), Not(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), SetSort(), QuantifierRef.sort(), ArrayRef.sort(), Var(), and Xor().
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 1673 of file z3py.py.
Referenced by Goal.as_expr(), ApplyResult.as_expr(), BoolVal(), BoolSortRef.cast(), UserPropagateBase.conflict(), AlgebraicNumRef.index(), is_false(), is_quantifier(), Re(), and Solver.to_smt2().
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 1720 of file z3py.py.
Referenced by And(), BoolVector(), and Or().
def z3py.BV2Int | ( | a, | |
is_signed = False |
|||
) |
Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) >>> BV2Int(b).sort() Int >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) >>> x > BV2Int(b, is_signed=False) x > BV2Int(b) >>> x > BV2Int(b, is_signed=True) x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [x = 2, b = 1]
Definition at line 3935 of file z3py.py.
Referenced by BV2Int().
def z3py.BVAddNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4421 of file z3py.py.
def z3py.BVAddNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4428 of file z3py.py.
def z3py.BVMulNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4463 of file z3py.py.
def z3py.BVMulNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4470 of file z3py.py.
def z3py.BVRedAnd | ( | a | ) |
def z3py.BVRedOr | ( | a | ) |
def z3py.BVSDivNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4449 of file z3py.py.
def z3py.BVSNegNoOverflow | ( | a | ) |
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4456 of file z3py.py.
def z3py.BVSubNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4435 of file z3py.py.
def z3py.BVSubNoUnderflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4442 of file z3py.py.
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)
Definition at line 3386 of file z3py.py.
Referenced by Cbrt().
def z3py.Complement | ( | re | ) |
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 4044 of file z3py.py.
Referenced by SeqRef.__add__(), SeqRef.__radd__(), Concat(), Contains(), and BitVecRef.size().
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 8628 of file z3py.py.
def z3py.Const | ( | name, | |
sort | |||
) |
Create a constant of the given sort. >>> Const('x', IntSort()) x
Definition at line 1405 of file z3py.py.
Referenced by BitVecSort(), BoolSort(), Const(), Consts(), DeclareSort(), FPSort(), IntSort(), is_finite_domain(), is_finite_domain_value(), IsMember(), IsSubset(), RealSort(), DatatypeSortRef.recognizer(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
def z3py.Consts | ( | names, | |
sort | |||
) |
Create 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 1417 of file z3py.py.
Referenced by Consts(), Ext(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def z3py.Contains | ( | a, | |
b | |||
) |
Check if 'a' contains 'b' >>> s1 = Contains("abc", "ab") >>> simplify(s1) True >>> s2 = Contains("abc", "bc") >>> simplify(s2) True >>> x, y, z = Strings('x y z') >>> s3 = Contains(Concat(x,y,z), y) >>> simplify(s3) True
Definition at line 10789 of file z3py.py.
Referenced by Contains().
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 5092 of file z3py.py.
Referenced by Datatype.create(), and CreateDatatypes().
def z3py.DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpreted 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 690 of file z3py.py.
Referenced by DeclareSort(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def z3py.Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 4714 of file z3py.py.
Referenced by Default(), and is_default().
def z3py.describe_probes | ( | ) |
Display a (tabular) description of all available probes in Z3.
Definition at line 8549 of file z3py.py.
def z3py.describe_tactics | ( | ) |
Display a (tabular) description of all available tactics in Z3.
Definition at line 8343 of file z3py.py.
def z3py.disable_trace | ( | msg | ) |
Definition at line 81 of file z3py.py.
def z3py.DisjointSum | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tagged union sort base on a set of underlying sorts Example: >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
Definition at line 5305 of file z3py.py.
Referenced by DisjointSum().
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 1372 of file z3py.py.
Referenced by Distinct(), is_distinct(), and simplify().
def z3py.Empty | ( | s | ) |
Create the empty sequence of the given sort >>> e = Empty(StringSort()) >>> e2 = StringVal("") >>> print(e.eq(e2)) True >>> e3 = Empty(SeqSort(IntSort())) >>> print(e3) Empty(Seq(Int)) >>> e4 = Empty(ReSort(SeqSort(IntSort()))) >>> print(e4) Empty(ReSort(Seq(Int)))
Definition at line 10720 of file z3py.py.
Referenced by Empty().
def z3py.EmptySet | ( | s | ) |
Create the empty set >>> EmptySet(IntSort()) K(Int, False)
Definition at line 4856 of file z3py.py.
Referenced by EmptySet().
def z3py.enable_trace | ( | msg | ) |
Definition at line 77 of file z3py.py.
def z3py.ensure_prop_closures | ( | ) |
Definition at line 11110 of file z3py.py.
Referenced by UserPropagateBase.__init__().
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 5317 of file z3py.py.
Referenced by EnumSort(), and Context.MkEnumSort().
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 471 of file z3py.py.
Referenced by BitVec(), BitVecSort(), eq(), FP(), FPSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), main_ctx(), Select(), substitute(), and Var().
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. >>> 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 2205 of file z3py.py.
Referenced by Fixedpoint.abstract(), Exists(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), and QuantifierRef.is_lambda().
def z3py.Ext | ( | a, | |
b | |||
) |
Return extensionality index for one-dimensional arrays. >> a, b = Consts('a b', SetSort(IntSort())) >> Ext(a, b) Ext(a, b)
Definition at line 4802 of file z3py.py.
Referenced by Ext().
def z3py.Extract | ( | high, | |
low, | |||
a | |||
) |
Create a Z3 bit-vector extraction expression. Extract is overloaded to also work on sequence extraction. The functions SubString and SubSeq are redirected to Extract. For this case, the arguments are reinterpreted as: high - is a sequence (string) low - is an offset a - is the length to be extracted >>> x = BitVec('x', 8) >>> Extract(6, 2, x) Extract(6, 2, x) >>> Extract(6, 2, x).sort() BitVec(5) >>> simplify(Extract(StringVal("abcd"),2,1)) "c"
Definition at line 4090 of file z3py.py.
Referenced by Extract(), SubSeq(), and SubString().
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 8586 of file z3py.py.
Referenced by FailIf().
def z3py.FiniteDomainSort | ( | name, | |
sz, | |||
ctx = None |
|||
) |
Create a named finite domain sort of a given size sz
Definition at line 7590 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), is_finite_domain(), is_finite_domain_sort(), is_finite_domain_value(), and Context.MkFiniteDomainSort().
def z3py.FiniteDomainVal | ( | val, | |
sort, | |||
ctx = None |
|||
) |
Return a Z3 finite-domain value. If `ctx=None`, then the global context is used. >>> s = FiniteDomainSort('S', 256) >>> FiniteDomainVal(255, s) 255 >>> FiniteDomainVal('100', s) 100
Definition at line 7660 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), and is_finite_domain_value().
def z3py.Float128 | ( | ctx = None | ) |
def z3py.Float16 | ( | ctx = None | ) |
def z3py.Float32 | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 9242 of file z3py.py.
Referenced by FPRef.__neg__(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), and fpUnsignedToFP().
def z3py.Float64 | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 9254 of file z3py.py.
Referenced by fpFPToFP(), and fpToFP().
def z3py.FloatDouble | ( | ctx = None | ) |
def z3py.FloatHalf | ( | ctx = None | ) |
def z3py.FloatQuadruple | ( | ctx = None | ) |
def z3py.FloatSingle | ( | ctx = None | ) |
def z3py.ForAll | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 forall formula. The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations. >>> 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 2187 of file z3py.py.
Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), ForAll(), get_var_index(), is_app(), is_const(), QuantifierRef.is_exists(), is_expr(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), is_var(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.FP | ( | name, | |
fpsort, | |||
ctx = None |
|||
) |
Return a floating-point constant named `name`. `fpsort` is the floating-point sort. If `ctx=None`, then the global context is used. >>> x = FP('x', FPSort(8, 24)) >>> is_fp(x) True >>> x.ebits() 8 >>> x.sort() FPSort(8, 24) >>> word = FPSort(8, 24) >>> x2 = FP('x', word) >>> eq(x, x2) True
Definition at line 9898 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FP(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPs(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().
def z3py.fpAbs | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point absolute value expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FPVal(1.0, s) >>> fpAbs(x) fpAbs(1) >>> y = FPVal(-20.0, s) >>> y -1.25*(2**4) >>> fpAbs(y) fpAbs(-1.25*(2**4)) >>> fpAbs(-1.25*(2**4)) fpAbs(-1.25*(2**4)) >>> fpAbs(x).sort() FPSort(8, 24)
Definition at line 9941 of file z3py.py.
Referenced by fpAbs().
def z3py.fpAdd | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpAdd(rm, x, y) fpAdd(RNE(), x, y) >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ x + y >>> fpAdd(rm, x, y).sort() FPSort(8, 24)
Definition at line 10032 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__radd__(), fpAdd(), and FPs().
def z3py.fpBVToFP | ( | v, | |
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a bit-vector term to a floating-point term. >>> x_bv = BitVecVal(0x3F800000, 32) >>> x_fp = fpBVToFP(x_bv, Float32()) >>> x_fp fpToFP(1065353216) >>> simplify(x_fp) 1
Definition at line 10354 of file z3py.py.
Referenced by fpBVToFP().
def z3py.fpDiv | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point division expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpDiv(rm, x, y) fpDiv(RNE(), x, y) >>> fpDiv(rm, x, y).sort() FPSort(8, 24)
Definition at line 10079 of file z3py.py.
Referenced by FPRef.__div__(), FPRef.__rdiv__(), and fpDiv().
def z3py.fpEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `fpEQ(other, self)`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpEQ(x, y) fpEQ(x, y) >>> fpEQ(x, y).sexpr() '(fp.eq x y)'
def z3py.fpFMA | ( | rm, | |
a, | |||
b, | |||
c, | |||
ctx = None |
|||
) |
def z3py.fpFP | ( | sgn, | |
exp, | |||
sig, | |||
ctx = None |
|||
) |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. >>> s = FPSort(8, 24) >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) >>> print(x) fpFP(1, 127, 4194304) >>> xv = FPVal(-1.5, s) >>> print(xv) -1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() sat >>> xv = FPVal(+1.5, s) >>> print(xv) 1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() unsat
Definition at line 10286 of file z3py.py.
Referenced by fpFP().
def z3py.fpFPToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision. >>> x_sgl = FPVal(1.0, Float32()) >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) >>> x_dbl fpToFP(RNE(), 1) >>> simplify(x_dbl) 1 >>> x_dbl.sort() FPSort(11, 53)
Definition at line 10371 of file z3py.py.
Referenced by fpFPToFP().
def z3py.fpGEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other >= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGEQ(x, y) x >= y >>> (x >= y).sexpr() '(fp.geq x y)'
Definition at line 10250 of file z3py.py.
Referenced by FPRef.__ge__(), and fpGEQ().
def z3py.fpGT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other > self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGT(x, y) x > y >>> (x > y).sexpr() '(fp.gt x y)'
Definition at line 10238 of file z3py.py.
Referenced by FPRef.__gt__(), and fpGT().
def z3py.fpInfinity | ( | s, | |
negative | |||
) |
Create a Z3 floating-point +oo or -oo term.
Definition at line 9826 of file z3py.py.
def z3py.fpIsInf | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isInfinite expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> fpIsInf(x) fpIsInf(x)
Definition at line 10168 of file z3py.py.
Referenced by fpIsInf().
def z3py.fpIsNaN | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isNaN expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpIsNaN(x) fpIsNaN(x)
Definition at line 10156 of file z3py.py.
Referenced by fpIsNaN().
def z3py.fpIsNegative | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsPositive | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsSubnormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsZero | ( | a, | |
ctx = None |
|||
) |
def z3py.fpLEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other <= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLEQ(x, y) x <= y >>> (x <= y).sexpr() '(fp.leq x y)'
Definition at line 10226 of file z3py.py.
Referenced by FPRef.__le__(), and fpLEQ().
def z3py.fpLT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other < self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) x < y >>> (x < y).sexpr() '(fp.lt x y)'
Definition at line 10214 of file z3py.py.
Referenced by FPRef.__lt__(), and fpLT().
def z3py.fpMax | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point maximum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMax(x, y) fpMax(x, y) >>> fpMax(x, y).sort() FPSort(8, 24)
Definition at line 10123 of file z3py.py.
Referenced by fpMax().
def z3py.fpMin | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point minimum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMin(x, y) fpMin(x, y) >>> fpMin(x, y).sort() FPSort(8, 24)
Definition at line 10108 of file z3py.py.
Referenced by fpMin().
def z3py.fpMinusInfinity | ( | s | ) |
def z3py.fpMinusZero | ( | s | ) |
Create a Z3 floating-point -0.0 term.
Definition at line 9839 of file z3py.py.
Referenced by FPVal().
def z3py.fpMul | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point multiplication expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMul(rm, x, y) fpMul(RNE(), x, y) >>> fpMul(rm, x, y).sort() FPSort(8, 24)
Definition at line 10064 of file z3py.py.
Referenced by FPRef.__mul__(), FPRef.__rmul__(), fpMul(), and FPs().
def z3py.fpNaN | ( | s | ) |
Create a Z3 floating-point NaN term. >>> s = FPSort(8, 24) >>> set_fpa_pretty(True) >>> fpNaN(s) NaN >>> pb = get_fpa_pretty() >>> set_fpa_pretty(False) >>> fpNaN(s) fpNaN(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 9786 of file z3py.py.
def z3py.fpNeg | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> fpNeg(x) -x >>> fpNeg(x).sort() FPSort(8, 24)
Definition at line 9964 of file z3py.py.
Referenced by FPRef.__neg__(), and fpNeg().
def z3py.fpNEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `Not(fpEQ(other, self))`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpNEQ(x, y) Not(fpEQ(x, y)) >>> (x != y).sexpr() '(distinct x y)'
Definition at line 10274 of file z3py.py.
Referenced by fpNEQ().
def z3py.fpPlusInfinity | ( | s | ) |
Create a Z3 floating-point +oo term. >>> s = FPSort(8, 24) >>> pb = get_fpa_pretty() >>> set_fpa_pretty(True) >>> fpPlusInfinity(s) +oo >>> set_fpa_pretty(False) >>> fpPlusInfinity(s) fpPlusInfinity(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 9803 of file z3py.py.
Referenced by fpPlusInfinity(), and FPVal().
def z3py.fpPlusZero | ( | s | ) |
def z3py.fpRealToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a real term to a floating-point term. >>> x_r = RealVal(1.5) >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) >>> x_fp fpToFP(RNE(), 3/2) >>> simplify(x_fp) 1.5
Definition at line 10391 of file z3py.py.
Referenced by fpRealToFP().
def z3py.fpRem | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point remainder expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpRem(x, y) fpRem(x, y) >>> fpRem(x, y).sort() FPSort(8, 24)
Definition at line 10094 of file z3py.py.
Referenced by FPRef.__mod__(), FPRef.__rmod__(), and fpRem().
def z3py.fpRoundToIntegral | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.FPs | ( | names, | |
fpsort, | |||
ctx = None |
|||
) |
Return an array of floating-point constants. >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) fpMul(RNE(), fpAdd(RNE(), x, y), z)
Definition at line 9922 of file z3py.py.
Referenced by fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), fpNEQ(), and FPs().
def z3py.fpSignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a signed bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFP(RNE(), 4294967291) >>> simplify(x_fp) -1.25*(2**2)
Definition at line 10409 of file z3py.py.
Referenced by fpSignedToFP().
def z3py.FPSort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. >>> Single = FPSort(8, 24) >>> Double = FPSort(11, 53) >>> Single FPSort(8, 24) >>> x = Const('x', Single) >>> eq(x, FP('x', FPSort(8, 24))) True
Definition at line 9727 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), FPSort(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), get_default_fp_sort(), is_fp(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.mkFPSort(), Context.MkFPSort(), Context.MkFPSort128(), Context.mkFPSort128(), Context.MkFPSort16(), Context.mkFPSort16(), Context.MkFPSort32(), Context.mkFPSort32(), Context.MkFPSort64(), Context.mkFPSort64(), Context.MkFPSortDouble(), Context.mkFPSortDouble(), Context.MkFPSortHalf(), Context.mkFPSortHalf(), Context.MkFPSortQuadruple(), Context.mkFPSortQuadruple(), Context.MkFPSortSingle(), Context.mkFPSortSingle(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), and FPRef.sort().
def z3py.fpSqrt | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.fpSub | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point subtraction expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpSub(rm, x, y) fpSub(RNE(), x, y) >>> fpSub(rm, x, y).sort() FPSort(8, 24)
Definition at line 10049 of file z3py.py.
Referenced by FPRef.__rsub__(), FPRef.__sub__(), and fpSub().
def z3py.fpToFP | ( | a1, | |
a2 = None , |
|||
a3 = None , |
|||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression from other term sorts to floating-point. From a bit-vector term in IEEE 754-2008 format: >>> x = FPVal(1.0, Float32()) >>> x_bv = fpToIEEEBV(x) >>> simplify(fpToFP(x_bv, Float32())) 1 From a floating-point term with different precision: >>> x = FPVal(1.0, Float32()) >>> x_db = fpToFP(RNE(), x, Float64()) >>> x_db.sort() FPSort(11, 53) From a real term: >>> x_r = RealVal(1.5) >>> simplify(fpToFP(RNE(), x_r, Float32())) 1.5 From a signed bit-vector term: >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> simplify(fpToFP(RNE(), x_signed, Float32())) -1.25*(2**2)
Definition at line 10315 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), and fpToFP().
def z3py.fpToFPUnsigned | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.
Definition at line 10445 of file z3py.py.
Referenced by fpUnsignedToFP().
def z3py.fpToIEEEBV | ( | x, | |
ctx = None |
|||
) |
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToIEEEBV(x) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10519 of file z3py.py.
Referenced by fpToFP(), and fpToIEEEBV().
def z3py.fpToReal | ( | x, | |
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to real. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToReal(x) >>> print(is_fp(x)) True >>> print(is_real(y)) True >>> print(is_fp(y)) False >>> print(is_real(x)) False
Definition at line 10499 of file z3py.py.
Referenced by fpToReal().
def z3py.fpToSBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10455 of file z3py.py.
Referenced by fpToSBV().
def z3py.fpToUBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10477 of file z3py.py.
Referenced by fpToUBV().
def z3py.fpUnsignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFPUnsigned(RNE(), 4294967291) >>> simplify(x_fp) 1*(2**32)
Definition at line 10427 of file z3py.py.
Referenced by fpUnsignedToFP().
def z3py.FPVal | ( | sig, | |
exp = None , |
|||
fps = None , |
|||
ctx = None |
|||
) |
Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used. >>> v = FPVal(20.0, FPSort(8, 24)) >>> v 1.25*(2**4) >>> print("0x%.8x" % v.exponent_as_long(False)) 0x00000004 >>> v = FPVal(2.25, FPSort(8, 24)) >>> v 1.125*(2**1) >>> v = FPVal(-2.25, FPSort(8, 24)) >>> v -1.125*(2**1) >>> FPVal(-0.0, FPSort(8, 24)) -0.0 >>> FPVal(0.0, FPSort(8, 24)) +0.0 >>> FPVal(+0.0, FPSort(8, 24)) +0.0
Definition at line 9852 of file z3py.py.
Referenced by FPNumRef.exponent(), fpAbs(), fpFP(), fpFPToFP(), fpToFP(), FPVal(), is_expr(), is_fp_value(), FPNumRef.isNegative(), set_default_fp_sort(), FPNumRef.sign_as_bv(), FPNumRef.significand(), and FPNumRef.significand_as_bv().
def z3py.fpZero | ( | s, | |
negative | |||
) |
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 1735 of file z3py.py.
Referenced by FreshBool().
def z3py.FreshConst | ( | sort, | |
prefix = "c" |
|||
) |
def z3py.FreshFunction | ( | * | sig | ) |
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 883 of file z3py.py.
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 3249 of file z3py.py.
Referenced by FreshInt().
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 3306 of file z3py.py.
Referenced by FreshReal().
def z3py.Full | ( | s | ) |
Create the regular expression that accepts the universal language >>> e = Full(ReSort(SeqSort(IntSort()))) >>> print(e) Full(ReSort(Seq(Int))) >>> e1 = Full(ReSort(StringSort())) >>> print(e1) Full(ReSort(String))
Definition at line 10740 of file z3py.py.
Referenced by Full().
def z3py.FullSet | ( | s | ) |
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 860 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ModelRef.__getitem__(), ModelRef.__len__(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), FuncDeclRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), is_ast(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_func_decl(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_var(), Lambda(), Map(), MultiPattern(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), substitute(), substitute_vars(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
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 6589 of file z3py.py.
Referenced by ModelRef.get_interp().
def z3py.get_default_fp_sort | ( | ctx = None | ) |
def z3py.get_default_rounding_mode | ( | ctx = None | ) |
Retrieves the global default rounding mode.
Definition at line 9116 of file z3py.py.
Referenced by set_default_fp_sort().
def z3py.get_full_version | ( | ) |
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 4621 of file z3py.py.
Referenced by get_map_func().
def z3py.get_param | ( | name | ) |
Return the value of a Z3 global (or module) parameter >>> get_param('nlsat.reorder') 'true'
Definition at line 306 of file z3py.py.
Referenced by get_param().
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 1303 of file z3py.py.
Referenced by get_var_index().
def z3py.get_version | ( | ) |
Definition at line 94 of file z3py.py.
def z3py.get_version_string | ( | ) |
Definition at line 85 of file z3py.py.
def z3py.help_simplify | ( | ) |
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 8670 of file z3py.py.
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 1349 of file z3py.py.
Referenced by BoolRef.__mul__(), ArithRef.__mul__(), BV2Int(), If(), Lambda(), and RecAddDefinition().
def z3py.Implies | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 implies expression. >>> p, q = Bools('p q') >>> Implies(p, q) Implies(p, q)
Definition at line 1749 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Solver.consequences(), Implies(), is_implies(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().
def z3py.IndexOf | ( | s, | |
substr, | |||
offset = None |
|||
) |
Retrieve the index of substring within a string starting at a specified offset. >>> simplify(IndexOf("abcabc", "bc", 0)) 1 >>> simplify(IndexOf("abcabc", "bc", 2)) 4
Definition at line 10823 of file z3py.py.
Referenced by IndexOf().
def z3py.InRe | ( | s, | |
re | |||
) |
Create regular expression membership test >>> re = Union(Re("a"),Re("b")) >>> print (simplify(InRe("a", re))) True >>> print (simplify(InRe("b", re))) True >>> print (simplify(InRe("c", re))) False
Definition at line 10924 of file z3py.py.
Referenced by InRe(), Loop(), Option(), Plus(), Range(), Star(), and Union().
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 3210 of file z3py.py.
Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), Probe.__call__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), Probe.__gt__(), Probe.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), Probe.__lt__(), ArithRef.__mod__(), ExprRef.__ne__(), Probe.__ne__(), 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(), ExprRef.arg(), Goal.as_expr(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), SortRef.cast(), Solver.check(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), Distinct(), eq(), AstRef.eq(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), get_var_index(), AstRef.hash(), If(), Goal.insert(), Solver.insert(), Int(), Ints(), IntVector(), is_app(), is_app_of(), is_arith(), is_arith_sort(), is_ast(), is_bv(), is_const(), QuantifierRef.is_exists(), is_expr(), is_finite_domain(), QuantifierRef.is_forall(), is_fp(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_int_value(), QuantifierRef.is_lambda(), is_pattern(), is_probe(), is_quantifier(), is_real(), ArithSortRef.is_real(), is_select(), is_sort(), is_to_real(), is_var(), K(), AstMap.keys(), Statistics.keys(), FuncDeclRef.kind(), Solver.model(), MultiPattern(), ExprRef.num_args(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), OrElse(), ParOr(), QuantifierRef.pattern(), Solver.pop(), Solver.push(), AstVector.push(), Solver.reason_unknown(), RecAddDefinition(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), AstRef.sexpr(), Solver.sexpr(), SimpleSolver(), simplify(), Goal.simplify(), solve(), SolverFor(), ExprRef.sort(), ArithRef.sort(), Solver.statistics(), Store(), substitute(), substitute_vars(), ToReal(), AstVector.translate(), AstRef.translate(), Goal.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.Int2BV | ( | a, | |
num_bits | |||
) |
Return the z3 expression Int2BV(a, num_bits). It is a bit-vector of width num_bits and represents the modulo of a by 2^num_bits
Definition at line 3958 of file z3py.py.
def z3py.Intersect | ( | * | args | ) |
Create intersection of regular expressions. >>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 10958 of file z3py.py.
Referenced by Intersect().
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 3223 of file z3py.py.
Referenced by Tactic.__call__(), ArithRef.__ge__(), Goal.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ApplyResult.__len__(), ArithRef.__lt__(), AndThen(), Tactic.apply(), Goal.convert_model(), Goal.depth(), FailIf(), Goal.get(), Goal.inconsistent(), Ints(), is_add(), is_distinct(), is_div(), is_eq(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Lambda(), parse_smt2_string(), ParThen(), Goal.prec(), Product(), Repeat(), Goal.size(), Store(), Sum(), Then(), Solver.unsat_core(), Update(), When(), With(), and WithParams().
def z3py.IntSort | ( | ctx = None | ) |
Return the integer 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 3100 of file z3py.py.
Referenced by FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), SortRef.__ne__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ArithSortRef.cast(), ExprRef.children(), QuantifierRef.children(), Const(), DatatypeSortRef.constructor(), Consts(), Datatype.create(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), FreshInt(), Full(), FullSet(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), Context.getIntSort(), Int(), IntSort(), IntVal(), is_app(), is_arith_sort(), is_array(), is_ast(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), is_expr(), is_finite_domain_sort(), QuantifierRef.is_forall(), is_func_decl(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_sort(), is_store(), SeqSortRef.is_string(), is_var(), IsMember(), IsSubset(), K(), SortRef.kind(), Lambda(), Map(), Context.mkIntSort(), MultiPattern(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), RecAddDefinition(), DatatypeSortRef.recognizer(), Select(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), SortRef.subsort(), substitute(), substitute_vars(), TupleSort(), Update(), FuncEntry.value(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.IntToStr | ( | s | ) |
Convert integer expression to string
Definition at line 10878 of file z3py.py.
Referenced by StrToInt().
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 3150 of file z3py.py.
Referenced by SeqRef.__getitem__(), AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_binary_string(), IntNumRef.as_long(), IntNumRef.as_string(), SeqRef.at(), AlgebraicNumRef.index(), IndexOf(), IntVal(), is_app(), is_arith(), is_ast(), is_const(), is_expr(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), SeqSort(), and substitute().
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
Definition at line 3236 of file z3py.py.
Referenced by IntVector(), Product(), and Sum().
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
Definition at line 2754 of file z3py.py.
Referenced by is_add().
def z3py.is_algebraic_value | ( | a | ) |
Return `True` if `a` is an algebraic 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 2740 of file z3py.py.
Referenced by is_algebraic_value().
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
Definition at line 1585 of file z3py.py.
Referenced by is_and().
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 1233 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
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 1336 of file z3py.py.
Referenced by is_add(), is_and(), is_app_of(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
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 2627 of file z3py.py.
Referenced by is_algebraic_value(), is_arith(), is_int(), is_int_value(), is_rational_value(), and is_real().
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 2326 of file z3py.py.
Referenced by is_arith_sort(), and ArithSortRef.subsort().
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 4556 of file z3py.py.
Referenced by Ext(), is_array(), and Map().
def z3py.is_array_sort | ( | a | ) |
def z3py.is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 6584 of file z3py.py.
Referenced by get_as_array_func(), and ModelRef.get_interp().
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 450 of file z3py.py.
Referenced by eq(), AstRef.eq(), is_ast(), and ReSort().
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 1535 of file z3py.py.
Referenced by BoolSort(), is_bool(), is_quantifier(), and prove().
def z3py.is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression. >>> b = BitVec('b', 32) >>> is_bv(b) True >>> is_bv(b + 10) True >>> is_bv(Int('x')) False
Definition at line 3906 of file z3py.py.
Referenced by BitVec(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
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 3438 of file z3py.py.
Referenced by BitVecVal(), fpToSBV(), fpToUBV(), is_bv_sort(), and BitVecSortRef.subsort().
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 3920 of file z3py.py.
Referenced by is_bv_value().
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 1259 of file z3py.py.
Referenced by ModelRef.__getitem__(), Solver.assert_and_track(), Optimize.assert_and_track(), ModelRef.get_interp(), get_var_index(), is_const(), is_quantifier(), is_var(), and prove().
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 4570 of file z3py.py.
Referenced by is_const_array().
def z3py.is_default | ( | a | ) |
Return `True` if `a` is a Z3 default array expression. >>> d = Default(K(IntSort(), 10)) >>> is_default(d) True
Definition at line 4612 of file z3py.py.
Referenced by is_default().
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 1643 of file z3py.py.
Referenced by is_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 2790 of file z3py.py.
Referenced by is_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
Definition at line 1633 of file z3py.py.
Referenced by AstRef.__bool__(), and is_eq().
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 >>> is_expr(FPVal(1.0)) True
Definition at line 1210 of file z3py.py.
Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), ExprRef.children(), Concat(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_expr(), is_quantifier(), is_sort(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), substitute(), and substitute_vars().
def z3py.is_false | ( | a | ) |
Return `True` if `a` is the Z3 false expression. >>> p = Bool('p') >>> is_false(p) False >>> is_false(False) False >>> is_false(BoolVal(False)) True
Definition at line 1571 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and is_false().
def z3py.is_finite_domain | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain expression. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain(b) True >>> is_finite_domain(Int('x')) False
Definition at line 7621 of file z3py.py.
Referenced by is_finite_domain(), and is_finite_domain_value().
def z3py.is_finite_domain_sort | ( | s | ) |
Return True if `s` is a Z3 finite-domain sort. >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) True >>> is_finite_domain_sort(IntSort()) False
Definition at line 7598 of file z3py.py.
Referenced by FiniteDomainVal(), and is_finite_domain_sort().
def z3py.is_finite_domain_value | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain value. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain_value(b) False >>> b = FiniteDomainVal(10, s) >>> b 10 >>> is_finite_domain_value(b) True
Definition at line 7675 of file z3py.py.
Referenced by is_finite_domain_value().
def z3py.is_fp | ( | a | ) |
Return `True` if `a` is a Z3 floating-point expression. >>> b = FP('b', FPSort(8, 24)) >>> is_fp(b) True >>> is_fp(b + 1.0) True >>> is_fp(Int('x')) False
Definition at line 9698 of file z3py.py.
Referenced by FP(), fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and set_default_fp_sort().
def z3py.is_fp_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point sort. >>> is_fp_sort(FPSort(8, 24)) True >>> is_fp_sort(IntSort()) False
Definition at line 9282 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().
def z3py.is_fp_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point numeral value. >>> b = FP('b', FPSort(8, 24)) >>> is_fp_value(b) False >>> b = FPVal(1.0, FPSort(8, 24)) >>> b 1 >>> is_fp_value(b) True
Definition at line 9712 of file z3py.py.
Referenced by is_fp_value().
def z3py.is_fprm | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode expression. >>> rm = RNE() >>> is_fprm(rm) True >>> rm = 1.0 >>> is_fprm(rm) False
Definition at line 9542 of file z3py.py.
Referenced by fpFPToFP(), fpNeg(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_fprm(), and is_fprm_value().
def z3py.is_fprm_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point rounding mode sort. >>> is_fprm_sort(FPSort(8, 24)) False >>> is_fprm_sort(RNE().sort()) True
Definition at line 9293 of file z3py.py.
Referenced by is_fprm_sort().
def z3py.is_fprm_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 9555 of file z3py.py.
Referenced by set_default_rounding_mode().
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 847 of file z3py.py.
Referenced by is_func_decl(), Map(), and prove().
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
Definition at line 2855 of file z3py.py.
Referenced by is_ge().
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
Definition at line 2867 of file z3py.py.
Referenced by is_gt().
def z3py.is_idiv | ( | a | ) |
Return `True` if `a` is an expression of the form b div c. >>> x, y = Ints('x y') >>> is_idiv(x / y) True >>> is_idiv(x + y) False
def z3py.is_implies | ( | a | ) |
Return `True` if `a` is a Z3 implication expression. >>> p, q = Bools('p q') >>> is_implies(Implies(p, q)) True >>> is_implies(And(p, q)) False
Definition at line 1609 of file z3py.py.
Referenced by is_implies().
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 2648 of file z3py.py.
Referenced by Int(), IntSort(), is_int(), and RealSort().
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 2694 of file z3py.py.
Referenced by is_int_value().
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
Definition at line 2879 of file z3py.py.
Referenced by is_is_int().
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
Definition at line 4583 of file z3py.py.
Referenced by is_K().
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
Definition at line 2831 of file z3py.py.
Referenced by is_le().
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
Definition at line 2843 of file z3py.py.
Referenced by is_lt().
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 4596 of file z3py.py.
Referenced by get_map_func(), and is_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
Definition at line 2819 of file z3py.py.
Referenced by is_mod().
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
Definition at line 2766 of file z3py.py.
Referenced by is_mul().
def z3py.is_not | ( | a | ) |
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
Definition at line 1597 of file z3py.py.
Referenced by is_or().
def z3py.is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. >>> 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 1897 of file z3py.py.
Referenced by is_pattern(), is_quantifier(), and MultiPattern().
def z3py.is_probe | ( | p | ) |
Return `True` if `p` is a Z3 probe. >>> is_probe(Int('x')) False >>> is_probe(Probe('memory')) True
Definition at line 8511 of file z3py.py.
Referenced by eq(), is_probe(), mk_not(), and Not().
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 2138 of file z3py.py.
Referenced by Exists(), and is_quantifier().
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 2718 of file z3py.py.
Referenced by RatNumRef.denominator(), is_rational_value(), and RatNumRef.numerator().
def z3py.is_re | ( | s | ) |
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 2667 of file z3py.py.
Referenced by fpRealToFP(), fpToFP(), fpToReal(), is_real(), Real(), and RealSort().
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
Definition at line 4820 of file z3py.py.
Referenced by is_select().
def z3py.is_seq | ( | a | ) |
Return `True` if `a` is a Z3 sequence expression. >>> print (is_seq(Unit(IntVal(0)))) True >>> print (is_seq(StringVal("abc"))) True
Definition at line 10658 of file z3py.py.
Referenced by SeqRef.__gt__(), Concat(), Extract(), and is_seq().
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 646 of file z3py.py.
Referenced by ArraySort(), CreateDatatypes(), FreshFunction(), Function(), is_sort(), IsSubset(), K(), prove(), RecFunction(), 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
Definition at line 4833 of file z3py.py.
Referenced by is_store().
def z3py.is_string | ( | a | ) |
Return `True` if `a` is a Z3 string expression. >>> print (is_string(StringVal("ab"))) True
Definition at line 10668 of file z3py.py.
Referenced by is_string().
def z3py.is_string_value | ( | a | ) |
return 'True' if 'a' is a Z3 string constant expression. >>> print (is_string_value(StringVal("a"))) True >>> print (is_string_value(StringVal("a") + StringVal("b"))) False
Definition at line 10676 of file z3py.py.
Referenced by is_string_value().
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
Definition at line 2778 of file z3py.py.
Referenced by is_sub().
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
Definition at line 2906 of file z3py.py.
Referenced by is_to_int().
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 2891 of file z3py.py.
Referenced by is_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 1553 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and is_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 1278 of file z3py.py.
Referenced by get_var_index(), and is_var().
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 3356 of file z3py.py.
Referenced by is_is_int(), and IsInt().
def z3py.IsMember | ( | e, | |
s | |||
) |
Check if e is a member of set s >>> a = Const('a', SetSort(IntSort())) >>> IsMember(1, a) a[1]
Definition at line 4943 of file z3py.py.
Referenced by IsMember().
def z3py.IsSubset | ( | a, | |
b | |||
) |
Check if a is a subset of b >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> IsSubset(a, b) subset(a, b)
Definition at line 4954 of file z3py.py.
Referenced by IsSubset().
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 4780 of file z3py.py.
Referenced by Default(), EmptySet(), FullSet(), is_const_array(), is_default(), is_K(), and K().
def z3py.Lambda | ( | vs, | |
body | |||
) |
Create a Z3 lambda expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> mem0 = Array('mem0', IntSort(), IntSort()) >>> lo, hi, e, i = Ints('lo hi e i') >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i])) >>> mem1 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
Definition at line 2226 of file z3py.py.
Referenced by QuantifierRef.is_lambda(), Lambda(), and Context.MkLambda().
def z3py.LastIndexOf | ( | s, | |
substr | |||
) |
Retrieve the last index of substring within a string
Definition at line 10843 of file z3py.py.
def z3py.Length | ( | s | ) |
Obtain the length of a sequence 's' >>> l = Length(StringVal("abc")) >>> simplify(l) 3
Definition at line 10852 of file z3py.py.
Referenced by Length().
def z3py.LinearOrder | ( | a, | |
index | |||
) |
def z3py.Loop | ( | re, | |
lo, | |||
hi = 0 |
|||
) |
Create the regular expression accepting between a lower and upper bound repetitions >>> re = Loop(Re("a"), 1, 3) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("aaaa", re))) False >>> print(simplify(InRe("", re))) False
Definition at line 11020 of file z3py.py.
Referenced by Loop().
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 4261 of file z3py.py.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), and LShR().
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 238 of file z3py.py.
Referenced by SeqRef.__gt__(), help_simplify(), main_ctx(), simplify_param_descrs(), and Goal.translate().
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 4757 of file z3py.py.
Referenced by Context.Context(), get_map_func(), is_map(), and Map().
def z3py.mk_not | ( | a | ) |
def z3py.Model | ( | ctx = None | ) |
Definition at line 6579 of file z3py.py.
Referenced by Goal.ConvertModel(), Goal.convertModel(), Optimize.getModel(), Solver.getModel(), and Optimize.set_on_model().
def z3py.MultiPattern | ( | * | args | ) |
Create a Z3 multi-pattern using the given expressions `*args` >>> 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 1915 of file z3py.py.
Referenced by MultiPattern().
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 1779 of file z3py.py.
Referenced by AndThen(), ApplyResult.as_expr(), Solver.consequences(), Goal.convert_model(), Distinct(), FailIf(), fpNEQ(), is_not(), mk_not(), Not(), prove(), simplify(), Then(), When(), and Xor().
def z3py.open_log | ( | fname | ) |
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 119 of file z3py.py.
def z3py.Option | ( | re | ) |
Create the regular expression that optionally accepts the argument. >>> re = Option(Re("a")) >>> print(simplify(InRe("a", re))) True >>> print(simplify(InRe("", re))) True >>> print(simplify(InRe("aa", re))) False
Definition at line 10989 of file z3py.py.
Referenced by Option().
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 1846 of file z3py.py.
Referenced by ApplyResult.__getitem__(), ApplyResult.__len__(), ApplyResult.as_expr(), Bools(), Goal.convert_model(), is_and(), is_or(), Or(), OrElse(), ParThen(), prove(), Repeat(), and simplify().
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 8204 of file z3py.py.
def z3py.ParAndThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
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 8225 of file z3py.py.
Referenced by ParOr().
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 9092 of file z3py.py.
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))') [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 9071 of file z3py.py.
Referenced by parse_smt2_file(), and parse_smt2_string().
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 8244 of file z3py.py.
Referenced by ParAndThen(), and ParThen().
def z3py.PartialOrder | ( | a, | |
index | |||
) |
def z3py.PbEq | ( | args, | |
k, | |||
ctx = None |
|||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 8867 of file z3py.py.
Referenced by PbEq().
def z3py.PbGe | ( | args, | |
k | |||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
Definition at line 8856 of file z3py.py.
Referenced by PbGe().
def z3py.PbLe | ( | args, | |
k | |||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
Definition at line 8845 of file z3py.py.
Referenced by PbLe().
def z3py.PiecewiseLinearOrder | ( | a, | |
index | |||
) |
def z3py.Plus | ( | re | ) |
Create the regular expression accepting one or more repetitions of argument. >>> re = Plus(Re("a")) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("ab", re))) False >>> print(simplify(InRe("", re))) False
Definition at line 10976 of file z3py.py.
Referenced by Plus().
def z3py.PrefixOf | ( | a, | |
b | |||
) |
Check if 'a' is a prefix of 'b' >>> s1 = PrefixOf("ab", "abc") >>> simplify(s1) True >>> s2 = PrefixOf("bc", "abc") >>> simplify(s2) False
Definition at line 10759 of file z3py.py.
Referenced by PrefixOf().
def z3py.probe_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the probe named `name`. >>> d = probe_description('memory')
Definition at line 8540 of file z3py.py.
Referenced by describe_probes(), and probe_description().
def z3py.probes | ( | ctx = None | ) |
Return a list of all available probes in Z3. >>> l = probes() >>> l.count('memory') == 1 True
Definition at line 8529 of file z3py.py.
Referenced by describe_probes(), and probes().
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 8756 of file z3py.py.
def z3py.prove | ( | claim, | |
show = False , |
|||
** | 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 8939 of file z3py.py.
Referenced by Default(), Map(), prove(), Store(), and Update().
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 3197 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), RatNumRef.numerator(), and Q().
def z3py.Range | ( | lo, | |
hi, | |||
ctx = None |
|||
) |
Create the range regular expression over two sequences of length 1 >>> range = Range("a","z") >>> print(simplify(InRe("b", range))) True >>> print(simplify(InRe("bb", range))) False
Definition at line 11033 of file z3py.py.
Referenced by Range().
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 3181 of file z3py.py.
def z3py.Re | ( | s, | |
ctx = None |
|||
) |
The regular expression that accepts sequence 's' >>> s1 = Re("ab") >>> s2 = Re(StringVal("ab")) >>> s3 = Re(Unit(BoolVal(True)))
Definition at line 10885 of file z3py.py.
Referenced by InRe(), Intersect(), Loop(), Option(), Plus(), Re(), Star(), and Union().
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 3263 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), is_bool(), is_func_decl(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_is_int(), is_rational_value(), is_real(), ArithSortRef.is_real(), ArithRef.is_real(), is_to_int(), is_true(), IsInt(), main_ctx(), Real(), Reals(), RealVector(), Tactic.solver(), ExprRef.sort(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
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
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 3117 of file z3py.py.
Referenced by FuncDeclRef.__call__(), FuncDeclRef.arity(), SortRef.cast(), ArithSortRef.cast(), FuncDeclRef.domain(), FreshReal(), Context.getRealSort(), is_arith_sort(), Context.mkRealSort(), FuncDeclRef.range(), Real(), RealSort(), RealVal(), RealVar(), SortRef.subsort(), and QuantifierRef.var_sort().
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 3162 of file z3py.py.
Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), fpRealToFP(), fpToFP(), AlgebraicNumRef.index(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), RatVal(), RealVal(), and Sqrt().
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 1451 of file z3py.py.
Referenced by RealVar(), and 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 1462 of file z3py.py.
Referenced by RealVarVector().
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 3291 of file z3py.py.
Referenced by RealVector().
def z3py.RecAddDefinition | ( | f, | |
args, | |||
body | |||
) |
Set the body of a recursive function. Recursive definitions can be simplified if they are applied to ground arguments. >>> ctx = Context() >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) >>> n = Int('n', ctx) >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) >>> simplify(fac(5)) 120 >>> s = Solver(ctx=ctx) >>> s.add(fac(n) < 3) >>> s.check() sat >>> s.model().eval(fac(5)) 120
Definition at line 924 of file z3py.py.
Referenced by RecAddDefinition().
def z3py.RecFunction | ( | name, | |
* | sig | ||
) |
Create a new Z3 recursive with the given sorts.
Definition at line 906 of file z3py.py.
Referenced by RecAddDefinition().
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 8293 of file z3py.py.
Referenced by Repeat().
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 4383 of file z3py.py.
Referenced by RepeatBitVec().
def z3py.Replace | ( | s, | |
src, | |||
dst | |||
) |
Replace the first occurrence of 'src' by 'dst' in 's' >>> r = Replace("aaa", "a", "b") >>> simplify(r) "baa"
Definition at line 10808 of file z3py.py.
Referenced by Replace().
def z3py.reset_params | ( | ) |
def z3py.ReSort | ( | s | ) |
Definition at line 10904 of file z3py.py.
Referenced by Empty(), Full(), and Context.MkReSort().
def z3py.RNA | ( | ctx = None | ) |
Definition at line 9507 of file z3py.py.
Referenced by get_default_rounding_mode().
def z3py.RNE | ( | ctx = None | ) |
Definition at line 9497 of file z3py.py.
Referenced by fpAbs(), fpAdd(), fpDiv(), fpFPToFP(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRealToFP(), FPs(), fpSignedToFP(), fpSub(), fpToFP(), fpUnsignedToFP(), get_default_rounding_mode(), is_fprm(), and is_fprm_sort().
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 4293 of file z3py.py.
Referenced by RotateLeft().
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 4309 of file z3py.py.
Referenced by RotateRight().
def z3py.RoundNearestTiesToAway | ( | ctx = None | ) |
def z3py.RoundNearestTiesToEven | ( | ctx = None | ) |
def z3py.RoundTowardNegative | ( | ctx = None | ) |
def z3py.RoundTowardPositive | ( | ctx = None | ) |
def z3py.RoundTowardZero | ( | ctx = None | ) |
def z3py.RTN | ( | ctx = None | ) |
Definition at line 9527 of file z3py.py.
Referenced by get_default_rounding_mode().
def z3py.RTP | ( | ctx = None | ) |
Definition at line 9517 of file z3py.py.
Referenced by get_default_rounding_mode().
def z3py.RTZ | ( | ctx = None | ) |
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 4742 of file z3py.py.
Referenced by Select().
def z3py.SeqSort | ( | s | ) |
Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True
Definition at line 10579 of file z3py.py.
Referenced by Empty(), Full(), SeqSortRef.is_string(), Context.MkSeqSort(), and SeqSort().
def z3py.set_default_fp_sort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
def z3py.set_default_rounding_mode | ( | rm, | |
ctx = None |
|||
) |
def z3py.set_option | ( | * | args, |
** | kws | ||
) |
def z3py.set_param | ( | * | args, |
** | kws | ||
) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 270 of file z3py.py.
Referenced by set_option(), and set_param().
def z3py.SetAdd | ( | s, | |
e | |||
) |
Add element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetAdd(a, 1) Store(a, 1, True)
Definition at line 4900 of file z3py.py.
Referenced by SetAdd().
def z3py.SetComplement | ( | s | ) |
The complement of set s >>> a = Const('a', SetSort(IntSort())) >>> SetComplement(a) complement(a)
Definition at line 4922 of file z3py.py.
Referenced by SetComplement().
def z3py.SetDel | ( | s, | |
e | |||
) |
Remove element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetDel(a, 1) Store(a, 1, False)
Definition at line 4911 of file z3py.py.
Referenced by SetDel().
def z3py.SetDifference | ( | a, | |
b | |||
) |
The set difference of a and b >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetDifference(a, b) setminus(a, b)
Definition at line 4932 of file z3py.py.
Referenced by SetDifference().
def z3py.SetHasSize | ( | a, | |
k | |||
) |
def z3py.SetIntersect | ( | * | args | ) |
Take the union of sets >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetIntersect(a, b) intersection(a, b)
Definition at line 4887 of file z3py.py.
Referenced by SetIntersect().
def z3py.SetSort | ( | s | ) |
Sets.
Create a set sort over element sort s
Definition at line 4851 of file z3py.py.
Referenced by Ext(), IsMember(), IsSubset(), Context.MkSetSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
def z3py.SetUnion | ( | * | args | ) |
Take the union of sets >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetUnion(a, b) union(a, b)
Definition at line 4874 of file z3py.py.
Referenced by SetUnion().
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 4325 of file z3py.py.
Referenced by SignExt().
def z3py.SimpleSolver | ( | ctx = None , |
|
logFile = 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 7293 of file z3py.py.
Referenced by Solver.reason_unknown(), SimpleSolver(), and Solver.statistics().
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 8645 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(), Contains(), CreateDatatypes(), Distinct(), eq(), AstRef.eq(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), AstRef.hash(), If(), IndexOf(), InRe(), is_algebraic_value(), is_true(), K(), Length(), Loop(), LShR(), Not(), Option(), Plus(), PrefixOf(), Q(), Range(), RatVal(), RecAddDefinition(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), Expr< R extends Sort >.simplify(), simplify(), Star(), StrToInt(), SuffixOf(), Union(), Xor(), and ZeroExt().
def z3py.simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 8675 of file z3py.py.
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 8878 of file z3py.py.
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 8908 of file z3py.py.
def z3py.SolverFor | ( | logic, | |
ctx = None , |
|||
logFile = 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 7272 of file z3py.py.
Referenced by SolverFor().
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 3373 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), is_algebraic_value(), and Sqrt().
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 4240 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
def z3py.Star | ( | re | ) |
Create the regular expression accepting zero or more repetitions of argument. >>> re = Star(Re("a")) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("ab", re))) False >>> print(simplify(InRe("", re))) True
Definition at line 11007 of file z3py.py.
Referenced by Star().
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 4725 of file z3py.py.
Referenced by is_array(), is_store(), SetAdd(), SetDel(), and Store().
def z3py.String | ( | name, | |
ctx = None |
|||
) |
Return a string constant named `name`. If `ctx=None`, then the global context is used. >>> x = String('x')
Definition at line 10693 of file z3py.py.
Referenced by Context.Context(), Statistics.getEntries(), Statistics.getKeys(), Context.getProbeNames(), Context.getTacticNames(), String(), Strings(), and FuncInterp< R extends Sort >.toString().
def z3py.Strings | ( | names, | |
ctx = None |
|||
) |
Return a tuple of String constants.
Definition at line 10702 of file z3py.py.
Referenced by Contains().
def z3py.StringSort | ( | ctx = None | ) |
Create a string sort >>> s = StringSort() >>> print(s) String
Definition at line 10569 of file z3py.py.
Referenced by DisjointSum(), Empty(), Full(), SeqSortRef.is_string(), String(), StringSort(), and TupleSort().
def z3py.StringVal | ( | s, | |
ctx = None |
|||
) |
create a string expression
Definition at line 10686 of file z3py.py.
Referenced by SeqRef.__gt__(), ExprRef.children(), Empty(), Extract(), AlgebraicNumRef.index(), is_seq(), is_string(), is_string_value(), Length(), and Re().
def z3py.StrToInt | ( | s | ) |
Convert string expression to integer >>> a = StrToInt("1") >>> simplify(1 == a) True >>> b = StrToInt("2") >>> simplify(1 == b) False >>> c = StrToInt(IntToStr(2)) >>> simplify(1 == c) False
Definition at line 10862 of file z3py.py.
Referenced by StrToInt().
def z3py.SubSeq | ( | s, | |
offset, | |||
length | |||
) |
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 8680 of file z3py.py.
Referenced by Expr< R extends Sort >.substitute(), and substitute().
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 8709 of file z3py.py.
Referenced by substitute_vars().
def z3py.SubString | ( | s, | |
offset, | |||
length | |||
) |
def z3py.SuffixOf | ( | a, | |
b | |||
) |
Check if 'a' is a suffix of 'b' >>> s1 = SuffixOf("ab", "abc") >>> simplify(s1) False >>> s2 = SuffixOf("bc", "abc") >>> simplify(s2) True
Definition at line 10774 of file z3py.py.
Referenced by SuffixOf().
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 8730 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), RealVector(), and Sum().
def z3py.tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 8334 of file z3py.py.
Referenced by describe_tactics(), and tactic_description().
def z3py.tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3. >>> l = tactics() >>> l.count('simplify') == 1 True
Definition at line 8323 of file z3py.py.
Referenced by describe_tactics(), and tactics().
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 8191 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), ApplyResult.__len__(), Goal.convert_model(), Goal.depth(), Statistics.get_key_value(), Statistics.keys(), Repeat(), Tactic.solver(), and Then().
def z3py.to_symbol | ( | s, | |
ctx = None |
|||
) |
Convert an integer or string into a Z3 symbol.
Definition at line 129 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), is_quantifier(), prove(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().
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 3338 of file z3py.py.
Referenced by is_to_int(), and ToInt().
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 3320 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), SortRef.cast(), is_to_real(), and ToReal().
def z3py.TransitiveClosure | ( | f | ) |
Given a binary relation R, such that the two arguments have the same sort create the transitive closure relation R+. The transitive closure R+ is a new relation.
Definition at line 11064 of file z3py.py.
def z3py.TreeOrder | ( | a, | |
index | |||
) |
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 8314 of file z3py.py.
def z3py.TupleSort | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tuple sort base on a set of underlying sorts Example: >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
Definition at line 5293 of file z3py.py.
Referenced by Context.MkTupleSort(), Context.mkTupleSort(), and TupleSort().
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 4198 of file z3py.py.
Referenced by BitVecRef.__div__(), BitVecRef.__rdiv__(), and UDiv().
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 4162 of file z3py.py.
Referenced by BitVecRef.__ge__(), and UGE().
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 4180 of file z3py.py.
Referenced by BitVecRef.__gt__(), and UGT().
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 4126 of file z3py.py.
Referenced by BitVecRef.__le__(), and ULE().
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 4144 of file z3py.py.
Referenced by BitVecRef.__lt__(), and ULT().
def z3py.Union | ( | * | args | ) |
Create union of regular expressions. >>> re = Union(Re("a"), Re("b"), Re("c")) >>> print (simplify(InRe("d", re))) False
Definition at line 10938 of file z3py.py.
Referenced by ReRef.__add__(), InRe(), and Union().
def z3py.Unit | ( | a | ) |
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
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 4219 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
def z3py.user_prop_diseq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
def z3py.user_prop_eq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
def z3py.user_prop_final | ( | ctx, | |
cb | |||
) |
def z3py.user_prop_fixed | ( | ctx, | |
cb, | |||
id, | |||
value | |||
) |
def z3py.user_prop_fresh | ( | id, | |
ctx | |||
) |
def z3py.user_prop_pop | ( | ctx, | |
num_scopes | |||
) |
def z3py.user_prop_push | ( | 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 1438 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), get_var_index(), is_pattern(), is_var(), MultiPattern(), QuantifierRef.pattern(), RealVar(), RealVarVector(), substitute_vars(), and Var().
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 8608 of file z3py.py.
Referenced by When().
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 8265 of file z3py.py.
Referenced by Goal.prec(), and With().
def z3py.WithParams | ( | t, | |
p | |||
) |
Return a tactic that applies tactic `t` using the given configuration options. >>> x, y = Ints('x y') >>> p = ParamsRef() >>> p.set("som", True) >>> t = WithParams(Tactic('simplify'), p) >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]]
Definition at line 8279 of file z3py.py.
Referenced by WithParams().
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 1763 of file z3py.py.
Referenced by Xor().
def z3py.z3_debug | ( | ) |
Definition at line 64 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), ExprRef.children(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), describe_probes(), Distinct(), FuncDeclRef.domain(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), AlgebraicNumRef.index(), Intersect(), is_quantifier(), is_sort(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), prove(), RatVal(), RealSort(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
def z3py.z3_error_handler | ( | c, | |
e | |||
) |
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 4355 of file z3py.py.
Referenced by ZeroExt().
sat = CheckSatResult(Z3_L_TRUE) |
unknown = CheckSatResult(Z3_L_UNDEF) |
unsat = CheckSatResult(Z3_L_FALSE) |