|
Z3
|
|
|
Z3
|
|
Functions | |
| def | z3_debug () |
| def | enable_trace (msg) |
| def | disable_trace (msg) |
| def | get_version_string () |
| def | get_version () |
| def | get_full_version () |
| def | open_log (fname) |
| def | append_log (s) |
| def | to_symbol (s, ctx=None) |
| def | z3_error_handler (c, e) |
| def | main_ctx () |
| def | get_ctx (ctx) |
| def | set_param (*args, **kws) |
| def | reset_params () |
| def | set_option (*args, **kws) |
| def | get_param (name) |
| def | is_ast (a) |
| def | eq (a, b) |
| def | is_sort (s) |
| def | DeclareSort (name, ctx=None) |
| def | is_func_decl (a) |
| def | Function (name, *sig) |
| def | FreshFunction (*sig) |
| def | RecFunction (name, *sig) |
| def | RecAddDefinition (f, args, body) |
| def | 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 (a, b, c, ctx=None) |
| def | Distinct (*args) |
| def | Const (name, sort) |
| def | Consts (names, sort) |
| def | FreshConst (sort, prefix="c") |
| def | Var (idx, s) |
| def | RealVar (idx, ctx=None) |
| def | RealVarVector (n, ctx=None) |
| def | is_bool (a) |
| def | is_true (a) |
| def | is_false (a) |
| def | is_and (a) |
| def | is_or (a) |
| def | is_implies (a) |
| def | is_not (a) |
| def | is_eq (a) |
| def | is_distinct (a) |
| def | BoolSort (ctx=None) |
| def | BoolVal (val, ctx=None) |
| def | Bool (name, ctx=None) |
| def | Bools (names, ctx=None) |
| def | BoolVector (prefix, sz, ctx=None) |
| def | FreshBool (prefix="b", ctx=None) |
| def | Implies (a, b, ctx=None) |
| def | Xor (a, b, ctx=None) |
| def | Not (a, ctx=None) |
| def | mk_not (a) |
| def | And (*args) |
| def | Or (*args) |
| def | is_pattern (a) |
| def | MultiPattern (*args) |
| def | is_quantifier (a) |
| def | ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
| def | Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
| def | Lambda (vs, body) |
| def | is_arith_sort (s) |
| def | is_arith (a) |
| def | is_int (a) |
| def | is_real (a) |
| def | is_int_value (a) |
| def | is_rational_value (a) |
| def | is_algebraic_value (a) |
| def | is_add (a) |
| def | is_mul (a) |
| def | is_sub (a) |
| def | is_div (a) |
| def | is_idiv (a) |
| def | is_mod (a) |
| def | is_le (a) |
| def | is_lt (a) |
| def | is_ge (a) |
| def | is_gt (a) |
| def | is_is_int (a) |
| def | is_to_real (a) |
| def | is_to_int (a) |
| def | IntSort (ctx=None) |
| def | RealSort (ctx=None) |
| def | IntVal (val, ctx=None) |
| def | RealVal (val, ctx=None) |
| def | RatVal (a, b, ctx=None) |
| def | Q (a, b, ctx=None) |
| def | Int (name, ctx=None) |
| def | Ints (names, ctx=None) |
| def | IntVector (prefix, sz, ctx=None) |
| def | FreshInt (prefix="x", ctx=None) |
| def | Real (name, ctx=None) |
| def | Reals (names, ctx=None) |
| def | RealVector (prefix, sz, ctx=None) |
| def | FreshReal (prefix="b", ctx=None) |
| def | ToReal (a) |
| def | ToInt (a) |
| def | IsInt (a) |
| def | Sqrt (a, ctx=None) |
| def | Cbrt (a, ctx=None) |
| def | is_bv_sort (s) |
| def | is_bv (a) |
| def | is_bv_value (a) |
| def | BV2Int (a, is_signed=False) |
| def | Int2BV (a, num_bits) |
| def | BitVecSort (sz, ctx=None) |
| def | BitVecVal (val, bv, ctx=None) |
| def | BitVec (name, bv, ctx=None) |
| def | BitVecs (names, bv, ctx=None) |
| def | Concat (*args) |
| def | Extract (high, low, a) |
| def | ULE (a, b) |
| def | ULT (a, b) |
| def | UGE (a, b) |
| def | UGT (a, b) |
| def | UDiv (a, b) |
| def | URem (a, b) |
| def | SRem (a, b) |
| def | LShR (a, b) |
| def | RotateLeft (a, b) |
| def | RotateRight (a, b) |
| def | SignExt (n, a) |
| def | ZeroExt (n, a) |
| def | RepeatBitVec (n, a) |
| def | BVRedAnd (a) |
| def | BVRedOr (a) |
| def | BVAddNoOverflow (a, b, signed) |
| def | BVAddNoUnderflow (a, b) |
| def | BVSubNoOverflow (a, b) |
| def | BVSubNoUnderflow (a, b, signed) |
| def | BVSDivNoOverflow (a, b) |
| def | BVSNegNoOverflow (a) |
| def | BVMulNoOverflow (a, b, signed) |
| def | BVMulNoUnderflow (a, b) |
| def | is_array_sort (a) |
| def | is_array (a) |
| def | is_const_array (a) |
| def | is_K (a) |
| def | is_map (a) |
| def | is_default (a) |
| def | get_map_func (a) |
| def | ArraySort (*sig) |
| def | Array (name, *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 | SetHasSize (a, k) |
| def | is_select (a) |
| def | is_store (a) |
| def | SetSort (s) |
| Sets. More... | |
| def | EmptySet (s) |
| def | FullSet (s) |
| def | SetUnion (*args) |
| def | SetIntersect (*args) |
| def | SetAdd (s, e) |
| def | SetDel (s, e) |
| def | SetComplement (s) |
| def | SetDifference (a, b) |
| def | IsMember (e, s) |
| def | IsSubset (a, b) |
| def | CreateDatatypes (*ds) |
| def | DatatypeSort (name, ctx=None) |
| def | TupleSort (name, sorts, ctx=None) |
| def | DisjointSum (name, sorts, ctx=None) |
| def | EnumSort (name, values, ctx=None) |
| def | args2params (arguments, keywords, ctx=None) |
| def | Model (ctx=None) |
| def | is_as_array (n) |
| def | get_as_array_func (n) |
| def | SolverFor (logic, ctx=None, logFile=None) |
| def | SimpleSolver (ctx=None, logFile=None) |
| def | FiniteDomainSort (name, sz, ctx=None) |
| def | is_finite_domain_sort (s) |
| def | is_finite_domain (a) |
| def | FiniteDomainVal (val, sort, ctx=None) |
| def | is_finite_domain_value (a) |
| def | AndThen (*ts, **ks) |
| def | Then (*ts, **ks) |
| def | OrElse (*ts, **ks) |
| def | ParOr (*ts, **ks) |
| def | ParThen (t1, t2, ctx=None) |
| def | ParAndThen (t1, t2, ctx=None) |
| def | With (t, *args, **keys) |
| def | WithParams (t, p) |
| def | Repeat (t, max=4294967295, ctx=None) |
| def | TryFor (t, ms, ctx=None) |
| def | tactics (ctx=None) |
| def | tactic_description (name, ctx=None) |
| def | describe_tactics () |
| def | is_probe (p) |
| def | probes (ctx=None) |
| def | probe_description (name, ctx=None) |
| def | describe_probes () |
| def | FailIf (p, ctx=None) |
| def | When (p, t, ctx=None) |
| def | Cond (p, t1, t2, ctx=None) |
| def | simplify (a, *arguments, **keywords) |
| Utils. More... | |
| def | help_simplify () |
| def | simplify_param_descrs () |
| def | substitute (t, *m) |
| def | substitute_vars (t, *m) |
| def | 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 (args, k, ctx=None) |
| def | solve (*args, **keywords) |
| def | solve_using (s, *args, **keywords) |
| def | prove (claim, show=False, **keywords) |
| def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
| def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
| def | get_default_rounding_mode (ctx=None) |
| def | set_default_rounding_mode (rm, ctx=None) |
| def | get_default_fp_sort (ctx=None) |
| def | set_default_fp_sort (ebits, sbits, ctx=None) |
| def | Float16 (ctx=None) |
| def | FloatHalf (ctx=None) |
| def | Float32 (ctx=None) |
| def | FloatSingle (ctx=None) |
| def | Float64 (ctx=None) |
| def | FloatDouble (ctx=None) |
| def | Float128 (ctx=None) |
| def | FloatQuadruple (ctx=None) |
| def | is_fp_sort (s) |
| def | is_fprm_sort (s) |
| def | RoundNearestTiesToEven (ctx=None) |
| def | RNE (ctx=None) |
| def | RoundNearestTiesToAway (ctx=None) |
| def | RNA (ctx=None) |
| def | RoundTowardPositive (ctx=None) |
| def | RTP (ctx=None) |
| def | RoundTowardNegative (ctx=None) |
| def | RTN (ctx=None) |
| def | RoundTowardZero (ctx=None) |
| def | RTZ (ctx=None) |
| def | is_fprm (a) |
| def | is_fprm_value (a) |
| def | is_fp (a) |
| def | is_fp_value (a) |
| def | FPSort (ebits, sbits, ctx=None) |
| def | fpNaN (s) |
| def | fpPlusInfinity (s) |
| def | fpMinusInfinity (s) |
| def | fpInfinity (s, negative) |
| def | fpPlusZero (s) |
| def | fpMinusZero (s) |
| def | fpZero (s, negative) |
| def | FPVal (sig, exp=None, fps=None, ctx=None) |
| def | FP (name, fpsort, ctx=None) |
| def | FPs (names, fpsort, ctx=None) |
| def | fpAbs (a, ctx=None) |
| def | fpNeg (a, ctx=None) |
| def | fpAdd (rm, a, b, ctx=None) |
| def | fpSub (rm, a, b, ctx=None) |
| def | fpMul (rm, a, b, ctx=None) |
| def | fpDiv (rm, a, b, ctx=None) |
| def | fpRem (a, b, ctx=None) |
| def | fpMin (a, b, ctx=None) |
| def | fpMax (a, b, ctx=None) |
| def | fpFMA (rm, a, b, c, ctx=None) |
| def | fpSqrt (rm, a, ctx=None) |
| def | fpRoundToIntegral (rm, a, ctx=None) |
| def | fpIsNaN (a, ctx=None) |
| def | fpIsInf (a, ctx=None) |
| def | fpIsZero (a, ctx=None) |
| def | fpIsNormal (a, ctx=None) |
| def | fpIsSubnormal (a, ctx=None) |
| def | fpIsNegative (a, ctx=None) |
| def | fpIsPositive (a, ctx=None) |
| def | fpLT (a, b, ctx=None) |
| def | fpLEQ (a, b, ctx=None) |
| def | fpGT (a, b, ctx=None) |
| def | fpGEQ (a, b, ctx=None) |
| def | fpEQ (a, b, ctx=None) |
| def | fpNEQ (a, b, ctx=None) |
| def | fpFP (sgn, exp, sig, ctx=None) |
| def | fpToFP (a1, a2=None, a3=None, ctx=None) |
| def | fpBVToFP (v, sort, ctx=None) |
| def | fpFPToFP (rm, v, sort, ctx=None) |
| def | fpRealToFP (rm, v, sort, ctx=None) |
| def | fpSignedToFP (rm, v, sort, ctx=None) |
| def | fpUnsignedToFP (rm, v, sort, ctx=None) |
| def | fpToFPUnsigned (rm, x, s, ctx=None) |
| def | fpToSBV (rm, x, s, ctx=None) |
| def | fpToUBV (rm, x, s, ctx=None) |
| def | fpToReal (x, ctx=None) |
| def | fpToIEEEBV (x, ctx=None) |
| def | StringSort (ctx=None) |
| def | CharSort (ctx=None) |
| def | SeqSort (s) |
| def | CharVal (ch, ctx=None) |
| def | CharFromBv (ch, ctx=None) |
| def | CharToBv (ch, ctx=None) |
| def | CharToInt (ch, ctx=None) |
| def | CharIsDigit (ch, ctx=None) |
| def | is_seq (a) |
| def | is_string (a) |
| def | is_string_value (a) |
| def | StringVal (s, ctx=None) |
| def | String (name, ctx=None) |
| def | Strings (names, ctx=None) |
| def | SubString (s, offset, length) |
| def | SubSeq (s, offset, length) |
| def | Empty (s) |
| def | Full (s) |
| def | Unit (a) |
| def | PrefixOf (a, b) |
| def | SuffixOf (a, b) |
| def | Contains (a, b) |
| def | Replace (s, src, dst) |
| def | IndexOf (s, substr, offset=None) |
| def | LastIndexOf (s, substr) |
| def | Length (s) |
| def | StrToInt (s) |
| def | IntToStr (s) |
| def | StrToCode (s) |
| def | StrFromCode (c) |
| def | Re (s, ctx=None) |
| def | ReSort (s) |
| def | is_re (s) |
| def | InRe (s, re) |
| def | Union (*args) |
| def | Intersect (*args) |
| def | Plus (re) |
| def | Option (re) |
| def | Complement (re) |
| def | Star (re) |
| def | Loop (re, lo, hi=0) |
| def | Range (lo, hi, ctx=None) |
| def | Diff (a, b, ctx=None) |
| def | AllChar (regex_sort, ctx=None) |
| def | PartialOrder (a, index) |
| def | LinearOrder (a, index) |
| def | TreeOrder (a, index) |
| def | PiecewiseLinearOrder (a, index) |
| def | TransitiveClosure (f) |
| def | ensure_prop_closures () |
| def | user_prop_push (ctx, cb) |
| def | user_prop_pop (ctx, cb, num_scopes) |
| def | to_ContextObj (ptr) |
| def | user_prop_fresh (ctx, _new_ctx) |
| def | to_Ast (ptr) |
| 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_ref, phase_ref) |
| def | PropagateFunction (name, *sig) |
Variables | |
| Z3_DEBUG = __debug__ | |
| sat = CheckSatResult(Z3_L_TRUE) | |
| unsat = CheckSatResult(Z3_L_FALSE) | |
| unknown = CheckSatResult(Z3_L_UNDEF) | |
| def z3py.Abs | ( | arg | ) |
| def z3py.AllChar | ( | regex_sort, | |
ctx = None |
|||
| ) |
| 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 1840 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Goal.as_expr(), 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 8272 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 5457 of file z3py.py.
Referenced by Tactic.apply(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), and With().
| def z3py.Array | ( | name, | |
| * | sorts | ||
| ) |
| 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 4691 of file z3py.py.
Referenced by Array(), Context.MkArraySort(), and SetSort().
| def z3py.AtLeast | ( | * | args | ) |
| def z3py.AtMost | ( | * | args | ) |
| def z3py.BitVec | ( | name, | |
| bv, | |||
ctx = None |
|||
| ) |
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.
>>> x = BitVec('x', 16)
>>> is_bv(x)
True
>>> x.size()
16
>>> x.sort()
BitVec(16)
>>> word = BitVecSort(16)
>>> x2 = BitVec('x', word)
>>> eq(x, x2)
True
Definition at line 4028 of file z3py.py.
Referenced by BitVecs().
| def z3py.BitVecs | ( | names, | |
| bv, | |||
ctx = None |
|||
| ) |
| 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 3996 of file z3py.py.
Referenced by BitVec(), BitVecVal(), Context.mkBitVecSort(), and Context.MkBitVecSort().
| 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
| 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 1719 of file z3py.py.
Referenced by Solver.assert_and_track(), Optimize.assert_and_track(), Bools(), and BoolVector().
| def z3py.Bools | ( | names, | |
ctx = None |
|||
| ) |
| 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 1682 of file z3py.py.
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), Solver.check(), FreshBool(), Context.getBoolSort(), If(), Implies(), Context.mkBoolSort(), Not(), SetSort(), QuantifierRef.sort(), and Xor().
| def z3py.BoolVal | ( | val, | |
ctx = None |
|||
| ) |
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. >>> BoolVal(True) True >>> is_true(BoolVal(True)) True >>> is_true(True) False >>> is_false(BoolVal(False)) True
Definition at line 1700 of file z3py.py.
Referenced by Goal.as_expr(), ApplyResult.as_expr(), BoolSortRef.cast(), UserPropagateBase.conflict(), AlgebraicNumRef.index(), is_quantifier(), and Solver.to_smt2().
| def z3py.BoolVector | ( | prefix, | |
| sz, | |||
ctx = None |
|||
| ) |
| 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 3964 of file z3py.py.
| def z3py.BVAddNoOverflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
| def z3py.BVAddNoUnderflow | ( | a, | |
| b | |||
| ) |
| def z3py.BVMulNoOverflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
| def z3py.BVMulNoUnderflow | ( | a, | |
| b | |||
| ) |
| def z3py.BVRedAnd | ( | a | ) |
| def z3py.BVRedOr | ( | a | ) |
| def z3py.BVSDivNoOverflow | ( | a, | |
| b | |||
| ) |
| def z3py.BVSNegNoOverflow | ( | a | ) |
| def z3py.BVSubNoOverflow | ( | a, | |
| b | |||
| ) |
| def z3py.BVSubNoUnderflow | ( | a, | |
| b, | |||
| signed | |||
| ) |
| def z3py.Cbrt | ( | a, | |
ctx = None |
|||
| ) |
Return a Z3 expression which represents the cubic root of a.
>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)
| def z3py.CharSort | ( | ctx = None | ) |
Create a character sort >>> ch = CharSort() >>> print(ch) Char
Definition at line 10730 of file z3py.py.
Referenced by Context.mkCharSort().
| def z3py.CharToBv | ( | ch, | |
ctx = None |
|||
| ) |
| def z3py.CharToInt | ( | ch, | |
ctx = None |
|||
| ) |
| def z3py.CharVal | ( | ch, | |
ctx = None |
|||
| ) |
| def z3py.Complement | ( | re | ) |
| def z3py.Concat | ( | * | args | ) |
Create a Z3 bit-vector concatenation expression.
>>> v = BitVecVal(1, 4)
>>> Concat(v, v+1, v)
Concat(Concat(1, 1 + 1), 1)
>>> simplify(Concat(v, v+1, v))
289
>>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
121
Definition at line 4073 of file z3py.py.
Referenced by SeqRef.__add__(), and SeqRef.__radd__().
| 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 8729 of file z3py.py.
Referenced by If().
| def z3py.Const | ( | name, | |
| sort | |||
| ) |
| def z3py.Consts | ( | names, | |
| sort | |||
| ) |
| def z3py.Contains | ( | a, | |
| b | |||
| ) |
| 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 5149 of file z3py.py.
Referenced by Datatype.create().
| def z3py.DatatypeSort | ( | name, | |
ctx = None |
|||
| ) |
Create a reference to a sort that was declared, or will be declared, as a recursive datatype
Definition at line 5349 of file z3py.py.
Referenced by Context.MkDatatypeSort(), and Context.MkDatatypeSorts().
| def z3py.DeclareSort | ( | name, | |
ctx = None |
|||
| ) |
| def z3py.Default | ( | a | ) |
| 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.
| def z3py.Diff | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.disable_trace | ( | msg | ) |
| def z3py.DisjointSum | ( | name, | |
| sorts, | |||
ctx = None |
|||
| ) |
Create a named tagged union sort base on a set of underlying sorts
Example:
>>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
| def z3py.Distinct | ( | * | args | ) |
Create a Z3 distinct expression.
>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))
Definition at line 1399 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 10930 of file z3py.py.
| def z3py.EmptySet | ( | s | ) |
| def z3py.enable_trace | ( | msg | ) |
| def z3py.ensure_prop_closures | ( | ) |
| 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 5378 of file z3py.py.
Referenced by Context.MkEnumSort().
| def z3py.eq | ( | a, | |
| b | |||
| ) |
Return `True` if `a` and `b` are structurally identical AST nodes.
>>> x = Int('x')
>>> y = Int('y')
>>> eq(x, y)
False
>>> eq(x + 1, x + 1)
True
>>> eq(x + 1, 1 + x)
False
>>> eq(simplify(x + 1), simplify(1 + x))
True
Definition at line 472 of file z3py.py.
Referenced by 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 2231 of file z3py.py.
Referenced by Fixedpoint.abstract().
| def z3py.Ext | ( | a, | |
| b | |||
| ) |
| def z3py.Extract | ( | high, | |
| low, | |||
| a | |||
| ) |
Create a Z3 bit-vector extraction expression.
Extract is overloaded to also work on sequence extraction.
The functions SubString and SubSeq are redirected to Extract.
For this case, the arguments are reinterpreted as:
high - is a sequence (string)
low - is an offset
a - is the length to be extracted
>>> x = BitVec('x', 8)
>>> Extract(6, 2, x)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort()
BitVec(5)
>>> simplify(Extract(StringVal("abcd"),2,1))
"c"
Definition at line 4119 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 8687 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 7691 of file z3py.py.
Referenced by Context.MkFiniteDomainSort().
| def z3py.FiniteDomainVal | ( | val, | |
| sort, | |||
ctx = None |
|||
| ) |
| def z3py.Float128 | ( | ctx = None | ) |
| def z3py.Float16 | ( | ctx = None | ) |
| def z3py.Float32 | ( | ctx = None | ) |
| def z3py.Float64 | ( | ctx = None | ) |
| def z3py.FloatDouble | ( | ctx = None | ) |
| def z3py.FloatHalf | ( | ctx = None | ) |
| def z3py.FloatQuadruple | ( | ctx = None | ) |
| def z3py.FloatSingle | ( | ctx = None | ) |
| def z3py.ForAll | ( | vs, | |
| body, | |||
weight = 1, |
|||
qid = "", |
|||
skid = "", |
|||
patterns = [], |
|||
no_patterns = [] |
|||
| ) |
Create a Z3 forall formula.
The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> ForAll([x, y], f(x, y) >= x)
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, weight=10)
ForAll([x, y], f(x, y) >= x)
Definition at line 2213 of file z3py.py.
Referenced by Fixedpoint.abstract().
| 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 10047 of file z3py.py.
Referenced by FPs().
| 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 10090 of file z3py.py.
| def z3py.fpAdd | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point addition expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpAdd(rm, x, y)
fpAdd(RNE(), x, y)
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
x + y
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)
Definition at line 10181 of file z3py.py.
Referenced by FPRef.__add__(), and FPRef.__radd__().
| def z3py.fpBVToFP | ( | v, | |
| sort, | |||
ctx = None |
|||
| ) |
| def z3py.fpDiv | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point division expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpDiv(rm, x, y)
fpDiv(RNE(), x, y)
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)
Definition at line 10228 of file z3py.py.
Referenced by FPRef.__div__(), and FPRef.__rdiv__().
| def z3py.fpEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpFMA | ( | rm, | |
| a, | |||
| b, | |||
| c, | |||
ctx = None |
|||
| ) |
| def z3py.fpFP | ( | sgn, | |
| exp, | |||
| sig, | |||
ctx = None |
|||
| ) |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. >>> s = FPSort(8, 24) >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) >>> print(x) fpFP(1, 127, 4194304) >>> xv = FPVal(-1.5, s) >>> print(xv) -1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() sat >>> xv = FPVal(+1.5, s) >>> print(xv) 1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() unsat
| def z3py.fpFPToFP | ( | rm, | |
| v, | |||
| sort, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision. >>> x_sgl = FPVal(1.0, Float32()) >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) >>> x_dbl fpToFP(RNE(), 1) >>> simplify(x_dbl) 1 >>> x_dbl.sort() FPSort(11, 53)
Definition at line 10520 of file z3py.py.
| def z3py.fpGEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create the Z3 floating-point expression `other >= self`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGEQ(x, y)
x >= y
>>> (x >= y).sexpr()
'(fp.geq x y)'
Definition at line 10399 of file z3py.py.
Referenced by FPRef.__ge__().
| def z3py.fpGT | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create the Z3 floating-point expression `other > self`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpGT(x, y)
x > y
>>> (x > y).sexpr()
'(fp.gt x y)'
Definition at line 10387 of file z3py.py.
Referenced by FPRef.__gt__().
| def z3py.fpInfinity | ( | s, | |
| negative | |||
| ) |
| def z3py.fpIsInf | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsNaN | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsNegative | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsNormal | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsPositive | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsSubnormal | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpIsZero | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.fpLEQ | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create the Z3 floating-point expression `other <= self`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLEQ(x, y)
x <= y
>>> (x <= y).sexpr()
'(fp.leq x y)'
Definition at line 10375 of file z3py.py.
Referenced by FPRef.__le__().
| def z3py.fpLT | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create the Z3 floating-point expression `other < self`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpLT(x, y)
x < y
>>> (x < y).sexpr()
'(fp.lt x y)'
Definition at line 10363 of file z3py.py.
Referenced by FPRef.__lt__().
| def z3py.fpMax | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpMin | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
| def z3py.fpMinusInfinity | ( | s | ) |
| def z3py.fpMinusZero | ( | s | ) |
| def z3py.fpMul | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point multiplication expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMul(rm, x, y)
fpMul(RNE(), x, y)
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)
Definition at line 10213 of file z3py.py.
Referenced by FPRef.__mul__(), and FPRef.__rmul__().
| def z3py.fpNaN | ( | s | ) |
| 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 10113 of file z3py.py.
Referenced by FPRef.__neg__().
| 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 9952 of file z3py.py.
Referenced by FPVal().
| def z3py.fpPlusZero | ( | s | ) |
| def z3py.fpRealToFP | ( | rm, | |
| v, | |||
| sort, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point conversion expression that represents the conversion from a real term to a floating-point term. >>> x_r = RealVal(1.5) >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) >>> x_fp fpToFP(RNE(), 3/2) >>> simplify(x_fp) 1.5
Definition at line 10540 of file z3py.py.
| def z3py.fpRem | ( | a, | |
| b, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point remainder expression.
>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpRem(x, y)
fpRem(x, y)
>>> fpRem(x, y).sort()
FPSort(8, 24)
Definition at line 10243 of file z3py.py.
Referenced by FPRef.__mod__(), and FPRef.__rmod__().
| def z3py.fpRoundToIntegral | ( | rm, | |
| a, | |||
ctx = None |
|||
| ) |
| def z3py.FPs | ( | names, | |
| fpsort, | |||
ctx = None |
|||
| ) |
| 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 10558 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 9876 of file z3py.py.
Referenced by get_default_fp_sort(), Context.mkFPSort(), Context.mkFPSort128(), Context.MkFPSort128(), Context.mkFPSort16(), Context.MkFPSort16(), Context.mkFPSort32(), Context.MkFPSort32(), Context.mkFPSort64(), Context.MkFPSort64(), Context.mkFPSortDouble(), Context.MkFPSortDouble(), Context.mkFPSortHalf(), Context.MkFPSortHalf(), Context.mkFPSortQuadruple(), Context.MkFPSortQuadruple(), Context.mkFPSortSingle(), and Context.MkFPSortSingle().
| def z3py.fpSqrt | ( | rm, | |
| a, | |||
ctx = None |
|||
| ) |
| def z3py.fpSub | ( | rm, | |
| a, | |||
| b, | |||
ctx = None |
|||
| ) |
Create a Z3 floating-point subtraction expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpSub(rm, x, y)
fpSub(RNE(), x, y)
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)
Definition at line 10198 of file z3py.py.
Referenced by FPRef.__rsub__(), and FPRef.__sub__().
| 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)
| 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 10594 of file z3py.py.
| 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 10668 of file z3py.py.
| def z3py.fpToReal | ( | x, | |
ctx = None |
|||
| ) |
| 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 10604 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 10626 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 10576 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 10001 of file z3py.py.
Referenced by set_default_fp_sort().
| def z3py.fpZero | ( | s, | |
| negative | |||
| ) |
| def z3py.FreshBool | ( | prefix = "b", |
|
ctx = None |
|||
| ) |
| def z3py.FreshConst | ( | sort, | |
prefix = "c" |
|||
| ) |
| def z3py.FreshFunction | ( | * | sig | ) |
| def z3py.FreshInt | ( | prefix = "x", |
|
ctx = None |
|||
| ) |
| def z3py.FreshReal | ( | prefix = "b", |
|
ctx = None |
|||
| ) |
| def z3py.Full | ( | s | ) |
| def z3py.FullSet | ( | s | ) |
| def z3py.Function | ( | name, | |
| * | sig | ||
| ) |
| def z3py.get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
Definition at line 6690 of file z3py.py.
Referenced by ModelRef.get_interp().
| def z3py.get_ctx | ( | ctx | ) |
| def z3py.get_default_fp_sort | ( | ctx = None | ) |
| def z3py.get_default_rounding_mode | ( | ctx = None | ) |
Retrieves the global default rounding mode.
Definition at line 9265 of file z3py.py.
Referenced by set_default_fp_sort().
| def z3py.get_full_version | ( | ) |
| def z3py.get_map_func | ( | a | ) |
Return the function declaration associated with a Z3 map array expression.
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a = Map(f, b)
>>> eq(f, get_map_func(a))
True
>>> get_map_func(a)
f
>>> get_map_func(a)(0)
f(0)
Definition at line 4667 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 1330 of file z3py.py.
| 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 1376 of file z3py.py.
Referenced by BoolRef.__mul__(), ArithRef.__mul__(), and Abs().
| 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 1776 of file z3py.py.
Referenced by Fixedpoint.add_rule(), 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 11034 of file z3py.py.
| def z3py.InRe | ( | s, | |
| re | |||
| ) |
| 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 3239 of file z3py.py.
Referenced by Ints(), and IntVector().
| def z3py.Int2BV | ( | a, | |
| num_bits | |||
| ) |
| def z3py.Intersect | ( | * | args | ) |
| def z3py.Ints | ( | names, | |
ctx = None |
|||
| ) |
| 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 3129 of file z3py.py.
Referenced by FreshInt(), Context.getIntSort(), Int(), IntVal(), and Context.mkIntSort().
| def z3py.IntToStr | ( | s | ) |
| 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 3179 of file z3py.py.
Referenced by SeqRef.__getitem__(), SeqRef.at(), AlgebraicNumRef.index(), and IndexOf().
| def z3py.IntVector | ( | prefix, | |
| sz, | |||
ctx = None |
|||
| ) |
| def z3py.is_add | ( | a | ) |
Return `True` if `a` is an expression of the form b + c.
>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False
| def z3py.is_algebraic_value | ( | a | ) |
| def z3py.is_and | ( | a | ) |
Return `True` if `a` is a Z3 and expression.
>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False
| def z3py.is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application.
Note that, constants are function applications with 0 arguments.
>>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')
>>> is_app(ForAll(x, x >= 0))
False
Definition at line 1260 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
| def z3py.is_app_of | ( | a, | |
| k | |||
| ) |
Return `True` if `a` is an application of the given kind `k`.
>>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Z3_OP_ADD)
True
>>> is_app_of(n, Z3_OP_MUL)
False
Definition at line 1363 of file z3py.py.
Referenced by is_add(), is_and(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
| def z3py.is_arith | ( | a | ) |
Return `True` if `a` is an arithmetical expression.
>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True
Definition at line 2656 of file z3py.py.
Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().
| def z3py.is_arith_sort | ( | s | ) |
Return `True` if s is an arithmetical sort (type).
>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True
Definition at line 2355 of file z3py.py.
Referenced by ArithSortRef.subsort().
| def z3py.is_array | ( | a | ) |
| def z3py.is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 6685 of file z3py.py.
Referenced by get_as_array_func(), and ModelRef.get_interp().
| def z3py.is_ast | ( | a | ) |
Return `True` if `a` is an AST node.
>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False
Definition at line 451 of file z3py.py.
Referenced by AstRef.eq(), eq(), and ReSort().
| def z3py.is_bool | ( | a | ) |
Return `True` if `a` is a Z3 Boolean expression.
>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True
Definition at line 1562 of file z3py.py.
Referenced by is_quantifier(), and prove().
| def z3py.is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression.
>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False
Definition at line 3935 of file z3py.py.
Referenced by BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
| def z3py.is_bv_sort | ( | s | ) |
Return True if `s` is a Z3 bit-vector sort. >>> is_bv_sort(BitVecSort(32)) True >>> is_bv_sort(IntSort()) False
Definition at line 3467 of file z3py.py.
Referenced by BitVecVal(), fpToSBV(), fpToUBV(), and BitVecSortRef.subsort().
| 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 1286 of file z3py.py.
Referenced by ModelRef.__getitem__(), Solver.assert_and_track(), Optimize.assert_and_track(), ModelRef.get_interp(), is_quantifier(), and prove().
| def z3py.is_const_array | ( | a | ) |
| def z3py.is_default | ( | a | ) |
| def z3py.is_distinct | ( | a | ) |
| def z3py.is_div | ( | a | ) |
| def z3py.is_eq | ( | a | ) |
Return `True` if `a` is a Z3 equality expression.
>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
Definition at line 1660 of file z3py.py.
Referenced by AstRef.__bool__().
| def z3py.is_expr | ( | a | ) |
Return `True` if `a` is a Z3 expression.
>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True
>>> is_expr(FPVal(1.0))
True
Definition at line 1237 of file z3py.py.
Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), CharFromBv(), CharIsDigit(), Concat(), deserialize(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), StrFromCode(), StrToCode(), substitute(), substitute_funs(), substitute_vars(), and ModelRef.update_value().
| def z3py.is_false | ( | a | ) |
Return `True` if `a` is the Z3 false expression.
>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True
Definition at line 1598 of file z3py.py.
Referenced by AstRef.__bool__().
| 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 7722 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 7699 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 9847 of file z3py.py.
Referenced by fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp_value(), and set_default_fp_sort().
| def z3py.is_fp_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point sort. >>> is_fp_sort(FPSort(8, 24)) True >>> is_fp_sort(IntSort()) False
Definition at line 9431 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 9691 of file z3py.py.
Referenced by fpFPToFP(), fpNeg(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), and is_fprm_value().
| def z3py.is_fprm_sort | ( | s | ) |
| def z3py.is_fprm_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 9704 of file z3py.py.
Referenced by set_default_rounding_mode().
| def z3py.is_func_decl | ( | a | ) |
Return `True` if `a` is a Z3 function declaration.
>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False
Definition at line 850 of file z3py.py.
Referenced by Map(), prove(), substitute_funs(), and ModelRef.update_value().
| def z3py.is_ge | ( | a | ) |
Return `True` if `a` is an expression of the form b >= c.
>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False
| def z3py.is_gt | ( | a | ) |
Return `True` if `a` is an expression of the form b > c.
>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False
| def z3py.is_idiv | ( | a | ) |
Return `True` if `a` is an expression of the form b div c.
>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False
| def z3py.is_implies | ( | a | ) |
| def z3py.is_int | ( | a | ) |
| 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 2723 of file z3py.py.
| def z3py.is_is_int | ( | a | ) |
Return `True` if `a` is an expression of the form IsInt(b).
>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False
| def z3py.is_K | ( | a | ) |
Return `True` if `a` is a Z3 constant array.
>>> a = K(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False
| def z3py.is_le | ( | a | ) |
Return `True` if `a` is an expression of the form b <= c.
>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False
| def z3py.is_lt | ( | a | ) |
Return `True` if `a` is an expression of the form b < c.
>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False
| def z3py.is_map | ( | a | ) |
Return `True` if `a` is a Z3 map array expression.
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False
Definition at line 4642 of file z3py.py.
Referenced by get_map_func().
| def z3py.is_mod | ( | a | ) |
Return `True` if `a` is an expression of the form b % c.
>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False
| def z3py.is_mul | ( | a | ) |
Return `True` if `a` is an expression of the form b * c.
>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False
| def z3py.is_not | ( | a | ) |
| def z3py.is_or | ( | a | ) |
Return `True` if `a` is a Z3 or expression.
>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False
| def z3py.is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
>>> 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 1924 of file z3py.py.
Referenced by is_quantifier(), and 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 2747 of file z3py.py.
| 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 2696 of file z3py.py.
Referenced by fpRealToFP(), and fpToFP().
| def z3py.is_select | ( | a | ) |
Return `True` if `a` is a Z3 array select application.
>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True
| def z3py.is_seq | ( | a | ) |
Return `True` if `a` is a Z3 sequence expression.
>>> print (is_seq(Unit(IntVal(0))))
True
>>> print (is_seq(StringVal("abc")))
True
Definition at line 10869 of file z3py.py.
Referenced by CharIsDigit(), Concat(), and Extract().
| def z3py.is_sort | ( | s | ) |
Return `True` if `s` is a Z3 sort.
>>> is_sort(IntSort())
True
>>> is_sort(Int('x'))
False
>>> is_expr(Int('x'))
True
Definition at line 647 of file z3py.py.
Referenced by ArraySort(), CreateDatatypes(), FreshFunction(), Function(), IsSubset(), K(), PropagateFunction(), prove(), RecFunction(), and Var().
| def z3py.is_store | ( | a | ) |
Return `True` if `a` is a Z3 array store application.
>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> is_store(Store(a, 0, 1))
True
| def z3py.is_string | ( | a | ) |
| def z3py.is_string_value | ( | a | ) |
| def z3py.is_sub | ( | a | ) |
Return `True` if `a` is an expression of the form b - c.
>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False
| def z3py.is_to_int | ( | a | ) |
Return `True` if `a` is an expression of the form ToInt(b).
>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False
| def z3py.is_to_real | ( | a | ) |
| def z3py.is_true | ( | a | ) |
Return `True` if `a` is the Z3 true expression.
>>> p = Bool('p')
>>> is_true(p)
False
>>> is_true(simplify(p == p))
True
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False
Definition at line 1580 of file z3py.py.
Referenced by AstRef.__bool__().
| 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 1305 of file z3py.py.
Referenced by get_var_index().
| def z3py.IsInt | ( | a | ) |
| def z3py.IsMember | ( | e, | |
| s | |||
| ) |
| def z3py.IsSubset | ( | a, | |
| b | |||
| ) |
| 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 4837 of file z3py.py.
Referenced by ModelRef.get_interp().
| 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 2252 of file z3py.py.
Referenced by Context.MkLambda().
| def z3py.LastIndexOf | ( | s, | |
| substr | |||
| ) |
| def z3py.Length | ( | s | ) |
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
Definition at line 11063 of file z3py.py.
Referenced by NativeContext.MkAdd(), NativeContext.MkAnd(), NativeContext.MkFreshFuncDecl(), NativeContext.MkFuncDecl(), NativeContext.MkMul(), NativeContext.MkOr(), NativeContext.MkSub(), and NativeContext.MkTupleSort().
| def z3py.Loop | ( | re, | |
| lo, | |||
hi = 0 |
|||
| ) |
| 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 4290 of file z3py.py.
| def z3py.main_ctx | ( | ) |
Return a reference to the global Z3 context.
>>> x = Real('x')
>>> x.ctx == main_ctx()
True
>>> c = Context()
>>> c == main_ctx()
False
>>> x2 = Real('x', c)
>>> x2.ctx == c
True
>>> eq(x, x2)
False
Definition at line 239 of file z3py.py.
Referenced by CharIsDigit(), help_simplify(), and simplify_param_descrs().
| 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 4814 of file z3py.py.
Referenced by Context.Context().
| def z3py.mk_not | ( | a | ) |
| def z3py.Model | ( | ctx = None | ) |
Definition at line 6680 of file z3py.py.
Referenced by Goal.ConvertModel(), Goal.convertModel(), Optimize.getModel(), Solver.getModel(), and Optimize.set_on_model().
| def z3py.MultiPattern | ( | * | args | ) |
Create a Z3 multi-pattern using the given expressions `*args`
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
>>> q
ForAll(x, f(x) != g(x))
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
MultiPattern(f(Var(0)), g(Var(0)))
Definition at line 1942 of file z3py.py.
| def z3py.Not | ( | a, | |
ctx = None |
|||
| ) |
| def z3py.open_log | ( | fname | ) |
| def z3py.Option | ( | re | ) |
| 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 1873 of file z3py.py.
Referenced by ApplyResult.as_expr().
| 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]]
| 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 9241 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 9220 of file z3py.py.
| 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 8345 of file z3py.py.
Referenced by ParAndThen().
| def z3py.PbEq | ( | args, | |
| k, | |||
ctx = None |
|||
| ) |
| def z3py.PbGe | ( | args, | |
| k | |||
| ) |
| def z3py.PbLe | ( | args, | |
| k | |||
| ) |
| def z3py.Plus | ( | re | ) |
| def z3py.PrefixOf | ( | a, | |
| b | |||
| ) |
| def z3py.probe_description | ( | name, | |
ctx = None |
|||
| ) |
Return a short description for the probe named `name`.
>>> d = probe_description('memory')
Definition at line 8641 of file z3py.py.
Referenced by describe_probes().