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 | DeclareTypeVar (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 (bv) |
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 | SeqMap (f, s) |
def | SeqMapI (f, i, s) |
def | SeqFoldLeft (f, a, s) |
def | SeqFoldLeftI (f, i, a, s) |
def | StrToInt (s) |
def | IntToStr (s) |
def | StrToCode (s) |
def | StrFromCode (c) |
def | Re (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 | to_Ast (ptr) |
def | to_ContextObj (ptr) |
def | to_AstVectorObj (ptr) |
def | on_clause_eh (ctx, p, n, dep, clause) |
def | ensure_prop_closures () |
def | user_prop_push (ctx, cb) |
def | user_prop_pop (ctx, cb, num_scopes) |
def | user_prop_fresh (ctx, _new_ctx) |
def | user_prop_fixed (ctx, cb, id, value) |
def | user_prop_created (ctx, cb, id) |
def | user_prop_final (ctx, cb) |
def | user_prop_eq (ctx, cb, x, y) |
def | user_prop_diseq (ctx, cb, x, y) |
def | user_prop_decide (ctx, cb, t, idx, phase) |
def | PropagateFunction (name, *sig) |
Variables | |
Z3_DEBUG = __debug__ | |
sat = CheckSatResult(Z3_L_TRUE) | |
unsat = CheckSatResult(Z3_L_FALSE) | |
unknown = CheckSatResult(Z3_L_UNDEF) | |
def z3py.Abs | ( | arg | ) |
def z3py.AllChar | ( | regex_sort, | |
ctx = None |
|||
) |
def z3py.And | ( | * | args | ) |
Create a Z3 and-expression or and-probe. >>> p, q, r = Bools('p q r') >>> And(p, q, r) And(p, q, r) >>> P = BoolVector('p', 5) >>> And(P) And(p__0, p__1, p__2, p__3, p__4)
Definition at line 1889 of file z3py.py.
Referenced by BoolRef.__and__(), Fixedpoint.add_rule(), Goal.as_expr(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().
def z3py.AndThen | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in sequence. >>> x, y = Ints('x y') >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 8430 of file z3py.py.
Referenced by Then().
def z3py.append_log | ( | s | ) |
def z3py.args2params | ( | arguments, | |
keywords, | |||
ctx = None |
|||
) |
Convert python arguments into a Z3_params object. A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true)
Definition at line 5512 of file z3py.py.
Referenced by Tactic.apply(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), Simplifier.using_params(), and With().
def z3py.Array | ( | name, | |
* | sorts | ||
) |
def z3py.ArraySort | ( | * | sig | ) |
Return the Z3 array sort with the given domain and range sorts. >>> A = ArraySort(IntSort(), BoolSort()) >>> A Array(Int, Bool) >>> A.domain() Int >>> A.range() Bool >>> AA = ArraySort(IntSort(), A) >>> AA Array(Int, Array(Int, Bool))
Definition at line 4746 of file z3py.py.
Referenced by Array(), Context.MkArraySort(), and SetSort().
def z3py.AtLeast | ( | * | args | ) |
def z3py.AtMost | ( | * | args | ) |
def z3py.BitVec | ( | name, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. If `ctx=None`, then the global context is used. >>> x = BitVec('x', 16) >>> is_bv(x) True >>> x.size() 16 >>> x.sort() BitVec(16) >>> word = BitVecSort(16) >>> x2 = BitVec('x', word) >>> eq(x, x2) True
Definition at line 4083 of file z3py.py.
Referenced by BitVecs().
def z3py.BitVecs | ( | names, | |
bv, | |||
ctx = None |
|||
) |
def z3py.BitVecSort | ( | sz, | |
ctx = None |
|||
) |
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. >>> Byte = BitVecSort(8) >>> Word = BitVecSort(16) >>> Byte BitVec(8) >>> x = Const('x', Byte) >>> eq(x, BitVec('x', 8)) True
Definition at line 4051 of file z3py.py.
Referenced by BitVec(), BitVecVal(), Context.mkBitVecSort(), and Context.MkBitVecSort().
def z3py.BitVecVal | ( | val, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. >>> v = BitVecVal(10, 32) >>> v 10 >>> print("0x%.8x" % v.as_long()) 0x0000000a
def z3py.Bool | ( | name, | |
ctx = None |
|||
) |
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. >>> p = Bool('p') >>> q = Bool('q') >>> And(p, q) And(p, q)
Definition at line 1768 of file z3py.py.
Referenced by Solver.assert_and_track(), Optimize.assert_and_track(), Bools(), and BoolVector().
def z3py.Bools | ( | names, | |
ctx = None |
|||
) |
def z3py.BoolSort | ( | ctx = None | ) |
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. >>> BoolSort() Bool >>> p = Const('p', BoolSort()) >>> is_bool(p) True >>> r = Function('r', IntSort(), IntSort(), BoolSort()) >>> r(0, 1) r(0, 1) >>> is_bool(r(0, 1)) True
Definition at line 1731 of file z3py.py.
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), Solver.check(), FreshBool(), Context.getBoolSort(), If(), Implies(), Context.mkBoolSort(), Not(), SetSort(), QuantifierRef.sort(), and Xor().
def z3py.BoolVal | ( | val, | |
ctx = None |
|||
) |
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. >>> BoolVal(True) True >>> is_true(BoolVal(True)) True >>> is_true(True) False >>> is_false(BoolVal(False)) True
Definition at line 1749 of file z3py.py.
Referenced by Goal.as_expr(), ApplyResult.as_expr(), BoolSortRef.cast(), UserPropagateBase.conflict(), AlgebraicNumRef.index(), is_quantifier(), and Solver.to_smt2().
def z3py.BoolVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
def z3py.BV2Int | ( | a, | |
is_signed = False |
|||
) |
Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) >>> BV2Int(b).sort() Int >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) >>> x > BV2Int(b, is_signed=False) x > BV2Int(b) >>> x > BV2Int(b, is_signed=True) x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [x = 2, b = 1]
Definition at line 4019 of file z3py.py.
def z3py.BVAddNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
def z3py.BVAddNoUnderflow | ( | a, | |
b | |||
) |
def z3py.BVMulNoOverflow | ( | a, | |
b, | |||
signed | |||
) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4547 of file z3py.py.
def z3py.BVMulNoUnderflow | ( | a, | |
b | |||
) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4554 of file z3py.py.
def z3py.BVRedAnd | ( | a | ) |
def z3py.BVRedOr | ( | a | ) |
def z3py.BVSDivNoOverflow | ( | a, | |
b | |||
) |
def z3py.BVSNegNoOverflow | ( | a | ) |
def z3py.BVSubNoOverflow | ( | a, | |
b | |||
) |
def z3py.BVSubNoUnderflow | ( | a, | |
b, | |||
signed | |||
) |
def z3py.Cbrt | ( | a, | |
ctx = None |
|||
) |
def z3py.CharFromBv | ( | bv | ) |
def z3py.CharSort | ( | ctx = None | ) |
Create a character sort >>> ch = CharSort() >>> print(ch) Char
Definition at line 10888 of file z3py.py.
Referenced by Context.mkCharSort().
def z3py.CharVal | ( | ch, | |
ctx = None |
|||
) |
def z3py.Complement | ( | re | ) |
def z3py.Concat | ( | * | args | ) |
Create a Z3 bit-vector concatenation expression. >>> v = BitVecVal(1, 4) >>> Concat(v, v+1, v) Concat(Concat(1, 1 + 1), 1) >>> simplify(Concat(v, v+1, v)) 289 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long()) 121
Definition at line 4128 of file z3py.py.
Referenced by SeqRef.__add__(), and SeqRef.__radd__().
def z3py.Cond | ( | p, | |
t1, | |||
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
Definition at line 8887 of file z3py.py.
Referenced by If().
def z3py.Const | ( | name, | |
sort | |||
) |
def z3py.Consts | ( | names, | |
sort | |||
) |
def z3py.Contains | ( | a, | |
b | |||
) |
Check if 'a' contains 'b' >>> s1 = Contains("abc", "ab") >>> simplify(s1) True >>> s2 = Contains("abc", "bc") >>> simplify(s2) True >>> x, y, z = Strings('x y z') >>> s3 = Contains(Concat(x,y,z), y) >>> simplify(s3) True
Definition at line 11158 of file z3py.py.
def z3py.CreateDatatypes | ( | * | ds | ) |
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. In the following example we define a Tree-List using two mutually recursive datatypes. >>> TreeList = Datatype('TreeList') >>> Tree = Datatype('Tree') >>> # Tree has two constructors: leaf and node >>> Tree.declare('leaf', ('val', IntSort())) >>> # a node contains a list of trees >>> Tree.declare('node', ('children', TreeList)) >>> TreeList.declare('nil') >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) >>> Tree.val(Tree.leaf(10)) val(leaf(10)) >>> simplify(Tree.val(Tree.leaf(10))) 10 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) >>> n1 node(cons(leaf(10), cons(leaf(20), nil))) >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) >>> simplify(n2 == n1) False >>> simplify(TreeList.car(Tree.children(n2)) == n1) True
Definition at line 5204 of file z3py.py.
Referenced by Datatype.create().
def z3py.DatatypeSort | ( | name, | |
ctx = None |
|||
) |
Create a reference to a sort that was declared, or will be declared, as a recursive datatype
Definition at line 5404 of file z3py.py.
Referenced by Context.MkDatatypeSort(), and Context.MkDatatypeSorts().
def z3py.DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpreted sort named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context. >>> A = DeclareSort('A') >>> a = Const('a', A) >>> b = Const('b', A) >>> a.sort() == A True >>> b.sort() == A True >>> a == b a == b
Definition at line 695 of file z3py.py.
def z3py.DeclareTypeVar | ( | name, | |
ctx = None |
|||
) |
def z3py.Default | ( | a | ) |
def z3py.describe_probes | ( | ) |
def z3py.describe_tactics | ( | ) |
def z3py.deserialize | ( | st | ) |
inverse function to the serialize method on ExprRef. It is made available to make it easier for users to serialize expressions back and forth between strings. Solvers can be serialized using the 'sexpr()' method.
def z3py.Diff | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.disable_trace | ( | msg | ) |
def z3py.DisjointSum | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tagged union sort base on a set of underlying sorts Example: >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
def z3py.Distinct | ( | * | args | ) |
Create a Z3 distinct expression. >>> x = Int('x') >>> y = Int('y') >>> Distinct(x, y) x != y >>> z = Int('z') >>> Distinct(x, y, z) Distinct(x, y, z) >>> simplify(Distinct(x, y, z)) Distinct(x, y, z) >>> simplify(Distinct(x, y, z), blast_distinct=True) And(Not(x == y), Not(x == z), Not(y == z))
Definition at line 1422 of file z3py.py.
def z3py.Empty | ( | s | ) |
Create the empty sequence of the given sort >>> e = Empty(StringSort()) >>> e2 = StringVal("") >>> print(e.eq(e2)) True >>> e3 = Empty(SeqSort(IntSort())) >>> print(e3) Empty(Seq(Int)) >>> e4 = Empty(ReSort(SeqSort(IntSort()))) >>> print(e4) Empty(ReSort(Seq(Int)))
Definition at line 11088 of file z3py.py.
def z3py.EmptySet | ( | s | ) |
def z3py.enable_trace | ( | msg | ) |
def z3py.ensure_prop_closures | ( | ) |
def z3py.EnumSort | ( | name, | |
values, | |||
ctx = None |
|||
) |
Return a new enumeration sort named `name` containing the given values. The result is a pair (sort, list of constants). Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Definition at line 5433 of file z3py.py.
Referenced by Context.MkEnumSort().
def z3py.eq | ( | a, | |
b | |||
) |
Return `True` if `a` and `b` are structurally identical AST nodes. >>> x = Int('x') >>> y = Int('y') >>> eq(x, y) False >>> eq(x + 1, x + 1) True >>> eq(x + 1, 1 + x) False >>> eq(simplify(x + 1), simplify(1 + x)) True
Definition at line 472 of file z3py.py.
Referenced by substitute().
def z3py.Exists | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 exists formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> q = Exists([x, y], f(x, y) >= x, skid="foo") >>> q Exists([x, y], f(x, y) >= x) >>> is_quantifier(q) True >>> r = Tactic('nnf')(q).as_expr() >>> is_quantifier(r) False
Definition at line 2290 of file z3py.py.
Referenced by Fixedpoint.abstract().
def z3py.Ext | ( | a, | |
b | |||
) |
Return extensionality index for one-dimensional arrays. >> a, b = Consts('a b', SetSort(IntSort())) >> Ext(a, b) Ext(a, b)
Definition at line 4914 of file z3py.py.
def z3py.Extract | ( | high, | |
low, | |||
a | |||
) |
Create a Z3 bit-vector extraction expression. Extract is overloaded to also work on sequence extraction. The functions SubString and SubSeq are redirected to Extract. For this case, the arguments are reinterpreted as: high - is a sequence (string) low - is an offset a - is the length to be extracted >>> x = BitVec('x', 8) >>> Extract(6, 2, x) Extract(6, 2, x) >>> Extract(6, 2, x).sort() BitVec(5) >>> simplify(Extract(StringVal("abcd"),2,1)) "c"
Definition at line 4174 of file z3py.py.
Referenced by SubSeq(), and SubString().
def z3py.FailIf | ( | p, | |
ctx = None |
|||
) |
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 8845 of file z3py.py.
def z3py.FiniteDomainSort | ( | name, | |
sz, | |||
ctx = None |
|||
) |
Create a named finite domain sort of a given size sz
Definition at line 7783 of file z3py.py.
Referenced by Context.MkFiniteDomainSort().
def z3py.FiniteDomainVal | ( | val, | |
sort, | |||
ctx = None |
|||
) |
def z3py.Float128 | ( | ctx = None | ) |
def z3py.Float16 | ( | ctx = None | ) |
def z3py.Float32 | ( | ctx = None | ) |
def z3py.Float64 | ( | ctx = None | ) |
def z3py.FloatDouble | ( | ctx = None | ) |
def z3py.FloatHalf | ( | ctx = None | ) |
def z3py.FloatQuadruple | ( | ctx = None | ) |
def z3py.FloatSingle | ( | ctx = None | ) |
def z3py.ForAll | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 forall formula. The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') >>> ForAll([x, y], f(x, y) >= x) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ]) ForAll([x, y], f(x, y) >= x) >>> ForAll([x, y], f(x, y) >= x, weight=10) ForAll([x, y], f(x, y) >= x)
Definition at line 2272 of file z3py.py.
Referenced by Fixedpoint.abstract().
def z3py.FP | ( | name, | |
fpsort, | |||
ctx = None |
|||
) |
Return a floating-point constant named `name`. `fpsort` is the floating-point sort. If `ctx=None`, then the global context is used. >>> x = FP('x', FPSort(8, 24)) >>> is_fp(x) True >>> x.ebits() 8 >>> x.sort() FPSort(8, 24) >>> word = FPSort(8, 24) >>> x2 = FP('x', word) >>> eq(x, x2) True
Definition at line 10205 of file z3py.py.
Referenced by FPs().
def z3py.fpAbs | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point absolute value expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FPVal(1.0, s) >>> fpAbs(x) fpAbs(1) >>> y = FPVal(-20.0, s) >>> y -1.25*(2**4) >>> fpAbs(y) fpAbs(-1.25*(2**4)) >>> fpAbs(-1.25*(2**4)) fpAbs(-1.25*(2**4)) >>> fpAbs(x).sort() FPSort(8, 24)
Definition at line 10248 of file z3py.py.
def z3py.fpAdd | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpAdd(rm, x, y) x + y >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ fpAdd(RTZ(), x, y) >>> fpAdd(rm, x, y).sort() FPSort(8, 24)
Definition at line 10339 of file z3py.py.
Referenced by FPRef.__add__(), and FPRef.__radd__().
def z3py.fpBVToFP | ( | v, | |
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a bit-vector term to a floating-point term. >>> x_bv = BitVecVal(0x3F800000, 32) >>> x_fp = fpBVToFP(x_bv, Float32()) >>> x_fp fpToFP(1065353216) >>> simplify(x_fp) 1
Definition at line 10661 of file z3py.py.
def z3py.fpDiv | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point division expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpDiv(rm, x, y) x / y >>> fpDiv(rm, x, y).sort() FPSort(8, 24)
Definition at line 10386 of file z3py.py.
Referenced by FPRef.__div__(), and FPRef.__rdiv__().
def z3py.fpEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpFMA | ( | rm, | |
a, | |||
b, | |||
c, | |||
ctx = None |
|||
) |
def z3py.fpFP | ( | sgn, | |
exp, | |||
sig, | |||
ctx = None |
|||
) |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. >>> s = FPSort(8, 24) >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) >>> print(x) fpFP(1, 127, 4194304) >>> xv = FPVal(-1.5, s) >>> print(xv) -1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() sat >>> xv = FPVal(+1.5, s) >>> print(xv) 1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() unsat
def z3py.fpFPToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision. >>> x_sgl = FPVal(1.0, Float32()) >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) >>> x_dbl fpToFP(RNE(), 1) >>> simplify(x_dbl) 1 >>> x_dbl.sort() FPSort(11, 53)
Definition at line 10678 of file z3py.py.
def z3py.fpGEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other >= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGEQ(x, y) x >= y >>> (x >= y).sexpr() '(fp.geq x y)'
Definition at line 10557 of file z3py.py.
Referenced by FPRef.__ge__().
def z3py.fpGT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other > self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGT(x, y) x > y >>> (x > y).sexpr() '(fp.gt x y)'
Definition at line 10545 of file z3py.py.
Referenced by FPRef.__gt__().
def z3py.fpInfinity | ( | s, | |
negative | |||
) |
def z3py.fpIsInf | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNaN | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNegative | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsPositive | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsSubnormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsZero | ( | a, | |
ctx = None |
|||
) |
def z3py.fpLEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other <= self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLEQ(x, y) x <= y >>> (x <= y).sexpr() '(fp.leq x y)'
Definition at line 10533 of file z3py.py.
Referenced by FPRef.__le__().
def z3py.fpLT | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create the Z3 floating-point expression `other < self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) x < y >>> (x < y).sexpr() '(fp.lt x y)'
Definition at line 10521 of file z3py.py.
Referenced by FPRef.__lt__().
def z3py.fpMax | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpMin | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpMinusInfinity | ( | s | ) |
def z3py.fpMinusZero | ( | s | ) |
def z3py.fpMul | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point multiplication expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpMul(rm, x, y) x * y >>> fpMul(rm, x, y).sort() FPSort(8, 24)
Definition at line 10371 of file z3py.py.
Referenced by FPRef.__mul__(), and FPRef.__rmul__().
def z3py.fpNaN | ( | s | ) |
Create a Z3 floating-point NaN term. >>> s = FPSort(8, 24) >>> set_fpa_pretty(True) >>> fpNaN(s) NaN >>> pb = get_fpa_pretty() >>> set_fpa_pretty(False) >>> fpNaN(s) fpNaN(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 10093 of file z3py.py.
Referenced by FPVal().
def z3py.fpNeg | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> fpNeg(x) -x >>> fpNeg(x).sort() FPSort(8, 24)
Definition at line 10271 of file z3py.py.
Referenced by FPRef.__neg__().
def z3py.fpNEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpPlusInfinity | ( | s | ) |
Create a Z3 floating-point +oo term. >>> s = FPSort(8, 24) >>> pb = get_fpa_pretty() >>> set_fpa_pretty(True) >>> fpPlusInfinity(s) +oo >>> set_fpa_pretty(False) >>> fpPlusInfinity(s) fpPlusInfinity(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 10110 of file z3py.py.
Referenced by FPVal().
def z3py.fpPlusZero | ( | s | ) |
def z3py.fpRealToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a real term to a floating-point term. >>> x_r = RealVal(1.5) >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) >>> x_fp fpToFP(RNE(), 3/2) >>> simplify(x_fp) 1.5
Definition at line 10698 of file z3py.py.
def z3py.fpRem | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point remainder expression. >>> s = FPSort(8, 24) >>> x = FP('x', s) >>> y = FP('y', s) >>> fpRem(x, y) fpRem(x, y) >>> fpRem(x, y).sort() FPSort(8, 24)
Definition at line 10401 of file z3py.py.
Referenced by FPRef.__mod__(), and FPRef.__rmod__().
def z3py.fpRoundToIntegral | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.FPs | ( | names, | |
fpsort, | |||
ctx = None |
|||
) |
def z3py.fpSignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a signed bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFP(RNE(), 4294967291) >>> simplify(x_fp) -1.25*(2**2)
Definition at line 10716 of file z3py.py.
def z3py.FPSort | ( | ebits, | |
sbits, | |||
ctx = None |
|||
) |
Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used. >>> Single = FPSort(8, 24) >>> Double = FPSort(11, 53) >>> Single FPSort(8, 24) >>> x = Const('x', Single) >>> eq(x, FP('x', FPSort(8, 24))) True
Definition at line 10034 of file z3py.py.
Referenced by get_default_fp_sort(), Context.mkFPSort(), Context.MkFPSort(), Context.MkFPSort128(), Context.mkFPSort128(), Context.MkFPSort16(), Context.mkFPSort16(), Context.MkFPSort32(), Context.mkFPSort32(), Context.MkFPSort64(), Context.mkFPSort64(), Context.MkFPSortDouble(), Context.mkFPSortDouble(), Context.MkFPSortHalf(), Context.mkFPSortHalf(), Context.MkFPSortQuadruple(), Context.mkFPSortQuadruple(), Context.MkFPSortSingle(), and Context.mkFPSortSingle().
def z3py.fpSqrt | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.fpSub | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point subtraction expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpSub(rm, x, y) x - y >>> fpSub(rm, x, y).sort() FPSort(8, 24)
Definition at line 10356 of file z3py.py.
Referenced by FPRef.__rsub__(), and FPRef.__sub__().
def z3py.fpToFP | ( | a1, | |
a2 = None , |
|||
a3 = None , |
|||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression from other term sorts to floating-point. From a bit-vector term in IEEE 754-2008 format: >>> x = FPVal(1.0, Float32()) >>> x_bv = fpToIEEEBV(x) >>> simplify(fpToFP(x_bv, Float32())) 1 From a floating-point term with different precision: >>> x = FPVal(1.0, Float32()) >>> x_db = fpToFP(RNE(), x, Float64()) >>> x_db.sort() FPSort(11, 53) From a real term: >>> x_r = RealVal(1.5) >>> simplify(fpToFP(RNE(), x_r, Float32())) 1.5 From a signed bit-vector term: >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> simplify(fpToFP(RNE(), x_signed, Float32())) -1.25*(2**2)
def z3py.fpToFPUnsigned | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.
Definition at line 10752 of file z3py.py.
def z3py.fpToIEEEBV | ( | x, | |
ctx = None |
|||
) |
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToIEEEBV(x) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10826 of file z3py.py.
def z3py.fpToReal | ( | x, | |
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to real. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToReal(x) >>> print(is_fp(x)) True >>> print(is_real(y)) True >>> print(is_fp(y)) False >>> print(is_real(x)) False
Definition at line 10806 of file z3py.py.
def z3py.fpToSBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToSBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10762 of file z3py.py.
def z3py.fpToUBV | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToUBV(RTZ(), x, BitVecSort(32)) >>> print(is_fp(x)) True >>> print(is_bv(y)) True >>> print(is_fp(y)) False >>> print(is_bv(x)) False
Definition at line 10784 of file z3py.py.
def z3py.fpUnsignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFPUnsigned(RNE(), 4294967291) >>> simplify(x_fp) 1*(2**32)
Definition at line 10734 of file z3py.py.
def z3py.FPVal | ( | sig, | |
exp = None , |
|||
fps = None , |
|||
ctx = None |
|||
) |
Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used. >>> v = FPVal(20.0, FPSort(8, 24)) >>> v 1.25*(2**4) >>> print("0x%.8x" % v.exponent_as_long(False)) 0x00000004 >>> v = FPVal(2.25, FPSort(8, 24)) >>> v 1.125*(2**1) >>> v = FPVal(-2.25, FPSort(8, 24)) >>> v -1.125*(2**1) >>> FPVal(-0.0, FPSort(8, 24)) -0.0 >>> FPVal(0.0, FPSort(8, 24)) +0.0 >>> FPVal(+0.0, FPSort(8, 24)) +0.0
Definition at line 10159 of file z3py.py.
Referenced by set_default_fp_sort().
def z3py.fpZero | ( | s, | |
negative | |||
) |
def z3py.FreshBool | ( | prefix = "b" , |
|
ctx = None |
|||
) |
Return a fresh Boolean constant in the given context using the given prefix. If `ctx=None`, then the global context is used. >>> b1 = FreshBool() >>> b2 = FreshBool() >>> eq(b1, b2) False
Definition at line 1811 of file z3py.py.
def z3py.FreshConst | ( | sort, | |
prefix = "c" |
|||
) |
def z3py.FreshFunction | ( | * | sig | ) |
def z3py.FreshInt | ( | prefix = "x" , |
|
ctx = None |
|||
) |
def z3py.FreshReal | ( | prefix = "b" , |
|
ctx = None |
|||
) |
def z3py.Full | ( | s | ) |
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 11108 of file z3py.py.
def z3py.FullSet | ( | s | ) |
def z3py.Function | ( | name, | |
* | sig | ||
) |
Create a new Z3 uninterpreted function with the given sorts. >>> f = Function('f', IntSort(), IntSort()) >>> f(f(0)) f(f(0))
Definition at line 881 of file z3py.py.
def z3py.get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
Definition at line 6745 of file z3py.py.
Referenced by ModelRef.get_interp().
def z3py.get_default_fp_sort | ( | ctx = None | ) |
def z3py.get_default_rounding_mode | ( | ctx = None | ) |
Retrieves the global default rounding mode.
Definition at line 9423 of file z3py.py.
Referenced by set_default_fp_sort().
def z3py.get_full_version | ( | ) |
def z3py.get_map_func | ( | a | ) |
Return the function declaration associated with a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> eq(f, get_map_func(a)) True >>> get_map_func(a) f >>> get_map_func(a)(0) f(0)
Definition at line 4722 of file z3py.py.
def z3py.get_param | ( | name | ) |
def z3py.get_var_index | ( | a | ) |
Return the de-Bruijn index of the Z3 bounded variable `a`. >>> x = Int('x') >>> y = Int('y') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # Z3 replaces x and y with bound variables when ForAll is executed. >>> q = ForAll([x, y], f(x, y) == x + y) >>> q.body() f(Var(1), Var(0)) == Var(1) + Var(0) >>> b = q.body() >>> b.arg(0) f(Var(1), Var(0)) >>> v1 = b.arg(0).arg(0) >>> v2 = b.arg(0).arg(1) >>> v1 Var(1) >>> v2 Var(0) >>> get_var_index(v1) 1 >>> get_var_index(v2) 0
Definition at line 1353 of file z3py.py.
def z3py.get_version | ( | ) |
def z3py.help_simplify | ( | ) |
def z3py.If | ( | a, | |
b, | |||
c, | |||
ctx = None |
|||
) |
Create a Z3 if-then-else expression. >>> x = Int('x') >>> y = Int('y') >>> max = If(x > y, x, y) >>> max If(x > y, x, y) >>> simplify(max) If(x <= y, y, x)
Definition at line 1399 of file z3py.py.
Referenced by BoolRef.__add__(), BoolRef.__mul__(), ArithRef.__mul__(), and Abs().
def z3py.Implies | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 implies expression. >>> p, q = Bools('p q') >>> Implies(p, q) Implies(p, q)
Definition at line 1825 of file z3py.py.
Referenced by Fixedpoint.add_rule(), and Fixedpoint.update_rule().
def z3py.IndexOf | ( | s, | |
substr, | |||
offset = None |
|||
) |
Retrieve the index of substring within a string starting at a specified offset. >>> simplify(IndexOf("abcabc", "bc", 0)) 1 >>> simplify(IndexOf("abcabc", "bc", 2)) 4
Definition at line 11192 of file z3py.py.
def z3py.InRe | ( | s, | |
re | |||
) |
Create regular expression membership test >>> re = Union(Re("a"),Re("b")) >>> print (simplify(InRe("a", re))) True >>> print (simplify(InRe("b", re))) True >>> print (simplify(InRe("c", re))) False
Definition at line 11331 of file z3py.py.
def z3py.Int | ( | name, | |
ctx = None |
|||
) |
Return an integer constant named `name`. If `ctx=None`, then the global context is used. >>> x = Int('x') >>> is_int(x) True >>> is_int(x + 1) True
Definition at line 3294 of file z3py.py.
Referenced by Ints(), and IntVector().
def z3py.Int2BV | ( | a, | |
num_bits | |||
) |
def z3py.Intersect | ( | * | args | ) |
def z3py.Ints | ( | names, | |
ctx = None |
|||
) |
def z3py.IntSort | ( | ctx = None | ) |
Return the integer sort in the given context. If `ctx=None`, then the global context is used. >>> IntSort() Int >>> x = Const('x', IntSort()) >>> is_int(x) True >>> x.sort() == IntSort() True >>> x.sort() == BoolSort() False
Definition at line 3188 of file z3py.py.
Referenced by FreshInt(), Context.getIntSort(), Int(), IntVal(), and Context.mkIntSort().
def z3py.IntToStr | ( | s | ) |
def z3py.IntVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 integer value. If `ctx=None`, then the global context is used. >>> IntVal(1) 1 >>> IntVal("100") 100
Definition at line 3234 of file z3py.py.
Referenced by SeqRef.__getitem__(), BoolRef.__mul__(), SeqRef.at(), AlgebraicNumRef.index(), and IndexOf().
def z3py.IntVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
def z3py.is_add | ( | a | ) |
def z3py.is_algebraic_value | ( | a | ) |
def z3py.is_and | ( | a | ) |
def z3py.is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application. Note that, constants are function applications with 0 arguments. >>> a = Int('a') >>> is_app(a) True >>> is_app(a + 1) True >>> is_app(IntSort()) False >>> is_app(1) False >>> is_app(IntVal(1)) True >>> x = Int('x') >>> is_app(ForAll(x, x >= 0)) False
Definition at line 1283 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
def z3py.is_app_of | ( | a, | |
k | |||
) |
Return `True` if `a` is an application of the given kind `k`. >>> x = Int('x') >>> n = x + 1 >>> is_app_of(n, Z3_OP_ADD) True >>> is_app_of(n, Z3_OP_MUL) False
Definition at line 1386 of file z3py.py.
Referenced by is_add(), is_and(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
def z3py.is_arith | ( | a | ) |
Return `True` if `a` is an arithmetical expression. >>> x = Int('x') >>> is_arith(x) True >>> is_arith(x + 1) True >>> is_arith(1) False >>> is_arith(IntVal(1)) True >>> y = Real('y') >>> is_arith(y) True >>> is_arith(y + 1) True
Definition at line 2715 of file z3py.py.
Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().
def z3py.is_arith_sort | ( | s | ) |
Return `True` if s is an arithmetical sort (type). >>> is_arith_sort(IntSort()) True >>> is_arith_sort(RealSort()) True >>> is_arith_sort(BoolSort()) False >>> n = Int('x') + 1 >>> is_arith_sort(n.sort()) True
Definition at line 2414 of file z3py.py.
Referenced by ArithSortRef.subsort().
def z3py.is_array | ( | a | ) |
def z3py.is_array_sort | ( | a | ) |
def z3py.is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 6740 of file z3py.py.
Referenced by get_as_array_func(), and ModelRef.get_interp().
def z3py.is_ast | ( | a | ) |
Return `True` if `a` is an AST node. >>> is_ast(10) False >>> is_ast(IntVal(10)) True >>> is_ast(Int('x')) True >>> is_ast(BoolSort()) True >>> is_ast(Function('f', IntSort(), IntSort())) True >>> is_ast("x") False >>> is_ast(Solver()) False
Definition at line 451 of file z3py.py.
Referenced by eq(), AstRef.eq(), and ReSort().
def z3py.is_bool | ( | a | ) |
Return `True` if `a` is a Z3 Boolean expression. >>> p = Bool('p') >>> is_bool(p) True >>> q = Bool('q') >>> is_bool(And(p, q)) True >>> x = Real('x') >>> is_bool(x) False >>> is_bool(x == 0) True
Definition at line 1611 of file z3py.py.
Referenced by is_quantifier(), and prove().
def z3py.is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression. >>> b = BitVec('b', 32) >>> is_bv(b) True >>> is_bv(b + 10) True >>> is_bv(Int('x')) False
Definition at line 3990 of file z3py.py.
Referenced by BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
def z3py.is_bv_sort | ( | s | ) |
Return True if `s` is a Z3 bit-vector sort. >>> is_bv_sort(BitVecSort(32)) True >>> is_bv_sort(IntSort()) False
Definition at line 3522 of file z3py.py.
Referenced by BitVecVal(), fpToSBV(), fpToUBV(), and BitVecSortRef.subsort().
def z3py.is_bv_value | ( | a | ) |
def z3py.is_const | ( | a | ) |
Return `True` if `a` is Z3 constant/variable expression. >>> a = Int('a') >>> is_const(a) True >>> is_const(a + 1) False >>> is_const(1) False >>> is_const(IntVal(1)) True >>> x = Int('x') >>> is_const(ForAll(x, x >= 0)) False
Definition at line 1309 of file z3py.py.
Referenced by ModelRef.__getitem__(), Solver.assert_and_track(), Optimize.assert_and_track(), ModelRef.get_interp(), is_quantifier(), and prove().
def z3py.is_const_array | ( | a | ) |
def z3py.is_default | ( | a | ) |
def z3py.is_distinct | ( | a | ) |
def z3py.is_div | ( | a | ) |
def z3py.is_eq | ( | a | ) |
Return `True` if `a` is a Z3 equality expression. >>> x, y = Ints('x y') >>> is_eq(x == y) True
Definition at line 1709 of file z3py.py.
Referenced by AstRef.__bool__().
def z3py.is_expr | ( | a | ) |
Return `True` if `a` is a Z3 expression. >>> a = Int('a') >>> is_expr(a) True >>> is_expr(a + 1) True >>> is_expr(IntSort()) False >>> is_expr(1) False >>> is_expr(IntVal(1)) True >>> x = Int('x') >>> is_expr(ForAll(x, x >= 0)) True >>> is_expr(FPVal(1.0)) True
Definition at line 1260 of file z3py.py.
Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), CharFromBv(), CharIsDigit(), Concat(), deserialize(), Diff(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), Loop(), MultiPattern(), Option(), Plus(), Range(), Replace(), SeqMapI(), simplify(), Sqrt(), Star(), StrFromCode(), StrToCode(), substitute(), substitute_funs(), substitute_vars(), and ModelRef.update_value().
def z3py.is_false | ( | a | ) |
Return `True` if `a` is the Z3 false expression. >>> p = Bool('p') >>> is_false(p) False >>> is_false(False) False >>> is_false(BoolVal(False)) True
Definition at line 1647 of file z3py.py.
Referenced by AstRef.__bool__().
def z3py.is_finite_domain | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain expression. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain(b) True >>> is_finite_domain(Int('x')) False
Definition at line 7814 of file z3py.py.
Referenced by is_finite_domain_value().
def z3py.is_finite_domain_sort | ( | s | ) |
Return True if `s` is a Z3 finite-domain sort. >>> is_finite_domain_sort(FiniteDomainSort('S', 100)) True >>> is_finite_domain_sort(IntSort()) False
Definition at line 7791 of file z3py.py.
Referenced by FiniteDomainVal().
def z3py.is_finite_domain_value | ( | a | ) |
def z3py.is_fp | ( | a | ) |
Return `True` if `a` is a Z3 floating-point expression. >>> b = FP('b', FPSort(8, 24)) >>> is_fp(b) True >>> is_fp(b + 1.0) True >>> is_fp(Int('x')) False
Definition at line 10005 of file z3py.py.
Referenced by fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp_value(), and set_default_fp_sort().
def z3py.is_fp_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point sort. >>> is_fp_sort(FPSort(8, 24)) True >>> is_fp_sort(IntSort()) False
Definition at line 9589 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().
def z3py.is_fp_value | ( | a | ) |
def z3py.is_fprm | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode expression. >>> rm = RNE() >>> is_fprm(rm) True >>> rm = 1.0 >>> is_fprm(rm) False
Definition at line 9849 of file z3py.py.
Referenced by fpFPToFP(), fpNeg(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), and is_fprm_value().
def z3py.is_fprm_sort | ( | s | ) |
def z3py.is_fprm_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 9862 of file z3py.py.
Referenced by set_default_rounding_mode().
def z3py.is_func_decl | ( | a | ) |
Return `True` if `a` is a Z3 function declaration. >>> f = Function('f', IntSort(), IntSort()) >>> is_func_decl(f) True >>> x = Real('x') >>> is_func_decl(x) False
Definition at line 868 of file z3py.py.
Referenced by Map(), prove(), substitute_funs(), and ModelRef.update_value().
def z3py.is_ge | ( | a | ) |
def z3py.is_gt | ( | a | ) |
def z3py.is_idiv | ( | a | ) |
def z3py.is_implies | ( | a | ) |
def z3py.is_int | ( | a | ) |
def z3py.is_int_value | ( | a | ) |
Return `True` if `a` is an integer value of sort Int. >>> is_int_value(IntVal(1)) True >>> is_int_value(1) False >>> is_int_value(Int('x')) False >>> n = Int('x') + 1 >>> n x + 1 >>> n.arg(1) 1 >>> is_int_value(n.arg(1)) True >>> is_int_value(RealVal("1/3")) False >>> is_int_value(RealVal(1)) False
Definition at line 2782 of file z3py.py.
def z3py.is_is_int | ( | a | ) |
def z3py.is_K | ( | a | ) |
def z3py.is_le | ( | a | ) |
def z3py.is_lt | ( | a | ) |
def z3py.is_map | ( | a | ) |
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 4697 of file z3py.py.
Referenced by get_map_func().
def z3py.is_mod | ( | a | ) |
def z3py.is_mul | ( | a | ) |
def z3py.is_not | ( | a | ) |
def z3py.is_or | ( | a | ) |
def z3py.is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) >>> q ForAll(x, f(x) == 0) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) f(Var(0))
Definition at line 1973 of file z3py.py.
Referenced by is_quantifier(), and MultiPattern().
def z3py.is_probe | ( | p | ) |
def z3py.is_quantifier | ( | a | ) |
def z3py.is_rational_value | ( | a | ) |
Return `True` if `a` is rational value of sort Real. >>> is_rational_value(RealVal(1)) True >>> is_rational_value(RealVal("3/5")) True >>> is_rational_value(IntVal(1)) False >>> is_rational_value(1) False >>> n = Real('x') + 1 >>> n.arg(1) 1 >>> is_rational_value(n.arg(1)) True >>> is_rational_value(Real('x')) False
Definition at line 2806 of file z3py.py.
def z3py.is_re | ( | s | ) |
def z3py.is_real | ( | a | ) |
Return `True` if `a` is a real expression. >>> x = Int('x') >>> is_real(x + 1) False >>> y = Real('y') >>> is_real(y) True >>> is_real(y + 1) True >>> is_real(1) False >>> is_real(RealVal(1)) True
Definition at line 2755 of file z3py.py.
Referenced by fpRealToFP(), and fpToFP().
def z3py.is_select | ( | a | ) |
def z3py.is_seq | ( | a | ) |
Return `True` if `a` is a Z3 sequence expression. >>> print (is_seq(Unit(IntVal(0)))) True >>> print (is_seq(StringVal("abc"))) True
Definition at line 11027 of file z3py.py.
Referenced by CharIsDigit(), Concat(), and Extract().
def z3py.is_sort | ( | s | ) |
Return `True` if `s` is a Z3 sort. >>> is_sort(IntSort()) True >>> is_sort(Int('x')) False >>> is_expr(Int('x')) True
Definition at line 647 of file z3py.py.
Referenced by ArraySort(), CreateDatatypes(), FreshFunction(), Function(), IsSubset(), K(), PropagateFunction(), prove(), RecFunction(), and Var().
def z3py.is_store | ( | a | ) |
def z3py.is_string | ( | a | ) |
def z3py.is_string_value | ( | a | ) |
def z3py.is_sub | ( | a | ) |
def z3py.is_to_int | ( | a | ) |
def z3py.is_to_real | ( | a | ) |
def z3py.is_true | ( | a | ) |
Return `True` if `a` is the Z3 true expression. >>> p = Bool('p') >>> is_true(p) False >>> is_true(simplify(p == p)) True >>> x = Real('x') >>> is_true(x == 0) False >>> # True is a Python Boolean expression >>> is_true(True) False
Definition at line 1629 of file z3py.py.
Referenced by AstRef.__bool__().
def z3py.is_var | ( | a | ) |
Return `True` if `a` is variable. Z3 uses de-Bruijn indices for representing bound variables in quantifiers. >>> x = Int('x') >>> is_var(x) False >>> is_const(x) True >>> f = Function('f', IntSort(), IntSort()) >>> # Z3 replaces x with bound variables when ForAll is executed. >>> q = ForAll(x, f(x) == x) >>> b = q.body() >>> b f(Var(0)) == Var(0) >>> b.arg(1) Var(0) >>> is_var(b.arg(1)) True
Definition at line 1328 of file z3py.py.
Referenced by get_var_index().
def z3py.IsInt | ( | a | ) |
Return the Z3 predicate IsInt(a). >>> x = Real('x') >>> IsInt(x + "1/2") IsInt(x + 1/2) >>> solve(IsInt(x + "1/2"), x > 0, x < 1) [x = 1/2] >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2") no solution
Definition at line 3440 of file z3py.py.
def z3py.IsMember | ( | e, | |
s | |||
) |
def z3py.IsSubset | ( | a, | |
b | |||
) |
def z3py.K | ( | dom, | |
v | |||
) |
Return a Z3 constant array expression. >>> a = K(IntSort(), 10) >>> a K(Int, 10) >>> a.sort() Array(Int, Int) >>> i = Int('i') >>> a[i] K(Int, 10)[i] >>> simplify(a[i]) 10
Definition at line 4892 of file z3py.py.
Referenced by ModelRef.get_interp().
def z3py.Lambda | ( | vs, | |
body | |||
) |
Create a Z3 lambda expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> mem0 = Array('mem0', IntSort(), IntSort()) >>> lo, hi, e, i = Ints('lo hi e i') >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i])) >>> mem1 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
Definition at line 2311 of file z3py.py.
Referenced by Context.MkLambda().
def z3py.LastIndexOf | ( | s, | |
substr | |||
) |
def z3py.Length | ( | s | ) |
Obtain the length of a sequence 's' >>> l = Length(StringVal("abc")) >>> simplify(l) 3
Definition at line 11221 of file z3py.py.
Referenced by NativeContext.MkAdd(), NativeContext.MkAnd(), NativeContext.MkApp(), NativeContext.MkFreshFuncDecl(), NativeContext.MkFuncDecl(), NativeContext.MkMul(), NativeContext.MkOr(), NativeContext.MkSub(), and NativeContext.MkTupleSort().
def z3py.LinearOrder | ( | a, | |
index | |||
) |
def z3py.Loop | ( | re, | |
lo, | |||
hi = 0 |
|||
) |
Create the regular expression accepting between a lower and upper bound repetitions >>> re = Loop(Re("a"), 1, 3) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("aaaa", re))) False >>> print(simplify(InRe("", re))) False
Definition at line 11433 of file z3py.py.
def z3py.LShR | ( | a, | |
b | |||
) |
Create the Z3 expression logical right shift. Use the operator >> for the arithmetical right shift. >>> x, y = BitVecs('x y', 32) >>> LShR(x, y) LShR(x, y) >>> (x >> y).sexpr() '(bvashr x y)' >>> LShR(x, y).sexpr() '(bvlshr x y)' >>> BitVecVal(4, 3) 4 >>> BitVecVal(4, 3).as_signed_long() -4 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long() -2 >>> simplify(BitVecVal(4, 3) >> 1) 6 >>> simplify(LShR(BitVecVal(4, 3), 1)) 2 >>> simplify(BitVecVal(2, 3) >> 1) 1 >>> simplify(LShR(BitVecVal(2, 3), 1)) 1
Definition at line 4345 of file z3py.py.
def z3py.main_ctx | ( | ) |
Return a reference to the global Z3 context. >>> x = Real('x') >>> x.ctx == main_ctx() True >>> c = Context() >>> c == main_ctx() False >>> x2 = Real('x', c) >>> x2.ctx == c True >>> eq(x, x2) False
Definition at line 239 of file z3py.py.
Referenced by CharIsDigit(), help_simplify(), and simplify_param_descrs().
def z3py.Map | ( | f, | |
* | args | ||
) |
Return a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> a1 = Array('a1', IntSort(), IntSort()) >>> a2 = Array('a2', IntSort(), IntSort()) >>> b = Map(f, a1, a2) >>> b Map(f, a1, a2) >>> prove(b[0] == f(a1[0], a2[0])) proved
Definition at line 4869 of file z3py.py.
Referenced by Context.Context().
def z3py.Model | ( | ctx = None | ) |
Definition at line 6735 of file z3py.py.
Referenced by Goal.ConvertModel(), Goal.convertModel(), Optimize.getModel(), Solver.getModel(), and Optimize.set_on_model().
def z3py.MultiPattern | ( | * | args | ) |
Create a Z3 multi-pattern using the given expressions `*args` >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ]) >>> q ForAll(x, f(x) != g(x)) >>> q.num_patterns() 1 >>> is_pattern(q.pattern(0)) True >>> q.pattern(0) MultiPattern(f(Var(0)), g(Var(0)))
Definition at line 1991 of file z3py.py.
def z3py.Not | ( | a, | |
ctx = None |
|||
) |
Create a Z3 not expression or probe. >>> p = Bool('p') >>> Not(Not(p)) Not(Not(p)) >>> simplify(Not(Not(p))) p
Definition at line 1855 of file z3py.py.
Referenced by BoolRef.__invert__(), fpNEQ(), mk_not(), and prove().
def z3py.on_clause_eh | ( | ctx, | |
p, | |||
n, | |||
dep, | |||
clause | |||
) |
def z3py.open_log | ( | fname | ) |
def z3py.Option | ( | re | ) |
Create the regular expression that optionally accepts the argument. >>> re = Option(Re("a")) >>> print(simplify(InRe("a", re))) True >>> print(simplify(InRe("", re))) True >>> print(simplify(InRe("aa", re))) False
Definition at line 11398 of file z3py.py.
def z3py.Or | ( | * | args | ) |
Create a Z3 or-expression or or-probe. >>> p, q, r = Bools('p q r') >>> Or(p, q, r) Or(p, q, r) >>> P = BoolVector('p', 5) >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 1922 of file z3py.py.
Referenced by BoolRef.__or__(), and ApplyResult.as_expr().
def z3py.OrElse | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = OrElse(Tactic('split-clause'), Tactic('skip')) >>> # Tactic split-clause fails if there is no clause in the given goal. >>> t(x == 0) [[x == 0]] >>> t(Or(x == 0, x == 1)) [[x == 0], [x == 1]]
def z3py.ParAndThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
def z3py.ParOr | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail). >>> x = Int('x') >>> t = ParOr(Tactic('simplify'), Tactic('fail')) >>> t(x + 1 == 2) [[x == 1]]
def z3py.parse_smt2_file | ( | f, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a file in SMT 2.0 format using the given sorts and decls. This function is similar to parse_smt2_string().
Definition at line 9399 of file z3py.py.
def z3py.parse_smt2_string | ( | s, | |
sorts = {} , |
|||
decls = {} , |
|||
ctx = None |
|||
) |
Parse a string in SMT 2.0 format using the given sorts and decls. The arguments sorts and decls are Python dictionaries used to initialize the symbol table used for the SMT 2.0 parser. >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))') [x > 0, x < 10] >>> x, y = Ints('x y') >>> f = Function('f', IntSort(), IntSort()) >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f}) [x + f(y) > 0] >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() }) [a > 0]
Definition at line 9378 of file z3py.py.
def z3py.ParThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. >>> x, y = Ints('x y') >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) >>> t(And(Or(x == 1, x == 2), y == x + 1)) [[x == 1, y == 2], [x == 2, y == 3]]
Definition at line 8503 of file z3py.py.
Referenced by ParAndThen().
def z3py.PartialOrder | ( | a, | |
index | |||
) |
def z3py.PbEq | ( | args, | |
k, | |||
ctx = None |
|||
) |
def z3py.PbGe | ( | args, | |
k | |||
) |
def z3py.PbLe | ( | args, | |
k | |||
) |
def z3py.PiecewiseLinearOrder | ( | a, | |
index | |||
) |
def z3py.Plus | ( | re | ) |
def z3py.PrefixOf | ( | a, | |
b | |||
) |
def z3py.probe_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the probe named `name`. >>> d = probe_description('memory')
Definition at line 8799 of file z3py.py.
Referenced by describe_probes().
def z3py.probes | ( | ctx = None | ) |
Return a list of all available probes in Z3. >>> l = probes() >>> l.count('memory') == 1 True
Definition at line 8788 of file z3py.py.
Referenced by describe_probes().
def z3py.Product | ( | * | args | ) |
Create the product of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Product(a, b, c) a*b*c >>> Product([a, b, c]) a*b*c >>> A = IntVector('a', 5) >>> Product(A) a__0*a__1*a__2*a__3*a__4
Definition at line 9040 of file z3py.py.
def z3py.PropagateFunction | ( | name, | |
* | sig | ||
) |
Create a function that gets tracked by user propagator. Every term headed by this function symbol is tracked. If a term is fixed and the fixed callback is registered a callback is invoked that the term headed by this function is fixed.
Definition at line 11677 of file z3py.py.
def z3py.prove | ( | claim, | |
show = False , |
|||
** | keywords | ||
) |
def z3py.Q | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.Range | ( | lo, | |
hi, | |||
ctx = None |
|||
) |
Create the range regular expression over two sequences of length 1 >>> range = Range("a","z") >>> print(simplify(InRe("b", range))) True >>> print(simplify(InRe("bb", range))) False
Definition at line 11448 of file z3py.py.
def z3py.RatVal | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 3265 of file z3py.py.
Referenced by Q().
def z3py.Re | ( | s, | |
ctx = None |
|||
) |
def z3py.Real | ( | name, | |
ctx = None |
|||
) |
Return a real constant named `name`. If `ctx=None`, then the global context is used. >>> x = Real('x') >>> is_real(x) True >>> is_real(x + 1) True
Definition at line 3347 of file z3py.py.
Referenced by Reals(), and RealVector().
def z3py.Reals | ( | names, | |
ctx = None |
|||
) |
def z3py.RealSort | ( | ctx = None | ) |
Return the real sort in the given context. If `ctx=None`, then the global context is used. >>> RealSort() Real >>> x = Const('x', RealSort()) >>> is_real(x) True >>> is_int(x) False >>> x.sort() == RealSort() True
Definition at line 3205 of file z3py.py.
Referenced by FreshReal(), Context.getRealSort(), Context.mkRealSort(), Real(), RealVal(), and RealVar().
def z3py.RealVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 real value. `val` may be a Python int, long, float or string representing a number in decimal or rational notation. If `ctx=None`, then the global context is used. >>> RealVal(1) 1 >>> RealVal(1).sort() Real >>> RealVal("3/5") 3/5 >>> RealVal("1.5") 3/2
Definition at line 3246 of file z3py.py.
Referenced by Cbrt(), deserialize(), AlgebraicNumRef.index(), RatVal(), and Sqrt().
def z3py.RealVar | ( | idx, | |
ctx = None |
|||
) |
Create a real free variable. Free variables are used to create quantified formulas. They are also used to create polynomials. >>> RealVar(0) Var(0)
Definition at line 1503 of file z3py.py.
Referenced by RealVarVector().
def z3py.RealVarVector | ( | n, | |
ctx = None |
|||
) |
def z3py.RealVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
def z3py.RecAddDefinition | ( | f, | |
args, | |||
body | |||
) |
Set the body of a recursive function. Recursive definitions can be simplified if they are applied to ground arguments. >>> ctx = Context() >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx)) >>> n = Int('n', ctx) >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1))) >>> simplify(fac(5)) 120 >>> s = Solver(ctx=ctx) >>> s.add(fac(n) < 3) >>> s.check() sat >>> s.model().eval(fac(5)) 120
Definition at line 945 of file z3py.py.
def z3py.RecFunction | ( | name, | |
* | sig | ||
) |
Create a new Z3 recursive with the given sorts.
Definition at line 927 of file z3py.py.
def z3py.Repeat | ( | t, | |
max = 4294967295 , |
|||
ctx = None |
|||
) |
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached. >>> x, y = Ints('x y') >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y) >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip'))) >>> r = t(c) >>> for subgoal in r: print(subgoal) [x == 0, y == 0, x > y] [x == 0, y == 1, x > y] [x == 1, y == 0, x > y] [x == 1, y == 1, x > y] >>> t = Then(t, Tactic('propagate-values')) >>> t(c) [[x == 1, y == 0]]
Definition at line 8552 of file z3py.py.
def z3py.RepeatBitVec | ( | n, | |
a | |||
) |
Return an expression representing `n` copies of `a`. >>> x = BitVec('x', 8) >>> n = RepeatBitVec(4, x) >>> n RepeatBitVec(4, x) >>> n.size() 32 >>> v0 = BitVecVal(10, 4) >>> print("%.x" % v0.as_long()) a >>> v = simplify(RepeatBitVec(4, v0)) >>> v.size() 16 >>> print("%.x" % v.as_long()) aaaa
Definition at line 4467 of file z3py.py.
def z3py.Replace | ( | s, | |
src, | |||
dst | |||
) |
Replace the first occurrence of 'src' by 'dst' in 's' >>> r = Replace("aaa", "a", "b") >>> simplify(r) "baa"
Definition at line 11177 of file z3py.py.
def z3py.reset_params | ( | ) |
def z3py.ReSort | ( | s | ) |
Definition at line 11311 of file z3py.py.
Referenced by Context.MkReSort().
def z3py.RNA | ( | ctx = None | ) |
Definition at line 9814 of file z3py.py.
Referenced by get_default_rounding_mode().
def z3py.RNE | ( | ctx = None | ) |
Definition at line 9804 of file z3py.py.
Referenced by get_default_rounding_mode().
def z3py.RotateLeft | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the left `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateLeft(a, b) RotateLeft(a, b) >>> simplify(RotateLeft(a, 0)) a >>> simplify(RotateLeft(a, 16)) a
Definition at line 4377 of file z3py.py.
def z3py.RotateRight | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the right `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateRight(a, b) RotateRight(a, b) >>> simplify(RotateRight(a, 0)) a >>> simplify(RotateRight(a, 16)) a
Definition at line 4393 of file z3py.py.
def z3py.RoundTowardNegative | ( | ctx = None | ) |
def z3py.RoundTowardPositive | ( | ctx = None | ) |
def z3py.RoundTowardZero | ( | ctx = None | ) |
def z3py.RTN | ( | ctx = None | ) |
def z3py.RTP | ( | ctx = None | ) |
def z3py.RTZ | ( | ctx = None | ) |
def z3py.Select | ( | a, | |
* | args | ||
) |
def z3py.SeqFoldLeft | ( | f, | |
a, | |||
s | |||
) |
def z3py.SeqFoldLeftI | ( | f, | |
i, | |||
a, | |||
s | |||
) |
Definition at line 11250 of file z3py.py.
def z3py.SeqMap | ( | f, | |
s | |||
) |
def z3py.SeqMapI | ( | f, | |
i, | |||
s | |||
) |
def z3py.SeqSort | ( | s | ) |
Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True
Definition at line 10898 of file z3py.py.
Referenced by Context.MkSeqSort().
def z3py.set_option | ( | * | args, |
** | kws | ||
) |
def z3py.set_param | ( | * | args, |
** | kws | ||
) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 271 of file z3py.py.
Referenced by set_option().
def z3py.SetAdd | ( | s, | |
e | |||
) |
def z3py.SetComplement | ( | s | ) |
def z3py.SetDel | ( | s, | |
e | |||
) |
def z3py.SetDifference | ( | a, | |
b | |||
) |
The set difference of a and b >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetDifference(a, b) setminus(a, b)
Definition at line 5044 of file z3py.py.
def z3py.SetHasSize | ( | a, | |
k | |||
) |
def z3py.SetIntersect | ( | * | args | ) |
Take the union of sets >>> a = Const('a', SetSort(IntSort())) >>> b = Const('b', SetSort(IntSort())) >>> SetIntersect(a, b) intersection(a, b)
Definition at line 4999 of file z3py.py.
def z3py.SetSort | ( | s | ) |
Sets.
Create a set sort over element sort s
Definition at line 4963 of file z3py.py.
Referenced by Context.MkSetSort().
def z3py.SetUnion | ( | * | args | ) |
def z3py.SignExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra sign-bits. >>> x = BitVec('x', 16) >>> n = SignExt(8, x) >>> n.size() 24 >>> n SignExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(SignExt(6, v0)) >>> v 254 >>> v.size() 8 >>> print("%.x" % v.as_long()) fe
Definition at line 4409 of file z3py.py.
def z3py.SimpleSolver | ( | ctx = None , |
|
logFile = None |
|||
) |
def z3py.simplify | ( | a, | |
* | arguments, | ||
** | keywords | ||
) |
Utils.
Simplify the expression `a` using the given options. This function has many options. Use `help_simplify` to obtain the complete list. >>> x = Int('x') >>> y = Int('y') >>> simplify(x + 1 + y + x + 1) 2 + 2*x + y >>> simplify((x + 1)*(y + 1), som=True) 1 + x + y + x*y >>> simplify(Distinct(x, y, 1), blast_distinct=True) And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1)))
Definition at line 8904 of file z3py.py.
Referenced by Q(), RatVal(), and Expr< R extends Sort >.simplify().
def z3py.simplify_param_descrs | ( | ) |
def z3py.solve | ( | * | args, |
** | keywords | ||
) |
def z3py.solve_using | ( | s, | |
* | args, | ||
** | keywords | ||
) |
Solve the constraints `*args` using solver `s`. This is a simple function for creating demonstrations. It is similar to `solve`, but it uses the given solver `s`. It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check.
Definition at line 9196 of file z3py.py.
def z3py.SolverFor | ( | logic, | |
ctx = None , |
|||
logFile = None |
|||
) |
Create a solver customized for the given logic. The parameter `logic` is a string. It should be contains the name of a SMT-LIB logic. See https://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 7465 of file z3py.py.
def z3py.Sqrt | ( | a, | |
ctx = None |
|||
) |
def z3py.SRem | ( | a, | |
b | |||
) |
Create the Z3 expression signed remainder. Use the operator % for signed modulus, and URem() for unsigned remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> SRem(x, y) SRem(x, y) >>> SRem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)'
Definition at line 4324 of file z3py.py.
def z3py.Star | ( | re | ) |
def z3py.Store | ( | a, | |
* | args | ||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Store(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 4836 of file z3py.py.
Referenced by ModelRef.get_interp().
def z3py.StrFromCode | ( | c | ) |
def z3py.String | ( | name, | |
ctx = None |
|||
) |
Return a string constant named `name`. If `ctx=None`, then the global context is used. >>> x = String('x')
Definition at line 11061 of file z3py.py.
Referenced by Context.Context(), Statistics.getEntries(), Statistics.getKeys(), Context.getProbeNames(), Context.getSimplifierNames(), Context.getTacticNames(), Context.mkString(), Strings(), and FuncInterp< R extends Sort >.toString().
def z3py.Strings | ( | names, | |
ctx = None |
|||
) |
def z3py.StringSort | ( | ctx = None | ) |
def z3py.StringVal | ( | s, | |
ctx = None |
|||
) |
create a string expression
Definition at line 11054 of file z3py.py.
Referenced by CharIsDigit(), deserialize(), Extract(), and AlgebraicNumRef.index().
def z3py.StrToCode | ( | s | ) |
def z3py.StrToInt | ( | s | ) |
def z3py.SubSeq | ( | s, | |
offset, | |||
length | |||
) |
def z3py.substitute | ( | t, | |
* | m | ||
) |
Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to. >>> x = Int('x') >>> y = Int('y') >>> substitute(x + 1, (x, y + 1)) y + 1 + 1 >>> f = Function('f', IntSort(), IntSort()) >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1))) 1 + 1
Definition at line 8939 of file z3py.py.
Referenced by Expr< R extends Sort >.substitute().
def z3py.substitute_funs | ( | t, | |
* | m | ||
) |
Apply substitution m on t, m is a list of pairs of a function and expression (from, to) Every occurrence in to of the function from is replaced with the expression to. The expression to can have free variables, that refer to the arguments of from. For examples, see
Definition at line 8992 of file z3py.py.
def z3py.substitute_vars | ( | t, | |
* | m | ||
) |
Substitute the free variables in t with the expression in m. >>> v0 = Var(0, IntSort()) >>> v1 = Var(1, IntSort()) >>> x = Int('x') >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> # replace v0 with x+1 and v1 with x >>> substitute_vars(f(v0, v1), x + 1, x) f(x + 1, x)
Definition at line 8972 of file z3py.py.
def z3py.SubString | ( | s, | |
offset, | |||
length | |||
) |
def z3py.SuffixOf | ( | a, | |
b | |||
) |
def z3py.Sum | ( | * | args | ) |
Create the sum of the Z3 expressions. >>> a, b, c = Ints('a b c') >>> Sum(a, b, c) a + b + c >>> Sum([a, b, c]) a + b + c >>> A = IntVector('a', 5) >>> Sum(A) a__0 + a__1 + a__2 + a__3 + a__4
Definition at line 9014 of file z3py.py.
def z3py.tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 8593 of file z3py.py.
Referenced by describe_tactics().
def z3py.tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3. >>> l = tactics() >>> l.count('simplify') == 1 True
Definition at line 8582 of file z3py.py.
Referenced by describe_tactics().
def z3py.Then | ( | * | ts, |
** | ks | ||
) |
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). >>> x, y = Ints('x y') >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
def z3py.to_Ast | ( | ptr | ) |
Definition at line 11502 of file z3py.py.
Referenced by on_clause_eh(), user_prop_created(), user_prop_decide(), user_prop_diseq(), user_prop_eq(), and user_prop_fixed().
def z3py.to_AstVectorObj | ( | ptr | ) |
def z3py.to_ContextObj | ( | ptr | ) |
def z3py.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(), DeclareTypeVar(), 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 z3py.ToInt | ( | a | ) |
def z3py.ToReal | ( | a | ) |
def z3py.TransitiveClosure | ( | f | ) |
Given a binary relation R, such that the two arguments have the same sort create the transitive closure relation R+. The transitive closure R+ is a new relation.
Definition at line 11495 of file z3py.py.
def z3py.TreeOrder | ( | a, | |
index | |||
) |
def z3py.TryFor | ( | t, | |
ms, | |||
ctx = None |
|||
) |
Return a tactic that applies `t` to a given goal for `ms` milliseconds. If `t` does not terminate in `ms` milliseconds, then it fails.
Definition at line 8573 of file z3py.py.
def z3py.TupleSort | ( | name, | |
sorts, | |||
ctx = None |
|||
) |
Create a named tuple sort base on a set of underlying sorts Example: >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
Definition at line 5409 of file z3py.py.
Referenced by Context.MkTupleSort(), and Context.mkTupleSort().
def z3py.UDiv | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) division `self / other`. Use the operator / for signed division. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> UDiv(x, y) UDiv(x, y) >>> UDiv(x, y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)'
Definition at line 4282 of file z3py.py.
def z3py.UGE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other >= self`. Use the operator >= for signed greater than or equal to. >>> x, y = BitVecs('x y', 32) >>> UGE(x, y) UGE(x, y) >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)'
Definition at line 4246 of file z3py.py.
def z3py.UGT | ( | a, | |
b | |||
) |
def z3py.ULE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other <= self`. Use the operator <= for signed less than or equal to. >>> x, y = BitVecs('x y', 32) >>> ULE(x, y) ULE(x, y) >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)'
Definition at line 4210 of file z3py.py.
def z3py.ULT | ( | a, | |
b | |||
) |
def z3py.Union | ( | * | args | ) |
Create union of regular expressions. >>> re = Union(Re("a"), Re("b"), Re("c")) >>> print (simplify(InRe("d", re))) False
Definition at line 11345 of file z3py.py.
Referenced by ReRef.__add__().
def z3py.Update | ( | a, | |
* | args | ||
) |
Return a Z3 store array expression. >>> a = Array('a', IntSort(), IntSort()) >>> i, v = Ints('i v') >>> s = Update(a, i, v) >>> s.sort() Array(Int, Int) >>> prove(s[i] == v) proved >>> j = Int('j') >>> prove(Implies(i != j, s[j] == a[j])) proved
Definition at line 4793 of file z3py.py.
Referenced by Store().
def z3py.URem | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) remainder `self % other`. Use the operator % for signed modulus, and SRem() for signed remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> URem(x, y) URem(x, y) >>> URem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> URem(x, y).sexpr() '(bvurem x y)'
Definition at line 4303 of file z3py.py.
def z3py.user_prop_fresh | ( | ctx, | |
_new_ctx | |||
) |
def z3py.Var | ( | idx, | |
s | |||
) |
Create a Z3 free variable. Free variables are used to create quantified formulas. A free variable with index n is bound when it occurs within the scope of n+1 quantified declarations. >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False
Definition at line 1488 of file z3py.py.
Referenced by RealVar().
def z3py.When | ( | p, | |
t, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. >>> t = When(Probe('size') > 2, Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 8867 of file z3py.py.
def z3py.With | ( | t, | |
* | args, | ||
** | keys | ||
) |
Return a tactic that applies tactic `t` using the given configuration options. >>> x, y = Ints('x y') >>> t = With(Tactic('simplify'), som=True) >>> t((x + 1)*(y + 2) == 0) [[2*x + y + x*y == -2]]
Definition at line 8524 of file z3py.py.
def z3py.WithParams | ( | t, | |
p | |||
) |
def z3py.Xor | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 Xor expression. >>> p, q = Bools('p q') >>> Xor(p, q) Xor(p, q) >>> simplify(Xor(p, q)) Not(p == q)
Definition at line 1839 of file z3py.py.
Referenced by BoolRef.__xor__().
def z3py.z3_debug | ( | ) |
Definition at line 62 of file z3py.py.
Referenced by 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(), Diff(), Distinct(), 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(), Loop(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Option(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), Plus(), PropagateFunction(), prove(), Range(), RatVal(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), Star(), 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 z3py.ZeroExt | ( | n, | |
a | |||
) |
Return a bit-vector expression with `n` extra zero-bits. >>> x = BitVec('x', 16) >>> n = ZeroExt(8, x) >>> n.size() 24 >>> n ZeroExt(8, x) >>> n.sort() BitVec(24) >>> v0 = BitVecVal(2, 2) >>> v0 2 >>> v0.size() 2 >>> v = simplify(ZeroExt(6, v0)) >>> v 2 >>> v.size() 8
Definition at line 4439 of file z3py.py.
sat = CheckSatResult(Z3_L_TRUE) |
unknown = CheckSatResult(Z3_L_UNDEF) |
unsat = CheckSatResult(Z3_L_FALSE) |