Functions | |
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 | main_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 | 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 | 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_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 | 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 | 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 | 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 | 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 (d, r) |
def | Array (name, dom, rng) |
def | Update (a, i, v) |
def | Default (a) |
def | Store (a, i, v) |
def | Select (a, i) |
def | Map (f, args) |
def | K (dom, v) |
def | Ext (a, b) |
def | is_select (a) |
def | is_store (a) |
def | CreateDatatypes (ds) |
def | EnumSort (name, values, ctx=None) |
def | args2params (arguments, keywords, ctx=None) |
def | is_as_array (n) |
def | get_as_array_func (n) |
def | SolverFor (logic, ctx=None) |
def | SimpleSolver (ctx=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 | Repeat (t, max=4294967295, ctx=None) |
def | TryFor (t, ms, ctx=None) |
def | tactics (ctx=None) |
def | tactic_description (name, ctx=None) |
def | describe_tactics () |
def | is_probe (p) |
def | probes (ctx=None) |
def | probe_description (name, ctx=None) |
def | describe_probes () |
def | FailIf (p, ctx=None) |
def | When (p, t, ctx=None) |
def | Cond (p, t1, t2, ctx=None) |
def | simplify (a, arguments, keywords) |
Utils. More... | |
def | help_simplify () |
def | simplify_param_descrs () |
def | substitute (t, m) |
def | substitute_vars (t, m) |
def | Sum (args) |
def | Product (args) |
def | AtMost (args) |
def | AtLeast (args) |
def | PbLe (args, k) |
def | PbEq (args, k) |
def | solve (args, keywords) |
def | solve_using (s, args, keywords) |
def | prove (claim, keywords) |
def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
def | Interpolant (a, ctx=None) |
def | tree_interpolant (pat, p=None, ctx=None) |
def | binary_interpolant (a, b, p=None, ctx=None) |
def | sequence_interpolant (v, p=None, ctx=None) |
def | get_default_rounding_mode (ctx=None) |
def | set_default_rounding_mode (rm, ctx=None) |
def | get_default_fp_sort (ctx=None) |
def | set_default_fp_sort (ebits, sbits, ctx=None) |
def | Float16 (ctx=None) |
def | FloatHalf (ctx=None) |
def | Float32 (ctx=None) |
def | FloatSingle (ctx=None) |
def | Float64 (ctx=None) |
def | FloatDouble (ctx=None) |
def | Float128 (ctx=None) |
def | FloatQuadruple (ctx=None) |
def | is_fp_sort (s) |
def | is_fprm_sort (s) |
def | RoundNearestTiesToEven (ctx=None) |
def | RNE (ctx=None) |
def | RoundNearestTiesToAway (ctx=None) |
def | RNA (ctx=None) |
def | RoundTowardPositive (ctx=None) |
def | RTP (ctx=None) |
def | RoundTowardNegative (ctx=None) |
def | RTN (ctx=None) |
def | RoundTowardZero (ctx=None) |
def | RTZ (ctx=None) |
def | is_fprm (a) |
def | is_fprm_value (a) |
def | is_fp (a) |
def | is_fp_value (a) |
def | FPSort (ebits, sbits, ctx=None) |
def | fpNaN (s) |
def | fpPlusInfinity (s) |
def | fpMinusInfinity (s) |
def | fpInfinity (s, negative) |
def | fpPlusZero (s) |
def | fpMinusZero (s) |
def | fpZero (s, negative) |
def | FPVal (sig, exp=None, fps=None, ctx=None) |
def | FP (name, fpsort, ctx=None) |
def | FPs (names, fpsort, ctx=None) |
def | fpAbs (a, ctx=None) |
def | fpNeg (a, ctx=None) |
def | fpAdd (rm, a, b, ctx=None) |
def | fpSub (rm, a, b, ctx=None) |
def | fpMul (rm, a, b, ctx=None) |
def | fpDiv (rm, a, b, ctx=None) |
def | fpRem (a, b, ctx=None) |
def | fpMin (a, b, ctx=None) |
def | fpMax (a, b, ctx=None) |
def | fpFMA (rm, a, b, c, ctx=None) |
def | fpSqrt (rm, a, ctx=None) |
def | fpRoundToIntegral (rm, a, ctx=None) |
def | fpIsNaN (a, ctx=None) |
def | fpIsInf (a, ctx=None) |
def | fpIsZero (a, ctx=None) |
def | fpIsNormal (a, ctx=None) |
def | fpIsSubnormal (a, ctx=None) |
def | fpIsNegative (a, ctx=None) |
def | fpIsPositive (a, ctx=None) |
def | fpLT (a, b, ctx=None) |
def | fpLEQ (a, b, ctx=None) |
def | fpGT (a, b, ctx=None) |
def | fpGEQ (a, b, ctx=None) |
def | fpEQ (a, b, ctx=None) |
def | fpNEQ (a, b, ctx=None) |
def | fpFP (sgn, exp, sig, ctx=None) |
def | fpToFP (a1, a2=None, a3=None, ctx=None) |
def | fpBVToFP (v, sort, ctx=None) |
def | fpFPToFP (rm, v, sort, ctx=None) |
def | fpRealToFP (rm, v, sort, ctx=None) |
def | fpSignedToFP (rm, v, sort, ctx=None) |
def | fpUnsignedToFP (rm, v, sort, ctx=None) |
def | fpToFPUnsigned (rm, x, s, ctx=None) |
def | fpToSBV (rm, x, s, ctx=None) |
def | fpToUBV (rm, x, s, ctx=None) |
def | fpToReal (x, ctx=None) |
def | fpToIEEEBV (x, ctx=None) |
def | StringSort (ctx=None) |
def | SeqSort (s) |
def | is_seq (a) |
def | is_string (a) |
def | is_string_value (a) |
def | StringVal (s, ctx=None) |
def | String (name, ctx=None) |
def | Strings (names, ctx=None) |
def | Empty (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) |
def | IndexOf (s, substr, offset) |
def | Length (s) |
def | Re (s, ctx=None) |
def | ReSort (s) |
def | is_re (s) |
def | InRe (s, re) |
def | Union (args) |
def | Plus (re) |
def | Option (re) |
def | Star (re) |
Variables | |
sat = CheckSatResult(Z3_L_TRUE) | |
unsat = CheckSatResult(Z3_L_FALSE) | |
unknown = CheckSatResult(Z3_L_UNDEF) | |
def z3py.And | ( | args | ) |
Create a Z3 and-expression or and-probe. >>> p, q, r = Bools('p q r') >>> And(p, q, r) And(p, q, r) >>> P = BoolVector('p', 5) >>> And(P) And(p__0, p__1, p__2, p__3, p__4)
Definition at line 1550 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Bool(), Bools(), BoolVector(), Fixedpoint.query(), tree_interpolant(), 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 7049 of file z3py.py.
Referenced by Context.Then(), and Then().
def z3py.append_log | ( | s | ) |
def z3py.args2params | ( | arguments, | |
keywords, | |||
ctx = None |
|||
) |
Convert python arguments into a Z3_params object. A ':' is added to the keywords, and '_' is replaced with '-' >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) (params model true relevancy 2 elim_and true)
Definition at line 4644 of file z3py.py.
Referenced by Tactic.apply(), Fixedpoint.set(), Optimize.set(), simplify(), and With().
def z3py.Array | ( | name, | |
dom, | |||
rng | |||
) |
Return an array constant named `name` with the given domain and range sorts. >>> a = Array('a', IntSort(), IntSort()) >>> a.sort() Array(Int, Int) >>> a[0] a[0]
Definition at line 4131 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ArraySort(), ArrayRef.domain(), get_map_func(), is_array(), is_const_array(), is_K(), is_map(), is_select(), is_store(), K(), Map(), ArrayRef.range(), Select(), ArrayRef.sort(), Store(), and Update().
def z3py.ArraySort | ( | d, | |
r | |||
) |
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 4110 of file z3py.py.
Referenced by ArraySortRef.domain(), Context.mkArraySort(), Context.MkArraySort(), ArraySortRef.range(), Sort.toString(), and Sort.ToString().
def z3py.AtLeast | ( | args | ) |
def z3py.AtMost | ( | args | ) |
def z3py.binary_interpolant | ( | a, | |
b, | |||
p = None , |
|||
ctx = None |
|||
) |
Compute an interpolant for a binary conjunction. If a & b is unsatisfiable, returns an interpolant for a & b. This is a formula phi such that 1) a implies phi 2) b implies not phi 3) All the uninterpreted symbols of phi occur in both a and b. If a & b is satisfiable, raises an object of class ModelRef that represents a model of a &b. If neither a proof of unsatisfiability nor a model is obtained (for example, because of a timeout, or because models are disabled) then None is returned. If parameters p are supplied, these are used in creating the solver that determines satisfiability. x = Int('x') print(binary_interpolant(x<0,x>2)) Not(x >= 0)
Definition at line 7968 of file z3py.py.
def z3py.BitVec | ( | name, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort. If `ctx=None`, then the global context is used. >>> x = BitVec('x', 16) >>> is_bv(x) True >>> x.size() 16 >>> x.sort() BitVec(16) >>> word = BitVecSort(16) >>> x2 = BitVec('x', word) >>> eq(x, x2) True
Definition at line 3560 of file z3py.py.
Referenced by BitVecRef.__add__(), BitVecRef.__and__(), BitVecRef.__div__(), BitVecRef.__invert__(), BitVecRef.__mod__(), BitVecRef.__mul__(), BitVecRef.__neg__(), BitVecRef.__or__(), BitVecRef.__pos__(), BitVecRef.__radd__(), BitVecRef.__rand__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), BitVecRef.__rrshift__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BitVecs(), BitVecSort(), BV2Int(), Extract(), is_bv(), is_bv_value(), RepeatBitVec(), SignExt(), BitVecRef.size(), BitVecRef.sort(), SRem(), UDiv(), URem(), and ZeroExt().
def z3py.BitVecs | ( | names, | |
bv, | |||
ctx = None |
|||
) |
Return a tuple of bit-vector constants of size bv. >>> x, y, z = BitVecs('x y z', 16) >>> x.size() 16 >>> x.sort() BitVec(16) >>> Sum(x, y, z) 0 + x + y + z >>> Product(x, y, z) 1*x*y*z >>> simplify(Product(x, y, z)) x*y*z
Definition at line 3583 of file z3py.py.
Referenced by BitVecRef.__ge__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__rshift__(), LShR(), RotateLeft(), RotateRight(), UGE(), UGT(), ULE(), and ULT().
def z3py.BitVecSort | ( | sz, | |
ctx = None |
|||
) |
Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. >>> Byte = BitVecSort(8) >>> Word = BitVecSort(16) >>> Byte BitVec(8) >>> x = Const('x', Byte) >>> eq(x, BitVec('x', 8)) True
Definition at line 3530 of file z3py.py.
Referenced by BitVec(), BitVecSortRef.cast(), fpSignedToFP(), fpToFP(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), is_bv_sort(), Context.mkBitVecSort(), Context.MkBitVecSort(), BitVecSortRef.size(), BitVecRef.sort(), Sort.toString(), and Sort.ToString().
def z3py.BitVecVal | ( | val, | |
bv, | |||
ctx = None |
|||
) |
Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used. >>> v = BitVecVal(10, 32) >>> v 10 >>> print("0x%.8x" % v.as_long()) 0x0000000a
Definition at line 3544 of file z3py.py.
Referenced by BitVecRef.__lshift__(), BitVecRef.__rshift__(), BitVecNumRef.as_long(), BitVecNumRef.as_signed_long(), Concat(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), is_bv_value(), LShR(), RepeatBitVec(), SignExt(), and ZeroExt().
def z3py.Bool | ( | name, | |
ctx = None |
|||
) |
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used. >>> p = Bool('p') >>> q = Bool('q') >>> And(p, q) And(p, q)
Definition at line 1442 of file z3py.py.
Referenced by Solver.assert_and_track(), and Not().
def z3py.Bools | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Boolean constants. `names` is a single string containing all names separated by blank spaces. If `ctx=None`, then the global context is used. >>> p, q, r = Bools('p q r') >>> And(p, Or(q, r)) And(p, Or(q, r))
Definition at line 1453 of file z3py.py.
Referenced by And(), Solver.consequences(), Implies(), Or(), Solver.unsat_core(), and Xor().
def z3py.BoolSort | ( | ctx = None | ) |
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used. >>> BoolSort() Bool >>> p = Const('p', BoolSort()) >>> is_bool(p) True >>> r = Function('r', IntSort(), IntSort(), BoolSort()) >>> r(0, 1) r(0, 1) >>> is_bool(r(0, 1)) True
Definition at line 1407 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ArraySort(), Fixedpoint.assert_exprs(), ArraySortRef.domain(), ArrayRef.domain(), Context.getBoolSort(), If(), IntSort(), is_arith_sort(), Context.mkBoolSort(), Context.MkBoolSort(), ArraySortRef.range(), ArrayRef.range(), ArrayRef.sort(), Sort.toString(), and Sort.ToString().
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 1424 of file z3py.py.
Referenced by ApplyResult.as_expr(), BoolSortRef.cast(), Re(), and Solver.to_smt2().
def z3py.BoolVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
Return a list of Boolean constants of size `sz`. The constants are named using the given prefix. If `ctx=None`, then the global context is used. >>> P = BoolVector('p', 3) >>> P [p__0, p__1, p__2] >>> And(P) And(p__0, p__1, p__2)
Definition at line 1468 of file z3py.py.
Referenced by And(), and Or().
def z3py.BV2Int | ( | a, | |
is_signed = False |
|||
) |
Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) >>> BV2Int(b).sort() Int >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) >>> x > BV2Int(b, is_signed=False) x > BV2Int(b) >>> x > BV2Int(b, is_signed=True) x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2]
Definition at line 3508 of file z3py.py.
def z3py.BVRedAnd | ( | a | ) |
def z3py.BVRedOr | ( | a | ) |
def z3py.Cbrt | ( | a, | |
ctx = None |
|||
) |
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 3603 of file z3py.py.
Referenced by Contains(), and BitVecRef.size().
def z3py.Cond | ( | p, | |
t1, | |||
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise. >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
Definition at line 7452 of file z3py.py.
Referenced by If().
def z3py.Const | ( | name, | |
sort | |||
) |
Create a constant of the given sort. >>> Const('x', IntSort()) x
Definition at line 1193 of file z3py.py.
Referenced by BitVecSort(), Consts(), FPSort(), IntSort(), RealSort(), and DatatypeSortRef.recognizer().
def z3py.Consts | ( | names, | |
sort | |||
) |
Create a 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 1204 of file z3py.py.
Referenced by EnumSort.ConstDecl(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def z3py.Contains | ( | a, | |
b | |||
) |
def z3py.CreateDatatypes | ( | ds | ) |
Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects. In the following example we define a Tree-List using two mutually recursive datatypes. >>> TreeList = Datatype('TreeList') >>> Tree = Datatype('Tree') >>> # Tree has two constructors: leaf and node >>> Tree.declare('leaf', ('val', IntSort())) >>> # a node contains a list of trees >>> Tree.declare('node', ('children', TreeList)) >>> TreeList.declare('nil') >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList)) >>> Tree, TreeList = CreateDatatypes(Tree, TreeList) >>> Tree.val(Tree.leaf(10)) val(leaf(10)) >>> simplify(Tree.val(Tree.leaf(10))) 10 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))) >>> n1 node(cons(leaf(10), cons(leaf(20), nil))) >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) >>> simplify(n2 == n1) False >>> simplify(TreeList.car(Tree.children(n2)) == n1) True
Definition at line 4385 of file z3py.py.
Referenced by Datatype.create().
def z3py.DeclareSort | ( | name, | |
ctx = None |
|||
) |
Create a new uninterpred 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 600 of file z3py.py.
Referenced by ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sorts().
def z3py.Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 4165 of file z3py.py.
Referenced by is_default().
def z3py.describe_probes | ( | ) |
def z3py.describe_tactics | ( | ) |
def z3py.disable_trace | ( | msg | ) |
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 1162 of file z3py.py.
def z3py.Empty | ( | s | ) |
def z3py.enable_trace | ( | msg | ) |
def z3py.EnumSort | ( | name, | |
values, | |||
ctx = None |
|||
) |
Return a new enumeration sort named `name` containing the given values. The result is a pair (sort, list of constants). Example: >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
Definition at line 4574 of file z3py.py.
Referenced by Context.mkEnumSort(), Context.MkEnumSort(), and EnumSort.TesterDecl().
def z3py.eq | ( | a, | |
b | |||
) |
Return `True` if `a` and `b` are structurally identical AST nodes. >>> x = Int('x') >>> y = Int('y') >>> eq(x, y) False >>> eq(x + 1, x + 1) True >>> eq(x + 1, 1 + x) False >>> eq(simplify(x + 1), simplify(1 + x)) True
Definition at line 400 of file z3py.py.
Referenced by BitVec(), BitVecSort(), FP(), FPSort(), FreshBool(), FreshInt(), FreshReal(), get_map_func(), Select(), and substitute().
def z3py.Exists | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 exists formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> 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 1895 of file z3py.py.
Referenced by Fixedpoint.abstract(), and QuantifierRef.is_forall().
def z3py.Ext | ( | a, | |
b | |||
) |
def z3py.Extract | ( | high, | |
low, | |||
a | |||
) |
Create a Z3 bit-vector extraction expression, or create a string extraction expression. >>> 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 3648 of file z3py.py.
def z3py.FailIf | ( | p, | |
ctx = None |
|||
) |
Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal. >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 7415 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 6563 of file z3py.py.
Referenced by Context.mkFiniteDomainSort(), Context.MkFiniteDomainSort(), Sort.toString(), and Sort.ToString().
def z3py.FiniteDomainVal | ( | val, | |
sort, | |||
ctx = None |
|||
) |
def z3py.Float128 | ( | ctx = None | ) |
def z3py.Float16 | ( | ctx = None | ) |
def z3py.Float32 | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 8155 of file z3py.py.
Referenced by FPRef.__neg__(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), and fpUnsignedToFP().
def z3py.Float64 | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 8165 of file z3py.py.
Referenced by fpFPToFP(), and fpToFP().
def z3py.FloatDouble | ( | ctx = None | ) |
def z3py.FloatHalf | ( | ctx = None | ) |
def z3py.FloatQuadruple | ( | ctx = None | ) |
def z3py.FloatSingle | ( | ctx = None | ) |
def z3py.ForAll | ( | vs, | |
body, | |||
weight = 1 , |
|||
qid = "" , |
|||
skid = "" , |
|||
patterns = [] , |
|||
no_patterns = [] |
|||
) |
Create a Z3 forall formula. The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> 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 1876 of file z3py.py.
Referenced by Fixedpoint.abstract(), QuantifierRef.body(), QuantifierRef.children(), QuantifierRef.is_forall(), is_pattern(), is_quantifier(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.FP | ( | name, | |
fpsort, | |||
ctx = None |
|||
) |
Return a floating-point constant named `name`. `fpsort` is the floating-point sort. If `ctx=None`, then the global context is used. >>> x = FP('x', FPSort(8, 24)) >>> is_fp(x) True >>> x.ebits() 8 >>> x.sort() FPSort(8, 24) >>> word = FPSort(8, 24) >>> x2 = FP('x', word) >>> eq(x, x2) True
Definition at line 8717 of file z3py.py.
Referenced by FPRef.__add__(), FPRef.__div__(), FPRef.__mul__(), FPRef.__neg__(), FPRef.__radd__(), FPRef.__rdiv__(), FPRef.__rmul__(), FPRef.__rsub__(), FPRef.__sub__(), fpAdd(), fpDiv(), fpIsInf(), fpIsNaN(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRem(), FPSort(), fpSub(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp(), is_fp_value(), and FPRef.sort().
def z3py.fpAbs | ( | a, | |
ctx = None |
|||
) |
Create a Z3 floating-point absolute value expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FPVal(1.0, s) >>> fpAbs(x) fpAbs(1) >>> y = FPVal(-20.0, s) >>> y -1.25*(2**4) >>> fpAbs(y) fpAbs(-1.25*(2**4)) >>> fpAbs(-1.25*(2**4)) fpAbs(-1.25*(2**4)) >>> fpAbs(x).sort() FPSort(8, 24)
Definition at line 8758 of file z3py.py.
def z3py.fpAdd | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
Create a Z3 floating-point addition expression. >>> s = FPSort(8, 24) >>> rm = RNE() >>> x = FP('x', s) >>> y = FP('y', s) >>> fpAdd(rm, x, y) fpAdd(RNE(), x, y) >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ x + y >>> fpAdd(rm, x, y).sort() FPSort(8, 24)
Definition at line 8847 of file z3py.py.
Referenced by FPs().
def z3py.fpBVToFP | ( | v, | |
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a bit-vector term to a floating-point term. >>> x_bv = BitVecVal(0x3F800000, 32) >>> x_fp = fpBVToFP(x_bv, Float32()) >>> x_fp fpToFP(1065353216) >>> simplify(x_fp) 1
Definition at line 9144 of file z3py.py.
def z3py.fpDiv | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
def z3py.fpEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpFMA | ( | rm, | |
a, | |||
b, | |||
c, | |||
ctx = None |
|||
) |
def z3py.fpFP | ( | sgn, | |
exp, | |||
sig, | |||
ctx = None |
|||
) |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp. >>> s = FPSort(8, 24) >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23)) >>> print(x) fpFP(1, 127, 4194304) >>> xv = FPVal(-1.5, s) >>> print(xv) -1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() sat >>> xv = FPVal(+1.5, s) >>> print(xv) 1.5 >>> slvr = Solver() >>> slvr.add(fpEQ(x, xv)) >>> slvr.check() unsat
def z3py.fpFPToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a floating-point term to a floating-point term of different precision. >>> x_sgl = FPVal(1.0, Float32()) >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64()) >>> x_dbl fpToFP(RNE(), 1) >>> simplify(x_dbl) 1 >>> x_dbl.sort() FPSort(11, 53)
Definition at line 9160 of file z3py.py.
def z3py.fpGEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpGT | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpInfinity | ( | s, | |
negative | |||
) |
def z3py.fpIsInf | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNaN | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNegative | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsNormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsPositive | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsSubnormal | ( | a, | |
ctx = None |
|||
) |
def z3py.fpIsZero | ( | a, | |
ctx = None |
|||
) |
def z3py.fpLEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpLT | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpMax | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpMin | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpMinusInfinity | ( | s | ) |
def z3py.fpMinusZero | ( | s | ) |
def z3py.fpMul | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
def z3py.fpNaN | ( | s | ) |
Create a Z3 floating-point NaN term. >>> s = FPSort(8, 24) >>> set_fpa_pretty(True) >>> fpNaN(s) NaN >>> pb = get_fpa_pretty() >>> set_fpa_pretty(False) >>> fpNaN(s) fpNaN(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 8614 of file z3py.py.
def z3py.fpNeg | ( | a, | |
ctx = None |
|||
) |
def z3py.fpNEQ | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpPlusInfinity | ( | s | ) |
Create a Z3 floating-point +oo term. >>> s = FPSort(8, 24) >>> pb = get_fpa_pretty() >>> set_fpa_pretty(True) >>> fpPlusInfinity(s) +oo >>> set_fpa_pretty(False) >>> fpPlusInfinity(s) fpPlusInfinity(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 8630 of file z3py.py.
def z3py.fpPlusZero | ( | s | ) |
def z3py.fpRealToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a real term to a floating-point term. >>> x_r = RealVal(1.5) >>> x_fp = fpRealToFP(RNE(), x_r, Float32()) >>> x_fp fpToFP(RNE(), 3/2) >>> simplify(x_fp) 1.5
Definition at line 9179 of file z3py.py.
def z3py.fpRem | ( | a, | |
b, | |||
ctx = None |
|||
) |
def z3py.fpRoundToIntegral | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.FPs | ( | names, | |
fpsort, | |||
ctx = None |
|||
) |
Return an array of floating-point constants. >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) fpMul(RNE(), fpAdd(RNE(), x, y), z)
Definition at line 8740 of file z3py.py.
Referenced by fpEQ(), fpGEQ(), fpGT(), fpLEQ(), fpLT(), and fpNEQ().
def z3py.fpSignedToFP | ( | rm, | |
v, | |||
sort, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression that represents the conversion from a signed bit-vector term (encoding an integer) to a floating-point term. >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32()) >>> x_fp fpToFP(RNE(), 4294967291) >>> simplify(x_fp) -1.25*(2**2)
Definition at line 9196 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 8556 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(), FPNumRef.exponent_as_long(), FP(), fpAbs(), fpAdd(), fpDiv(), fpEQ(), fpFP(), fpFPToFP(), fpGEQ(), fpGT(), fpIsInf(), fpIsNaN(), fpLEQ(), fpLT(), fpMax(), fpMin(), fpMul(), fpNaN(), fpNeg(), fpNEQ(), fpPlusInfinity(), fpRem(), FPs(), fpSub(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FPVal(), is_fp(), is_fp_sort(), is_fp_value(), is_fprm_sort(), FPNumRef.isNegative(), Context.MkFPRTZ(), Context.mkFPSort(), Context.mkFPSort128(), Context.MkFPSort128(), Context.mkFPSort16(), Context.MkFPSort16(), Context.mkFPSort32(), Context.MkFPSort32(), Context.mkFPSort64(), Context.MkFPSort64(), Context.mkFPSortDouble(), Context.MkFPSortDouble(), Context.mkFPSortHalf(), Context.MkFPSortHalf(), Context.mkFPSortQuadruple(), Context.MkFPSortQuadruple(), Context.mkFPSortSingle(), Context.MkFPSortSingle(), FPSortRef.sbits(), FPRef.sbits(), FPNumRef.sign(), FPNumRef.significand(), FPRef.sort(), Sort.toString(), and Sort.ToString().
def z3py.fpSqrt | ( | rm, | |
a, | |||
ctx = None |
|||
) |
def z3py.fpSub | ( | rm, | |
a, | |||
b, | |||
ctx = None |
|||
) |
def z3py.fpToFP | ( | a1, | |
a2 = None , |
|||
a3 = None , |
|||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression from other term sorts to floating-point. From a bit-vector term in IEEE 754-2008 format: >>> x = FPVal(1.0, Float32()) >>> x_bv = fpToIEEEBV(x) >>> simplify(fpToFP(x_bv, Float32())) 1 From a floating-point term with different precision: >>> x = FPVal(1.0, Float32()) >>> x_db = fpToFP(RNE(), x, Float64()) >>> x_db.sort() FPSort(11, 53) From a real term: >>> x_r = RealVal(1.5) >>> simplify(fpToFP(RNE(), x_r, Float32())) 1.5 From a signed bit-vector term: >>> x_signed = BitVecVal(-5, BitVecSort(32)) >>> simplify(fpToFP(RNE(), x_signed, Float32())) -1.25*(2**2)
Definition at line 9106 of file z3py.py.
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), and fpSignedToFP().
def z3py.fpToFPUnsigned | ( | rm, | |
x, | |||
s, | |||
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.
Definition at line 9230 of file z3py.py.
Referenced by fpUnsignedToFP().
def z3py.fpToIEEEBV | ( | x, | |
ctx = None |
|||
) |
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector represenatation 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 9300 of file z3py.py.
Referenced by fpToFP().
def z3py.fpToReal | ( | x, | |
ctx = None |
|||
) |
Create a Z3 floating-point conversion expression, from floating-point expression to real. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToReal(x) >>> print(is_fp(x)) True >>> print(is_real(y)) True >>> print(is_fp(y)) False >>> print(is_real(x)) False
Definition at line 9281 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
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
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 9213 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()) 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 8673 of file z3py.py.
Referenced by fpAbs(), fpFP(), fpFPToFP(), fpToFP(), and is_fp_value().
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 1482 of file z3py.py.
def z3py.FreshInt | ( | prefix = 'x' , |
|
ctx = None |
|||
) |
Return a fresh integer constant in the given context using the given prefix. >>> x = FreshInt() >>> y = FreshInt() >>> eq(x, y) False >>> x.sort() Int
Definition at line 2843 of file z3py.py.
def z3py.FreshReal | ( | prefix = 'b' , |
|
ctx = None |
|||
) |
Return a fresh real constant in the given context using the given prefix. >>> x = FreshReal() >>> y = FreshReal() >>> eq(x, y) False >>> x.sort() Real
Definition at line 2895 of file z3py.py.
def z3py.Function | ( | name, | |
sig | |||
) |
Create a new Z3 uninterpreted function with the given sorts. >>> f = Function('f', IntSort(), IntSort()) >>> f(f(0)) f(f(0))
Definition at line 738 of file z3py.py.
Referenced by ModelRef.__getitem__(), ModelRef.__len__(), FuncEntry.arg_value(), FuncInterp.arity(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), QuantifierRef.children(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), QuantifierRef.is_forall(), is_map(), is_pattern(), is_quantifier(), Map(), MultiPattern(), FuncEntry.num_args(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
def z3py.get_default_rounding_mode | ( | ctx = None | ) |
def z3py.get_full_version | ( | ) |
def z3py.get_map_func | ( | a | ) |
Return the function declaration associated with a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort()) >>> b = Array('b', IntSort(), IntSort()) >>> a = Map(f, b) >>> eq(f, get_map_func(a)) True >>> get_map_func(a) f >>> get_map_func(a)(0) f(0)
Definition at line 4093 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 1096 of file z3py.py.
def z3py.get_version | ( | ) |
def z3py.get_version_string | ( | ) |
def z3py.help_simplify | ( | ) |
def z3py.If | ( | a, | |
b, | |||
c, | |||
ctx = None |
|||
) |
Create a Z3 if-then-else expression. >>> x = Int('x') >>> y = Int('y') >>> max = If(x > y, x, y) >>> max If(x > y, x, y) >>> simplify(max) If(x <= y, y, x)
Definition at line 1140 of file z3py.py.
Referenced by BoolRef.__mul__(), and BV2Int().
def z3py.Implies | ( | a, | |
b, | |||
ctx = None |
|||
) |
Create a Z3 implies expression. >>> p, q = Bools('p q') >>> Implies(p, q) Implies(p, q) >>> simplify(Implies(p, q)) Or(Not(p), q)
Definition at line 1495 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Solver.consequences(), Store(), Solver.unsat_core(), Update(), and Fixedpoint.update_rule().
def z3py.IndexOf | ( | s, | |
substr, | |||
offset | |||
) |
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
def z3py.InRe | ( | s, | |
re | |||
) |
def z3py.Int | ( | name, | |
ctx = None |
|||
) |
Return an integer constant named `name`. If `ctx=None`, then the global context is used. >>> x = Int('x') >>> is_int(x) True >>> is_int(x + 1) True
Definition at line 2808 of file z3py.py.
Referenced by ArithRef.__add__(), AstVector.__contains__(), AstMap.__contains__(), ArithRef.__div__(), Statistics.__getattr__(), ArrayRef.__getitem__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ArithRef.__mod__(), ArithRef.__neg__(), ArithRef.__pos__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rsub__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), Goal.add(), Solver.add(), Goal.append(), Solver.append(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.assertions(), binary_interpolant(), QuantifierRef.body(), BV2Int(), Solver.check(), QuantifierRef.children(), ModelRef.decls(), AstMap.erase(), ModelRef.eval(), ModelRef.evaluate(), Exists(), ForAll(), ModelRef.get_interp(), Statistics.get_key_value(), Goal.insert(), Solver.insert(), Interpolant(), is_arith(), is_arith_sort(), is_bv(), QuantifierRef.is_forall(), is_fp(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_int_value(), is_pattern(), is_quantifier(), ArithSortRef.is_real(), is_real(), is_select(), is_to_real(), K(), AstMap.keys(), Statistics.keys(), Solver.model(), MultiPattern(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), Solver.pop(), AstVector.push(), Solver.push(), Solver.reason_unknown(), AstMap.reset(), Solver.reset(), AstVector.resize(), Select(), sequence_interpolant(), Solver.sexpr(), Goal.simplify(), ArithRef.sort(), Solver.statistics(), Store(), ToReal(), Goal.translate(), AstVector.translate(), tree_interpolant(), Update(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
def z3py.Interpolant | ( | a, | |
ctx = None |
|||
) |
Create an interpolation operator. The argument is an interpolation pattern (see tree_interpolant). >>> x = Int('x') >>> print(Interpolant(x>0)) interp(x > 0)
Definition at line 7889 of file z3py.py.
Referenced by tree_interpolant().
def z3py.Ints | ( | names, | |
ctx = None |
|||
) |
Return a tuple of Integer constants. >>> x, y, z = Ints('x y z') >>> Sum(x, y, z) x + y + z
Definition at line 2820 of file z3py.py.
Referenced by ArithRef.__ge__(), Goal.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), Goal.__len__(), ArithRef.__lt__(), Goal.depth(), Goal.get(), Goal.inconsistent(), is_add(), is_div(), is_ge(), is_gt(), is_idiv(), is_le(), is_lt(), is_mod(), is_mul(), is_sub(), Goal.prec(), Goal.size(), Store(), Solver.unsat_core(), and Update().
def z3py.IntSort | ( | ctx = None | ) |
Return the integer sort in the given context. If `ctx=None`, then the global context is used. >>> IntSort() Int >>> x = Const('x', IntSort()) >>> is_int(x) True >>> x.sort() == IntSort() True >>> x.sort() == BoolSort() False
Definition at line 2705 of file z3py.py.
Referenced by ArrayRef.__getitem__(), ModelRef.__getitem__(), ModelRef.__len__(), DatatypeSortRef.accessor(), FuncEntry.arg_value(), FuncInterp.arity(), Array(), ArraySort(), FuncEntry.as_list(), FuncInterp.as_list(), QuantifierRef.body(), ArithSortRef.cast(), QuantifierRef.children(), DatatypeSortRef.constructor(), Datatype.create(), CreateDatatypes(), Datatype.declare(), ModelRef.decls(), Default(), ArraySortRef.domain(), ArrayRef.domain(), FuncInterp.else_value(), Empty(), FuncInterp.entry(), Exists(), ForAll(), ModelRef.get_interp(), get_map_func(), Context.getIntSort(), is_arith_sort(), is_array(), is_bv_sort(), is_const_array(), is_default(), QuantifierRef.is_forall(), is_fp_sort(), is_K(), is_map(), is_pattern(), is_quantifier(), is_select(), is_store(), SeqSortRef.is_string(), K(), Map(), Context.mkIntSort(), Context.MkIntSort(), MultiPattern(), FuncEntry.num_args(), DatatypeSortRef.num_constructors(), FuncInterp.num_entries(), QuantifierRef.num_patterns(), QuantifierRef.num_vars(), QuantifierRef.pattern(), ArraySortRef.range(), ArrayRef.range(), DatatypeSortRef.recognizer(), Select(), SeqSort(), ArrayRef.sort(), Store(), Sort.toString(), Sort.ToString(), Update(), FuncEntry.value(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and QuantifierRef.weight().
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 2752 of file z3py.py.
Referenced by AstMap.__len__(), ArithRef.__mod__(), ArithRef.__pow__(), ArithRef.__rpow__(), AstMap.__setitem__(), IntNumRef.as_long(), IntNumRef.as_string(), is_arith(), is_int(), is_int_value(), is_rational_value(), is_seq(), AstMap.keys(), AstMap.reset(), and SeqSort().
def z3py.IntVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
def z3py.is_add | ( | a | ) |
def z3py.is_algebraic_value | ( | a | ) |
def z3py.is_and | ( | a | ) |
def z3py.is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application. Note that, constants are function applications with 0 arguments. >>> a = Int('a') >>> is_app(a) True >>> is_app(a + 1) True >>> is_app(IntSort()) False >>> is_app(1) False >>> is_app(IntVal(1)) True >>> x = Int('x') >>> is_app(ForAll(x, x >= 0)) False
Definition at line 1029 of file z3py.py.
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), expr.hi(), is_app_of(), expr.is_const(), is_const(), expr.lo(), ExprRef.num_args(), and expr.operator Z3_app().
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 1128 of file z3py.py.
Referenced by is_and(), is_distinct(), is_eq(), is_false(), is_not(), is_or(), and is_true().
def z3py.is_arith | ( | a | ) |
def z3py.is_arith_sort | ( | s | ) |
def z3py.is_array | ( | a | ) |
Return `True` if `a` is a Z3 array expression. >>> a = Array('a', IntSort(), IntSort()) >>> is_array(a) True >>> is_array(Store(a, 0, 1)) True >>> is_array(a[0]) False
Definition at line 4033 of file z3py.py.
Referenced by sort.array_domain(), and sort.array_range().
def z3py.is_as_array | ( | n | ) |
def z3py.is_ast | ( | a | ) |
Return `True` if `a` is an AST node. >>> is_ast(10) False >>> is_ast(IntVal(10)) True >>> is_ast(Int('x')) True >>> is_ast(BoolSort()) True >>> is_ast(Function('f', IntSort(), IntSort())) True >>> is_ast("x") False >>> is_ast(Solver()) False
Definition at line 380 of file z3py.py.
Referenced by AstRef.eq(), and eq().
def z3py.is_bool | ( | a | ) |
Return `True` if `a` is a Z3 Boolean expression. >>> p = Bool('p') >>> is_bool(p) True >>> q = Bool('q') >>> is_bool(And(p, q)) True >>> x = Real('x') >>> is_bool(x) False >>> is_bool(x == 0) True
Definition at line 1307 of file z3py.py.
Referenced by BoolSort(), and prove().
def z3py.is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression. >>> b = BitVec('b', 32) >>> is_bv(b) True >>> is_bv(b + 10) True >>> is_bv(Int('x')) False
Definition at line 3481 of file z3py.py.
Referenced by BitVec(), sort.bv_size(), fpToIEEEBV(), fpToSBV(), fpToUBV(), Product(), and Sum().
def z3py.is_bv_sort | ( | s | ) |
def z3py.is_bv_value | ( | a | ) |
def z3py.is_const | ( | a | ) |
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 1387 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 1007 of file z3py.py.
Referenced by SortRef.cast(), BoolSortRef.cast(), ExprRef.children(), is_var(), simplify(), substitute(), and substitute_vars().
def z3py.is_false | ( | a | ) |
Return `True` if `a` is the Z3 false expression. >>> p = Bool('p') >>> is_false(p) False >>> is_false(False) False >>> is_false(BoolVal(False)) True
Definition at line 1341 of file z3py.py.
Referenced by AstRef.__bool__(), and BoolVal().
def z3py.is_finite_domain | ( | a | ) |
Return `True` if `a` is a Z3 finite-domain expression. >>> s = FiniteDomainSort('S', 100) >>> b = Const('b', s) >>> is_finite_domain(b) True >>> is_finite_domain(Int('x')) False
Definition at line 6592 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 6570 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 8529 of file z3py.py.
Referenced by FP(), fpToIEEEBV(), fpToReal(), fpToSBV(), and fpToUBV().
def z3py.is_fp_sort | ( | s | ) |
def z3py.is_fp_value | ( | a | ) |
def z3py.is_fprm | ( | a | ) |
def z3py.is_fprm_sort | ( | s | ) |
def z3py.is_fprm_value | ( | a | ) |
def z3py.is_func_decl | ( | a | ) |
def z3py.is_ge | ( | a | ) |
def z3py.is_gt | ( | a | ) |
def z3py.is_idiv | ( | a | ) |
def z3py.is_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 2310 of file z3py.py.
Referenced by Int(), IntSort(), sort.is_arith(), and RealSort().
def z3py.is_int_value | ( | a | ) |
Return `True` if `a` is an integer value of sort Int. >>> is_int_value(IntVal(1)) True >>> is_int_value(1) False >>> is_int_value(Int('x')) False >>> n = Int('x') + 1 >>> n x + 1 >>> n.arg(1) 1 >>> is_int_value(n.arg(1)) True >>> is_int_value(RealVal("1/3")) False >>> is_int_value(RealVal(1)) False
Definition at line 2352 of file z3py.py.
def z3py.is_is_int | ( | a | ) |
def z3py.is_K | ( | a | ) |
def z3py.is_le | ( | a | ) |
def z3py.is_lt | ( | a | ) |
def z3py.is_map | ( | a | ) |
def z3py.is_mod | ( | a | ) |
def z3py.is_mul | ( | a | ) |
def z3py.is_not | ( | a | ) |
def z3py.is_or | ( | a | ) |
def z3py.is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> 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 1630 of file z3py.py.
Referenced by MultiPattern().
def z3py.is_probe | ( | p | ) |
def z3py.is_quantifier | ( | a | ) |
Return `True` if `a` is a Z3 quantifier. >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0) >>> is_quantifier(q) True >>> is_quantifier(f(x)) False
Definition at line 1833 of file z3py.py.
Referenced by expr.body(), and Exists().
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 2375 of file z3py.py.
Referenced by RatNumRef.denominator(), and RatNumRef.numerator().
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 2328 of file z3py.py.
Referenced by fpToReal(), sort.is_arith(), Real(), and RealSort().
def z3py.is_select | ( | a | ) |
def z3py.is_seq | ( | a | ) |
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 563 of file z3py.py.
Referenced by Function(), prove(), 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 1324 of file z3py.py.
Referenced by AstRef.__bool__(), and BoolVal().
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 1072 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 2942 of file z3py.py.
Referenced by is_is_int().
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 4229 of file z3py.py.
Referenced by Default(), is_const_array(), is_default(), and is_K().
def z3py.Length | ( | s | ) |
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 3807 of file z3py.py.
Referenced by BitVecRef.__rlshift__(), BitVecRef.__rrshift__(), and BitVecRef.__rshift__().
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 197 of file z3py.py.
Referenced by help_simplify(), simplify_param_descrs(), and Goal.translate().
def z3py.Map | ( | f, | |
args | |||
) |
Return a Z3 map array expression. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> a1 = Array('a1', IntSort(), IntSort()) >>> a2 = Array('a2', IntSort(), IntSort()) >>> b = Map(f, a1, a2) >>> b Map(f, a1, a2) >>> prove(b[0] == f(a1[0], a2[0])) proved
Definition at line 4207 of file z3py.py.
Referenced by Context.Context(), get_map_func(), is_map(), and InterpolationContext.mkContext().
def z3py.MultiPattern | ( | args | ) |
Create a Z3 multi-pattern using the given expressions `*args` See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> 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 1649 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 1525 of file z3py.py.
Referenced by AtLeast(), binary_interpolant(), Solver.consequences(), fpNEQ(), Implies(), prove(), sequence_interpolant(), tree_interpolant(), and Xor().
def z3py.open_log | ( | fname | ) |
def z3py.Option | ( | re | ) |
def z3py.Or | ( | args | ) |
Create a Z3 or-expression or or-probe. >>> p, q, r = Bools('p q r') >>> Or(p, q, r) Or(p, q, r) >>> P = BoolVector('p', 5) >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 1583 of file z3py.py.
Referenced by ApplyResult.as_expr(), Bools(), and Implies().
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 7879 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))') And(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 7859 of file z3py.py.
Referenced by parse_smt2_file().
def z3py.ParThen | ( | t1, | |
t2, | |||
ctx = None |
|||
) |
Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel. >>> x, y = Ints('x y') >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values')) >>> t(And(Or(x == 1, x == 2), y == x + 1)) [[x == 1, y == 2], [x == 2, y == 3]]
Definition at line 7118 of file z3py.py.
Referenced by ParAndThen().
def z3py.PbEq | ( | args, | |
k | |||
) |
def z3py.PbLe | ( | args, | |
k | |||
) |
def z3py.Plus | ( | re | ) |
def z3py.PrefixOf | ( | a, | |
b | |||
) |
def z3py.probe_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the probe named `name`. >>> d = probe_description('memory')
Definition at line 7374 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 7364 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 7572 of file z3py.py.
Referenced by BitVecs().
def z3py.prove | ( | claim, | |
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 7735 of file z3py.py.
Referenced by Default(), Map(), Store(), and Update().
def z3py.Q | ( | a, | |
b, | |||
ctx = None |
|||
) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. >>> Q(3,5) 3/5 >>> Q(3,5).sort() Real
Definition at line 2796 of file z3py.py.
Referenced by RatNumRef.as_string(), RatNumRef.denominator(), and RatNumRef.numerator().
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
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 2856 of file z3py.py.
Referenced by ArithRef.__div__(), ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mul__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rpow__(), Cbrt(), is_arith(), ArithSortRef.is_int(), ArithRef.is_int(), is_int(), is_is_int(), is_rational_value(), ArithSortRef.is_real(), ArithRef.is_real(), is_real(), is_to_int(), IsInt(), ArithRef.sort(), Sqrt(), ToInt(), and QuantifierRef.var_sort().
def z3py.Reals | ( | names, | |
ctx = None |
|||
) |
def z3py.RealSort | ( | ctx = None | ) |
Return the real sort in the given context. If `ctx=None`, then the global context is used. >>> RealSort() Real >>> x = Const('x', RealSort()) >>> is_real(x) True >>> is_int(x) False >>> x.sort() == RealSort() True
Definition at line 2721 of file z3py.py.
Referenced by ArithSortRef.cast(), Context.getRealSort(), is_arith_sort(), Context.mkRealSort(), Context.MkRealSort(), RealVar(), Sort.toString(), Sort.ToString(), and QuantifierRef.var_sort().
def z3py.RealVal | ( | val, | |
ctx = None |
|||
) |
Return a Z3 real value. `val` may be a Python int, long, float or string representing a number in decimal or rational notation. If `ctx=None`, then the global context is used. >>> RealVal(1) 1 >>> RealVal(1).sort() Real >>> RealVal("3/5") 3/5 >>> RealVal("1.5") 3/2
Definition at line 2763 of file z3py.py.
Referenced by RatNumRef.as_decimal(), RatNumRef.as_fraction(), RatNumRef.denominator_as_long(), fpRealToFP(), fpToFP(), is_algebraic_value(), is_int_value(), is_rational_value(), is_real(), RatNumRef.numerator(), and RatNumRef.numerator_as_long().
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 1230 of file z3py.py.
Referenced by RealVarVector().
def z3py.RealVarVector | ( | n, | |
ctx = None |
|||
) |
def z3py.RealVector | ( | prefix, | |
sz, | |||
ctx = None |
|||
) |
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 7149 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 3924 of file z3py.py.
def z3py.Replace | ( | s, | |
src, | |||
dst | |||
) |
def z3py.reset_params | ( | ) |
def z3py.ReSort | ( | s | ) |
Definition at line 9584 of file z3py.py.
Referenced by Context.mkReSort(), Context.MkReSort(), Sort.toString(), and Sort.ToString().
def z3py.RNA | ( | ctx = None | ) |
def z3py.RNE | ( | ctx = None | ) |
Definition at line 8401 of file z3py.py.
Referenced by fpAbs(), fpAdd(), fpDiv(), fpFPToFP(), fpMax(), fpMin(), fpMul(), fpNeg(), fpRealToFP(), FPs(), fpSignedToFP(), fpSub(), fpToFP(), fpUnsignedToFP(), is_fprm(), and is_fprm_sort().
def z3py.RotateLeft | ( | a, | |
b | |||
) |
Return an expression representing `a` rotated to the left `b` times. >>> a, b = BitVecs('a b', 16) >>> RotateLeft(a, b) RotateLeft(a, b) >>> simplify(RotateLeft(a, 0)) a >>> simplify(RotateLeft(a, 16)) a
Definition at line 3838 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 3853 of file z3py.py.
def z3py.RoundNearestTiesToAway | ( | ctx = None | ) |
def z3py.RoundNearestTiesToEven | ( | ctx = None | ) |
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, | |
i | |||
) |
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 9357 of file z3py.py.
Referenced by Empty(), SeqSortRef.is_string(), Context.mkSeqSort(), Context.MkSeqSort(), Context.mkStringSort(), Sort.toString(), and Sort.ToString().
def z3py.sequence_interpolant | ( | v, | |
p = None , |
|||
ctx = None |
|||
) |
Compute interpolant for a sequence of formulas. If len(v) == N, and if the conjunction of the formulas in v is unsatisfiable, the interpolant is a sequence of formulas w such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1: 1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N) 2) All uninterpreted symbols in w[i] occur in both v[0]..v[i] and v[i+1]..v[n] Requires len(v) >= 1. If a & b is satisfiable, raises an object of class ModelRef that represents a model of a & b. If neither a proof of unsatisfiability nor a model is obtained (for example, because of a timeout, or because models are disabled) then None is returned. If parameters p are supplied, these are used in creating the solver that determines satisfiability. >>> x = Int('x') >>> y = Int('y') >>> print(sequence_interpolant([x < 0, y == x , y > 2])) [Not(x >= 0), Not(y >= 0)]
Definition at line 7996 of file z3py.py.
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 223 of file z3py.py.
Referenced by set_option().
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 3868 of file z3py.py.
def z3py.SimpleSolver | ( | ctx = 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 6301 of file z3py.py.
Referenced by Solver.reason_unknown(), and Solver.statistics().
def z3py.simplify | ( | a, | |
arguments, | |||
keywords | |||
) |
Utils.
Simplify the expression `a` using the given options. This function has many options. Use `help_simplify` to obtain the complete list. >>> x = Int('x') >>> y = Int('y') >>> simplify(x + 1 + y + x + 1) 2 + 2*x + y >>> simplify((x + 1)*(y + 1), som=True) 1 + x + y + x*y >>> simplify(Distinct(x, y, 1), blast_distinct=True) And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1)))
Definition at line 7468 of file z3py.py.
Referenced by BitVecRef.__invert__(), BitVecRef.__lshift__(), ArithRef.__mod__(), ArithRef.__neg__(), BitVecRef.__neg__(), ArithRef.__pow__(), ArithRef.__rpow__(), BitVecRef.__rshift__(), AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), BitVecs(), Concat(), Contains(), CreateDatatypes(), Extract(), fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpUnsignedToFP(), Implies(), IndexOf(), InRe(), is_algebraic_value(), K(), Length(), LShR(), Not(), Option(), Plus(), PrefixOf(), DatatypeSortRef.recognizer(), RepeatBitVec(), Replace(), RotateLeft(), RotateRight(), SignExt(), Star(), SuffixOf(), Union(), Xor(), and ZeroExt().
def z3py.simplify_param_descrs | ( | ) |
def z3py.solve | ( | args, | |
keywords | |||
) |
Solve the constraints `*args`. This is a simple function for creating demonstrations. It creates a solver, configure it using the options in `keywords`, adds the constraints in `args`, and invokes check. >>> a = Int('a') >>> solve(a > 0, a < 2) [a = 1]
Definition at line 7678 of file z3py.py.
Referenced by BV2Int(), and IsInt().
def z3py.solve_using | ( | s, | |
args, | |||
keywords | |||
) |
Solve the constraints `*args` using solver `s`. This is a simple function for creating demonstrations. It is similar to `solve`, but it uses the given solver `s`. It configures solver `s` using the options in `keywords`, adds the constraints in `args`, and invokes check.
Definition at line 7706 of file z3py.py.
def z3py.SolverFor | ( | logic, | |
ctx = 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 6281 of file z3py.py.
def z3py.Sqrt | ( | a, | |
ctx = None |
|||
) |
Return a Z3 expression which represents the square root of a. >>> x = Real('x') >>> Sqrt(x) x**(1/2)
Definition at line 2958 of file z3py.py.
Referenced by AlgebraicNumRef.approx(), AlgebraicNumRef.as_decimal(), and is_algebraic_value().
def z3py.SRem | ( | a, | |
b | |||
) |
Create the Z3 expression signed remainder. Use the operator % for signed modulus, and URem() for unsigned remainder. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> SRem(x, y) SRem(x, y) >>> SRem(x, y).sort() BitVec(32) >>> (x % y).sexpr() '(bvsmod x y)' >>> SRem(x, y).sexpr() '(bvsrem x y)'
Definition at line 3787 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and URem().
def z3py.Star | ( | re | ) |
Create the regular expression accepting zero or more repetitions of argument. >>> re = Star(Re("a")) >>> print(simplify(InRe("aa", re))) True >>> print(simplify(InRe("ab", re))) False >>> print(simplify(InRe("", re))) True
Definition at line 9660 of file z3py.py.
def z3py.Store | ( | a, | |
i, | |||
v | |||
) |
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 4176 of file z3py.py.
Referenced by is_array(), and is_store().
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 9443 of file z3py.py.
Referenced by Probe.apply(), Native.applyResultToString(), Native.astMapToString(), Native.astToString(), Native.astVectorToString(), Native.benchmarkToSmtlibString(), Context.Context(), Native.fixedpointGetHelp(), Native.fixedpointGetReasonUnknown(), Native.fixedpointToString(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSignificandString(), Native.funcDeclToString(), Native.getDeclRationalParameter(), Statistics.getEntries(), Native.getErrorMsg(), Native.getFullVersion(), Statistics.getKeys(), Native.getNumeralDecimalString(), Native.getNumeralString(), FuncDecl.Parameter.getParameterKind(), Native.getProbeName(), Context.getProbeNames(), Native.getSmtlibError(), Tactic.getSolver(), StringSymbol.getString(), Native.getString(), Native.getSymbolString(), Native.getTacticName(), Context.getTacticNames(), Native.goalToString(), Native.interpolationProfile(), InterpolationContext.mkContext(), Optimize.MkMinimize(), Context.mkSymbol(), Native.modelToString(), Native.optimizeGetHelp(), Native.optimizeGetReasonUnknown(), Native.optimizeToString(), Native.paramDescrsGetDocumentation(), Native.paramDescrsToString(), Native.paramsToString(), Native.patternToString(), Native.probeGetDescr(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.simplifyGetHelp(), Native.solverGetHelp(), Native.solverGetReasonUnknown(), Native.solverToString(), Native.sortToString(), Native.statsGetKey(), Native.statsToString(), Native.tacticGetDescr(), Native.tacticGetHelp(), Statistics.Entry.toString(), and FuncInterp.toString().
def z3py.Strings | ( | names, | |
ctx = None |
|||
) |
Return a tuple of String constants.
Definition at line 9451 of file z3py.py.
Referenced by Contains().
def z3py.StringSort | ( | ctx = None | ) |
Create a string sort >>> s = StringSort() >>> print(s) String
Definition at line 9347 of file z3py.py.
Referenced by Empty(), and SeqSortRef.is_string().
def z3py.StringVal | ( | s, | |
ctx = None |
|||
) |
create a string expression
Definition at line 9438 of file z3py.py.
Referenced by Empty(), Extract(), is_seq(), is_string(), is_string_value(), Length(), and Re().
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 7500 of file z3py.py.
Referenced by expr.simplify().
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 7526 of file z3py.py.
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 7546 of file z3py.py.
Referenced by BitVecs(), Ints(), IntVector(), Reals(), and RealVector().
def z3py.tactic_description | ( | name, | |
ctx = None |
|||
) |
Return a short description for the tactic named `name`. >>> d = tactic_description('simplify')
Definition at line 7186 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 7176 of file z3py.py.
Referenced by describe_tactics().
def z3py.Then | ( | ts, | |
ks | |||
) |
Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks). >>> x, y = Ints('x y') >>> t = Then(Tactic('simplify'), Tactic('solve-eqs')) >>> t(And(x == 0, y > x + 1)) [[Not(y <= 1)]] >>> t(And(x == 0, y > x + 1)).as_expr() Not(y <= 1)
Definition at line 7068 of file z3py.py.
Referenced by Statistics.__getattr__(), Statistics.__getitem__(), Statistics.__len__(), Goal.depth(), Statistics.get_key_value(), and Statistics.keys().
def z3py.to_symbol | ( | s, | |
ctx = None |
|||
) |
Convert an integer or string into a Z3 symbol.
Definition at line 100 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Const(), DeclareSort(), FiniteDomainSort(), Function(), prove(), Fixedpoint.set_predicate_representation(), SolverFor(), and Fixedpoint.update_rule().
def z3py.ToInt | ( | a | ) |
Return the Z3 expression ToInt(a). >>> x = Real('x') >>> x.sort() Real >>> n = ToInt(x) >>> n ToInt(x) >>> n.sort() Int
Definition at line 2925 of file z3py.py.
Referenced by is_to_int().
def z3py.ToReal | ( | a | ) |
Return the Z3 expression ToReal(a). >>> x = Int('x') >>> x.sort() Int >>> n = ToReal(x) >>> n ToReal(x) >>> n.sort() Real
Definition at line 2908 of file z3py.py.
Referenced by ArithRef.__ge__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), and is_to_real().
def z3py.tree_interpolant | ( | pat, | |
p = None , |
|||
ctx = None |
|||
) |
Compute interpolant for a tree of formulas. The input is an interpolation pattern over a set of formulas C. The pattern pat is a formula combining the formulas in C using logical conjunction and the "interp" operator (see Interp). This interp operator is logically the identity operator. It marks the sub-formulas of the pattern for which interpolants should be computed. The interpolant is a map sigma from marked subformulas to formulas, such that, for each marked subformula phi of pat (where phi sigma is phi with sigma(psi) substituted for each subformula psi of phi such that psi in dom(sigma)): 1) phi sigma implies sigma(phi), and 2) sigma(phi) is in the common uninterpreted vocabulary between the formulas of C occurring in phi and those not occurring in phi and moreover pat sigma implies false. In the simplest case an interpolant for the pattern "(and (interp A) B)" maps A to an interpolant for A /\ B. The return value is a vector of formulas representing sigma. This vector contains sigma(phi) for each marked subformula of pat, in pre-order traversal. This means that subformulas of phi occur before phi in the vector. Also, subformulas that occur multiply in pat will occur multiply in the result vector. If pat is satisfiable, raises an object of class ModelRef that represents a model of pat. If neither a proof of unsatisfiability nor a model is obtained (for example, because of a timeout, or because models are disabled) then None is returned. If parameters p are supplied, these are used in creating the solver that determines satisfiability. >>> x = Int('x') >>> y = Int('y') >>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))) [Not(x >= 0), Not(y <= 2)] # >>> g = And(Interpolant(x<0),x<2) # >>> try: # ... print tree_interpolant(g).sexpr() # ... except ModelRef as m: # ... print m.sexpr() (define-fun x () Int (- 1))
Definition at line 7903 of file z3py.py.
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 7168 of file z3py.py.
def z3py.UDiv | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) division `self / other`. Use the operator / for signed division. >>> x = BitVec('x', 32) >>> y = BitVec('y', 32) >>> UDiv(x, y) UDiv(x, y) >>> UDiv(x, y).sort() BitVec(32) >>> (x / y).sexpr() '(bvsdiv x y)' >>> UDiv(x, y).sexpr() '(bvudiv x y)'
Definition at line 3747 of file z3py.py.
Referenced by BitVecRef.__div__(), and BitVecRef.__rdiv__().
def z3py.UGE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other >= self`. Use the operator >= for signed greater than or equal to. >>> x, y = BitVecs('x y', 32) >>> UGE(x, y) UGE(x, y) >>> (x >= y).sexpr() '(bvsge x y)' >>> UGE(x, y).sexpr() '(bvuge x y)'
Definition at line 3713 of file z3py.py.
Referenced by BitVecRef.__ge__().
def z3py.UGT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other > self`. Use the operator > for signed greater than. >>> x, y = BitVecs('x y', 32) >>> UGT(x, y) UGT(x, y) >>> (x > y).sexpr() '(bvsgt x y)' >>> UGT(x, y).sexpr() '(bvugt x y)'
Definition at line 3730 of file z3py.py.
Referenced by BitVecRef.__gt__().
def z3py.ULE | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other <= self`. Use the operator <= for signed less than or equal to. >>> x, y = BitVecs('x y', 32) >>> ULE(x, y) ULE(x, y) >>> (x <= y).sexpr() '(bvsle x y)' >>> ULE(x, y).sexpr() '(bvule x y)'
Definition at line 3679 of file z3py.py.
Referenced by BitVecRef.__le__().
def z3py.ULT | ( | a, | |
b | |||
) |
Create the Z3 expression (unsigned) `other < self`. Use the operator < for signed less than. >>> x, y = BitVecs('x y', 32) >>> ULT(x, y) ULT(x, y) >>> (x < y).sexpr() '(bvslt x y)' >>> ULT(x, y).sexpr() '(bvult x y)'
Definition at line 3696 of file z3py.py.
Referenced by BitVecRef.__lt__().
def z3py.Union | ( | args | ) |
def z3py.Unit | ( | a | ) |
def z3py.Update | ( | a, | |
i, | |||
v | |||
) |
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 3767 of file z3py.py.
Referenced by BitVecRef.__mod__(), BitVecRef.__rmod__(), and SRem().
def z3py.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 1218 of file z3py.py.
Referenced by QuantifierRef.body(), QuantifierRef.children(), is_pattern(), MultiPattern(), QuantifierRef.pattern(), and RealVar().
def z3py.When | ( | p, | |
t, | |||
ctx = None |
|||
) |
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified. >>> t = When(Probe('size') > 2, Tactic('simplify')) >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x > 0) >>> g.add(y > 0) >>> t(g) [[x > 0, y > 0]] >>> g.add(x == y + 1) >>> t(g) [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 7434 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 7136 of file z3py.py.
Referenced by Goal.prec().
def z3py.Xor | ( | a, | |
b, | |||
ctx = None |
|||
) |
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 3897 of file z3py.py.
sat = CheckSatResult(Z3_L_TRUE) |
unknown = CheckSatResult(Z3_L_UNDEF) |
unsat = CheckSatResult(Z3_L_FALSE) |