|
Z3
|
|
|
Z3
|
|
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 Fixedpoint.add_rule(), Goal.as_expr(), Bool(), Bools(), BoolVector(), Lambda(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), 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.
Referenced by Context.Then(), and Then().
| def z3py.append_log | ( | s | ) |
| def z3py.args2params | ( | arguments, | |
| keywords, | |||
ctx = None |
|||
| ) |
Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'
>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
(params model true relevancy 2 elim_and true)
Definition at line 5396 of file z3py.py.
Referenced by Tactic.apply(), 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__(), 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(), 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 ArraySortRef.domain(), ArraySort< D, BoolSort >.getRange(), Context.MkArraySort(), ArraySortRef.range(), and Sort.Translate().
| def z3py.AtLeast | ( | args | ) |
| def z3py.AtMost | ( | args | ) |
| 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__(), 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__(), 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(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), BitVecRef.sort(), Sort.translate(), and Sort.Translate().
| 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(), 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 Solver.assert_and_track(), Optimize.assert_and_track(), 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(), Solver.consequences(), Implies(), Or(), 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 ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), ArrayRef.sort(), Sort.translate(), and Sort.Translate().
| 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 ApplyResult.as_expr(), BoolSortRef.cast(), 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(), 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.
| def z3py.BVAddNoOverflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
| def z3py.BVAddNoUnderflow | ( | a, | |
| b | |||
| ) |
| 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 | |||
| ) |
| def z3py.BVSNegNoOverflow | ( | a | ) |
| def z3py.BVSubNoOverflow | ( | a, | |
| b | |||
| ) |
| 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 |
|||
| ) |
| 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 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.
Referenced by If().
| 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(), Consts(), FPSort(), IntSort(), 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 EnumSort.ConstDecl(), 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.
| 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().
| 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 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 is_default().
| def z3py.describe_probes | ( | ) |
| def z3py.describe_tactics | ( | ) |
| def z3py.disable_trace | ( | msg | ) |
| 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()])
| 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.
| 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.
| def z3py.EmptySet | ( | s | ) |
| def z3py.enable_trace | ( | msg | ) |
| def z3py.EnumSort | ( | name, | |
| values, | |||
ctx = None |
|||
| ) |
Return a new enumeration sort named `name` containing the given values.
The result is a pair (sort, list of constants).
Example:
>>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Definition at line 5317 of file z3py.py.
Referenced by EnumSort< R >.getTesterDecl(), Context.MkEnumSort(), and EnumSort.TesterDecl().
| 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(), FP(), FPSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), Select(), and substitute().
| 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(), 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.
| 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.
| 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.
| 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 Context.MkFiniteDomainSort(), Sort.translate(), and Sort.Translate().
| 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.
| 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(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
| 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__(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), 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.
| 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 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.
| def z3py.fpDiv | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| 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
| 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.
| def z3py.fpGEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpGT | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpInfinity | ( | s, | |
| negative | |||
| ) |
| def z3py.fpIsInf | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsNaN | ( | a, | |
ctx = None |
|||
| ) |
| 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 |
|||
| ) |
| def z3py.fpLT | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpMax | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpMin | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpMinusInfinity | ( | s | ) |
| def z3py.fpMinusZero | ( | s | ) |
| def z3py.fpMul | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
| 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 |
|||
| ) |
| def z3py.fpNEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| 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.
| 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.
| def z3py.fpRem | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| 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(), and fpNEQ().
| 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.
| 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(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.MkFPRTZ(), 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(), FPRef.sort(), Sort.translate(), and Sort.Translate().
| def z3py.fpSqrt | ( | rm, | |
| a, | |||
ctx = None |
|||
| ) |
| def z3py.fpSub | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
| 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(), and fpSignedToFP().
| 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().
| 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.
| 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.
| 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.
| 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.
| 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(), is_fp_value(), FPNumRef.isNegative(), 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.
| def z3py.FreshConst | ( | sort, | |
prefix = "c" |
|||
| ) |
| def z3py.FreshFunction | ( | sig | ) |
| 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.
| 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.
| 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.
| 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 ModelRef.__getitem__(), ModelRef.__len__(), FuncEntry.arg_value(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), QuantifierRef.children(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), Lambda(), Map(), MultiPattern(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
| def z3py.get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
| def z3py.get_default_rounding_mode | ( | ctx = None | ) |
| 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.
| def z3py.get_param | ( | name | ) |
| def z3py.get_var_index | ( | a | ) |
Return the de-Bruijn index of the Z3 bounded variable `a`.
>>> x = Int('x')
>>> y = Int('y')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> # Z3 replaces x and y with bound variables when ForAll is executed.
>>> q = ForAll([x, y], f(x, y) == x + y)
>>> q.body()
f(Var(1), Var(0)) == Var(1) + Var(0)
>>> b = q.body()
>>> b.arg(0)
f(Var(1), Var(0))
>>> v1 = b.arg(0).arg(0)
>>> v2 = b.arg(0).arg(1)
>>> v1
Var(1)
>>> v2
Var(0)
>>> get_var_index(v1)
1
>>> get_var_index(v2)
0
Definition at line 1303 of file z3py.py.
| def z3py.get_version | ( | ) |
| def z3py.get_version_string | ( | ) |
| def z3py.help_simplify | ( | ) |
| 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__(), BV2Int(), and Lambda().
| 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(), 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.
| 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 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__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), QuantifierRef.is_lambda(), is_pattern(), is_quantifier(), ArithSortRef.is_real(), is_real(), is_select(), is_to_real(), K(), AstMap.keys(), Statistics.keys(), Solver.model(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), Solver.pop(), AstVector.push(), Solver.push(), Solver.reason_unknown(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
| def z3py.Int2BV | ( | a, | |
| num_bits | |||
| ) |
| def z3py.Intersect | ( | args | ) |
| 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 ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.convert_model(), Goal.depth(), Goal.get(), Goal.inconsistent(), is_add(), is_div(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Lambda(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().
| 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 ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), Full(), FullSet(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_fp_sort(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), SeqSortRef.is_string(), IsMember(), IsSubset(), K(), Lambda(), Map(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), Store(), Sort.translate(), Sort.Translate(), TupleSort(), Update(), FuncEntry.value(), 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 AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_binary_string(), IntNumRef.as_long(), IntNumRef.as_string(), is_arith(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), and SeqSort().
| def z3py.IntVector | ( | prefix, | |
| sz, | |||
ctx = None |
|||
| ) |
| def z3py.is_add | ( | a | ) |
| def z3py.is_algebraic_value | ( | a | ) |
| def z3py.is_and | ( | a | ) |
| 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(), expr.hi(), expr.is_and(), is_app_of(), expr.is_const(), is_const(), expr.is_distinct(), expr.is_eq(), expr.is_false(), expr.is_implies(), expr.is_ite(), expr.is_not(), expr.is_or(), expr.is_true(), expr.is_xor(), expr.lo(), ExprRef.num_args(), expr.operator Z3_app(), 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_and(), is_distinct(), is_eq(), is_false(), is_implies(), is_not(), is_or(), and is_true().
| def z3py.is_arith | ( | a | ) |
| def z3py.is_arith_sort | ( | s | ) |
| 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 sort.array_domain(), sort.array_range(), and expr.operator[]().
| def z3py.is_array_sort | ( | a | ) |
| def z3py.is_as_array | ( | n | ) |
| 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 AstRef.eq(), and eq().
| 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(), 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(), sort.bv_size(), fpToIEEEBV(), fpToSBV(), fpToUBV(), expr.mk_from_ieee_bv(), Product(), and Sum().
| def z3py.is_bv_sort | ( | s | ) |
| def z3py.is_bv_value | ( | a | ) |
| 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 Optimize.assert_and_track(), and prove().
| def z3py.is_const_array | ( | a | ) |
| def z3py.is_default | ( | a | ) |
| def z3py.is_distinct | ( | a | ) |
| def z3py.is_div | ( | a | ) |
| 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__().
| 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 SortRef.cast(), BoolSortRef.cast(), ExprRef.children(), is_var(), simplify(), 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__(), and BoolVal().
| 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_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().
| def z3py.is_finite_domain_value | ( | a | ) |
| 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(), fpToIEEEBV(), fpToReal(), fpToSBV(), and fpToUBV().
| def z3py.is_fp_sort | ( | s | ) |
| def z3py.is_fp_value | ( | a | ) |
| def z3py.is_fprm | ( | a | ) |
| def z3py.is_fprm_sort | ( | s | ) |
| def z3py.is_fprm_value | ( | a | ) |
| def z3py.is_func_decl | ( | a | ) |
| def z3py.is_ge | ( | a | ) |
| def z3py.is_gt | ( | a | ) |
| def z3py.is_idiv | ( | a | ) |
| def z3py.is_implies | ( | a | ) |
| def z3py.is_int | ( | a | ) |
Return `True` if `a` is an integer expression.
>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False
Definition at line 2648 of file z3py.py.
Referenced by Int(), IntSort(), 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.
| def z3py.is_is_int | ( | a | ) |
| def z3py.is_K | ( | a | ) |
| def z3py.is_le | ( | a | ) |
| def z3py.is_lt | ( | a | ) |
| def z3py.is_map | ( | a | ) |
| def z3py.is_mod | ( | a | ) |
| def z3py.is_mul | ( | a | ) |
| def z3py.is_not | ( | a | ) |
| def z3py.is_or | ( | a | ) |
| 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 MultiPattern().
| def z3py.is_probe | ( | p | ) |
| def z3py.is_quantifier | ( | a | ) |
Return `True` if `a` is a Z3 quantifier.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(f(x))
False
Definition at line 2138 of file z3py.py.
Referenced by expr.body(), and Exists().