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 Abs | ( | arg | ) |
def AllChar | ( | regex_sort, | |
ctx = None |
|||
) |
Create a regular expression that accepts all single character strings
Definition at line 11273 of file z3py.py.
def 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 Tactic.__call__(), Fixedpoint.add_rule(), And(), AndThen(), Tactic.apply(), Goal.as_expr(), ApplyResult.as_expr(), Bool(), Bools(), BoolVector(), Distinct(), is_and(), is_bool(), is_implies(), is_or(), Lambda(), ParThen(), prove(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Repeat(), simplify(), Then(), and Fixedpoint.update_rule().
def 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.
def append_log | ( | s | ) |
Append user-defined string to interaction log.
Definition at line 119 of file z3py.py.
def 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(), args2params(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), and With().
def 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 4724 of file z3py.py.
Referenced by ArrayRef.__getitem__(), Array(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Lambda(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), and Update().
def 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(), ArraySort(), ArraySortRef.domain(), SortRef.kind(), SortRef.name(), ArraySortRef.range(), and SetSort().
def AtLeast | ( | * | args | ) |
Create an at-most Pseudo-Boolean k constraint. >>> a, b, c = Bools('a b c') >>> f = AtLeast(a, b, c, 2)
Definition at line 8930 of file z3py.py.
Referenced by AtLeast().
def 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 8912 of file z3py.py.
Referenced by AtMost().
def 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 BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVec(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().
def 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 4052 of file z3py.py.
Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), BitVecs(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().
def 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(), BitVecSort(), BitVecVal(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), BitVecSortRef.size(), and BitVecRef.sort().
def 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 4011 of file z3py.py.
Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), BitVecVal(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().
def 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 SortRef.__eq__(), SortRef.__ne__(), Fixedpoint.add_rule(), Solver.assert_and_track(), Optimize.assert_and_track(), Bool(), Bools(), BoolVector(), is_bool(), is_false(), is_not(), is_true(), and Not().
def 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 1731 of file z3py.py.
Referenced by And(), AtLeast(), AtMost(), Bools(), Solver.consequences(), Implies(), is_and(), is_implies(), is_or(), Or(), PbEq(), PbGe(), PbLe(), prove(), Solver.unsat_core(), and Xor().
def 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 FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), SortRef.__ne__(), FuncDeclRef.arity(), ArraySort(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), BoolSort(), BoolSortRef.cast(), Solver.check(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FreshBool(), If(), Implies(), IntSort(), is_arith_sort(), is_ast(), SortRef.kind(), SortRef.name(), Not(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), SetSort(), QuantifierRef.sort(), ArrayRef.sort(), Var(), and Xor().
def 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(), BoolVal(), BoolSortRef.cast(), UserPropagateBase.conflict(), AlgebraicNumRef.index(), is_false(), is_quantifier(), Re(), and Solver.to_smt2().
def 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 1747 of file z3py.py.
Referenced by And(), BoolVector(), and Or().
def 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.
Referenced by BV2Int().
def BVAddNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4450 of file z3py.py.
def BVAddNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4457 of file z3py.py.
def BVMulNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4492 of file z3py.py.
def BVMulNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4499 of file z3py.py.
def BVRedAnd | ( | a | ) |
def BVRedOr | ( | a | ) |
def BVSDivNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4478 of file z3py.py.
def BVSNegNoOverflow | ( | a | ) |
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4485 of file z3py.py.
def BVSubNoOverflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4464 of file z3py.py.
def BVSubNoUnderflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4471 of file z3py.py.
def Cbrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the cubic root of a. >>> x = Real('x') >>> Cbrt(x) x**(1/3)
Definition at line 3415 of file z3py.py.
Referenced by Cbrt().
def CharFromBv | ( | ch, | |
ctx = None |
|||
) |
def CharIsDigit | ( | ch, | |
ctx = None |
|||
) |
def CharSort | ( | ctx = None | ) |
Create a character sort >>> ch = CharSort() >>> print(ch) Char
Definition at line 10730 of file z3py.py.
Referenced by CharSort().
def CharToBv | ( | ch, | |
ctx = None |
|||
) |
def CharToInt | ( | ch, | |
ctx = None |
|||
) |
def CharVal | ( | ch, | |
ctx = None |
|||
) |
Definition at line 10823 of file z3py.py.
Referenced by SeqRef.__gt__().
def Complement | ( | re | ) |
def 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__(), SeqRef.__radd__(), Concat(), Contains(), and BitVecRef.size().
def 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.
def Const | ( | name, | |
sort | |||
) |
Create a constant of the given sort. >>> Const('x', IntSort()) x
Definition at line 1432 of file z3py.py.
Referenced by BitVecSort(), BoolSort(), Const(), Consts(), DeclareSort(), FPSort(), IntSort(), is_finite_domain(), is_finite_domain_value(), IsMember(), IsSubset(), RealSort(), DatatypeSortRef.recognizer(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
def 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 1444 of file z3py.py.
Referenced by Consts(), Ext(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def 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 11000 of file z3py.py.
Referenced by Contains().
def 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(), and CreateDatatypes().
def 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.
def DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpreted sort named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context. >>> A = DeclareSort('A') >>> a = Const('a', A) >>> b = Const('b', A) >>> a.sort() == A True >>> b.sort() == A True >>> a == b a == b
Definition at line 693 of file z3py.py.
Referenced by DeclareSort(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 4770 of file z3py.py.
Referenced by Default(), and is_default().
def describe_probes | ( | ) |
Display a (tabular) description of all available probes in Z3.
Definition at line 8650 of file z3py.py.
def describe_tactics | ( | ) |
Display a (tabular) description of all available tactics in Z3.
Definition at line 8444 of file z3py.py.
def 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 1119 of file z3py.py.
def Diff | ( | a, | |
b, | |||
ctx = None |
|||
) |
def disable_trace | ( | msg | ) |
Definition at line 79 of file z3py.py.
def 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 5366 of file z3py.py.
Referenced by DisjointSum().
def 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.
Referenced by Distinct(), is_distinct(), and simplify().
def 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.
Referenced by Empty().
def EmptySet | ( | s | ) |
Create the empty set >>> EmptySet(IntSort()) K(Int, False)
Definition at line 4913 of file z3py.py.
Referenced by EmptySet().
def enable_trace | ( | msg | ) |
Definition at line 75 of file z3py.py.
def ensure_prop_closures | ( | ) |
Definition at line 11344 of file z3py.py.
Referenced by UserPropagateBase.__init__().
def 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 EnumSort().
def 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 BitVec(), BitVecSort(), eq(), FP(), FPSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), main_ctx(), Select(), substitute(), and Var().
def 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(), Exists(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), and QuantifierRef.is_lambda().
def 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 4859 of file z3py.py.
Referenced by Ext().
def 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 Extract(), SubSeq(), and SubString().
def 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.
Referenced by FailIf().
def 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 FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), is_finite_domain(), is_finite_domain_sort(), and is_finite_domain_value().
def 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 7761 of file z3py.py.
Referenced by FiniteDomainNumRef.as_long(), FiniteDomainNumRef.as_string(), FiniteDomainVal(), and is_finite_domain_value().
def Float128 | ( | ctx = None | ) |
def Float16 | ( | ctx = None | ) |
def Float32 | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 9391 of file z3py.py.
Referenced by FPRef.__neg__(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), and fpUnsignedToFP().
def Float64 | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 9403 of file z3py.py.
Referenced by fpFPToFP(), and fpToFP().
def FloatDouble | ( | ctx = None | ) |
def FloatHalf | ( | ctx = None | ) |
def FloatQuadruple | ( | ctx = None | ) |
def FloatSingle | ( | ctx = None | ) |
def 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(), QuantifierRef.body(), QuantifierRef.children(), ForAll(), get_var_index(), is_app(), is_const(), QuantifierRef.is_exists(), is_expr(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), is_var(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def 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 FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FP(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPs(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().
def 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.
Referenced by fpAbs().
def 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__(), FPRef.__radd__(), fpAdd(), and FPs().
def 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 10503 of file z3py.py.
Referenced by fpBVToFP().
def 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__(), FPRef.__rdiv__(), and fpDiv().
def fpEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `fpEQ(other, self)`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpEQ(x, y) fpEQ(x, y) >>> fpEQ(x, y).sexpr() '(fp.eq x y)'
def fpFMA | ( | rm, | |
a, | |||
b, | |||
c, | |||
ctx = None |
|||
) |
def 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 10435 of file z3py.py.
Referenced by fpFP().
def 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.
Referenced by fpFPToFP().
def 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__(), and fpGEQ().
def 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__(), and fpGT().
def fpInfinity | ( | s, | |
negative | |||
) |
Create a Z3 floating-point +oo or -oo term.
Definition at line 9975 of file z3py.py.
def fpIsInf | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isInfinite expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> fpIsInf(x) fpIsInf(x)
Definition at line 10317 of file z3py.py.
Referenced by fpIsInf().
def fpIsNaN | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point isNaN expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpIsNaN(x) fpIsNaN(x)
Definition at line 10305 of file z3py.py.
Referenced by fpIsNaN().
def fpIsNegative | ( | a, | |
ctx = None |
|||
) |
def fpIsNormal | ( | a, | |
ctx = None |
|||
) |
def fpIsPositive | ( | a, | |
ctx = None |
|||
) |
def fpIsSubnormal | ( | a, | |
ctx = None |
|||
) |
def fpIsZero | ( | a, | |
ctx = None |
|||
) |
def 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__(), and fpLEQ().
def 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__(), and fpLT().
def fpMax | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point maximum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMax(x, y) fpMax(x, y) >>> fpMax(x, y).sort() FPSort(8, 24)
Definition at line 10272 of file z3py.py.
Referenced by fpMax().
def fpMin | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point minimum expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMin(x, y) fpMin(x, y) >>> fpMin(x, y).sort() FPSort(8, 24)
Definition at line 10257 of file z3py.py.
Referenced by fpMin().
def fpMinusInfinity | ( | s | ) |
def fpMinusZero | ( | s | ) |
Create a Z3 floating-point -0.0 term.
Definition at line 9988 of file z3py.py.
Referenced by FPVal().
def 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__(), FPRef.__rmul__(), fpMul(), and FPs().
def 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 9935 of file z3py.py.
def 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__(), and fpNeg().
def fpNEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `Not(fpEQ(other, self))`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpNEQ(x, y) Not(fpEQ(x, y)) >>> (x != y).sexpr() '(distinct x y)'
Definition at line 10423 of file z3py.py.
Referenced by fpNEQ().
def 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 fpPlusInfinity(), and FPVal().
def fpPlusZero | ( | s | ) |
def 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.
Referenced by fpRealToFP().
def 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__(), FPRef.__rmod__(), and fpRem().
def fpRoundToIntegral | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def FPs | ( | names, | |
fpsort, | |||
ctx = None |
|||
) |
Return an array of floating-point constants. >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) fpMul(RNE(), fpAdd(RNE(), x, y), z)
Definition at line 10071 of file z3py.py.
Referenced by fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), fpNEQ(), and FPs().
def 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.
Referenced by fpSignedToFP().
def 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 FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), FPSortRef.cast(), FPSortRef.ebits(), FPRef.ebits(), FPNumRef.exponent(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), FPSort(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), get_default_fp_sort(), is_fp(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), and FPRef.sort().
def fpSqrt | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def 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__(), FPRef.__sub__(), and fpSub().
def 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 10464 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), and fpToFP().
def 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.
Referenced by fpUnsignedToFP().
def 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.
Referenced by fpToFP(), and fpToIEEEBV().
def 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 10648 of file z3py.py.
Referenced by fpToReal().
def 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.
Referenced by fpToSBV().
def 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.
Referenced by fpToUBV().
def 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.
Referenced by fpUnsignedToFP().
def 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 FPNumRef.exponent(), fpAbs(), fpFP(), fpFPToFP(), fpToFP(), FPVal(), is_expr(), is_fp_value(), FPNumRef.isNegative(), set_default_fp_sort(), FPNumRef.sign_as_bv(), FPNumRef.significand(), and FPNumRef.significand_as_bv().
def fpZero | ( | s, | |
negative | |||
) |
def 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 1762 of file z3py.py.
Referenced by FreshBool().
def FreshConst | ( | sort, | |
prefix = "c" |
|||
) |
def FreshFunction | ( | * | sig | ) |
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 886 of file z3py.py.
def 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 3278 of file z3py.py.
Referenced by FreshInt().
def 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 3335 of file z3py.py.
Referenced by FreshReal().
def 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 10950 of file z3py.py.
Referenced by Full().
def FullSet | ( | s | ) |
def 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 863 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ModelRef.__getitem__(), ModelRef.__len__(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), FuncDeclRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), is_ast(), QuantifierRef.is_exists(), QuantifierRef.is_forall(), is_func_decl(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_var(), Lambda(), Map(), MultiPattern(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), substitute(), substitute_vars(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def 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 get_default_fp_sort | ( | ctx = None | ) |
def 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 get_full_version | ( | ) |
def 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.
Referenced by get_map_func().
def get_param | ( | name | ) |
Return the value of a Z3 global (or module) parameter >>> get_param('nlsat.reorder') 'true'
Definition at line 307 of file z3py.py.
Referenced by get_param().
def 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.
Referenced by get_var_index().
def get_version | ( | ) |
Definition at line 92 of file z3py.py.
def get_version_string | ( | ) |
Definition at line 83 of file z3py.py.
def help_simplify | ( | ) |
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 8771 of file z3py.py.
def 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__(), Abs(), BV2Int(), If(), Lambda(), and RecAddDefinition().
def 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(), Solver.consequences(), Implies(), is_implies(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().
def 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.
Referenced by IndexOf().
def 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 11147 of file z3py.py.
Referenced by InRe(), Loop(), Option(), Plus(), Range(), Star(), and Union().
def 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 ArithRef.__add__(), FuncDeclRef.__call__(), Probe.__call__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), Probe.__gt__(), Probe.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), Probe.__lt__(), ArithRef.__mod__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), ExprRef.arg(), Goal.as_expr(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), QuantifierRef.body(), BV2Int(), SortRef.cast(), Solver.check(), ExprRef.children(), QuantifierRef.children(), ExprRef.decl(), ModelRef.decls(), Distinct(), eq(), AstRef.eq(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), get_var_index(), AstRef.hash(), If(), Goal.insert(), Solver.insert(), Int(), Ints(), IntVector(), is_app(), is_app_of(), is_arith(), is_arith_sort(), is_ast(), is_bv(), is_const(), QuantifierRef.is_exists(), is_expr(), is_finite_domain(), QuantifierRef.is_forall(), is_fp(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_int_value(), QuantifierRef.is_lambda(), is_pattern(), is_probe(), is_quantifier(), is_real(), ArithSortRef.is_real(), is_select(), is_sort(), is_to_real(), is_var(), K(), AstMap.keys(), Statistics.keys(), FuncDeclRef.kind(), Solver.model(), MultiPattern(), ExprRef.num_args(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), OrElse(), ParOr(), QuantifierRef.pattern(), Solver.pop(), Solver.push(), AstVector.push(), Solver.reason_unknown(), RecAddDefinition(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), AstRef.sexpr(), Solver.sexpr(), SimpleSolver(), simplify(), Goal.simplify(), solve(), SolverFor(), ExprRef.sort(), ArithRef.sort(), Solver.statistics(), Store(), substitute(), substitute_vars(), ToReal(), AstVector.translate(), AstRef.translate(), Goal.translate(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def 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 3987 of file z3py.py.
def Intersect | ( | * | args | ) |
Create intersection of regular expressions. >>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 11181 of file z3py.py.
Referenced by Intersect().
def 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 3252 of file z3py.py.
Referenced by Tactic.__call__(), ArithRef.__ge__(), Goal.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ApplyResult.__len__(), ArithRef.__lt__(), AndThen(), Tactic.apply(), Goal.convert_model(), Goal.depth(), FailIf(), Goal.get(), Goal.inconsistent(), Ints(), is_add(), is_distinct(), is_div(), is_eq(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Lambda(), parse_smt2_string(), ParThen(), Goal.prec(), Product(), Repeat(), Goal.size(), Store(), Sum(), Then(), Solver.unsat_core(), Update(), When(), With(), and WithParams().
def 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 FuncDeclRef.__call__(), SortRef.__eq__(), ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), SortRef.__ne__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncDeclRef.arity(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), BoolSort(), ArithSortRef.cast(), ExprRef.children(), QuantifierRef.children(), Const(), DatatypeSortRef.constructor(), Consts(), Datatype.create(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), ModelRef.decls(), Default(), DisjointSum(), ArraySortRef.domain(), ArrayRef.domain(), FuncDeclRef.domain(), FuncInterp.else_value(), Empty(), EmptySet(), FuncInterp.entry(), Exists(), Ext(), ForAll(), FreshInt(), Full(), FullSet(), Function(), ModelRef.get_interp(), get_map_func(), get_var_index(), Int(), IntSort(), IntVal(), is_app(), is_arith_sort(), is_array(), is_ast(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_exists(), is_expr(), is_finite_domain_sort(), QuantifierRef.is_forall(), is_func_decl(), is_K(), QuantifierRef.is_lambda(), is_map(), is_pattern(), is_quantifier(), is_select(), is_sort(), is_store(), SeqSortRef.is_string(), is_var(), IsMember(), IsSubset(), K(), SortRef.kind(), Lambda(), Map(), MultiPattern(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), parse_smt2_string(), QuantifierRef.pattern(), FuncDeclRef.range(), ArraySortRef.range(), ArrayRef.range(), RecAddDefinition(), DatatypeSortRef.recognizer(), Select(), SeqSort(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), ArrayRef.sort(), ExprRef.sort_kind(), Store(), SortRef.subsort(), substitute(), substitute_vars(), TupleSort(), Update(), FuncEntry.value(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def IntToStr | ( | s | ) |
Convert integer expression to string
Definition at line 11089 of file z3py.py.
Referenced by StrToInt().
def 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__(), AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_binary_string(), IntNumRef.as_long(), IntNumRef.as_string(), SeqRef.at(), AlgebraicNumRef.index(), IndexOf(), IntVal(), is_app(), is_arith(), is_ast(), is_const(), is_expr(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), SeqSort(), and substitute().
def IntVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of integer constants of size `sz`. >>> X = IntVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2
Definition at line 3265 of file z3py.py.
Referenced by IntVector(), Product(), and Sum().
def is_add | ( | a | ) |
Return `True` if `a` is an expression of the form b + c. >>> x, y = Ints('x y') >>> is_add(x + y) True >>> is_add(x - y) False
Definition at line 2783 of file z3py.py.
Referenced by is_add().
def is_algebraic_value | ( | a | ) |
Return `True` if `a` is an algebraic value of sort Real. >>> is_algebraic_value(RealVal("3/5")) False >>> n = simplify(Sqrt(2)) >>> n 1.4142135623? >>> is_algebraic_value(n) True
Definition at line 2769 of file z3py.py.
Referenced by is_algebraic_value().
def is_and | ( | a | ) |
Return `True` if `a` is a Z3 and expression. >>> p, q = Bools('p q') >>> is_and(And(p, q)) True >>> is_and(Or(p, q)) False
Definition at line 1612 of file z3py.py.
Referenced by is_and().
def 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(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
def 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_app_of(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
def 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_arith(), is_int(), is_int_value(), is_rational_value(), and is_real().
def 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 is_arith_sort(), and ArithSortRef.subsort().
def is_array | ( | a | ) |
Return `True` if `a` is a Z3 array expression. >>> a = Array('a', IntSort(), IntSort()) >>> is_array(a) True >>> is_array(Store(a, 0, 1)) True >>> is_array(a[0]) False
Definition at line 4602 of file z3py.py.
Referenced by Ext(), is_array(), and Map().
def is_array_sort | ( | a | ) |
def 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 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 eq(), AstRef.eq(), is_ast(), and ReSort().
def 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 BoolSort(), is_bool(), is_quantifier(), and prove().
def 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 BitVec(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToIEEEBV(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
def 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(), is_bv_sort(), and BitVecSortRef.subsort().
def is_bv_value | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector numeral value. >>> b = BitVec('b', 32) >>> is_bv_value(b) False >>> b = BitVecVal(10, 32) >>> b 10 >>> is_bv_value(b) True
Definition at line 3949 of file z3py.py.
Referenced by is_bv_value().
def 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(), get_var_index(), is_const(), is_quantifier(), is_var(), and prove().
def is_const_array | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_const_array(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_const_array(a) False
Definition at line 4616 of file z3py.py.
Referenced by is_const_array().
def is_default | ( | a | ) |
Return `True` if `a` is a Z3 default array expression. >>> d = Default(K(IntSort(), 10)) >>> is_default(d) True
Definition at line 4658 of file z3py.py.
Referenced by is_default().
def is_distinct | ( | a | ) |
Return `True` if `a` is a Z3 distinct expression. >>> x, y, z = Ints('x y z') >>> is_distinct(x == y) False >>> is_distinct(Distinct(x, y, z)) True
Definition at line 1670 of file z3py.py.
Referenced by is_distinct().
def is_div | ( | a | ) |
Return `True` if `a` is an expression of the form b / c. >>> x, y = Reals('x y') >>> is_div(x / y) True >>> is_div(x + y) False >>> x, y = Ints('x y') >>> is_div(x / y) False >>> is_idiv(x / y) True
Definition at line 2819 of file z3py.py.
Referenced by is_div().
def 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__(), and is_eq().
def 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_expr(), is_quantifier(), is_sort(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), StrFromCode(), StrToCode(), substitute(), substitute_funs(), substitute_vars(), and ModelRef.update_value().
def 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__(), BoolVal(), and is_false().
def 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(), and is_finite_domain_value().
def 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(), and is_finite_domain_sort().
def is_finite_domain_value | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain value. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain_value(b) False >>> b = FiniteDomainVal(10, s) >>> b 10 >>> is_finite_domain_value(b) True
Definition at line 7776 of file z3py.py.
Referenced by is_finite_domain_value().
def 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 FP(), fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and set_default_fp_sort().
def 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 is_fp_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point numeral value. >>> b = FP('b', FPSort(8, 24)) >>> is_fp_value(b) False >>> b = FPVal(1.0, FPSort(8, 24)) >>> b 1 >>> is_fp_value(b) True
Definition at line 9861 of file z3py.py.
Referenced by is_fp_value().
def 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(), is_fprm(), and is_fprm_value().
def is_fprm_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point rounding mode sort. >>> is_fprm_sort(FPSort(8, 24)) False >>> is_fprm_sort(RNE().sort()) True
Definition at line 9442 of file z3py.py.
Referenced by is_fprm_sort().
def 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 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 is_func_decl(), Map(), prove(), substitute_funs(), and ModelRef.update_value().
def is_ge | ( | a | ) |
Return `True` if `a` is an expression of the form b >= c. >>> x, y = Ints('x y') >>> is_ge(x >= y) True >>> is_ge(x == y) False
Definition at line 2884 of file z3py.py.
Referenced by is_ge().
def is_gt | ( | a | ) |
Return `True` if `a` is an expression of the form b > c. >>> x, y = Ints('x y') >>> is_gt(x > y) True >>> is_gt(x == y) False
Definition at line 2896 of file z3py.py.
Referenced by is_gt().
def 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 is_implies | ( | a | ) |
Return `True` if `a` is a Z3 implication expression. >>> p, q = Bools('p q') >>> is_implies(Implies(p, q)) True >>> is_implies(And(p, q)) False
Definition at line 1636 of file z3py.py.
Referenced by is_implies().
def is_int | ( | a | ) |
Return `True` if `a` is an integer expression. >>> x = Int('x') >>> is_int(x + 1) True >>> is_int(1) False >>> is_int(IntVal(1)) True >>> y = Real('y') >>> is_int(y) False >>> is_int(y + 1) False
Definition at line 2677 of file z3py.py.
Referenced by Int(), IntSort(), is_int(), and RealSort().
def 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.
Referenced by is_int_value().
def is_is_int | ( | a | ) |
Return `True` if `a` is an expression of the form IsInt(b). >>> x = Real('x') >>> is_is_int(IsInt(x)) True >>> is_is_int(x) False
Definition at line 2908 of file z3py.py.
Referenced by is_is_int().
def is_K | ( | a | ) |
Return `True` if `a` is a Z3 constant array. >>> a = K(IntSort(), 10) >>> is_K(a) True >>> a = Array('a', IntSort(), IntSort()) >>> is_K(a) False
Definition at line 4629 of file z3py.py.
Referenced by is_K().
def is_le | ( | a | ) |
Return `True` if `a` is an expression of the form b <= c. >>> x, y = Ints('x y') >>> is_le(x <= y) True >>> is_le(x < y) False
Definition at line 2860 of file z3py.py.
Referenced by is_le().
def is_lt | ( | a | ) |
Return `True` if `a` is an expression of the form b < c. >>> x, y = Ints('x y') >>> is_lt(x < y) True >>> is_lt(x == y) False
Definition at line 2872 of file z3py.py.
Referenced by is_lt().
def 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(), and is_map().
def is_mod | ( | a | ) |
Return `True` if `a` is an expression of the form b % c. >>> x, y = Ints('x y') >>> is_mod(x % y) True >>> is_mod(x + y) False
Definition at line 2848 of file z3py.py.
Referenced by is_mod().
def is_mul | ( | a | ) |
Return `True` if `a` is an expression of the form b * c. >>> x, y = Ints('x y') >>> is_mul(x * y) True >>> is_mul(x - y) False
Definition at line 2795 of file z3py.py.
Referenced by is_mul().
def is_not | ( | a | ) |
def is_or | ( | a | ) |
Return `True` if `a` is a Z3 or expression. >>> p, q = Bools('p q') >>> is_or(Or(p, q)) True >>> is_or(And(p, q)) False
Definition at line 1624 of file z3py.py.
Referenced by is_or().
def 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_pattern(), is_quantifier(), and MultiPattern().
def is_probe | ( | p | ) |
Return `True` if `p` is a Z3 probe. >>> is_probe(Int('x')) False >>> is_probe(Probe('memory')) True
Definition at line 8612 of file z3py.py.
Referenced by eq(), is_probe(), mk_not(), and Not().
def is_quantifier | ( | a | ) |
Return `True` if `a` is a Z3 quantifier. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> is_quantifier(q) True >>> is_quantifier(f(x)) False
Definition at line 2164 of file z3py.py.
Referenced by Exists(), and is_quantifier().
def 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.
Referenced by RatNumRef.denominator(), is_rational_value(), and RatNumRef.numerator().
def is_re | ( | s | ) |
def 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(), fpToFP(), fpToReal(), is_real(), Real(), and RealSort().
def is_select | ( | a | ) |
Return `True` if `a` is a Z3 array select application. >>> a = Array('a', IntSort(), IntSort()) >>> is_select(a) False >>> i = Int('i') >>> is_select(a[i]) True
Definition at line 4877 of file z3py.py.
Referenced by is_select().
def 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(), Extract(), and is_seq().
def 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(), is_sort(), IsSubset(), K(), PropagateFunction(), prove(), RecFunction(), and Var().
def is_store | ( | a | ) |
Return `True` if `a` is a Z3 array store application. >>> a = Array('a', IntSort(), IntSort()) >>> is_store(a) False >>> is_store(Store(a, 0, 1)) True
Definition at line 4890 of file z3py.py.
Referenced by is_store().
def is_string | ( | a | ) |
Return `True` if `a` is a Z3 string expression. >>> print (is_string(StringVal("ab"))) True
Definition at line 10879 of file z3py.py.
Referenced by is_string().
def is_string_value | ( | a | ) |
return 'True' if 'a' is a Z3 string constant expression. >>> print (is_string_value(StringVal("a"))) True >>> print (is_string_value(StringVal("a") + StringVal("b"))) False
Definition at line 10887 of file z3py.py.
Referenced by is_string_value().
def is_sub | ( | a | ) |
Return `True` if `a` is an expression of the form b - c. >>> x, y = Ints('x y') >>> is_sub(x - y) True >>> is_sub(x + y) False
Definition at line 2807 of file z3py.py.
Referenced by is_sub().
def is_to_int | ( | a | ) |
Return `True` if `a` is an expression of the form ToInt(b). >>> x = Real('x') >>> n = ToInt(x) >>> n ToInt(x) >>> is_to_int(n) True >>> is_to_int(x) False
Definition at line 2935 of file z3py.py.
Referenced by is_to_int().
def is_to_real | ( | a | ) |
Return `True` if `a` is an expression of the form ToReal(b). >>> x = Int('x') >>> n = ToReal(x) >>> n ToReal(x) >>> is_to_real(n) True >>> is_to_real(x) False
Definition at line 2920 of file z3py.py.
Referenced by is_to_real().
def 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__(), BoolVal(), and is_true().
def 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(), and is_var().
def 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 3385 of file z3py.py.
Referenced by is_is_int(), and IsInt().
def 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 5000 of file z3py.py.
Referenced by IsMember().
def 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 5011 of file z3py.py.
Referenced by IsSubset().
def 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 Default(), EmptySet(), FullSet(), ModelRef.get_interp(), is_const_array(), is_default(), is_K(), and K().
def 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 QuantifierRef.is_lambda(), and Lambda().
def LastIndexOf | ( | s, | |
substr | |||
) |
Retrieve the last index of substring within a string
Definition at line 11054 of file z3py.py.
def 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 Length().
def LinearOrder | ( | a, | |
index | |||
) |
def 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 11243 of file z3py.py.
Referenced by Loop().
def 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.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), and LShR().
def 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(), main_ctx(), simplify_param_descrs(), and Goal.translate().
def 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 get_map_func(), is_map(), and Map().
def Model | ( | ctx = None | ) |
Definition at line 6680 of file z3py.py.
Referenced by Optimize.set_on_model().
def 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.
Referenced by MultiPattern().
def 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 1806 of file z3py.py.
Referenced by AndThen(), ApplyResult.as_expr(), Solver.consequences(), Goal.convert_model(), Distinct(), FailIf(), fpNEQ(), is_not(), mk_not(), Not(), prove(), simplify(), Then(), When(), and Xor().
def open_log | ( | fname | ) |
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 114 of file z3py.py.
def 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 11212 of file z3py.py.
Referenced by Option().
def 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.__getitem__(), ApplyResult.__len__(), ApplyResult.as_expr(), Bools(), Goal.convert_model(), is_and(), is_or(), Or(), OrElse(), ParThen(), prove(), Repeat(), and simplify().
def OrElse | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) >>> # Tactic split-clause fails if there is no clause in the given goal. >>> t(x == 0) [[x == 0]] >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]]
Definition at line 8305 of file z3py.py.
def ParAndThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
def 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 8326 of file z3py.py.
Referenced by ParOr().
def 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 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.
Referenced by parse_smt2_file(), and parse_smt2_string().
def 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(), and ParThen().
def PartialOrder | ( | a, | |
index | |||
) |
def PbEq | ( | args, | |
k, | |||
ctx = None |
|||
) |
Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 8997 of file z3py.py.
Referenced by PbEq().
def 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 8986 of file z3py.py.
Referenced by PbGe().
def 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 8975 of file z3py.py.
Referenced by PbLe().
def PiecewiseLinearOrder | ( | a, | |
index | |||
) |
def 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 11199 of file z3py.py.
Referenced by Plus().
def 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 10970 of file z3py.py.
Referenced by PrefixOf().
def 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(), and probe_description().
def probes | ( | ctx = None | ) |
Return a list of all available probes in Z3. >>> l = probes() >>> l.count('memory') == 1 True
Definition at line 8630 of file z3py.py.
Referenced by describe_probes(), and probes().
def 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 8882 of file z3py.py.
def 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 11445 of file z3py.py.
def 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 9069 of file z3py.py.
Referenced by Default(), Map(), prove(), Store(), and Update().
def 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 3226 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), RatNumRef.numerator(), and Q().
def 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 11256 of file z3py.py.
Referenced by Range().
def RatVal | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 3210 of file z3py.py.
def 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 11108 of file z3py.py.
Referenced by InRe(), Intersect(), Loop(), Option(), Plus(), Re(), Star(), and Union().
def 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 3292 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), is_bool(), is_func_decl(), is_int(), ArithSortRef.is_int(), ArithRef.is_int(), is_is_int(), is_rational_value(), is_real(), ArithSortRef.is_real(), ArithRef.is_real(), is_to_int(), is_true(), IsInt(), main_ctx(), Real(), Reals(), RealVector(), Tactic.solver(), ExprRef.sort(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
def Reals | ( | names, | |
ctx = None |
|||
) |
Return a tuple of real constants. >>> x, y, z = Reals('x y z') >>> Sum(x, y, z) x + y + z >>> Sum(x, y, z).sort() Real
def 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 3146 of file z3py.py.
Referenced by FuncDeclRef.__call__(), FuncDeclRef.arity(), SortRef.cast(), ArithSortRef.cast(), FuncDeclRef.domain(), FreshReal(), is_arith_sort(), FuncDeclRef.range(), Real(), RealSort(), RealVal(), RealVar(), SortRef.subsort(), and QuantifierRef.var_sort().
def 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 3191 of file z3py.py.
Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), Cbrt(), RatNumRef.denominator_as_long(), fpRealToFP(), fpToFP(), AlgebraicNumRef.index(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), RatNumRef.numerator_as_long(), RatVal(), RealVal(), and Sqrt().
def RealVar | ( | idx, | |
ctx = None |
|||
) |
Create a real free variable. Free variables are used to create quantified formulas. They are also used to create polynomials. >>> RealVar(0) Var(0)
Definition at line 1478 of file z3py.py.
Referenced by RealVar(), and RealVarVector().
def RealVarVector | ( | n, | |
ctx = None |
|||
) |
Create a list of Real free variables. The variables have ids: 0, 1, ..., n-1 >>> x0, x1, x2, x3 = RealVarVector(4) >>> x2 Var(2)
Definition at line 1489 of file z3py.py.
Referenced by RealVarVector().
def RealVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of real constants of size `sz`. >>> X = RealVector('x', 3) >>> X [x__0, x__1, x__2] >>> Sum(X) x__0 + x__1 + x__2 >>> Sum(X).sort() Real
Definition at line 3320 of file z3py.py.
Referenced by RealVector().
def 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 927 of file z3py.py.
Referenced by RecAddDefinition().
def RecFunction | ( | name, | |
* | sig | ||
) |
Create a new Z3 recursive with the given sorts.
Definition at line 909 of file z3py.py.
Referenced by RecAddDefinition().
def 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 8394 of file z3py.py.
Referenced by Repeat().
def 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 4412 of file z3py.py.
Referenced by RepeatBitVec().
def 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 11019 of file z3py.py.
Referenced by Replace().
def reset_params | ( | ) |
def ReSort | ( | s | ) |
Definition at line 11127 of file z3py.py.
def RNA | ( | ctx = None | ) |
Definition at line 9656 of file z3py.py.
Referenced by get_default_rounding_mode().
def RNE | ( | ctx = None | ) |
Definition at line 9646 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 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 4322 of file z3py.py.
Referenced by RotateLeft().
def 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 4338 of file z3py.py.
Referenced by RotateRight().
def RoundNearestTiesToAway | ( | ctx = None | ) |
def RoundNearestTiesToEven | ( | ctx = None | ) |
def RoundTowardNegative | ( | ctx = None | ) |
def RoundTowardPositive | ( | ctx = None | ) |
def RoundTowardZero | ( | ctx = None | ) |
def RTN | ( | ctx = None | ) |
Definition at line 9676 of file z3py.py.
Referenced by get_default_rounding_mode().
def RTP | ( | ctx = None | ) |
Definition at line 9666 of file z3py.py.
Referenced by get_default_rounding_mode().
def RTZ | ( | ctx = None | ) |
def Select | ( | a, | |
* | args | ||
) |
Return a Z3 select array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i = Int('i') >>> Select(a, i) a[i] >>> eq(Select(a, i), a[i]) True
Definition at line 4798 of file z3py.py.
Referenced by Select().
def SeqSort | ( | s | ) |
Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True
Definition at line 10740 of file z3py.py.
Referenced by Empty(), Full(), SeqSortRef.is_string(), and SeqSort().
def set_default_fp_sort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
def set_default_rounding_mode | ( | rm, | |
ctx = None |
|||
) |
def set_option | ( | * | args, |
** | kws | ||
) |
def set_param | ( | * | args, |
** | kws | ||
) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 271 of file z3py.py.
Referenced by set_option(), and set_param().
def SetAdd | ( | s, | |
e | |||
) |
Add element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetAdd(a, 1) Store(a, 1, True)
Definition at line 4957 of file z3py.py.
Referenced by SetAdd().
def SetComplement | ( | s | ) |
The complement of set s >>> a = Const('a', SetSort(IntSort())) >>> SetComplement(a) complement(a)
Definition at line 4979 of file z3py.py.
Referenced by SetComplement().
def SetDel | ( | s, | |
e | |||
) |
Remove element e to set s >>> a = Const('a', SetSort(IntSort())) >>> SetDel(a, 1) Store(a, 1, False)
Definition at line 4968 of file z3py.py.
Referenced by SetDel().
def 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 4989 of file z3py.py.
Referenced by SetDifference().
def SetHasSize | ( | a, | |
k | |||
) |
def 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 4944 of file z3py.py.
Referenced by SetIntersect().
def SetSort | ( | s | ) |
Sets.
Create a set sort over element sort s
Definition at line 4908 of file z3py.py.
Referenced by Ext(), IsMember(), IsSubset(), SetAdd(), SetComplement(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
def 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 4931 of file z3py.py.
Referenced by SetUnion().
def 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 4354 of file z3py.py.
Referenced by SignExt().
def 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 7394 of file z3py.py.
Referenced by Solver.reason_unknown(), SimpleSolver(), and Solver.statistics().
def 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 8746 of file z3py.py.
Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), Contains(), CreateDatatypes(), Distinct(), eq(), AstRef.eq(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), AstRef.hash(), If(), IndexOf(), InRe(), is_algebraic_value(), is_true(), K(), Length(), Loop(), LShR(), Not(), Option(), Plus(), PrefixOf(), Q(), Range(), RatVal(), RecAddDefinition(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), simplify(), Star(), StrToInt(), SuffixOf(), Union(), Xor(), and ZeroExt().
def simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 8776 of file z3py.py.
def 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 9008 of file z3py.py.
def 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 9038 of file z3py.py.
def 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 7373 of file z3py.py.
Referenced by SolverFor().
def 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 3402 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), is_algebraic_value(), and Sqrt().
def 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 4269 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
def 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 11230 of file z3py.py.
Referenced by Star().
def 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 4781 of file z3py.py.
Referenced by ModelRef.get_interp(), is_array(), is_store(), SetAdd(), SetDel(), and Store().
def StrFromCode | ( | c | ) |
def 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 10903 of file z3py.py.
def Strings | ( | names, | |
ctx = None |
|||
) |
Return a tuple of String constants.
Definition at line 10912 of file z3py.py.
Referenced by Contains().
def StringSort | ( | ctx = None | ) |
Create a string sort >>> s = StringSort() >>> print(s) String
Definition at line 10721 of file z3py.py.
Referenced by DisjointSum(), Empty(), Full(), SeqSortRef.is_string(), String(), and TupleSort().
def StringVal | ( | s, | |
ctx = None |
|||
) |
create a string expression
Definition at line 10896 of file z3py.py.
Referenced by CharIsDigit(), deserialize(), Empty(), Extract(), AlgebraicNumRef.index(), is_seq(), is_string(), is_string_value(), Length(), and Re().
def StrToCode | ( | s | ) |
def 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 11073 of file z3py.py.
Referenced by StrToInt().
def SubSeq | ( | s, | |
offset, | |||
length | |||
) |
def 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 8781 of file z3py.py.
Referenced by substitute().
def substitute_funs | ( | t, | |
* | m | ||
) |
Apply subistitution 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 8834 of file z3py.py.
def 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 8814 of file z3py.py.
Referenced by substitute_vars().
def SubString | ( | s, | |
offset, | |||
length | |||
) |
def 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 10985 of file z3py.py.
Referenced by SuffixOf().
def 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 8856 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), RealVector(), and Sum().
def tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 8435 of file z3py.py.
Referenced by describe_tactics(), and tactic_description().
def tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3. >>> l = tactics() >>> l.count('simplify') == 1 True
Definition at line 8424 of file z3py.py.
Referenced by describe_tactics(), and tactics().
def 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 8292 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), ApplyResult.__len__(), Goal.convert_model(), Goal.depth(), Statistics.get_key_value(), Statistics.keys(), Repeat(), Tactic.solver(), and Then().
def to_Ast | ( | ptr | ) |
Definition at line 11380 of file z3py.py.
Referenced by user_prop_created(), user_prop_decide(), user_prop_diseq(), user_prop_eq(), and user_prop_fixed().
def to_ContextObj | ( | ptr | ) |
Definition at line 11361 of file z3py.py.
Referenced by user_prop_fresh().
def to_symbol | ( | s, | |
ctx = None |
|||
) |
Convert an integer or string into a Z3 symbol.
Definition at line 124 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DatatypeSort(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), is_quantifier(), PropagateFunction(), prove(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().
def 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 3367 of file z3py.py.
Referenced by is_to_int(), and ToInt().
def 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 3349 of file z3py.py.
Referenced by FuncDeclRef.__call__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), SortRef.cast(), is_to_real(), and ToReal().
def 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 11297 of file z3py.py.
def TreeOrder | ( | a, | |
index | |||
) |
def 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 8415 of file z3py.py.
def 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 5354 of file z3py.py.
Referenced by TupleSort().
def 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 4227 of file z3py.py.
Referenced by BitVecRef.__div__(), BitVecRef.__rdiv__(), and UDiv().
def 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 4191 of file z3py.py.
Referenced by BitVecRef.__ge__(), and UGE().
def 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 4209 of file z3py.py.
Referenced by BitVecRef.__gt__(), and UGT().
def 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 4155 of file z3py.py.
Referenced by BitVecRef.__le__(), and ULE().
def 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 4173 of file z3py.py.
Referenced by BitVecRef.__lt__(), and ULT().
def Union | ( | * | args | ) |
Create union of regular expressions. >>> re = Union(Re("a"), Re("b"), Re("c")) >>> print (simplify(InRe("d", re))) False
Definition at line 11161 of file z3py.py.
Referenced by ReRef.__add__(), InRe(), and Union().
def Unit | ( | a | ) |
def 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 4738 of file z3py.py.
def 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 4248 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), SRem(), and URem().
def user_prop_created | ( | ctx, | |
cb, | |||
id | |||
) |
def user_prop_decide | ( | ctx, | |
cb, | |||
t_ref, | |||
idx_ref, | |||
phase_ref | |||
) |
Definition at line 11424 of file z3py.py.
def user_prop_diseq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
Definition at line 11414 of file z3py.py.
def user_prop_eq | ( | ctx, | |
cb, | |||
x, | |||
y | |||
) |
def user_prop_final | ( | ctx, | |
cb | |||
) |
def user_prop_fixed | ( | ctx, | |
cb, | |||
id, | |||
value | |||
) |
def user_prop_fresh | ( | ctx, | |
_new_ctx | |||
) |
Definition at line 11367 of file z3py.py.
def user_prop_pop | ( | ctx, | |
cb, | |||
num_scopes | |||
) |
def user_prop_push | ( | ctx, | |
cb | |||
) |
def Var | ( | idx, | |
s | |||
) |
Create a Z3 free variable. Free variables are used to create quantified formulas. >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False
Definition at line 1465 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), get_var_index(), is_pattern(), is_var(), MultiPattern(), QuantifierRef.pattern(), RealVar(), RealVarVector(), substitute_vars(), and Var().
def 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 8709 of file z3py.py.
Referenced by When().
def 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 8366 of file z3py.py.
Referenced by Goal.prec(), and With().
def 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 8380 of file z3py.py.
Referenced by WithParams().
def 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 1790 of file z3py.py.
Referenced by Xor().
def z3_debug | ( | ) |
Definition at line 62 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), describe_probes(), deserialize(), Distinct(), FuncDeclRef.domain(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), AlgebraicNumRef.index(), Intersect(), is_quantifier(), is_sort(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), PropagateFunction(), prove(), RatVal(), RealSort(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_funs(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
def z3_error_handler | ( | c, | |
e | |||
) |
def 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 4384 of file z3py.py.
Referenced by ZeroExt().
sat = CheckSatResult(Z3_L_TRUE) |
unknown = CheckSatResult(Z3_L_UNDEF) |
unsat = CheckSatResult(Z3_L_FALSE) |