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 |
| 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 |
| def | eq |
| def | is_sort |
| def | DeclareSort |
| def | DeclareTypeVar |
| def | is_func_decl (a) |
| def | Function (name, sig) |
| def | FreshFunction (sig) |
| def | RecFunction (name, sig) |
| def | RecAddDefinition (f, args, body) |
| def | deserialize (st) |
| 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 |
| def | Distinct (args) |
| def | Const (name, sort) |
| def | Consts (names, sort) |
| def | FreshConst |
| def | Var |
| def | RealVar |
| def | RealVarVector |
| def | is_bool |
| def | is_true |
| def | is_false |
| def | is_and |
| def | is_or |
| def | is_implies |
| def | is_not |
| def | is_eq |
| def | is_distinct |
| def | BoolSort |
| def | BoolVal |
| def | Bool |
| def | Bools |
| def | BoolVector |
| def | FreshBool |
| def | Implies |
| def | Xor |
| def | Not |
| def | mk_not (a) |
| def | And (args) |
| def | Or (args) |
| def | is_pattern (a) |
| def | MultiPattern (args) |
| def | is_quantifier (a) |
| def | ForAll |
| def | Exists |
| def | Lambda (vs, body) |
| def | is_arith_sort |
| 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 |
| def | is_mul |
| def | is_sub |
| def | is_div |
| def | is_idiv |
| def | is_mod |
| def | is_le |
| def | is_lt |
| def | is_ge |
| def | is_gt |
| def | is_is_int |
| def | is_to_real |
| def | is_to_int |
| def | IntSort |
| def | RealSort |
| def | IntVal |
| def | RealVal |
| def | RatVal |
| def | Q |
| def | Int |
| def | Ints |
| def | IntVector |
| def | FreshInt |
| def | Real |
| def | Reals |
| def | RealVector |
| def | FreshReal |
| def | ToReal (a) |
| def | ToInt (a) |
| def | IsInt (a) |
| def | Sqrt |
| def | Cbrt |
| def | is_bv_sort (s) |
| def | is_bv (a) |
| def | is_bv_value (a) |
| def | BV2Int |
| def | Int2BV (a, num_bits) |
| def | BitVecSort |
| def | BitVecVal |
| def | BitVec |
| def | BitVecs |
| 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 |
| 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, sorts) |
| def | Update (a, args) |
| def | Default (a) |
| def | Store (a, args) |
| def | Select (a, args) |
| def | Map (f, args) |
| def | K (dom, v) |
| def | Ext (a, b) |
| 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 | DatatypeSort |
| def | TupleSort |
| def | DisjointSum |
| def | EnumSort |
| def | args2params |
| def | Model |
| def | is_as_array (n) |
| def | get_as_array_func (n) |
| def | SolverFor |
| def | SimpleSolver |
| def | FiniteDomainSort |
| def | is_finite_domain_sort (s) |
| def | is_finite_domain (a) |
| def | FiniteDomainVal |
| def | is_finite_domain_value (a) |
| def | AndThen (ts, ks) |
| def | Then (ts, ks) |
| def | OrElse (ts, ks) |
| def | ParOr (ts, ks) |
| def | ParThen |
| def | ParAndThen |
| def | With (t, args, keys) |
| def | WithParams (t, p) |
| def | Repeat |
| def | TryFor |
| def | tactics |
| def | tactic_description |
| def | describe_tactics () |
| def | is_probe (p) |
| def | probes |
| def | probe_description |
| def | describe_probes () |
| def | FailIf |
| def | When |
| def | Cond |
| def | simplify (a, arguments, keywords) |
| Utils. More... | |
| def | help_simplify () |
| def | simplify_param_descrs () |
| def | substitute (t, m) |
| def | substitute_vars (t, m) |
| def | substitute_funs (t, m) |
| def | Sum (args) |
| def | Product (args) |
| def | Abs (arg) |
| def | AtMost (args) |
| def | AtLeast (args) |
| def | PbLe (args, k) |
| def | PbGe (args, k) |
| def | PbEq |
| def | solve (args, keywords) |
| def | solve_using (s, args, keywords) |
| def | prove (claim, show=False, keywords) |
| def | parse_smt2_string |
| def | parse_smt2_file |
| def | get_default_rounding_mode |
| def | set_default_rounding_mode |
| def | get_default_fp_sort |
| def | set_default_fp_sort |
| def | Float16 |
| def | FloatHalf |
| def | Float32 |
| def | FloatSingle |
| def | Float64 |
| def | FloatDouble |
| def | Float128 |
| def | FloatQuadruple |
| def | is_fp_sort (s) |
| def | is_fprm_sort (s) |
| def | RoundNearestTiesToEven |
| def | RNE |
| def | RoundNearestTiesToAway |
| def | RNA |
| def | RoundTowardPositive |
| def | RTP |
| def | RoundTowardNegative |
| def | RTN |
| def | RoundTowardZero |
| def | RTZ |
| def | is_fprm (a) |
| def | is_fprm_value (a) |
| def | is_fp (a) |
| def | is_fp_value (a) |
| def | FPSort |
| 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 |
| def | FP |
| def | FPs |
| def | fpAbs |
| def | fpNeg |
| def | fpAdd |
| def | fpSub |
| def | fpMul |
| def | fpDiv |
| def | fpRem |
| def | fpMin |
| def | fpMax |
| def | fpFMA |
| def | fpSqrt |
| def | fpRoundToIntegral |
| def | fpIsNaN |
| def | fpIsInf |
| def | fpIsZero |
| def | fpIsNormal |
| def | fpIsSubnormal |
| def | fpIsNegative |
| def | fpIsPositive |
| def | fpLT |
| def | fpLEQ |
| def | fpGT |
| def | fpGEQ |
| def | fpEQ |
| def | fpNEQ |
| def | fpFP |
| def | fpToFP |
| def | fpBVToFP |
| def | fpFPToFP |
| def | fpRealToFP |
| def | fpSignedToFP |
| def | fpUnsignedToFP |
| def | fpToFPUnsigned |
| def | fpToSBV |
| def | fpToUBV |
| def | fpToReal |
| def | fpToIEEEBV |
| def | StringSort |
| def | CharSort |
| def | SeqSort (s) |
| def | CharVal |
| def | CharFromBv (bv) |
| def | CharToBv |
| def | CharToInt |
| def | CharIsDigit |
| def | is_seq (a) |
| def | is_string |
| def | is_string_value |
| def | StringVal |
| def | String |
| def | Strings |
| 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 |
| def | LastIndexOf (s, substr) |
| def | Length (s) |
| def | SeqMap (f, s) |
| def | SeqMapI (f, i, s) |
| def | SeqFoldLeft (f, a, s) |
| def | SeqFoldLeftI (f, i, a, s) |
| def | StrToInt (s) |
| def | IntToStr (s) |
| def | StrToCode (s) |
| def | StrFromCode (c) |
| def | Re |
| 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 |
| def | Range |
| def | Diff |
| def | AllChar |
| def | PartialOrder (a, index) |
| def | LinearOrder (a, index) |
| def | TreeOrder (a, index) |
| def | PiecewiseLinearOrder (a, index) |
| def | TransitiveClosure (f) |
| def | to_Ast (ptr) |
| def | to_ContextObj (ptr) |
| def | to_AstVectorObj (ptr) |
| def | on_clause_eh (ctx, p, n, dep, clause) |
| def | ensure_prop_closures () |
| def | user_prop_push (ctx, cb) |
| def | user_prop_pop (ctx, cb, num_scopes) |
| def | user_prop_fresh (ctx, _new_ctx) |
| def | user_prop_fixed (ctx, cb, id, value) |
| def | user_prop_created (ctx, cb, id) |
| def | user_prop_final (ctx, cb) |
| def | user_prop_eq (ctx, cb, x, y) |
| def | user_prop_diseq (ctx, cb, x, y) |
| def | user_prop_decide (ctx, cb, t_ref, idx, phase) |
| def | user_prop_binding (ctx, cb, q_ref, inst_ref) |
| def | PropagateFunction (name, sig) |
| def z3py.Abs | ( | arg | ) |
Create the absolute value of an arithmetic expression
Definition at line 9335 of file z3py.py.
Referenced by ArithRef.__abs__().
| def z3py.AllChar | ( | regex_sort, | |
ctx = None |
|||
| ) |
Create a regular expression that accepts all single character strings
Definition at line 11772 of file z3py.py.
| 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 1982 of file z3py.py.
Referenced by BoolRef.__and__(), 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 8700 of file z3py.py.
Referenced by 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 5695 of file z3py.py.
Referenced by Tactic.apply(), Fixedpoint.set(), Optimize.set(), simplify(), Simplifier.using_params(), and With().
| def z3py.Array | ( | name, | |
| sorts | |||
| ) |
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 4923 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 4890 of file z3py.py.
Referenced by SortRef.__gt__(), Array(), ArraySortRef.domain(), and ArraySortRef.range().
| def z3py.AtLeast | ( | args | ) |
Create an at-least Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)
Definition at line 9358 of file z3py.py.
| 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 9340 of file z3py.py.
| 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 4204 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 4228 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 4172 of file z3py.py.
Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), 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 4187 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 1861 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 1873 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 1824 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), DatatypeSort(), ArraySortRef.domain(), ArrayRef.domain(), If(), IntSort(), is_arith_sort(), ArraySortRef.range(), ArrayRef.range(), and ArrayRef.sort().
| 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 1842 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 1889 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 4140 of file z3py.py.
| def z3py.BVAddNoOverflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4649 of file z3py.py.
| def z3py.BVAddNoUnderflow | ( | a, | |
| b | |||
| ) |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4656 of file z3py.py.
| def z3py.BVMulNoOverflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4691 of file z3py.py.
| def z3py.BVMulNoUnderflow | ( | a, | |
| b | |||
| ) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4698 of file z3py.py.
| def z3py.BVRedAnd | ( | a | ) |
Return the reduction-and expression of `a`.
Definition at line 4635 of file z3py.py.
| def z3py.BVRedOr | ( | a | ) |
Return the reduction-or expression of `a`.
Definition at line 4642 of file z3py.py.
| def z3py.BVSDivNoOverflow | ( | a, | |
| b | |||
| ) |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4677 of file z3py.py.
| def z3py.BVSNegNoOverflow | ( | a | ) |
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4684 of file z3py.py.
| def z3py.BVSubNoOverflow | ( | a, | |
| b | |||
| ) |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4663 of file z3py.py.
| def z3py.BVSubNoUnderflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4670 of file z3py.py.
| def z3py.Cbrt | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.CharFromBv | ( | bv | ) |
| def z3py.CharSort | ( | ctx = None | ) |
Create a character sort >>> ch = CharSort() >>> print(ch) Char
Definition at line 11168 of file z3py.py.
| def z3py.Complement | ( | re | ) |
Create the complement regular expression.
Definition at line 11714 of file z3py.py.
| 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 4249 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 9157 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 1540 of file z3py.py.
Referenced by BitVecSort(), Consts(), FPSort(), IntSort(), IsMember(), IsSubset(), RealSort(), DatatypeSortRef.recognizer(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), and DatatypeRef.update_field().
| 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 1552 of file z3py.py.
Referenced by 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 11459 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 5341 of file z3py.py.
Referenced by Datatype.create().
| def z3py.DatatypeSort | ( | name, | |
params = None, |
|||
ctx = None |
|||
| ) |
Create a reference to a sort that was declared, or will be declared, as a recursive datatype.
Args:
name: name of the datatype sort
params: optional list/tuple of sort parameters for parametric datatypes
ctx: Z3 context (optional)
Example:
>>> # Non-parametric datatype
>>> TreeRef = DatatypeSort('Tree')
>>> # Parametric datatype with one parameter
>>> ListIntRef = DatatypeSort('List', [IntSort()])
>>> # Parametric datatype with multiple parameters
>>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()])
Definition at line 5567 of file z3py.py.
| def z3py.DeclareSort | ( | name, | |
ctx = None, |
|||
| SortRef | |||
| ) |
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 730 of file z3py.py.
Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
| def z3py.DeclareTypeVar | ( | name, | |
ctx = None |
|||
| ) |
Create a new type variable named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context.
Definition at line 758 of file z3py.py.
| def z3py.Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 4969 of file z3py.py.
Referenced by is_default().
| def z3py.describe_probes | ( | ) |
| def z3py.describe_tactics | ( | ) |
| def z3py.deserialize | ( | st | ) |
inverse function to the serialize method on ExprRef. It is made available to make it easier for users to serialize expressions back and forth between strings. Solvers can be serialized using the 'sexpr()' method.
Definition at line 1207 of file z3py.py.
| def z3py.Diff | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create the difference regular expression
Definition at line 11764 of file z3py.py.
| 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()])
Definition at line 5604 of file z3py.py.
| 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 1507 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 11389 of file z3py.py.
| def z3py.EmptySet | ( | s | ) |
Create the empty set >>> EmptySet(IntSort()) K(Int, False)
Definition at line 5105 of file z3py.py.
| def z3py.enable_trace | ( | msg | ) |
| def z3py.ensure_prop_closures | ( | ) |
Definition at line 11883 of file z3py.py.
| 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 5616 of file z3py.py.
| def z3py.eq | ( | a | ) |
Definition at line 503 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 2383 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 5058 of file z3py.py.
| def z3py.Extract | ( | high, | |
| low, | |||
| a | |||
| ) |
Create a Z3 bit-vector extraction expression or sequence extraction expression.
Extract is overloaded to work with both bit-vectors and sequences:
**Bit-vector extraction**: Extract(high, low, bitvector)
Extracts bits from position `high` down to position `low` (both inclusive).
- high: int - the highest bit position to extract (0-indexed from right)
- low: int - the lowest bit position to extract (0-indexed from right)
- bitvector: BitVecRef - the bit-vector to extract from
Returns a new bit-vector containing bits [high:low]
**Sequence extraction**: Extract(sequence, offset, length)
Extracts a subsequence starting at the given offset with the specified length.
The functions SubString and SubSeq are redirected to this form of Extract.
- sequence: SeqRef or str - the sequence to extract from
- offset: int - the starting position (0-indexed)
- length: int - the number of elements to extract
Returns a new sequence containing the extracted subsequence
>>> # Bit-vector extraction examples
>>> x = BitVec('x', 8)
>>> Extract(6, 2, x) # Extract bits 6 down to 2 (5 bits total)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort() # Result is a 5-bit vector
BitVec(5)
>>> Extract(7, 0, x) # Extract all 8 bits
Extract(7, 0, x)
>>> Extract(3, 3, x) # Extract single bit at position 3
Extract(3, 3, x)
>>> # Sequence extraction examples
>>> s = StringVal("hello")
>>> Extract(s, 1, 3) # Extract 3 characters starting at position 1
str.substr("hello", 1, 3)
>>> simplify(Extract(StringVal("abcd"), 2, 1)) # Extract 1 character at position 2
"c"
>>> simplify(Extract(StringVal("abcd"), 0, 2)) # Extract first 2 characters
"ab"
Definition at line 4295 of file z3py.py.
Referenced by 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 9115 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 8044 of file z3py.py.
| 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 8114 of file z3py.py.
| def z3py.Float128 | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 9843 of file z3py.py.
| def z3py.Float16 | ( | ctx = None | ) |
Floating-point 16-bit (half) sort.
Definition at line 9807 of file z3py.py.
| def z3py.Float32 | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 9819 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 9831 of file z3py.py.
Referenced by fpFPToFP(), and fpToFP().
| def z3py.FloatDouble | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 9837 of file z3py.py.
| def z3py.FloatHalf | ( | ctx = None | ) |
Floating-point 16-bit (half) sort.
Definition at line 9813 of file z3py.py.
| def z3py.FloatQuadruple | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 9849 of file z3py.py.
| def z3py.FloatSingle | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 9825 of file z3py.py.
| 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 2365 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 10485 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 10528 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)
x + y
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
fpAdd(RTZ(), x, y)
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)
Definition at line 10619 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 10941 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
Definition at line 10873 of file z3py.py.
| 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 10958 of file z3py.py.
| def z3py.fpGEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpGT | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpInfinity | ( | s, | |
| negative | |||
| ) |
Create a Z3 floating-point +oo or -oo term.
Definition at line 10413 of file z3py.py.
| 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 | ) |
Create a Z3 floating-point -oo term.
Definition at line 10407 of file z3py.py.
| def z3py.fpMinusZero | ( | s | ) |
Create a Z3 floating-point -0.0 term.
Definition at line 10426 of file z3py.py.
| 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 10373 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 10551 of file z3py.py.
| 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 10390 of file z3py.py.
| def z3py.fpPlusZero | ( | s | ) |
Create a Z3 floating-point +0.0 term.
Definition at line 10420 of file z3py.py.
| 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 10978 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)
(x + y) * z
Definition at line 10509 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 10996 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 10314 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(), 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 |
|||
| ) |
| 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 10902 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 11032 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 11106 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 11086 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 11042 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 11064 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 11014 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 10439 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 | |||
| ) |
Create a Z3 floating-point +0.0 or -0.0 term.
Definition at line 10432 of file z3py.py.
| 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 1904 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 3447 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 3504 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 11409 of file z3py.py.
| def z3py.FullSet | ( | s | ) |
Create the full set >>> FullSet(IntSort()) K(Int, True)
Definition at line 5114 of file z3py.py.
| 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 920 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 4866 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 1438 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 1484 of file z3py.py.
Referenced by ArithRef.__abs__(), BoolRef.__add__(), BoolRef.__mul__(), Abs(), 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 1918 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 11493 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 11632 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 3408 of file z3py.py.
Referenced by ArithRef.__abs__(), 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(), 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 | |||
| ) |
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 4163 of file z3py.py.
| def z3py.Intersect | ( | args | ) |
Create intersection of regular expressions.
>>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 11666 of file z3py.py.
| 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 3421 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 3298 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(), DatatypeSort(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), FreshInt(), Full(), FullSet(), ModelRef.get_interp(), get_map_func(), Int(), 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(), 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(), TupleSort(), Update(), DatatypeRef.update_field(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
| def z3py.IntToStr | ( | s | ) |
Convert integer expression to string
Definition at line 11574 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 3344 of file z3py.py.
Referenced by AstMap.__len__(), ArithRef.__mod__(), BoolRef.__mul__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_binary_string(), IntNumRef.as_long(), IntNumRef.as_string(), IndexOf(), is_arith(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), SeqSort(), and DatatypeRef.update_field().
| def z3py.IntVector | ( | prefix, | |
| sz, | |||
ctx = None |
|||
| ) |
| def z3py.is_algebraic_value | ( | 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 1368 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), ExprRef.kind(), ExprRef.num_args(), RecAddDefinition(), and ExprRef.update().
| 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 1471 of file z3py.py.
Referenced by is_add(), is_and(), is_distinct(), is_eq(), is_false(), is_implies(), is_not(), is_or(), 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 2819 of file z3py.py.
Referenced by is_algebraic_value().
| 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 6956 of file z3py.py.
Referenced by get_as_array_func().
| def z3py.is_ast | ( | a | ) |
| def z3py.is_bool | ( | a | ) |
| 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 4111 of file z3py.py.
Referenced by BitVec(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), Product(), and Sum().
| 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 3638 of file z3py.py.
Referenced by BitVecVal(), fpToSBV(), and fpToUBV().
| 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 1394 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_eq | ( | a | ) |
| 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 1345 of file z3py.py.
Referenced by SortRef.cast(), BoolSortRef.cast(), Cbrt(), CharFromBv(), Concat(), deserialize(), Diff(), IndexOf(), IntToStr(), is_var(), simplify(), substitute(), substitute_funs(), substitute_vars(), and ExprRef.update().
| def z3py.is_false | ( | a | ) |
Definition at line 1740 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and BoolRef.py_value().
| 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 8075 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 8052 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 10285 of file z3py.py.
Referenced by FP(), fpFPToFP(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), and fpToUBV().
| 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 9859 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().
| def z3py.is_fp_value | ( | a | ) |
| 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 10119 of file z3py.py.
Referenced by fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), and fpUnsignedToFP().
| def z3py.is_fprm_sort | ( | s | ) |
| def z3py.is_fprm_value | ( | a | ) |
| def z3py.is_func_decl | ( | a | ) |
Return `True` if `a` is a Z3 function declaration.
>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False
Definition at line 907 of file z3py.py.
Referenced by prove(), and substitute_funs().
| def z3py.is_int | ( | a, | |
| bool | |||
| ) |
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 2840 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 2886 of file z3py.py.
| def z3py.is_K | ( | a | ) |
| 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 4841 of file z3py.py.
Referenced by get_map_func().
| 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 2066 of file z3py.py.
Referenced by MultiPattern().
| def z3py.is_probe | ( | p | ) |
| def z3py.is_quantifier | ( | a | ) |
| 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 2910 of file z3py.py.
Referenced by RatNumRef.denominator(), 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 2859 of file z3py.py.
Referenced by fpRealToFP(), fpToFP(), fpToReal(), Real(), and RealSort().
| def z3py.is_select | ( | a | ) |
| def z3py.is_seq | ( | a | ) |
| def z3py.is_sort | ( | s | ) |
Definition at line 682 of file z3py.py.
Referenced by ArraySort(), CreateDatatypes(), FreshConst(), FreshFunction(), Function(), prove(), RecFunction(), and Var().
| def z3py.is_store | ( | a | ) |
| def z3py.is_true | ( | a | ) |
Definition at line 1722 of file z3py.py.
Referenced by AstRef.__bool__(), BoolVal(), and BoolRef.py_value().
| 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 1413 of file z3py.py.
Referenced by get_var_index().
| 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 3556 of file z3py.py.
Referenced by is_is_int().
| 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 5192 of file z3py.py.
| 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 5203 of file z3py.py.
| 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 5036 of file z3py.py.
Referenced by Default(), EmptySet(), FullSet(), is_const_array(), is_default(), and is_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 2404 of file z3py.py.
Referenced by QuantifierRef.is_lambda().
| def z3py.LastIndexOf | ( | s, | |
| substr | |||
| ) |
Retrieve the last index of substring within a string
Definition at line 11513 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 11522 of file z3py.py.
| 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 11734 of file z3py.py.
| 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 4489 of file z3py.py.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), and BitVecRef.__rshift__().
| def z3py.main_ctx | ( | Context | ) |
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 266 of file z3py.py.
Referenced by help_simplify(), 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 5013 of file z3py.py.
Referenced by get_map_func(), and is_map().
| def z3py.Model | ( | ctx = None, |
|
eval = {} |
|||
| ) |
Definition at line 6948 of file z3py.py.
Referenced by 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 2084 of file z3py.py.
| 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 1948 of file z3py.py.
Referenced by BoolRef.__invert__(), Solver.consequences(), Goal.convert_model(), fpNEQ(), mk_not(), prove(), and Xor().
| def z3py.on_clause_eh | ( | ctx, | |
| p, | |||
| n, | |||
| dep, | |||
| clause | |||
| ) |
Definition at line 11824 of file z3py.py.
Referenced by on_clause.on_clause().
| def z3py.open_log | ( | fname | ) |
| 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 11699 of file z3py.py.
| 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 2015 of file z3py.py.
Referenced by BoolRef.__or__(), ApplyResult.as_expr(), Bools(), and Goal.convert_model().
| 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]]
| 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 8754 of file z3py.py.
| 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 9669 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 9648 of file z3py.py.
Referenced by parse_smt2_file().
| 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 8773 of file z3py.py.
Referenced by ParAndThen().
| def z3py.PartialOrder | ( | a, | |
| index | |||
| ) |
| def z3py.PbEq | ( | args, | |
| k, | |||
ctx = None |
|||
| ) |
Create a Pseudo-Boolean equality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 9425 of file z3py.py.
| 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 9414 of file z3py.py.
| 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 9403 of file z3py.py.
| 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 11684 of file z3py.py.
| 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 11429 of file z3py.py.
| def z3py.probe_description | ( | name, | |
ctx = None |
|||
| ) |
Return a short description for the probe named `name`.
>>> d = probe_description('memory')
Definition at line 9069 of file z3py.py.
Referenced by describe_probes().
| def z3py.probes | ( | ctx = None | ) |
Return a list of all available probes in Z3.
>>> l = probes()
>>> l.count('memory') == 1
True
Definition at line 9058 of file z3py.py.
Referenced by describe_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 9310 of file z3py.py.
Referenced by BitVecs().
| def z3py.PropagateFunction | ( | name, | |
| sig | |||
| ) |
Create a function that gets tracked by user propagator. Every term headed by this function symbol is tracked. If a term is fixed and the fixed callback is registered a callback is invoked that the term headed by this function is fixed.
Definition at line 11989 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 9497 of file z3py.py.
Referenced by Default(), Map(), 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 3395 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), and RatNumRef.numerator().
| 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 11749 of file z3py.py.
| def z3py.RatVal | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. Note: Division by zero (b == 0) is allowed in Z3 symbolic expressions. Z3 can reason about such expressions symbolically. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 3375 of file z3py.py.
Referenced by Q().
| 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 11593 of file z3py.py.
Referenced by InRe(), Intersect(), Loop(), Option(), Plus(), 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 3461 of file z3py.py.
Referenced by ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_is_int(), is_rational_value(), ArithSortRef.is_real(), ArithRef.is_real(), is_real(), is_to_int(), IsInt(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
| def z3py.Reals | ( | names, | |
ctx = None |
|||
| ) |
| 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 3315 of file z3py.py.
Referenced by ArithSortRef.cast(), FreshReal(), is_arith_sort(), Real(), RealVar(), 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 3356 of file z3py.py.
Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), deserialize(), fpRealToFP(), fpToFP(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), and RatVal().
| def z3py.RealVar | ( | idx | ) |
| def z3py.RealVector | ( | prefix, | |
| sz, | |||
ctx = None |
|||
| ) |
| 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 984 of file z3py.py.
| def z3py.RecFunction | ( | name, | |
| sig | |||
| ) |
Create a new Z3 recursive with the given sorts.
Definition at line 966 of file z3py.py.
| 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 8822 of file z3py.py.
| 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 4611 of file z3py.py.
| 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 11478 of file z3py.py.
| def z3py.reset_params | ( | None | ) |
| def z3py.ReSort | ( | s | ) |
Definition at line 11612 of file z3py.py.
Referenced by Empty(), and Full().
| def z3py.RNA | ( | ctx = None | ) |
Definition at line 10084 of file z3py.py.
Referenced by get_default_rounding_mode().
| def z3py.RNE | ( | ctx = None | ) |
Definition at line 10074 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 4521 of file z3py.py.
| 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 4537 of file z3py.py.
| def z3py.RoundNearestTiesToAway | ( | ctx = None | ) |
Definition at line 10079 of file z3py.py.
| def z3py.RoundNearestTiesToEven | ( | ctx = None | ) |
Definition at line 10069 of file z3py.py.
| def z3py.RoundTowardNegative | ( | ctx = None | ) |
Definition at line 10099 of file z3py.py.
| def z3py.RoundTowardPositive | ( | ctx = None | ) |
Definition at line 10089 of file z3py.py.
| def z3py.RoundTowardZero | ( | ctx = None | ) |
Definition at line 10109 of file z3py.py.
| def z3py.RTN | ( | ctx = None | ) |
Definition at line 10104 of file z3py.py.
Referenced by get_default_rounding_mode().
| def z3py.RTP | ( | ctx = None | ) |
Definition at line 10094 of file z3py.py.
Referenced by get_default_rounding_mode().
| def z3py.RTZ | ( | ctx = None | ) |
Definition at line 10114 of file z3py.py.
Referenced by fpAdd(), fpToSBV(), fpToUBV(), and get_default_rounding_mode().
| def z3py.Select | ( | a, | |
| args | |||
| ) |
| def z3py.SeqFoldLeft | ( | f, | |
| a, | |||
| s | |||
| ) |
| def z3py.SeqFoldLeftI | ( | f, | |
| i, | |||
| a, | |||
| s | |||
| ) |
Definition at line 11551 of file z3py.py.
| def z3py.SeqMap | ( | f, | |
| s | |||
| ) |
| def z3py.SeqMapI | ( | f, | |
| i, | |||
| s | |||
| ) |
| 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 11178 of file z3py.py.
Referenced by Empty(), Full(), and SeqSortRef.is_string().
| 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 298 of file z3py.py.
Referenced by set_option().
| 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 5149 of file z3py.py.
| def z3py.SetComplement | ( | s | ) |
The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)
Definition at line 5171 of file z3py.py.
| 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 5160 of file z3py.py.
| 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 5181 of file z3py.py.
| 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 5136 of file z3py.py.
| def z3py.SetSort | ( | s | ) |
Sets.
Create a set sort over element sort s
Definition at line 5100 of file z3py.py.
Referenced by Ext(), IsMember(), IsSubset(), 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 5123 of file z3py.py.
| 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 4553 of file z3py.py.
| 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 7747 of file z3py.py.
Referenced by Solver.reason_unknown(), 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 9174 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(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), IndexOf(), InRe(), is_algebraic_value(), K(), Length(), Loop(), LShR(), Not(), Option(), Plus(), PrefixOf(), Q(), Range(), RatVal(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), Star(), StrToInt(), SubSeq(), SubString(), SuffixOf(), Union(), Xor(), and ZeroExt().
| def z3py.simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 9204 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 9436 of file z3py.py.
Referenced by BV2Int(), and IsInt().
| 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 9466 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 7726 of file z3py.py.
| 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 3573 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().
| def z3py.SRem | ( | a, | |
| b | |||
| ) |
Create the Z3 expression signed remainder.
Use the operator % for signed modulus, and URem() for unsigned remainder.
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'
Definition at line 4468 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), 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 11719 of file z3py.py.
| def z3py.Store | ( | a, | |
| args | |||
| ) |
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 4980 of file z3py.py.
Referenced by is_array(), is_store(), SetAdd(), and SetDel().
| def z3py.StrFromCode | ( | c | ) |
Convert code to a string
Definition at line 11587 of file z3py.py.
| 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 11344 of file z3py.py.
| def z3py.Strings | ( | names, | |
ctx = None |
|||
| ) |
Return a tuple of String constants.
Definition at line 11353 of file z3py.py.
Referenced by Contains().
| def z3py.StringSort | ( | ctx = None | ) |
Create a string sort >>> s = StringSort() >>> print(s) String
Definition at line 11159 of file z3py.py.
Referenced by DisjointSum(), Empty(), Full(), SeqSortRef.is_string(), String(), TupleSort(), and DatatypeRef.update_field().
| def z3py.StringVal | ( | s, | |
ctx = None |
|||
| ) |
create a string expression
Definition at line 11337 of file z3py.py.
Referenced by deserialize(), Empty(), Extract(), is_seq(), is_string(), is_string_value(), Length(), Re(), SubSeq(), and SubString().
| def z3py.StrToCode | ( | s | ) |
Convert a unit length string to integer code
Definition at line 11581 of file z3py.py.
| 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 11558 of file z3py.py.
| def z3py.SubSeq | ( | s, | |
| offset, | |||
| length | |||
| ) |
Extract substring or subsequence starting at offset.
This is a convenience function that redirects to Extract(s, offset, length).
>>> s = StringVal("hello world")
>>> SubSeq(s, 0, 5) # Extract "hello"
str.substr("hello world", 0, 5)
>>> simplify(SubSeq(StringVal("testing"), 2, 4))
"stin"
Definition at line 11375 of file z3py.py.
| 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 9209 of file z3py.py.
| def z3py.substitute_funs | ( | t, | |
| m | |||
| ) |
Apply substitution m on t, m is a list of pairs of a function and expression (from, to) Every occurrence in to of the function from is replaced with the expression to. The expression to can have free variables, that refer to the arguments of from. For examples, see
Definition at line 9262 of file z3py.py.
| 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 9242 of file z3py.py.
| def z3py.SubString | ( | s, | |
| offset, | |||
| length | |||
| ) |
Extract substring or subsequence starting at offset.
This is a convenience function that redirects to Extract(s, offset, length).
>>> s = StringVal("hello world")
>>> SubString(s, 6, 5) # Extract "world"
str.substr("hello world", 6, 5)
>>> simplify(SubString(StringVal("hello"), 1, 3))
"ell"
Definition at line 11361 of file z3py.py.
| 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 11444 of file z3py.py.
| 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 9284 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().
| def z3py.tactic_description | ( | name, | |
ctx = None |
|||
| ) |
Return a short description for the tactic named `name`.
>>> d = tactic_description('simplify')
Definition at line 8863 of file z3py.py.
Referenced by describe_tactics().
| def z3py.tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3.
>>> l = tactics()
>>> l.count('simplify') == 1
True
Definition at line 8852 of file z3py.py.
Referenced by describe_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 8720 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.convert_model(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().
| def z3py.to_Ast | ( | ptr | ) |
| def z3py.to_AstVectorObj | ( | ptr | ) |
| def z3py.to_symbol | ( | s, | |
ctx = None |
|||
| ) |
Convert an integer or string into a Z3 symbol.
Definition at line 132 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DatatypeSort(), DeclareSort(), DeclareTypeVar(), EnumSort(), FiniteDomainSort(), FP(), Function(), Int(), PropagateFunction(), prove(), Real(), RecFunction(), 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 3538 of file z3py.py.
Referenced by is_to_int().
| 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 3518 of file z3py.py.
Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().
| 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 11796 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 8843 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 5592 of file z3py.py.
| 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 4426 of file z3py.py.
Referenced by BitVecRef.__div__(), and BitVecRef.__rdiv__().
| 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 4390 of file z3py.py.
Referenced by BitVecRef.__ge__().
| 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 4408 of file z3py.py.
Referenced by BitVecRef.__gt__().
| 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 4354 of file z3py.py.
Referenced by BitVecRef.__le__().
| 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 4372 of file z3py.py.
Referenced by BitVecRef.__lt__().
| 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 11646 of file z3py.py.
Referenced by InRe().
| def z3py.Unit | ( | a | ) |
| def z3py.Update | ( | a, | |
| args | |||
| ) |
Return a Z3 store array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved
Definition at line 4937 of file z3py.py.
Referenced by Store().
| 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 4447 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().
| def z3py.user_prop_fresh | ( | ctx, | |
| _new_ctx | |||
| ) |
Definition at line 11901 of file z3py.py.
| def z3py.Var | ( | idx | ) |
Definition at line 1575 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().
| 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 9137 of file z3py.py.
| 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 8794 of file z3py.py.
Referenced by Goal.prec().
| 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 8808 of file z3py.py.
| 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 1932 of file z3py.py.
Referenced by BoolRef.__xor__().
| def z3py.z3_debug | ( | ) |
Definition at line 70 of file z3py.py.
Referenced by Probe.__call__(), Context.__init__(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), Concat(), Const(), CreateDatatypes(), ExprRef.decl(), Default(), describe_probes(), deserialize(), Diff(), Distinct(), EnumSort(), AstRef.eq(), eq(), Ext(), Extract(), FiniteDomainVal(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshConst(), FreshFunction(), Function(), get_as_array_func(), get_map_func(), get_var_index(), If(), Intersect(), is_sort(), IsInt(), K(), ExprRef.kind(), Loop(), Map(), MultiPattern(), ExprRef.num_args(), Option(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), Plus(), PropagateFunction(), prove(), Range(), RatVal(), RecFunction(), RepeatBitVec(), Select(), set_param(), SignExt(), simplify(), solve_using(), Star(), substitute(), substitute_funs(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Union(), ExprRef.update(), Update(), and Var().
| 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 4583 of file z3py.py.
| _dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN |
| tuple _on_clause_eh = Z3_on_clause_eh(on_clause_eh) |
| tuple _ROUNDING_MODES |
| tuple _user_prop_binding = Z3_on_binding_eh(user_prop_binding) |
| tuple _user_prop_created = Z3_created_eh(user_prop_created) |
| tuple _user_prop_decide = Z3_decide_eh(user_prop_decide) |
| tuple _user_prop_diseq = Z3_eq_eh(user_prop_diseq) |
| tuple _user_prop_eq = Z3_eq_eh(user_prop_eq) |
| tuple _user_prop_final = Z3_final_eh(user_prop_final) |
| tuple _user_prop_fixed = Z3_fixed_eh(user_prop_fixed) |
| tuple _user_prop_fresh = Z3_fresh_eh(user_prop_fresh) |
| tuple _user_prop_pop = Z3_pop_eh(user_prop_pop) |
| tuple _user_prop_push = Z3_push_eh(user_prop_push) |
| tuple sat = CheckSatResult(Z3_L_TRUE) |
| tuple unknown = CheckSatResult(Z3_L_UNDEF) |
| tuple unsat = CheckSatResult(Z3_L_FALSE) |
1.8.10