|
def | z3_debug () |
|
def | enable_trace (msg) |
|
def | disable_trace (msg) |
|
def | get_version_string () |
|
def | get_version () |
|
def | get_full_version () |
|
def | open_log (fname) |
|
def | append_log (s) |
|
def | to_symbol (s, ctx=None) |
|
def | z3_error_handler (c, e) |
|
def | main_ctx () |
|
def | get_ctx (ctx) |
|
def | set_param (*args, **kws) |
|
def | reset_params () |
|
def | set_option (*args, **kws) |
|
def | get_param (name) |
|
def | is_ast (a) |
|
def | eq (a, b) |
|
def | is_sort (s) |
|
def | DeclareSort (name, ctx=None) |
|
def | is_func_decl (a) |
|
def | Function (name, *sig) |
|
def | FreshFunction (*sig) |
|
def | RecFunction (name, *sig) |
|
def | RecAddDefinition (f, args, body) |
|
def | 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, 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 | 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 | 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 | Sum (*args) |
|
def | Product (*args) |
|
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, **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 | 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 | 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) |
|
def | IndexOf (s, substr, offset) |
|
def | LastIndexOf (s, substr) |
|
def | Length (s) |
|
def | StrToInt (s) |
|
def | IntToStr (s) |
|
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 | PartialOrder (a, index) |
|
def | LinearOrder (a, index) |
|
def | TreeOrder (a, index) |
|
def | PiecewiseLinearOrder (a, index) |
|
def | TransitiveClosure (f) |
|
def | ensure_prop_closures () |
|
def | user_prop_push (ctx) |
|
def | user_prop_pop (ctx, num_scopes) |
|
def | user_prop_fresh (id, ctx) |
|
def | user_prop_fixed (ctx, cb, id, value) |
|
def | user_prop_final (ctx, cb) |
|
def | user_prop_eq (ctx, cb, x, y) |
|
def | user_prop_diseq (ctx, cb, x, y) |
|
◆ And()
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 1700 of file z3py.py.
1701 """Create a Z3 and-expression or and-probe.
1703 >>> p, q, r = Bools('p q r')
1706 >>> P = BoolVector('p', 5)
1708 And(p__0, p__1, p__2, p__3, p__4)
1712 last_arg = args[len(args)-1]
1713 if isinstance(last_arg, Context):
1714 ctx = args[len(args)-1]
1715 args = args[:len(args)-1]
1716 elif len(args) == 1
and isinstance(args[0], AstVector):
1718 args = [a
for a
in args[0]]
1721 args = _get_args(args)
1722 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1724 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1725 if _has_probe(args):
1726 return _probe_and(args, ctx)
1728 args = _coerce_expr_list(args, ctx)
1729 _args, sz = _to_ast_array(args)
1730 return BoolRef(
Z3_mk_and(ctx.ref(), sz, _args), ctx)
Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().
◆ AndThen()
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 7804 of file z3py.py.
7805 """Return a tactic that applies the tactics in `*ts` in sequence.
7807 >>> x, y = Ints('x y')
7808 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7809 >>> t(And(x == 0, y > x + 1))
7811 >>> t(And(x == 0, y > x + 1)).as_expr()
7815 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7816 ctx = ks.get(
'ctx',
None)
7819 for i
in range(num - 1):
7820 r = _and_then(r, ts[i+1], ctx)
Referenced by Then().
◆ append_log()
Append user-defined string to interaction log.
Definition at line 105 of file z3py.py.
106 """Append user-defined string to interaction log. """
◆ args2params()
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 5111 of file z3py.py.
5112 """Convert python arguments into a Z3_params object.
5113 A ':' is added to the keywords, and '_' is replaced with '-'
5115 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5116 (params model true relevancy 2 elim_and true)
5119 _z3_assert(len(arguments) % 2 == 0,
"Argument list must have an even number of elements.")
Referenced by Tactic.apply(), Solver.set(), Fixedpoint.set(), Optimize.set(), simplify(), and With().
◆ Array()
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 4444 of file z3py.py.
4444 def Array(name, dom, rng):
4445 """Return an array constant named `name` with the given domain and range sorts.
4447 >>> a = Array('a', IntSort(), IntSort())
◆ ArraySort()
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 4412 of file z3py.py.
4413 """Return the Z3 array sort with the given domain and range sorts.
4415 >>> A = ArraySort(IntSort(), BoolSort())
4422 >>> AA = ArraySort(IntSort(), A)
4424 Array(Int, Array(Int, Bool))
4426 sig = _get_args(sig)
4428 _z3_assert(len(sig) > 1,
"At least two arguments expected")
4429 arity = len(sig) - 1
4434 _z3_assert(
is_sort(s),
"Z3 sort expected")
4435 _z3_assert(s.ctx == r.ctx,
"Context mismatch")
4439 dom = (Sort * arity)()
4440 for i
in range(arity):
Referenced by Array(), and SetSort().
◆ AtLeast()
def z3py.AtLeast |
( |
* |
args | ) |
|
Create an at-most Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)
Definition at line 8385 of file z3py.py.
8386 """Create an at-most Pseudo-Boolean k constraint.
8388 >>> a, b, c = Bools('a b c')
8389 >>> f = AtLeast(a, b, c, 2)
8391 args = _get_args(args)
8393 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8394 ctx = _ctx_from_ast_arg_list(args)
8396 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8397 args1 = _coerce_expr_list(args[:-1], ctx)
8399 _args, sz = _to_ast_array(args1)
◆ AtMost()
def z3py.AtMost |
( |
* |
args | ) |
|
Create an at-most Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtMost(a, b, c, 2)
Definition at line 8368 of file z3py.py.
8369 """Create an at-most Pseudo-Boolean k constraint.
8371 >>> a, b, c = Bools('a b c')
8372 >>> f = AtMost(a, b, c, 2)
8374 args = _get_args(args)
8376 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8377 ctx = _ctx_from_ast_arg_list(args)
8379 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8380 args1 = _coerce_expr_list(args[:-1], ctx)
8382 _args, sz = _to_ast_array(args1)
8383 return BoolRef(
Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
◆ BitVec()
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 3811 of file z3py.py.
3811 def BitVec(name, bv, ctx=None):
3812 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3813 If `ctx=None`, then the global context is used.
3815 >>> x = BitVec('x', 16)
3822 >>> word = BitVecSort(16)
3823 >>> x2 = BitVec('x', word)
3827 if isinstance(bv, BitVecSortRef):
Referenced by BitVecs().
◆ BitVecs()
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 3834 of file z3py.py.
3834 def BitVecs(names, bv, ctx=None):
3835 """Return a tuple of bit-vector constants of size bv.
3837 >>> x, y, z = BitVecs('x y z', 16)
3844 >>> Product(x, y, z)
3846 >>> simplify(Product(x, y, z))
3850 if isinstance(names, str):
3851 names = names.split(
" ")
3852 return [
BitVec(name, bv, ctx)
for name
in names]
◆ BitVecSort()
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 3781 of file z3py.py.
3782 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3784 >>> Byte = BitVecSort(8)
3785 >>> Word = BitVecSort(16)
3788 >>> x = Const('x', Byte)
3789 >>> eq(x, BitVec('x', 8))
Referenced by BitVec(), and BitVecVal().
◆ BitVecVal()
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 3795 of file z3py.py.
3796 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3798 >>> v = BitVecVal(10, 32)
3801 >>> print("0x%.8x" % v.as_long())
3806 return BitVecNumRef(
Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
◆ Bool()
def z3py.Bool |
( |
|
name, |
|
|
|
ctx = None |
|
) |
| |
◆ Bools()
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 1599 of file z3py.py.
1599 def Bools(names, ctx=None):
1600 """Return a tuple of Boolean constants.
1602 `names` is a single string containing all names separated by blank spaces.
1603 If `ctx=None`, then the global context is used.
1605 >>> p, q, r = Bools('p q r')
1606 >>> And(p, Or(q, r))
1610 if isinstance(names, str):
1611 names = names.split(
" ")
1612 return [
Bool(name, ctx)
for name
in names]
◆ BoolSort()
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 1553 of file z3py.py.
1554 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1558 >>> p = Const('p', BoolSort())
1561 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1564 >>> is_bool(r(0, 1))
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), Solver.check(), FreshBool(), If(), Implies(), Not(), SetSort(), QuantifierRef.sort(), and Xor().
◆ BoolVal()
def z3py.BoolVal |
( |
|
val, |
|
|
|
ctx = None |
|
) |
| |
◆ BoolVector()
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 1614 of file z3py.py.
1615 """Return a list of Boolean constants of size `sz`.
1617 The constants are named using the given prefix.
1618 If `ctx=None`, then the global context is used.
1620 >>> P = BoolVector('p', 3)
1624 And(p__0, p__1, p__2)
1626 return [
Bool(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
◆ BV2Int()
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 3751 of file z3py.py.
3751 def BV2Int(a, is_signed=False):
3752 """Return the Z3 expression BV2Int(a).
3754 >>> b = BitVec('b', 3)
3755 >>> BV2Int(b).sort()
3760 >>> x > BV2Int(b, is_signed=False)
3762 >>> x > BV2Int(b, is_signed=True)
3763 x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3764 >>> solve(x > BV2Int(b), b == 1, x < 3)
3768 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
3771 return ArithRef(
Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
◆ BVAddNoOverflow()
def z3py.BVAddNoOverflow |
( |
|
a, |
|
|
|
b, |
|
|
|
signed |
|
) |
| |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4206 of file z3py.py.
4207 """A predicate the determines that bit-vector addition does not overflow"""
4208 _check_bv_args(a, b)
4209 a, b = _coerce_exprs(a, b)
◆ BVAddNoUnderflow()
def z3py.BVAddNoUnderflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4212 of file z3py.py.
4213 """A predicate the determines that signed bit-vector addition does not underflow"""
4214 _check_bv_args(a, b)
4215 a, b = _coerce_exprs(a, b)
◆ BVMulNoOverflow()
def z3py.BVMulNoOverflow |
( |
|
a, |
|
|
|
b, |
|
|
|
signed |
|
) |
| |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4243 of file z3py.py.
4244 """A predicate the determines that bit-vector multiplication does not overflow"""
4245 _check_bv_args(a, b)
4246 a, b = _coerce_exprs(a, b)
◆ BVMulNoUnderflow()
def z3py.BVMulNoUnderflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4250 of file z3py.py.
4251 """A predicate the determines that bit-vector signed multiplication does not underflow"""
4252 _check_bv_args(a, b)
4253 a, b = _coerce_exprs(a, b)
◆ BVRedAnd()
Return the reduction-and expression of `a`.
Definition at line 4194 of file z3py.py.
4195 """Return the reduction-and expression of `a`."""
4197 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
◆ BVRedOr()
Return the reduction-or expression of `a`.
Definition at line 4200 of file z3py.py.
4201 """Return the reduction-or expression of `a`."""
4203 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4204 return BitVecRef(
Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
◆ BVSDivNoOverflow()
def z3py.BVSDivNoOverflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4231 of file z3py.py.
4232 """A predicate the determines that bit-vector signed division does not overflow"""
4233 _check_bv_args(a, b)
4234 a, b = _coerce_exprs(a, b)
◆ BVSNegNoOverflow()
def z3py.BVSNegNoOverflow |
( |
|
a | ) |
|
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4237 of file z3py.py.
4238 """A predicate the determines that bit-vector unary negation does not overflow"""
4240 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
◆ BVSubNoOverflow()
def z3py.BVSubNoOverflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4218 of file z3py.py.
4219 """A predicate the determines that bit-vector subtraction does not overflow"""
4220 _check_bv_args(a, b)
4221 a, b = _coerce_exprs(a, b)
◆ BVSubNoUnderflow()
def z3py.BVSubNoUnderflow |
( |
|
a, |
|
|
|
b, |
|
|
|
signed |
|
) |
| |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4225 of file z3py.py.
4226 """A predicate the determines that bit-vector subtraction does not underflow"""
4227 _check_bv_args(a, b)
4228 a, b = _coerce_exprs(a, b)
◆ Cbrt()
def z3py.Cbrt |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Return a Z3 expression which represents the cubic root of a.
>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)
Definition at line 3209 of file z3py.py.
3209 def Cbrt(a, ctx=None):
3210 """ Return a Z3 expression which represents the cubic root of a.
◆ Complement()
def z3py.Complement |
( |
|
re | ) |
|
Create the complement regular expression.
Definition at line 10446 of file z3py.py.
10447 """Create the complement regular expression."""
◆ Concat()
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 3854 of file z3py.py.
3855 """Create a Z3 bit-vector concatenation expression.
3857 >>> v = BitVecVal(1, 4)
3858 >>> Concat(v, v+1, v)
3859 Concat(Concat(1, 1 + 1), 1)
3860 >>> simplify(Concat(v, v+1, v))
3862 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3865 args = _get_args(args)
3868 _z3_assert(sz >= 2,
"At least two arguments expected.")
3875 if is_seq(args[0])
or isinstance(args[0], str):
3876 args = [_coerce_seq(s, ctx)
for s
in args]
3878 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
3881 v[i] = args[i].as_ast()
3886 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
3889 v[i] = args[i].as_ast()
3893 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
3895 for i
in range(sz - 1):
3896 r = BitVecRef(
Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
Referenced by SeqRef.__add__(), and SeqRef.__radd__().
◆ Cond()
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 8223 of file z3py.py.
8223 def Cond(p, t1, t2, ctx=None):
8224 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8226 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8228 p = _to_probe(p, ctx)
8229 t1 = _to_tactic(t1, ctx)
8230 t2 = _to_tactic(t2, ctx)
8231 return Tactic(
Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
Referenced by If().
◆ Const()
def z3py.Const |
( |
|
name, |
|
|
|
sort |
|
) |
| |
Create a constant of the given sort.
>>> Const('x', IntSort())
x
Definition at line 1321 of file z3py.py.
1321 def Const(name, sort):
1322 """Create a constant of the given sort.
1324 >>> Const('x', IntSort())
1328 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
Referenced by Consts().
◆ Consts()
def z3py.Consts |
( |
|
names, |
|
|
|
sort |
|
) |
| |
Create several constants of the given sort.
`names` is a string containing the names of all constants to be created.
Blank spaces separate the names of different constants.
>>> x, y, z = Consts('x y z', IntSort())
>>> x + y + z
x + y + z
Definition at line 1332 of file z3py.py.
1333 """Create several constants of the given sort.
1335 `names` is a string containing the names of all constants to be created.
1336 Blank spaces separate the names of different constants.
1338 >>> x, y, z = Consts('x y z', IntSort())
1342 if isinstance(names, str):
1343 names = names.split(
" ")
1344 return [
Const(name, sort)
for name
in names]
◆ Contains()
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 10240 of file z3py.py.
10241 """Check if 'a' contains 'b'
10242 >>> s1 = Contains("abc", "ab")
10245 >>> s2 = Contains("abc", "bc")
10248 >>> x, y, z = Strings('x y z')
10249 >>> s3 = Contains(Concat(x,y,z), y)
10253 ctx = _get_ctx2(a, b)
10254 a = _coerce_seq(a, ctx)
10255 b = _coerce_seq(b, ctx)
◆ CreateDatatypes()
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 4823 of file z3py.py.
4824 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4826 In the following example we define a Tree-List using two mutually recursive datatypes.
4828 >>> TreeList = Datatype('TreeList')
4829 >>> Tree = Datatype('Tree')
4830 >>> # Tree has two constructors: leaf and node
4831 >>> Tree.declare('leaf', ('val', IntSort()))
4832 >>> # a node contains a list of trees
4833 >>> Tree.declare('node', ('children', TreeList))
4834 >>> TreeList.declare('nil')
4835 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4836 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4837 >>> Tree.val(Tree.leaf(10))
4839 >>> simplify(Tree.val(Tree.leaf(10)))
4841 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4843 node(cons(leaf(10), cons(leaf(20), nil)))
4844 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4845 >>> simplify(n2 == n1)
4847 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4852 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
4853 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
4854 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
4855 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
4858 names = (Symbol * num)()
4859 out = (Sort * num)()
4860 clists = (ConstructorList * num)()
4862 for i
in range(num):
4865 num_cs = len(d.constructors)
4866 cs = (Constructor * num_cs)()
4867 for j
in range(num_cs):
4868 c = d.constructors[j]
4873 fnames = (Symbol * num_fs)()
4874 sorts = (Sort * num_fs)()
4875 refs = (ctypes.c_uint * num_fs)()
4876 for k
in range(num_fs):
4880 if isinstance(ftype, Datatype):
4882 _z3_assert(ds.count(ftype) == 1,
"One and only one occurrence of each datatype is expected")
4884 refs[k] = ds.index(ftype)
4887 _z3_assert(
is_sort(ftype),
"Z3 sort expected")
4888 sorts[k] = ftype.ast
4891 to_delete.append(ScopedConstructor(cs[j], ctx))
4893 to_delete.append(ScopedConstructorList(clists[i], ctx))
4897 for i
in range(num):
4898 dref = DatatypeSortRef(out[i], ctx)
4899 num_cs = dref.num_constructors()
4900 for j
in range(num_cs):
4901 cref = dref.constructor(j)
4902 cref_name = cref.name()
4903 cref_arity = cref.arity()
4904 if cref.arity() == 0:
4906 setattr(dref, cref_name, cref)
4907 rref = dref.recognizer(j)
4908 setattr(dref,
"is_" + cref_name, rref)
4909 for k
in range(cref_arity):
4910 aref = dref.accessor(j, k)
4911 setattr(dref, aref.name(), aref)
4913 return tuple(result)
Referenced by Datatype.create().
◆ DeclareSort()
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 637 of file z3py.py.
638 """Create a new uninterpreted sort named `name`.
640 If `ctx=None`, then the new sort is declared in the global Z3Py context.
642 >>> A = DeclareSort('A')
643 >>> a = Const('a', A)
644 >>> b = Const('b', A)
◆ Default()
Return a default value for array expression.
>>> b = K(IntSort(), 1)
>>> prove(Default(b) == 1)
proved
Definition at line 4478 of file z3py.py.
4479 """ Return a default value for array expression.
4480 >>> b = K(IntSort(), 1)
4481 >>> prove(Default(b) == 1)
4485 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
◆ describe_probes()
def z3py.describe_probes |
( |
| ) |
|
Display a (tabular) description of all available probes in Z3.
Definition at line 8153 of file z3py.py.
8154 """Display a (tabular) description of all available probes in Z3."""
8157 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8160 print(
'<tr style="background-color:#CFCFCF">')
8165 print(
'<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(
probe_description(p), 40)))
◆ describe_tactics()
def z3py.describe_tactics |
( |
| ) |
|
Display a (tabular) description of all available tactics in Z3.
Definition at line 7962 of file z3py.py.
7963 """Display a (tabular) description of all available tactics in Z3."""
7966 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7969 print(
'<tr style="background-color:#CFCFCF">')
7974 print(
'<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(
tactic_description(t), 40)))
◆ disable_trace()
def z3py.disable_trace |
( |
|
msg | ) |
|
◆ DisjointSum()
def z3py.DisjointSum |
( |
|
name, |
|
|
|
sorts, |
|
|
|
ctx = None |
|
) |
| |
Create a named tagged union sort base on a set of underlying sorts
Example:
>>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
Definition at line 5023 of file z3py.py.
5024 """Create a named tagged union sort base on a set of underlying sorts
5026 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5028 sum = Datatype(name, ctx)
5029 for i
in range(len(sorts)):
5030 sum.declare(
"inject%d" % i, (
"project%d" % i, sorts[i]))
5032 return sum, [(sum.constructor(i), sum.accessor(i, 0))
for i
in range(len(sorts))]
◆ Distinct()
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 1290 of file z3py.py.
1291 """Create a Z3 distinct expression.
1298 >>> Distinct(x, y, z)
1300 >>> simplify(Distinct(x, y, z))
1302 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1303 And(Not(x == y), Not(x == z), Not(y == z))
1305 args = _get_args(args)
1306 ctx = _ctx_from_ast_arg_list(args)
1308 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1309 args = _coerce_expr_list(args, ctx)
1310 _args, sz = _to_ast_array(args)
◆ Empty()
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 10175 of file z3py.py.
10176 """Create the empty sequence of the given sort
10177 >>> e = Empty(StringSort())
10178 >>> e2 = StringVal("")
10179 >>> print(e.eq(e2))
10181 >>> e3 = Empty(SeqSort(IntSort()))
10184 >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10186 Empty(ReSort(Seq(Int)))
10188 if isinstance(s, SeqSortRef):
10190 if isinstance(s, ReSortRef):
10192 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Empty")
◆ EmptySet()
Create the empty set
>>> EmptySet(IntSort())
K(Int, False)
Definition at line 4613 of file z3py.py.
4614 """Create the empty set
4615 >>> EmptySet(IntSort())
◆ enable_trace()
def z3py.enable_trace |
( |
|
msg | ) |
|
◆ ensure_prop_closures()
def z3py.ensure_prop_closures |
( |
| ) |
|
◆ EnumSort()
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 5035 of file z3py.py.
5035 def EnumSort(name, values, ctx=None):
5036 """Return a new enumeration sort named `name` containing the given values.
5038 The result is a pair (sort, list of constants).
5040 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5043 _z3_assert(isinstance(name, str),
"Name must be a string")
5044 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Eumeration sort values must be strings")
5045 _z3_assert(len(values) > 0,
"At least one value expected")
5048 _val_names = (Symbol * num)()
5049 for i
in range(num):
5051 _values = (FuncDecl * num)()
5052 _testers = (FuncDecl * num)()
5056 for i
in range(num):
5057 V.append(FuncDeclRef(_values[i], ctx))
5058 V = [a()
for a
in V]
◆ eq()
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 432 of file z3py.py.
433 """Return `True` if `a` and `b` are structurally identical AST nodes.
443 >>> eq(simplify(x + 1), simplify(1 + x))
Referenced by substitute().
◆ Exists()
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 2082 of file z3py.py.
2082 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2083 """Create a Z3 exists formula.
2085 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2088 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2091 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2093 Exists([x, y], f(x, y) >= x)
2094 >>> is_quantifier(q)
2096 >>> r = Tactic('nnf')(q).as_expr()
2097 >>> is_quantifier(r)
2100 return _mk_quantifier(
False, vs, body, weight, qid, skid, patterns, no_patterns)
Referenced by Fixedpoint.abstract().
◆ Ext()
Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
>> Ext(a, b)
Ext(a, b)
Definition at line 4563 of file z3py.py.
4564 """Return extensionality index for one-dimensional arrays.
4565 >> a, b = Consts('a b', SetSort(IntSort()))
4572 return _to_expr_ref(
Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
◆ Extract()
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 3899 of file z3py.py.
3900 """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3902 >>> x = BitVec('x', 8)
3903 >>> Extract(6, 2, x)
3905 >>> Extract(6, 2, x).sort()
3907 >>> simplify(Extract(StringVal("abcd"),2,1))
3910 if isinstance(high, str):
3914 offset, length = _coerce_exprs(low, a, s.ctx)
3915 return SeqRef(
Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3917 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
3918 _z3_assert(_is_int(high)
and high >= 0
and _is_int(low)
and low >= 0,
"First and second arguments must be non negative integers")
3919 _z3_assert(
is_bv(a),
"Third argument must be a Z3 bit-vector expression")
3920 return BitVecRef(
Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
Referenced by SubSeq(), and SubString().
◆ FailIf()
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 8186 of file z3py.py.
8187 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8189 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8191 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8192 >>> x, y = Ints('x y')
8198 >>> g.add(x == y + 1)
8200 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8202 p = _to_probe(p, ctx)
◆ FiniteDomainSort()
def z3py.FiniteDomainSort |
( |
|
name, |
|
|
|
sz, |
|
|
|
ctx = None |
|
) |
| |
Create a named finite domain sort of a given size sz
Definition at line 7278 of file z3py.py.
7279 """Create a named finite domain sort of a given size sz"""
7280 if not isinstance(name, Symbol):
◆ FiniteDomainVal()
def z3py.FiniteDomainVal |
( |
|
val, |
|
|
|
sort, |
|
|
|
ctx = None |
|
) |
| |
Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
>>> s = FiniteDomainSort('S', 256)
>>> FiniteDomainVal(255, s)
255
>>> FiniteDomainVal('100', s)
100
Definition at line 7346 of file z3py.py.
7347 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7349 >>> s = FiniteDomainSort('S', 256)
7350 >>> FiniteDomainVal(255, s)
7352 >>> FiniteDomainVal('100', s)
7358 return FiniteDomainNumRef(
Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
◆ Float128()
def z3py.Float128 |
( |
|
ctx = None | ) |
|
Floating-point 128-bit (quadruple) sort.
Definition at line 8816 of file z3py.py.
8817 """Floating-point 128-bit (quadruple) sort."""
◆ Float16()
def z3py.Float16 |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8786 of file z3py.py.
8787 """Floating-point 16-bit (half) sort."""
◆ Float32()
def z3py.Float32 |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8796 of file z3py.py.
8797 """Floating-point 32-bit (single) sort."""
◆ Float64()
def z3py.Float64 |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8806 of file z3py.py.
8807 """Floating-point 64-bit (double) sort."""
◆ FloatDouble()
def z3py.FloatDouble |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8811 of file z3py.py.
8812 """Floating-point 64-bit (double) sort."""
◆ FloatHalf()
def z3py.FloatHalf |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8791 of file z3py.py.
8792 """Floating-point 16-bit (half) sort."""
◆ FloatQuadruple()
def z3py.FloatQuadruple |
( |
|
ctx = None | ) |
|
Floating-point 128-bit (quadruple) sort.
Definition at line 8821 of file z3py.py.
8822 """Floating-point 128-bit (quadruple) sort."""
◆ FloatSingle()
def z3py.FloatSingle |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8801 of file z3py.py.
8802 """Floating-point 32-bit (single) sort."""
◆ ForAll()
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 2065 of file z3py.py.
2065 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2066 """Create a Z3 forall formula.
2068 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2070 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2073 >>> ForAll([x, y], f(x, y) >= x)
2074 ForAll([x, y], f(x, y) >= x)
2075 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2076 ForAll([x, y], f(x, y) >= x)
2077 >>> ForAll([x, y], f(x, y) >= x, weight=10)
2078 ForAll([x, y], f(x, y) >= x)
2080 return _mk_quantifier(
True, vs, body, weight, qid, skid, patterns, no_patterns)
Referenced by Fixedpoint.abstract().
◆ FP()
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 9401 of file z3py.py.
9401 def FP(name, fpsort, ctx=None):
9402 """Return a floating-point constant named `name`.
9403 `fpsort` is the floating-point sort.
9404 If `ctx=None`, then the global context is used.
9406 >>> x = FP('x', FPSort(8, 24))
9413 >>> word = FPSort(8, 24)
9414 >>> x2 = FP('x', word)
9418 if isinstance(fpsort, FPSortRef)
and ctx
is None:
Referenced by FPs().
◆ fpAbs()
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 9442 of file z3py.py.
9442 def fpAbs(a, ctx=None):
9443 """Create a Z3 floating-point absolute value expression.
9445 >>> s = FPSort(8, 24)
9447 >>> x = FPVal(1.0, s)
9450 >>> y = FPVal(-20.0, s)
9455 >>> fpAbs(-1.25*(2**4))
9461 [a] = _coerce_fp_expr_list([a], ctx)
◆ fpAdd()
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 9524 of file z3py.py.
9524 def fpAdd(rm, a, b, ctx=None):
9525 """Create a Z3 floating-point addition expression.
9527 >>> s = FPSort(8, 24)
9533 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9535 >>> fpAdd(rm, x, y).sort()
9538 return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
Referenced by FPRef.__add__(), and FPRef.__radd__().
◆ fpBVToFP()
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 9820 of file z3py.py.
9821 """Create a Z3 floating-point conversion expression that represents the
9822 conversion from a bit-vector term to a floating-point term.
9824 >>> x_bv = BitVecVal(0x3F800000, 32)
9825 >>> x_fp = fpBVToFP(x_bv, Float32())
9831 _z3_assert(
is_bv(v),
"First argument must be a Z3 bit-vector expression")
9832 _z3_assert(
is_fp_sort(sort),
"Second argument must be a Z3 floating-point sort.")
◆ fpDiv()
def z3py.fpDiv |
( |
|
rm, |
|
|
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point division expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpDiv(rm, x, y)
fpDiv(RNE(), x, y)
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)
Definition at line 9568 of file z3py.py.
9568 def fpDiv(rm, a, b, ctx=None):
9569 """Create a Z3 floating-point division expression.
9571 >>> s = FPSort(8, 24)
9577 >>> fpDiv(rm, x, y).sort()
9580 return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
Referenced by FPRef.__div__(), and FPRef.__rdiv__().
◆ fpEQ()
def z3py.fpEQ |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create the Z3 floating-point expression `fpEQ(other, self)`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpEQ(x, y)
fpEQ(x, y)
>>> fpEQ(x, y).sexpr()
'(fp.eq x y)'
Definition at line 9732 of file z3py.py.
9732 def fpEQ(a, b, ctx=None):
9733 """Create the Z3 floating-point expression `fpEQ(other, self)`.
9735 >>> x, y = FPs('x y', FPSort(8, 24))
9738 >>> fpEQ(x, y).sexpr()
9741 return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
Referenced by fpNEQ().
◆ fpFMA()
def z3py.fpFMA |
( |
|
rm, |
|
|
|
a, |
|
|
|
b, |
|
|
|
c, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point fused multiply-add expression.
Definition at line 9623 of file z3py.py.
9623 def fpFMA(rm, a, b, c, ctx=None):
9624 """Create a Z3 floating-point fused multiply-add expression.
9626 return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
◆ fpFP()
def z3py.fpFP |
( |
|
sgn, |
|
|
|
exp, |
|
|
|
sig, |
|
|
|
ctx = None |
|
) |
| |
Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
>>> s = FPSort(8, 24)
>>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
>>> print(x)
fpFP(1, 127, 4194304)
>>> xv = FPVal(-1.5, s)
>>> print(xv)
-1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
sat
>>> xv = FPVal(+1.5, s)
>>> print(xv)
1.5
>>> slvr = Solver()
>>> slvr.add(fpEQ(x, xv))
>>> slvr.check()
unsat
Definition at line 9754 of file z3py.py.
9754 def fpFP(sgn, exp, sig, ctx=None):
9755 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9757 >>> s = FPSort(8, 24)
9758 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9760 fpFP(1, 127, 4194304)
9761 >>> xv = FPVal(-1.5, s)
9765 >>> slvr.add(fpEQ(x, xv))
9768 >>> xv = FPVal(+1.5, s)
9772 >>> slvr.add(fpEQ(x, xv))
9777 _z3_assert(sgn.sort().size() == 1,
"sort mismatch")
9779 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,
"context mismatch")
9780 return FPRef(
Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
◆ fpFPToFP()
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 9836 of file z3py.py.
9836 def fpFPToFP(rm, v, sort, ctx=None):
9837 """Create a Z3 floating-point conversion expression that represents the
9838 conversion from a floating-point term to a floating-point term of different precision.
9840 >>> x_sgl = FPVal(1.0, Float32())
9841 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9849 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9850 _z3_assert(
is_fp(v),
"Second argument must be a Z3 floating-point expression.")
9851 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
◆ fpGEQ()
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 9721 of file z3py.py.
9721 def fpGEQ(a, b, ctx=None):
9722 """Create the Z3 floating-point expression `other >= self`.
9724 >>> x, y = FPs('x y', FPSort(8, 24))
9727 >>> (x >= y).sexpr()
9730 return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
Referenced by FPRef.__ge__().
◆ fpGT()
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 9710 of file z3py.py.
9710 def fpGT(a, b, ctx=None):
9711 """Create the Z3 floating-point expression `other > self`.
9713 >>> x, y = FPs('x y', FPSort(8, 24))
9719 return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
Referenced by FPRef.__gt__().
◆ fpInfinity()
def z3py.fpInfinity |
( |
|
s, |
|
|
|
negative |
|
) |
| |
Create a Z3 floating-point +oo or -oo term.
Definition at line 9335 of file z3py.py.
9336 """Create a Z3 floating-point +oo or -oo term."""
9337 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9338 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9339 return FPNumRef(
Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
◆ fpIsInf()
def z3py.fpIsInf |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isInfinite expression.
>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> fpIsInf(x)
fpIsInf(x)
Definition at line 9649 of file z3py.py.
9650 """Create a Z3 floating-point isInfinite expression.
9652 >>> s = FPSort(8, 24)
9657 return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
◆ fpIsNaN()
def z3py.fpIsNaN |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isNaN expression.
>>> s = FPSort(8, 24)
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpIsNaN(x)
fpIsNaN(x)
Definition at line 9638 of file z3py.py.
9639 """Create a Z3 floating-point isNaN expression.
9641 >>> s = FPSort(8, 24)
9647 return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
◆ fpIsNegative()
def z3py.fpIsNegative |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isNegative expression.
Definition at line 9674 of file z3py.py.
9675 """Create a Z3 floating-point isNegative expression.
9677 return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
◆ fpIsNormal()
def z3py.fpIsNormal |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isNormal expression.
Definition at line 9664 of file z3py.py.
9665 """Create a Z3 floating-point isNormal expression.
9667 return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
◆ fpIsPositive()
def z3py.fpIsPositive |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isPositive expression.
Definition at line 9679 of file z3py.py.
9680 """Create a Z3 floating-point isPositive expression.
9682 return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
◆ fpIsSubnormal()
def z3py.fpIsSubnormal |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isSubnormal expression.
Definition at line 9669 of file z3py.py.
9670 """Create a Z3 floating-point isSubnormal expression.
9672 return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
◆ fpIsZero()
def z3py.fpIsZero |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point isZero expression.
Definition at line 9659 of file z3py.py.
9660 """Create a Z3 floating-point isZero expression.
9662 return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
◆ fpLEQ()
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 9699 of file z3py.py.
9699 def fpLEQ(a, b, ctx=None):
9700 """Create the Z3 floating-point expression `other <= self`.
9702 >>> x, y = FPs('x y', FPSort(8, 24))
9705 >>> (x <= y).sexpr()
9708 return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
Referenced by FPRef.__le__().
◆ fpLT()
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 9688 of file z3py.py.
9688 def fpLT(a, b, ctx=None):
9689 """Create the Z3 floating-point expression `other < self`.
9691 >>> x, y = FPs('x y', FPSort(8, 24))
9697 return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
Referenced by FPRef.__lt__().
◆ fpMax()
def z3py.fpMax |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point maximum expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMax(x, y)
fpMax(x, y)
>>> fpMax(x, y).sort()
FPSort(8, 24)
Definition at line 9609 of file z3py.py.
9609 def fpMax(a, b, ctx=None):
9610 """Create a Z3 floating-point maximum expression.
9612 >>> s = FPSort(8, 24)
9618 >>> fpMax(x, y).sort()
9621 return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
◆ fpMin()
def z3py.fpMin |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point minimum expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMin(x, y)
fpMin(x, y)
>>> fpMin(x, y).sort()
FPSort(8, 24)
Definition at line 9595 of file z3py.py.
9595 def fpMin(a, b, ctx=None):
9596 """Create a Z3 floating-point minimum expression.
9598 >>> s = FPSort(8, 24)
9604 >>> fpMin(x, y).sort()
9607 return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
◆ fpMinusInfinity()
def z3py.fpMinusInfinity |
( |
|
s | ) |
|
Create a Z3 floating-point -oo term.
Definition at line 9330 of file z3py.py.
9331 """Create a Z3 floating-point -oo term."""
9332 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9333 return FPNumRef(
Z3_mk_fpa_inf(s.ctx_ref(), s.ast,
True), s.ctx)
Referenced by FPVal().
◆ fpMinusZero()
def z3py.fpMinusZero |
( |
|
s | ) |
|
Create a Z3 floating-point -0.0 term.
Definition at line 9346 of file z3py.py.
9347 """Create a Z3 floating-point -0.0 term."""
9348 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
Referenced by FPVal().
◆ fpMul()
def z3py.fpMul |
( |
|
rm, |
|
|
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point multiplication expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMul(rm, x, y)
fpMul(RNE(), x, y)
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)
Definition at line 9554 of file z3py.py.
9554 def fpMul(rm, a, b, ctx=None):
9555 """Create a Z3 floating-point multiplication expression.
9557 >>> s = FPSort(8, 24)
9563 >>> fpMul(rm, x, y).sort()
9566 return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
Referenced by FPRef.__mul__(), and FPRef.__rmul__().
◆ fpNaN()
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 9298 of file z3py.py.
9299 """Create a Z3 floating-point NaN term.
9301 >>> s = FPSort(8, 24)
9302 >>> set_fpa_pretty(True)
9305 >>> pb = get_fpa_pretty()
9306 >>> set_fpa_pretty(False)
9308 fpNaN(FPSort(8, 24))
9309 >>> set_fpa_pretty(pb)
9311 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
Referenced by FPVal().
◆ fpNeg()
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 9464 of file z3py.py.
9464 def fpNeg(a, ctx=None):
9465 """Create a Z3 floating-point addition expression.
9467 >>> s = FPSort(8, 24)
9476 [a] = _coerce_fp_expr_list([a], ctx)
Referenced by FPRef.__neg__().
◆ fpNEQ()
def z3py.fpNEQ |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
>>> x, y = FPs('x y', FPSort(8, 24))
>>> fpNEQ(x, y)
Not(fpEQ(x, y))
>>> (x != y).sexpr()
'(distinct x y)'
Definition at line 9743 of file z3py.py.
9743 def fpNEQ(a, b, ctx=None):
9744 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9746 >>> x, y = FPs('x y', FPSort(8, 24))
9749 >>> (x != y).sexpr()
◆ fpPlusInfinity()
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 9314 of file z3py.py.
9315 """Create a Z3 floating-point +oo term.
9317 >>> s = FPSort(8, 24)
9318 >>> pb = get_fpa_pretty()
9319 >>> set_fpa_pretty(True)
9320 >>> fpPlusInfinity(s)
9322 >>> set_fpa_pretty(False)
9323 >>> fpPlusInfinity(s)
9324 fpPlusInfinity(FPSort(8, 24))
9325 >>> set_fpa_pretty(pb)
9327 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9328 return FPNumRef(
Z3_mk_fpa_inf(s.ctx_ref(), s.ast,
False), s.ctx)
Referenced by FPVal().
◆ fpPlusZero()
Create a Z3 floating-point +0.0 term.
Definition at line 9341 of file z3py.py.
9342 """Create a Z3 floating-point +0.0 term."""
9343 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9344 return FPNumRef(
Z3_mk_fpa_zero(s.ctx_ref(), s.ast,
False), s.ctx)
Referenced by FPVal().
◆ fpRealToFP()
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 9855 of file z3py.py.
9856 """Create a Z3 floating-point conversion expression that represents the
9857 conversion from a real term to a floating-point term.
9859 >>> x_r = RealVal(1.5)
9860 >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9866 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9867 _z3_assert(
is_real(v),
"Second argument must be a Z3 expression or real sort.")
9868 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
◆ fpRem()
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 9582 of file z3py.py.
9582 def fpRem(a, b, ctx=None):
9583 """Create a Z3 floating-point remainder expression.
9585 >>> s = FPSort(8, 24)
9590 >>> fpRem(x, y).sort()
9593 return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
Referenced by FPRef.__mod__(), and FPRef.__rmod__().
◆ fpRoundToIntegral()
def z3py.fpRoundToIntegral |
( |
|
rm, |
|
|
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point roundToIntegral expression.
Definition at line 9633 of file z3py.py.
9634 """Create a Z3 floating-point roundToIntegral expression.
9636 return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
◆ FPs()
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 9424 of file z3py.py.
9424 def FPs(names, fpsort, ctx=None):
9425 """Return an array of floating-point constants.
9427 >>> x, y, z = FPs('x y z', FPSort(8, 24))
9434 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9435 fpMul(RNE(), fpAdd(RNE(), x, y), z)
9438 if isinstance(names, str):
9439 names = names.split(
" ")
9440 return [
FP(name, fpsort, ctx)
for name
in names]
◆ fpSignedToFP()
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 9872 of file z3py.py.
9873 """Create a Z3 floating-point conversion expression that represents the
9874 conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9876 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9877 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9879 fpToFP(RNE(), 4294967291)
9883 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9884 _z3_assert(
is_bv(v),
"Second argument must be a Z3 bit-vector expression")
9885 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
◆ FPSort()
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 9240 of file z3py.py.
9240 def FPSort(ebits, sbits, ctx=None):
9241 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9243 >>> Single = FPSort(8, 24)
9244 >>> Double = FPSort(11, 53)
9247 >>> x = Const('x', Single)
9248 >>> eq(x, FP('x', FPSort(8, 24)))
Referenced by get_default_fp_sort().
◆ fpSqrt()
def z3py.fpSqrt |
( |
|
rm, |
|
|
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point square root expression.
Definition at line 9628 of file z3py.py.
9628 def fpSqrt(rm, a, ctx=None):
9629 """Create a Z3 floating-point square root expression.
9631 return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
◆ fpSub()
def z3py.fpSub |
( |
|
rm, |
|
|
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point subtraction expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpSub(rm, x, y)
fpSub(RNE(), x, y)
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)
Definition at line 9540 of file z3py.py.
9540 def fpSub(rm, a, b, ctx=None):
9541 """Create a Z3 floating-point subtraction expression.
9543 >>> s = FPSort(8, 24)
9549 >>> fpSub(rm, x, y).sort()
9552 return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
Referenced by FPRef.__rsub__(), and FPRef.__sub__().
◆ fpToFP()
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 9782 of file z3py.py.
9782 def fpToFP(a1, a2=None, a3=None, ctx=None):
9783 """Create a Z3 floating-point conversion expression from other term sorts
9786 From a bit-vector term in IEEE 754-2008 format:
9787 >>> x = FPVal(1.0, Float32())
9788 >>> x_bv = fpToIEEEBV(x)
9789 >>> simplify(fpToFP(x_bv, Float32()))
9792 From a floating-point term with different precision:
9793 >>> x = FPVal(1.0, Float32())
9794 >>> x_db = fpToFP(RNE(), x, Float64())
9799 >>> x_r = RealVal(1.5)
9800 >>> simplify(fpToFP(RNE(), x_r, Float32()))
9803 From a signed bit-vector term:
9804 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9805 >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9818 raise Z3Exception(
"Unsupported combination of arguments for conversion to floating-point term.")
◆ fpToFPUnsigned()
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 9906 of file z3py.py.
9907 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9909 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9910 _z3_assert(
is_bv(x),
"Second argument must be a Z3 bit-vector expression")
9911 _z3_assert(
is_fp_sort(s),
"Third argument must be Z3 floating-point sort")
◆ fpToIEEEBV()
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 9976 of file z3py.py.
9977 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9979 The size of the resulting bit-vector is automatically determined.
9981 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9982 knows only one NaN and it will always produce the same bit-vector representation of
9985 >>> x = FP('x', FPSort(8, 24))
9986 >>> y = fpToIEEEBV(x)
9997 _z3_assert(
is_fp(x),
"First argument must be a Z3 floating-point expression")
◆ fpToReal()
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 9957 of file z3py.py.
9958 """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9960 >>> x = FP('x', FPSort(8, 24))
9964 >>> print(is_real(y))
9968 >>> print(is_real(x))
9972 _z3_assert(
is_fp(x),
"First argument must be a Z3 floating-point expression")
◆ fpToSBV()
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 9915 of file z3py.py.
9915 def fpToSBV(rm, x, s, ctx=None):
9916 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9918 >>> x = FP('x', FPSort(8, 24))
9919 >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9930 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9931 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9932 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9934 return BitVecRef(
Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
◆ fpToUBV()
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 9936 of file z3py.py.
9936 def fpToUBV(rm, x, s, ctx=None):
9937 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9939 >>> x = FP('x', FPSort(8, 24))
9940 >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9951 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9952 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9953 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9955 return BitVecRef(
Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
◆ fpUnsignedToFP()
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 9889 of file z3py.py.
9890 """Create a Z3 floating-point conversion expression that represents the
9891 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9893 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9894 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9896 fpToFPUnsigned(RNE(), 4294967291)
9900 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9901 _z3_assert(
is_bv(v),
"Second argument must be a Z3 bit-vector expression")
9902 _z3_assert(
is_fp_sort(sort),
"Third argument must be a Z3 floating-point sort.")
◆ FPVal()
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 9357 of file z3py.py.
9357 def FPVal(sig, exp=None, fps=None, ctx=None):
9358 """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9360 >>> v = FPVal(20.0, FPSort(8, 24))
9363 >>> print("0x%.8x" % v.exponent_as_long(False))
9365 >>> v = FPVal(2.25, FPSort(8, 24))
9368 >>> v = FPVal(-2.25, FPSort(8, 24))
9371 >>> FPVal(-0.0, FPSort(8, 24))
9373 >>> FPVal(0.0, FPSort(8, 24))
9375 >>> FPVal(+0.0, FPSort(8, 24))
9383 fps = _dflt_fps(ctx)
9387 val = _to_float_str(sig)
9388 if val ==
"NaN" or val ==
"nan":
9392 elif val ==
"0.0" or val ==
"+0.0":
9394 elif val ==
"+oo" or val ==
"+inf" or val ==
"+Inf":
9396 elif val ==
"-oo" or val ==
"-inf" or val ==
"-Inf":
9399 return FPNumRef(
Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
Referenced by set_default_fp_sort().
◆ fpZero()
def z3py.fpZero |
( |
|
s, |
|
|
|
negative |
|
) |
| |
Create a Z3 floating-point +0.0 or -0.0 term.
Definition at line 9351 of file z3py.py.
9352 """Create a Z3 floating-point +0.0 or -0.0 term."""
9353 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9354 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9355 return FPNumRef(
Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
◆ FreshBool()
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 1628 of file z3py.py.
1629 """Return a fresh Boolean constant in the given context using the given prefix.
1631 If `ctx=None`, then the global context is used.
1633 >>> b1 = FreshBool()
1634 >>> b2 = FreshBool()
◆ FreshConst()
def z3py.FreshConst |
( |
|
sort, |
|
|
|
prefix = 'c' |
|
) |
| |
Create a fresh constant of a specified sort
Definition at line 1346 of file z3py.py.
1347 """Create a fresh constant of a specified sort"""
1348 ctx = _get_ctx(sort.ctx)
◆ FreshFunction()
def z3py.FreshFunction |
( |
* |
sig | ) |
|
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 821 of file z3py.py.
822 """Create a new fresh Z3 uninterpreted function with the given sorts.
826 _z3_assert(len(sig) > 0,
"At least two arguments expected")
830 _z3_assert(
is_sort(rng),
"Z3 sort expected")
831 dom = (z3.Sort * arity)()
832 for i
in range(arity):
834 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
◆ FreshInt()
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 3081 of file z3py.py.
3081 def FreshInt(prefix='x', ctx=None):
3082 """Return a fresh integer constant in the given context using the given prefix.
◆ FreshReal()
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 3134 of file z3py.py.
3135 """Return a fresh real constant in the given context using the given prefix.
◆ Full()
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 10194 of file z3py.py.
10195 """Create the regular expression that accepts the universal language
10196 >>> e = Full(ReSort(SeqSort(IntSort())))
10198 Full(ReSort(Seq(Int)))
10199 >>> e1 = Full(ReSort(StringSort()))
10201 Full(ReSort(String))
10203 if isinstance(s, ReSortRef):
10205 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Full")
◆ FullSet()
Create the full set
>>> FullSet(IntSort())
K(Int, True)
Definition at line 4621 of file z3py.py.
4622 """Create the full set
4623 >>> FullSet(IntSort())
◆ Function()
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 799 of file z3py.py.
800 """Create a new Z3 uninterpreted function with the given sorts.
802 >>> f = Function('f', IntSort(), IntSort())
808 _z3_assert(len(sig) > 0,
"At least two arguments expected")
812 _z3_assert(
is_sort(rng),
"Z3 sort expected")
813 dom = (Sort * arity)()
814 for i
in range(arity):
816 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
◆ get_as_array_func()
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 6285 of file z3py.py.
6286 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6288 _z3_assert(
is_as_array(n),
"as-array Z3 expression expected.")
Referenced by ModelRef.get_interp().
◆ get_ctx()
◆ get_default_fp_sort()
def z3py.get_default_fp_sort |
( |
|
ctx = None | ) |
|
◆ get_default_rounding_mode()
def z3py.get_default_rounding_mode |
( |
|
ctx = None | ) |
|
Retrieves the global default rounding mode.
Definition at line 8683 of file z3py.py.
8684 """Retrieves the global default rounding mode."""
8685 global _dflt_rounding_mode
8686 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8688 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8690 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8692 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8694 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
Referenced by set_default_fp_sort().
◆ get_full_version()
def z3py.get_full_version |
( |
| ) |
|
◆ get_map_func()
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 4395 of file z3py.py.
4396 """Return the function declaration associated with a Z3 map array expression.
4398 >>> f = Function('f', IntSort(), IntSort())
4399 >>> b = Array('b', IntSort(), IntSort())
4401 >>> eq(f, get_map_func(a))
4405 >>> get_map_func(a)(0)
4409 _z3_assert(
is_map(a),
"Z3 array map expression expected.")
◆ get_param()
def z3py.get_param |
( |
|
name | ) |
|
Return the value of a Z3 global (or module) parameter
>>> get_param('nlsat.reorder')
'true'
Definition at line 273 of file z3py.py.
274 """Return the value of a Z3 global (or module) parameter
276 >>> get_param('nlsat.reorder')
279 ptr = (ctypes.c_char_p * 1)()
281 r = z3core._to_pystr(ptr[0])
283 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
◆ get_var_index()
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 1224 of file z3py.py.
1225 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1233 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1234 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1235 >>> q = ForAll([x, y], f(x, y) == x + y)
1237 f(Var(1), Var(0)) == Var(1) + Var(0)
1241 >>> v1 = b.arg(0).arg(0)
1242 >>> v2 = b.arg(0).arg(1)
1247 >>> get_var_index(v1)
1249 >>> get_var_index(v2)
1253 _z3_assert(
is_var(a),
"Z3 bound variable expected")
◆ get_version()
Definition at line 81 of file z3py.py.
82 major = ctypes.c_uint(0)
83 minor = ctypes.c_uint(0)
84 build = ctypes.c_uint(0)
85 rev = ctypes.c_uint(0)
87 return (major.value, minor.value, build.value, rev.value)
◆ get_version_string()
def z3py.get_version_string |
( |
| ) |
|
Definition at line 73 of file z3py.py.
74 major = ctypes.c_uint(0)
75 minor = ctypes.c_uint(0)
76 build = ctypes.c_uint(0)
77 rev = ctypes.c_uint(0)
79 return "%s.%s.%s" % (major.value, minor.value, build.value)
◆ help_simplify()
def z3py.help_simplify |
( |
| ) |
|
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 8263 of file z3py.py.
8264 """Return a string describing all options available for Z3 `simplify` procedure."""
◆ If()
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 1268 of file z3py.py.
1268 def If(a, b, c, ctx=None):
1269 """Create a Z3 if-then-else expression.
1273 >>> max = If(x > y, x, y)
1279 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1280 return Cond(a, b, c, ctx)
1282 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1285 b, c = _coerce_exprs(b, c, ctx)
1287 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1288 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
Referenced by BoolRef.__mul__(), and ArithRef.__mul__().
◆ Implies()
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 1641 of file z3py.py.
1642 """Create a Z3 implies expression.
1644 >>> p, q = Bools('p q')
1648 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1652 return BoolRef(
Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
Referenced by Fixedpoint.add_rule(), and Fixedpoint.update_rule().
◆ IndexOf() [1/2]
def z3py.IndexOf |
( |
|
s, |
|
|
|
substr |
|
) |
| |
◆ IndexOf() [2/2]
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
Definition at line 10276 of file z3py.py.
10276 def IndexOf(s, substr, offset):
10277 """Retrieve the index of substring within a string starting at a specified offset.
10278 >>> simplify(IndexOf("abcabc", "bc", 0))
10280 >>> simplify(IndexOf("abcabc", "bc", 2))
10286 ctx = _get_ctx2(s, substr, ctx)
10287 s = _coerce_seq(s, ctx)
10288 substr = _coerce_seq(substr, ctx)
10289 if _is_int(offset):
10290 offset =
IntVal(offset, ctx)
10291 return ArithRef(
Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
◆ InRe()
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 10373 of file z3py.py.
10374 """Create regular expression membership test
10375 >>> re = Union(Re("a"),Re("b"))
10376 >>> print (simplify(InRe("a", re)))
10378 >>> print (simplify(InRe("b", re)))
10380 >>> print (simplify(InRe("c", re)))
10383 s = _coerce_seq(s, re.ctx)
10384 return BoolRef(
Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
◆ Int()
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 3045 of file z3py.py.
3045 def Int(name, ctx=None):
3046 """Return an integer constant named `name`. If `ctx=None`, then the global context is used.
Referenced by Ints(), and IntVector().
◆ Int2BV()
def z3py.Int2BV |
( |
|
a, |
|
|
|
num_bits |
|
) |
| |
Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
modulo of a by 2^num_bits
Definition at line 3773 of file z3py.py.
3774 """Return the z3 expression Int2BV(a, num_bits).
3775 It is a bit-vector of width num_bits and represents the
3776 modulo of a by 2^num_bits
3779 return BitVecRef(
Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
◆ Intersect()
def z3py.Intersect |
( |
* |
args | ) |
|
Create intersection of regular expressions.
>>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 10405 of file z3py.py.
10406 """Create intersection of regular expressions.
10407 >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10409 args = _get_args(args)
10412 _z3_assert(sz > 0,
"At least one argument expected.")
10413 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10418 for i
in range(sz):
10419 v[i] = args[i].as_ast()
◆ Ints()
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 3057 of file z3py.py.
3057 def Ints(names, ctx=None):
3058 """Return a tuple of Integer constants.
3060 >>> x, y, z = Ints('x y z')
3065 if isinstance(names, str):
3066 names = names.split(
" ")
3067 return [
Int(name, ctx)
for name
in names]
◆ IntSort()
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 2942 of file z3py.py.
2943 """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2947 >>> x = Const('x', IntSort())
2950 >>> x.sort() == IntSort()
2952 >>> x.sort() == BoolSort()
Referenced by FreshInt(), Int(), and IntVal().
◆ IntToStr()
Convert integer expression to string
Definition at line 10327 of file z3py.py.
10328 """Convert integer expression to string"""
◆ IntVal()
def z3py.IntVal |
( |
|
val, |
|
|
|
ctx = None |
|
) |
| |
◆ IntVector()
def z3py.IntVector |
( |
|
prefix, |
|
|
|
sz, |
|
|
|
ctx = None |
|
) |
| |
Return a list of integer constants of size `sz`.
>>> X = IntVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
Definition at line 3069 of file z3py.py.
3070 """Return a list of integer constants of size `sz`.
3072 >>> X = IntVector('x', 3)
3079 return [
Int(
'%s__%s' % (prefix, i), ctx)
for i
in range(sz) ]
◆ is_add()
Return `True` if `a` is an expression of the form b + c.
>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False
Definition at line 2617 of file z3py.py.
2618 """Return `True` if `a` is an expression of the form b + c.
2620 >>> x, y = Ints('x y')
◆ is_algebraic_value()
def z3py.is_algebraic_value |
( |
|
a | ) |
|
Return `True` if `a` is an algebraic value of sort Real.
>>> is_algebraic_value(RealVal("3/5"))
False
>>> n = simplify(Sqrt(2))
>>> n
1.4142135623?
>>> is_algebraic_value(n)
True
Definition at line 2604 of file z3py.py.
2605 """Return `True` if `a` is an algebraic value of sort Real.
2607 >>> is_algebraic_value(RealVal("3/5"))
2609 >>> n = simplify(Sqrt(2))
2612 >>> is_algebraic_value(n)
2615 return is_arith(a)
and a.is_real()
and _is_algebraic(a.ctx, a.as_ast())
◆ is_and()
Return `True` if `a` is a Z3 and expression.
>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False
Definition at line 1489 of file z3py.py.
1490 """Return `True` if `a` is a Z3 and expression.
1492 >>> p, q = Bools('p q')
1493 >>> is_and(And(p, q))
1495 >>> is_and(Or(p, q))
◆ is_app()
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 1157 of file z3py.py.
1158 """Return `True` if `a` is a Z3 function application.
1160 Note that, constants are function applications with 0 arguments.
1167 >>> is_app(IntSort())
1171 >>> is_app(IntVal(1))
1174 >>> is_app(ForAll(x, x >= 0))
1177 if not isinstance(a, ExprRef):
1179 k = _ast_kind(a.ctx, a)
1180 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
◆ is_app_of()
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 1256 of file z3py.py.
1257 """Return `True` if `a` is an application of the given kind `k`.
1261 >>> is_app_of(n, Z3_OP_ADD)
1263 >>> is_app_of(n, Z3_OP_MUL)
1266 return is_app(a)
and a.decl().kind() == k
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().
◆ is_arith()
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 2498 of file z3py.py.
2499 """Return `True` if `a` is an arithmetical expression.
2508 >>> is_arith(IntVal(1))
2516 return isinstance(a, ArithRef)
Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().
◆ is_arith_sort()
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 2199 of file z3py.py.
2200 """Return `True` if s is an arithmetical sort (type).
2202 >>> is_arith_sort(IntSort())
2204 >>> is_arith_sort(RealSort())
2206 >>> is_arith_sort(BoolSort())
2208 >>> n = Int('x') + 1
2209 >>> is_arith_sort(n.sort())
2212 return isinstance(s, ArithSortRef)
Referenced by ArithSortRef.subsort().
◆ is_array()
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 4335 of file z3py.py.
4336 """Return `True` if `a` is a Z3 array expression.
4338 >>> a = Array('a', IntSort(), IntSort())
4341 >>> is_array(Store(a, 0, 1))
4346 return isinstance(a, ArrayRef)
Referenced by Ext(), and Map().
◆ is_array_sort()
def z3py.is_array_sort |
( |
|
a | ) |
|
◆ is_as_array()
def z3py.is_as_array |
( |
|
n | ) |
|
◆ is_ast()
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 412 of file z3py.py.
413 """Return `True` if `a` is an AST node.
417 >>> is_ast(IntVal(10))
421 >>> is_ast(BoolSort())
423 >>> is_ast(Function('f', IntSort(), IntSort()))
430 return isinstance(a, AstRef)
Referenced by eq(), AstRef.eq(), and ReSort().
◆ is_bool()
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 1442 of file z3py.py.
1443 """Return `True` if `a` is a Z3 Boolean expression.
1449 >>> is_bool(And(p, q))
1457 return isinstance(a, BoolRef)
Referenced by is_quantifier(), and prove().
◆ is_bv()
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 3724 of file z3py.py.
3725 """Return `True` if `a` is a Z3 bit-vector expression.
3727 >>> b = BitVec('b', 32)
3735 return isinstance(a, BitVecRef)
Referenced by BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), fpBVToFP(), fpFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), is_bv_value(), Product(), RepeatBitVec(), SignExt(), Sum(), and ZeroExt().
◆ is_bv_sort()
Return True if `s` is a Z3 bit-vector sort.
>>> is_bv_sort(BitVecSort(32))
True
>>> is_bv_sort(IntSort())
False
Definition at line 3259 of file z3py.py.
3260 """Return True if `s` is a Z3 bit-vector sort.
3262 >>> is_bv_sort(BitVecSort(32))
3264 >>> is_bv_sort(IntSort())
3267 return isinstance(s, BitVecSortRef)
Referenced by BitVecVal(), fpToSBV(), fpToUBV(), and BitVecSortRef.subsort().
◆ is_bv_value()
def z3py.is_bv_value |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 bit-vector numeral value.
>>> b = BitVec('b', 32)
>>> is_bv_value(b)
False
>>> b = BitVecVal(10, 32)
>>> b
10
>>> is_bv_value(b)
True
Definition at line 3737 of file z3py.py.
3738 """Return `True` if `a` is a Z3 bit-vector numeral value.
3740 >>> b = BitVec('b', 32)
3743 >>> b = BitVecVal(10, 32)
3749 return is_bv(a)
and _is_numeral(a.ctx, a.as_ast())
◆ is_const()
◆ is_const_array()
def z3py.is_const_array |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 constant array.
>>> a = K(IntSort(), 10)
>>> is_const_array(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_const_array(a)
False
Definition at line 4348 of file z3py.py.
4349 """Return `True` if `a` is a Z3 constant array.
4351 >>> a = K(IntSort(), 10)
4352 >>> is_const_array(a)
4354 >>> a = Array('a', IntSort(), IntSort())
4355 >>> is_const_array(a)
◆ is_default()
Return `True` if `a` is a Z3 default array expression.
>>> d = Default(K(IntSort(), 10))
>>> is_default(d)
True
Definition at line 4387 of file z3py.py.
4388 """Return `True` if `a` is a Z3 default array expression.
4389 >>> d = Default(K(IntSort(), 10))
4393 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
◆ is_distinct()
def z3py.is_distinct |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 distinct expression.
>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True
Definition at line 1542 of file z3py.py.
1543 """Return `True` if `a` is a Z3 distinct expression.
1545 >>> x, y, z = Ints('x y z')
1546 >>> is_distinct(x == y)
1548 >>> is_distinct(Distinct(x, y, z))
◆ is_div()
Return `True` if `a` is an expression of the form b / c.
>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True
Definition at line 2650 of file z3py.py.
2651 """Return `True` if `a` is an expression of the form b / c.
2653 >>> x, y = Reals('x y')
2658 >>> x, y = Ints('x y')
◆ is_eq()
Return `True` if `a` is a Z3 equality expression.
>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
Definition at line 1533 of file z3py.py.
1534 """Return `True` if `a` is a Z3 equality expression.
1536 >>> x, y = Ints('x y')
Referenced by AstRef.__bool__().
◆ is_expr()
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 1135 of file z3py.py.
1136 """Return `True` if `a` is a Z3 expression.
1143 >>> is_expr(IntSort())
1147 >>> is_expr(IntVal(1))
1150 >>> is_expr(ForAll(x, x >= 0))
1152 >>> is_expr(FPVal(1.0))
1155 return isinstance(a, ExprRef)
Referenced by SeqRef.__gt__(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), ExprRef.children(), Concat(), AlgebraicNumRef.index(), IndexOf(), IntToStr(), is_quantifier(), is_var(), K(), MultiPattern(), Replace(), simplify(), Sqrt(), substitute(), and substitute_vars().
◆ is_false()
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 1476 of file z3py.py.
1477 """Return `True` if `a` is the Z3 false expression.
1484 >>> is_false(BoolVal(False))
Referenced by AstRef.__bool__().
◆ is_finite_domain()
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 7307 of file z3py.py.
7308 """Return `True` if `a` is a Z3 finite-domain expression.
7310 >>> s = FiniteDomainSort('S', 100)
7311 >>> b = Const('b', s)
7312 >>> is_finite_domain(b)
7314 >>> is_finite_domain(Int('x'))
7317 return isinstance(a, FiniteDomainRef)
Referenced by is_finite_domain_value().
◆ is_finite_domain_sort()
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 7285 of file z3py.py.
7286 """Return True if `s` is a Z3 finite-domain sort.
7288 >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7290 >>> is_finite_domain_sort(IntSort())
7293 return isinstance(s, FiniteDomainSortRef)
Referenced by FiniteDomainVal().
◆ is_finite_domain_value()
def z3py.is_finite_domain_value |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 finite-domain value.
>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain_value(b)
False
>>> b = FiniteDomainVal(10, s)
>>> b
10
>>> is_finite_domain_value(b)
True
Definition at line 7360 of file z3py.py.
7361 """Return `True` if `a` is a Z3 finite-domain value.
7363 >>> s = FiniteDomainSort('S', 100)
7364 >>> b = Const('b', s)
7365 >>> is_finite_domain_value(b)
7367 >>> b = FiniteDomainVal(10, s)
7370 >>> is_finite_domain_value(b)
◆ is_fp()
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 9213 of file z3py.py.
9214 """Return `True` if `a` is a Z3 floating-point expression.
9216 >>> b = FP('b', FPSort(8, 24))
9224 return isinstance(a, FPRef)
Referenced by fpFPToFP(), fpIsPositive(), fpNeg(), fpToFP(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), is_fp_value(), and set_default_fp_sort().
◆ is_fp_sort()
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 8830 of file z3py.py.
8831 """Return True if `s` is a Z3 floating-point sort.
8833 >>> is_fp_sort(FPSort(8, 24))
8835 >>> is_fp_sort(IntSort())
8838 return isinstance(s, FPSortRef)
Referenced by fpBVToFP(), fpFPToFP(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpUnsignedToFP(), and FPVal().
◆ is_fp_value()
def z3py.is_fp_value |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 floating-point numeral value.
>>> b = FP('b', FPSort(8, 24))
>>> is_fp_value(b)
False
>>> b = FPVal(1.0, FPSort(8, 24))
>>> b
1
>>> is_fp_value(b)
True
Definition at line 9226 of file z3py.py.
9227 """Return `True` if `a` is a Z3 floating-point numeral value.
9229 >>> b = FP('b', FPSort(8, 24))
9232 >>> b = FPVal(1.0, FPSort(8, 24))
9238 return is_fp(a)
and _is_numeral(a.ctx, a.ast)
◆ is_fprm()
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 9077 of file z3py.py.
9078 """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9087 return isinstance(a, FPRMRef)
Referenced by fpFPToFP(), fpNeg(), fpRealToFP(), fpSignedToFP(), fpToFP(), fpToFPUnsigned(), fpToSBV(), fpToUBV(), fpUnsignedToFP(), and is_fprm_value().
◆ is_fprm_sort()
def z3py.is_fprm_sort |
( |
|
s | ) |
|
Return True if `s` is a Z3 floating-point rounding mode sort.
>>> is_fprm_sort(FPSort(8, 24))
False
>>> is_fprm_sort(RNE().sort())
True
Definition at line 8840 of file z3py.py.
8841 """Return True if `s` is a Z3 floating-point rounding mode sort.
8843 >>> is_fprm_sort(FPSort(8, 24))
8845 >>> is_fprm_sort(RNE().sort())
8848 return isinstance(s, FPRMSortRef)
◆ is_fprm_value()
def z3py.is_fprm_value |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 9089 of file z3py.py.
9090 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9091 return is_fprm(a)
and _is_numeral(a.ctx, a.ast)
Referenced by set_default_rounding_mode().
◆ is_func_decl()
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 787 of file z3py.py.
788 """Return `True` if `a` is a Z3 function declaration.
790 >>> f = Function('f', IntSort(), IntSort())
797 return isinstance(a, FuncDeclRef)
Referenced by Map(), and prove().
◆ is_ge()
Return `True` if `a` is an expression of the form b >= c.
>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False
Definition at line 2710 of file z3py.py.
2711 """Return `True` if `a` is an expression of the form b >= c.
2713 >>> x, y = Ints('x y')
◆ is_gt()
Return `True` if `a` is an expression of the form b > c.
>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False
Definition at line 2721 of file z3py.py.
2722 """Return `True` if `a` is an expression of the form b > c.
2724 >>> x, y = Ints('x y')
◆ is_idiv()
Return `True` if `a` is an expression of the form b div c.
>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False
Definition at line 2666 of file z3py.py.
2667 """Return `True` if `a` is an expression of the form b div c.
2669 >>> x, y = Ints('x y')
◆ is_implies()
Return `True` if `a` is a Z3 implication expression.
>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False
Definition at line 1511 of file z3py.py.
1512 """Return `True` if `a` is a Z3 implication expression.
1514 >>> p, q = Bools('p q')
1515 >>> is_implies(Implies(p, q))
1517 >>> is_implies(And(p, q))
◆ is_int()
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 2518 of file z3py.py.
2519 """Return `True` if `a` is an integer expression.
2526 >>> is_int(IntVal(1))
◆ is_int_value()
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 2560 of file z3py.py.
2561 """Return `True` if `a` is an integer value of sort Int.
2563 >>> is_int_value(IntVal(1))
2567 >>> is_int_value(Int('x'))
2569 >>> n = Int('x') + 1
2574 >>> is_int_value(n.arg(1))
2576 >>> is_int_value(RealVal("1/3"))
2578 >>> is_int_value(RealVal(1))
2581 return is_arith(a)
and a.is_int()
and _is_numeral(a.ctx, a.as_ast())
◆ is_is_int()
Return `True` if `a` is an expression of the form IsInt(b).
>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False
Definition at line 2732 of file z3py.py.
2733 """Return `True` if `a` is an expression of the form IsInt(b).
2736 >>> is_is_int(IsInt(x))
◆ is_K()
Return `True` if `a` is a Z3 constant array.
>>> a = K(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False
Definition at line 4360 of file z3py.py.
4361 """Return `True` if `a` is a Z3 constant array.
4363 >>> a = K(IntSort(), 10)
4366 >>> a = Array('a', IntSort(), IntSort())
◆ is_le()
Return `True` if `a` is an expression of the form b <= c.
>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False
Definition at line 2688 of file z3py.py.
2689 """Return `True` if `a` is an expression of the form b <= c.
2691 >>> x, y = Ints('x y')
◆ is_lt()
Return `True` if `a` is an expression of the form b < c.
>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False
Definition at line 2699 of file z3py.py.
2700 """Return `True` if `a` is an expression of the form b < c.
2702 >>> x, y = Ints('x y')
◆ is_map()
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 4372 of file z3py.py.
4373 """Return `True` if `a` is a Z3 map array expression.
4375 >>> f = Function('f', IntSort(), IntSort())
4376 >>> b = Array('b', IntSort(), IntSort())
Referenced by get_map_func().
◆ is_mod()
Return `True` if `a` is an expression of the form b % c.
>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False
Definition at line 2677 of file z3py.py.
2678 """Return `True` if `a` is an expression of the form b % c.
2680 >>> x, y = Ints('x y')
◆ is_mul()
Return `True` if `a` is an expression of the form b * c.
>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False
Definition at line 2628 of file z3py.py.
2629 """Return `True` if `a` is an expression of the form b * c.
2631 >>> x, y = Ints('x y')
◆ is_not()
Return `True` if `a` is a Z3 not expression.
>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True
Definition at line 1522 of file z3py.py.
1523 """Return `True` if `a` is a Z3 not expression.
Referenced by mk_not().
◆ is_or()
Return `True` if `a` is a Z3 or expression.
>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False
Definition at line 1500 of file z3py.py.
1501 """Return `True` if `a` is a Z3 or expression.
1503 >>> p, q = Bools('p q')
1506 >>> is_or(And(p, q))
◆ is_pattern()
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 1780 of file z3py.py.
1781 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1783 >>> f = Function('f', IntSort(), IntSort())
1785 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1787 ForAll(x, f(x) == 0)
1788 >>> q.num_patterns()
1790 >>> is_pattern(q.pattern(0))
1795 return isinstance(a, PatternRef)
Referenced by is_quantifier(), and MultiPattern().
◆ is_probe()
Return `True` if `p` is a Z3 probe.
>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True
Definition at line 8119 of file z3py.py.
8120 """Return `True` if `p` is a Z3 probe.
8122 >>> is_probe(Int('x'))
8124 >>> is_probe(Probe('memory'))
8127 return isinstance(p, Probe)
Referenced by eq(), mk_not(), and Not().
◆ is_quantifier()
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 2018 of file z3py.py.
2019 """Return `True` if `a` is a Z3 quantifier.
2021 >>> f = Function('f', IntSort(), IntSort())
2023 >>> q = ForAll(x, f(x) == 0)
2024 >>> is_quantifier(q)
2026 >>> is_quantifier(f(x))
2029 return isinstance(a, QuantifierRef)
◆ is_rational_value()
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 2583 of file z3py.py.
2584 """Return `True` if `a` is rational value of sort Real.
2586 >>> is_rational_value(RealVal(1))
2588 >>> is_rational_value(RealVal("3/5"))
2590 >>> is_rational_value(IntVal(1))
2592 >>> is_rational_value(1)
2594 >>> n = Real('x') + 1
2597 >>> is_rational_value(n.arg(1))
2599 >>> is_rational_value(Real('x'))
2602 return is_arith(a)
and a.is_real()
and _is_numeral(a.ctx, a.as_ast())
◆ is_re()
◆ is_real()
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 2536 of file z3py.py.
2537 """Return `True` if `a` is a real expression.
2549 >>> is_real(RealVal(1))
Referenced by fpRealToFP(), and fpToFP().
◆ is_select()
Return `True` if `a` is a Z3 array select application.
>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True
Definition at line 4579 of file z3py.py.
4580 """Return `True` if `a` is a Z3 array select application.
4582 >>> a = Array('a', IntSort(), IntSort())
◆ is_seq()
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 10114 of file z3py.py.
10115 """Return `True` if `a` is a Z3 sequence expression.
10116 >>> print (is_seq(Unit(IntVal(0))))
10118 >>> print (is_seq(StringVal("abc")))
10121 return isinstance(a, SeqRef)
Referenced by SeqRef.__gt__(), Concat(), and Extract().
◆ is_sort()
◆ is_store()
Return `True` if `a` is a Z3 array store application.
>>> a = Array('a', IntSort(), IntSort())
>>> is_store(a)
False
>>> is_store(Store(a, 0, 1))
True
Definition at line 4591 of file z3py.py.
4592 """Return `True` if `a` is a Z3 array store application.
4594 >>> a = Array('a', IntSort(), IntSort())
4597 >>> is_store(Store(a, 0, 1))
◆ is_string()
Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
True
Definition at line 10123 of file z3py.py.
10124 """Return `True` if `a` is a Z3 string expression.
10125 >>> print (is_string(StringVal("ab")))
10128 return isinstance(a, SeqRef)
and a.is_string()
◆ is_string_value()
def z3py.is_string_value |
( |
|
a | ) |
|
return 'True' if 'a' is a Z3 string constant expression.
>>> print (is_string_value(StringVal("a")))
True
>>> print (is_string_value(StringVal("a") + StringVal("b")))
False
Definition at line 10130 of file z3py.py.
10131 """return 'True' if 'a' is a Z3 string constant expression.
10132 >>> print (is_string_value(StringVal("a")))
10134 >>> print (is_string_value(StringVal("a") + StringVal("b")))
10137 return isinstance(a, SeqRef)
and a.is_string_value()
◆ is_sub()
Return `True` if `a` is an expression of the form b - c.
>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False
Definition at line 2639 of file z3py.py.
2640 """Return `True` if `a` is an expression of the form b - c.
2642 >>> x, y = Ints('x y')
◆ is_to_int()
Return `True` if `a` is an expression of the form ToInt(b).
>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False
Definition at line 2757 of file z3py.py.
2758 """Return `True` if `a` is an expression of the form ToInt(b).
◆ is_to_real()
Return `True` if `a` is an expression of the form ToReal(b).
>>> x = Int('x')
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> is_to_real(n)
True
>>> is_to_real(x)
False
Definition at line 2743 of file z3py.py.
2744 """Return `True` if `a` is an expression of the form ToReal(b).
◆ is_true()
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 1459 of file z3py.py.
1460 """Return `True` if `a` is the Z3 true expression.
1465 >>> is_true(simplify(p == p))
1470 >>> # True is a Python Boolean expression
Referenced by AstRef.__bool__().
◆ is_var()
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 1200 of file z3py.py.
1201 """Return `True` if `a` is variable.
1203 Z3 uses de-Bruijn indices for representing bound variables in
1211 >>> f = Function('f', IntSort(), IntSort())
1212 >>> # Z3 replaces x with bound variables when ForAll is executed.
1213 >>> q = ForAll(x, f(x) == x)
1219 >>> is_var(b.arg(1))
1222 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
Referenced by get_var_index().
◆ IsInt()
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 3181 of file z3py.py.
3182 """ Return the Z3 predicate IsInt(a).
3185 >>> IsInt(x + "1/2")
3187 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3189 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3193 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3195 return BoolRef(
Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
◆ IsMember()
def z3py.IsMember |
( |
|
e, |
|
|
|
s |
|
) |
| |
Check if e is a member of set s
>>> a = Const('a', SetSort(IntSort()))
>>> IsMember(1, a)
a[1]
Definition at line 4692 of file z3py.py.
4693 """ Check if e is a member of set s
4694 >>> a = Const('a', SetSort(IntSort()))
4698 ctx = _ctx_from_ast_arg_list([s,e])
4699 e = _py2expr(e, ctx)
◆ IsSubset()
def z3py.IsSubset |
( |
|
a, |
|
|
|
b |
|
) |
| |
Check if a is a subset of b
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> IsSubset(a, b)
subset(a, b)
Definition at line 4702 of file z3py.py.
4703 """ Check if a is a subset of b
4704 >>> a = Const('a', SetSort(IntSort()))
4705 >>> b = Const('b', SetSort(IntSort()))
4709 ctx = _ctx_from_ast_arg_list([a, b])
◆ K()
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 4542 of file z3py.py.
4543 """Return a Z3 constant array expression.
4545 >>> a = K(IntSort(), 10)
4557 _z3_assert(
is_sort(dom),
"Z3 sort expected")
4560 v = _py2expr(v, ctx)
◆ Lambda()
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 2102 of file z3py.py.
2103 """Create a Z3 lambda expression.
2105 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2106 >>> mem0 = Array('mem0', IntSort(), IntSort())
2107 >>> lo, hi, e, i = Ints('lo hi e i')
2108 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2110 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2116 _vs = (Ast * num_vars)()
2117 for i
in range(num_vars):
2119 _vs[i] = vs[i].as_ast()
2120 return QuantifierRef(
Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
◆ LastIndexOf()
def z3py.LastIndexOf |
( |
|
s, |
|
|
|
substr |
|
) |
| |
Retrieve the last index of substring within a string
Definition at line 10293 of file z3py.py.
10294 """Retrieve the last index of substring within a string"""
10296 ctx = _get_ctx2(s, substr, ctx)
10297 s = _coerce_seq(s, ctx)
10298 substr = _coerce_seq(substr, ctx)
◆ Length()
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
Definition at line 10302 of file z3py.py.
10303 """Obtain the length of a sequence 's'
10304 >>> l = Length(StringVal("abc"))
◆ LinearOrder()
def z3py.LinearOrder |
( |
|
a, |
|
|
|
index |
|
) |
| |
◆ Loop()
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 10462 of file z3py.py.
10462 def Loop(re, lo, hi=0):
10463 """Create the regular expression accepting between a lower and upper bound repetitions
10464 >>> re = Loop(Re("a"), 1, 3)
10465 >>> print(simplify(InRe("aa", re)))
10467 >>> print(simplify(InRe("aaaa", re)))
10469 >>> print(simplify(InRe("", re)))
10472 return ReRef(
Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
◆ LShR()
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 4054 of file z3py.py.
4055 """Create the Z3 expression logical right shift.
4057 Use the operator >> for the arithmetical right shift.
4059 >>> x, y = BitVecs('x y', 32)
4062 >>> (x >> y).sexpr()
4064 >>> LShR(x, y).sexpr()
4068 >>> BitVecVal(4, 3).as_signed_long()
4070 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4072 >>> simplify(BitVecVal(4, 3) >> 1)
4074 >>> simplify(LShR(BitVecVal(4, 3), 1))
4076 >>> simplify(BitVecVal(2, 3) >> 1)
4078 >>> simplify(LShR(BitVecVal(2, 3), 1))
4081 _check_bv_args(a, b)
4082 a, b = _coerce_exprs(a, b)
4083 return BitVecRef(
Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ 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 211 of file z3py.py.
212 """Return a reference to the global Z3 context.
215 >>> x.ctx == main_ctx()
220 >>> x2 = Real('x', c)
227 if _main_ctx
is None:
228 _main_ctx = Context()
Referenced by SeqRef.__gt__(), help_simplify(), and simplify_param_descrs().
◆ Map()
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 4520 of file z3py.py.
4521 """Return a Z3 map array expression.
4523 >>> f = Function('f', IntSort(), IntSort(), IntSort())
4524 >>> a1 = Array('a1', IntSort(), IntSort())
4525 >>> a2 = Array('a2', IntSort(), IntSort())
4526 >>> b = Map(f, a1, a2)
4529 >>> prove(b[0] == f(a1[0], a2[0]))
4532 args = _get_args(args)
4534 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4535 _z3_assert(
is_func_decl(f),
"First argument must be a Z3 function declaration")
4536 _z3_assert(all([
is_array(a)
for a
in args]),
"Z3 array expected expected")
4537 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4538 _args, sz = _to_ast_array(args)
4540 return ArrayRef(
Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
◆ mk_not()
◆ Model()
def z3py.Model |
( |
|
ctx = None | ) |
|
◆ MultiPattern()
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 1797 of file z3py.py.
1798 """Create a Z3 multi-pattern using the given expressions `*args`
1800 >>> f = Function('f', IntSort(), IntSort())
1801 >>> g = Function('g', IntSort(), IntSort())
1803 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1805 ForAll(x, f(x) != g(x))
1806 >>> q.num_patterns()
1808 >>> is_pattern(q.pattern(0))
1811 MultiPattern(f(Var(0)), g(Var(0)))
1814 _z3_assert(len(args) > 0,
"At least one argument expected")
1815 _z3_assert(all([
is_expr(a)
for a
in args ]),
"Z3 expressions expected")
1817 args, sz = _to_ast_array(args)
◆ Not()
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 1669 of file z3py.py.
1669 def Not(a, ctx=None):
1670 """Create a Z3 not expression or probe.
1675 >>> simplify(Not(Not(p)))
1678 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1685 return BoolRef(
Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
Referenced by fpNEQ(), mk_not(), and prove().
◆ open_log()
def z3py.open_log |
( |
|
fname | ) |
|
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 101 of file z3py.py.
102 """Log interaction to a file. This function must be invoked immediately after init(). """
◆ Option()
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 10434 of file z3py.py.
10435 """Create the regular expression that optionally accepts the argument.
10436 >>> re = Option(Re("a"))
10437 >>> print(simplify(InRe("a", re)))
10439 >>> print(simplify(InRe("", re)))
10441 >>> print(simplify(InRe("aa", re)))
◆ Or()
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 1732 of file z3py.py.
1733 """Create a Z3 or-expression or or-probe.
1735 >>> p, q, r = Bools('p q r')
1738 >>> P = BoolVector('p', 5)
1740 Or(p__0, p__1, p__2, p__3, p__4)
1744 last_arg = args[len(args)-1]
1745 if isinstance(last_arg, Context):
1746 ctx = args[len(args)-1]
1747 args = args[:len(args)-1]
1748 elif len(args) == 1
and isinstance(args[0], AstVector):
1750 args = [a
for a
in args[0]]
1753 args = _get_args(args)
1754 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1756 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1757 if _has_probe(args):
1758 return _probe_or(args, ctx)
1760 args = _coerce_expr_list(args, ctx)
1761 _args, sz = _to_ast_array(args)
1762 return BoolRef(
Z3_mk_or(ctx.ref(), sz, _args), ctx)
Referenced by ApplyResult.as_expr().
◆ OrElse()
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]]
Definition at line 7835 of file z3py.py.
7836 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
7839 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
7840 >>> # Tactic split-clause fails if there is no clause in the given goal.
7843 >>> t(Or(x == 0, x == 1))
7844 [[x == 0], [x == 1]]
7847 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7848 ctx = ks.get(
'ctx',
None)
7851 for i
in range(num - 1):
7852 r = _or_else(r, ts[i+1], ctx)
◆ ParAndThen()
def z3py.ParAndThen |
( |
|
t1, |
|
|
|
t2, |
|
|
|
ctx = None |
|
) |
| |
Alias for ParThen(t1, t2, ctx).
Definition at line 7887 of file z3py.py.
7888 """Alias for ParThen(t1, t2, ctx)."""
◆ ParOr()
def z3py.ParOr |
( |
* |
ts, |
|
|
** |
ks |
|
) |
| |
Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
>>> x = Int('x')
>>> t = ParOr(Tactic('simplify'), Tactic('fail'))
>>> t(x + 1 == 2)
[[x == 1]]
Definition at line 7855 of file z3py.py.
7855 def ParOr(*ts, **ks):
7856 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
7859 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
7864 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7865 ctx = _get_ctx(ks.get(
'ctx',
None))
7866 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7868 _args = (TacticObj * sz)()
7870 _args[i] = ts[i].tactic
◆ parse_smt2_file()
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 8660 of file z3py.py.
8661 """Parse a file in SMT 2.0 format using the given sorts and decls.
8663 This function is similar to parse_smt2_string().
8666 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8667 dsz, dnames, ddecls = _dict2darray(decls, ctx)
8668 return AstVector(
Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
◆ parse_smt2_string()
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 8640 of file z3py.py.
8641 """Parse a string in SMT 2.0 format using the given sorts and decls.
8643 The arguments sorts and decls are Python dictionaries used to initialize
8644 the symbol table used for the SMT 2.0 parser.
8646 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
8648 >>> x, y = Ints('x y')
8649 >>> f = Function('f', IntSort(), IntSort())
8650 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
8652 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
8656 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8657 dsz, dnames, ddecls = _dict2darray(decls, ctx)
◆ ParThen()
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 7873 of file z3py.py.
7873 def ParThen(t1, t2, ctx=None):
7874 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
7876 >>> x, y = Ints('x y')
7877 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
7878 >>> t(And(Or(x == 1, x == 2), y == x + 1))
7879 [[x == 1, y == 2], [x == 2, y == 3]]
7881 t1 = _to_tactic(t1, ctx)
7882 t2 = _to_tactic(t2, ctx)
7884 _z3_assert(t1.ctx == t2.ctx,
"Context mismatch")
Referenced by ParAndThen().
◆ PartialOrder()
def z3py.PartialOrder |
( |
|
a, |
|
|
|
index |
|
) |
| |
◆ PbEq()
def z3py.PbEq |
( |
|
args, |
|
|
|
k, |
|
|
|
ctx = None |
|
) |
| |
Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 8447 of file z3py.py.
8447 def PbEq(args, k, ctx = None):
8448 """Create a Pseudo-Boolean inequality k constraint.
8450 >>> a, b, c = Bools('a b c')
8451 >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
8453 _z3_check_cint_overflow(k,
"k")
8454 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8455 return BoolRef(
Z3_mk_pbeq(ctx.ref(), sz, _args, _coeffs, k), ctx)
◆ PbGe()
def z3py.PbGe |
( |
|
args, |
|
|
|
k |
|
) |
| |
Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbGe(((a,1),(b,3),(c,2)), 3)
Definition at line 8437 of file z3py.py.
8438 """Create a Pseudo-Boolean inequality k constraint.
8440 >>> a, b, c = Bools('a b c')
8441 >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8443 _z3_check_cint_overflow(k,
"k")
8444 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8445 return BoolRef(
Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
◆ PbLe()
def z3py.PbLe |
( |
|
args, |
|
|
|
k |
|
) |
| |
Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbLe(((a,1),(b,3),(c,2)), 3)
Definition at line 8427 of file z3py.py.
8428 """Create a Pseudo-Boolean inequality k constraint.
8430 >>> a, b, c = Bools('a b c')
8431 >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8433 _z3_check_cint_overflow(k,
"k")
8434 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8435 return BoolRef(
Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
◆ PiecewiseLinearOrder()
def z3py.PiecewiseLinearOrder |
( |
|
a, |
|
|
|
index |
|
) |
| |
◆ Plus()
Create the regular expression accepting one or more repetitions of argument.
>>> re = Plus(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
False
Definition at line 10422 of file z3py.py.
10423 """Create the regular expression accepting one or more repetitions of argument.
10424 >>> re = Plus(Re("a"))
10425 >>> print(simplify(InRe("aa", re)))
10427 >>> print(simplify(InRe("ab", re)))
10429 >>> print(simplify(InRe("", re)))
10432 return ReRef(
Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
◆ PrefixOf()
def z3py.PrefixOf |
( |
|
a, |
|
|
|
b |
|
) |
| |
Check if 'a' is a prefix of 'b'
>>> s1 = PrefixOf("ab", "abc")
>>> simplify(s1)
True
>>> s2 = PrefixOf("bc", "abc")
>>> simplify(s2)
False
Definition at line 10212 of file z3py.py.
10213 """Check if 'a' is a prefix of 'b'
10214 >>> s1 = PrefixOf("ab", "abc")
10217 >>> s2 = PrefixOf("bc", "abc")
10221 ctx = _get_ctx2(a, b)
10222 a = _coerce_seq(a, ctx)
10223 b = _coerce_seq(b, ctx)
10224 return BoolRef(
Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ probe_description()
def z3py.probe_description |
( |
|
name, |
|
|
|
ctx = None |
|
) |
| |
Return a short description for the probe named `name`.
>>> d = probe_description('memory')
Definition at line 8145 of file z3py.py.
8146 """Return a short description for the probe named `name`.
8148 >>> d = probe_description('memory')
Referenced by describe_probes().
◆ 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 8135 of file z3py.py.
8136 """Return a list of all available probes in Z3.
8139 >>> l.count('memory') == 1
Referenced by describe_probes().
◆ Product()
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 8343 of file z3py.py.
8344 """Create the product of the Z3 expressions.
8346 >>> a, b, c = Ints('a b c')
8347 >>> Product(a, b, c)
8349 >>> Product([a, b, c])
8351 >>> A = IntVector('a', 5)
8353 a__0*a__1*a__2*a__3*a__4
8355 args = _get_args(args)
8358 ctx = _ctx_from_ast_arg_list(args)
8360 return _reduce(
lambda a, b: a * b, args, 1)
8361 args = _coerce_expr_list(args, ctx)
8363 return _reduce(
lambda a, b: a * b, args, 1)
8365 _args, sz = _to_ast_array(args)
8366 return ArithRef(
Z3_mk_mul(ctx.ref(), sz, _args), ctx)
◆ prove()
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 8515 of file z3py.py.
8515 def prove(claim, **keywords):
8516 """Try to prove the given claim.
8518 This is a simple function for creating demonstrations. It tries to prove
8519 `claim` by showing the negation is unsatisfiable.
8521 >>> p, q = Bools('p q')
8522 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
8526 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8530 if keywords.get(
'show',
False):
8536 print(
"failed to prove")
8539 print(
"counterexample")
◆ Q()
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 3033 of file z3py.py.
3033 def Q(a, b, ctx=None):
3034 """Return a Z3 rational a/b.
3036 If `ctx=None`, then the global context is used.
◆ Range()
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 10474 of file z3py.py.
10474 def Range(lo, hi, ctx = None):
10475 """Create the range regular expression over two sequences of length 1
10476 >>> range = Range("a","z")
10477 >>> print(simplify(InRe("b", range)))
10479 >>> print(simplify(InRe("bb", range)))
10482 lo = _coerce_seq(lo, ctx)
10483 hi = _coerce_seq(hi, ctx)
10484 return ReRef(
Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
◆ RatVal()
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 3018 of file z3py.py.
3018 def RatVal(a, b, ctx=None):
3019 """Return a Z3 rational a/b.
3021 If `ctx=None`, then the global context is used.
3025 >>> RatVal(3,5).sort()
3029 _z3_assert(_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
3030 _z3_assert(_is_int(b)
or isinstance(b, str),
"Second argument cannot be converted into an integer")
Referenced by Q().
◆ Re()
def z3py.Re |
( |
|
s, |
|
|
|
ctx = None |
|
) |
| |
The regular expression that accepts sequence 's'
>>> s1 = Re("ab")
>>> s2 = Re(StringVal("ab"))
>>> s3 = Re(Unit(BoolVal(True)))
Definition at line 10334 of file z3py.py.
10334 def Re(s, ctx=None):
10335 """The regular expression that accepts sequence 's'
10337 >>> s2 = Re(StringVal("ab"))
10338 >>> s3 = Re(Unit(BoolVal(True)))
10340 s = _coerce_seq(s, ctx)
◆ Real()
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 3094 of file z3py.py.
3094 def Real(name, ctx=None):
3095 """Return a real constant named `name`. If `ctx=None`, then the global context is used.
Referenced by Reals(), and RealVector().
◆ Reals()
def z3py.Reals |
( |
|
names, |
|
|
|
ctx = None |
|
) |
| |
Return a tuple of real constants.
>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real
Definition at line 3106 of file z3py.py.
3106 def Reals(names, ctx=None):
3107 """Return a tuple of real constants.
3109 >>> x, y, z = Reals('x y z')
3112 >>> Sum(x, y, z).sort()
3116 if isinstance(names, str):
3117 names = names.split(
" ")
3118 return [
Real(name, ctx)
for name
in names]
◆ RealSort()
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 2958 of file z3py.py.
2959 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2963 >>> x = Const('x', RealSort())
2968 >>> x.sort() == RealSort()
Referenced by FreshReal(), Real(), RealVal(), and RealVar().
◆ RealVal()
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 3000 of file z3py.py.
3001 """Return a Z3 real value.
3003 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
3004 If `ctx=None`, then the global context is used.
3008 >>> RealVal(1).sort()
Referenced by Cbrt(), AlgebraicNumRef.index(), RatVal(), and Sqrt().
◆ RealVar()
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 1363 of file z3py.py.
1365 Create a real free variable. Free variables are used to create quantified formulas.
1366 They are also used to create polynomials.
Referenced by RealVarVector().
◆ RealVarVector()
def z3py.RealVarVector |
( |
|
n, |
|
|
|
ctx = None |
|
) |
| |
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1
>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)
Definition at line 1373 of file z3py.py.
1375 Create a list of Real free variables.
1376 The variables have ids: 0, 1, ..., n-1
1378 >>> x0, x1, x2, x3 = RealVarVector(4)
◆ RealVector()
def z3py.RealVector |
( |
|
prefix, |
|
|
|
sz, |
|
|
|
ctx = None |
|
) |
| |
Return a list of real constants of size `sz`.
>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real
Definition at line 3120 of file z3py.py.
3121 """Return a list of real constants of size `sz`.
3123 >>> X = RealVector('x', 3)
3132 return [
Real(
'%s__%s' % (prefix, i), ctx)
for i
in range(sz) ]
◆ RecAddDefinition()
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 860 of file z3py.py.
861 """Set the body of a recursive function.
862 Recursive definitions can be simplified if they are applied to ground
865 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
866 >>> n = Int('n', ctx)
867 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
870 >>> s = Solver(ctx=ctx)
871 >>> s.add(fac(n) < 3)
874 >>> s.model().eval(fac(5))
880 args = _get_args(args)
884 _args[i] = args[i].ast
◆ RecFunction()
def z3py.RecFunction |
( |
|
name, |
|
|
* |
sig |
|
) |
| |
Create a new Z3 recursive with the given sorts.
Definition at line 843 of file z3py.py.
844 """Create a new Z3 recursive with the given sorts."""
847 _z3_assert(len(sig) > 0,
"At least two arguments expected")
851 _z3_assert(
is_sort(rng),
"Z3 sort expected")
852 dom = (Sort * arity)()
853 for i
in range(arity):
855 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
◆ Repeat()
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 7917 of file z3py.py.
7917 def Repeat(t, max=4294967295, ctx=None):
7918 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
7920 >>> x, y = Ints('x y')
7921 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
7922 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
7924 >>> for subgoal in r: print(subgoal)
7925 [x == 0, y == 0, x > y]
7926 [x == 0, y == 1, x > y]
7927 [x == 1, y == 0, x > y]
7928 [x == 1, y == 1, x > y]
7929 >>> t = Then(t, Tactic('propagate-values'))
7933 t = _to_tactic(t, ctx)
◆ RepeatBitVec()
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 4171 of file z3py.py.
4172 """Return an expression representing `n` copies of `a`.
4174 >>> x = BitVec('x', 8)
4175 >>> n = RepeatBitVec(4, x)
4180 >>> v0 = BitVecVal(10, 4)
4181 >>> print("%.x" % v0.as_long())
4183 >>> v = simplify(RepeatBitVec(4, v0))
4186 >>> print("%.x" % v.as_long())
4190 _z3_assert(_is_int(n),
"First argument must be an integer")
4191 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4192 return BitVecRef(
Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
◆ Replace()
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 10259 of file z3py.py.
10260 """Replace the first occurrence of 'src' by 'dst' in 's'
10261 >>> r = Replace("aaa", "a", "b")
10265 ctx = _get_ctx2(dst, s)
10266 if ctx
is None and is_expr(src):
10268 src = _coerce_seq(src, ctx)
10269 dst = _coerce_seq(dst, ctx)
10270 s = _coerce_seq(s, ctx)
10271 return SeqRef(
Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
◆ reset_params()
def z3py.reset_params |
( |
| ) |
|
Reset all global (or module) parameters.
Definition at line 263 of file z3py.py.
264 """Reset all global (or module) parameters.
◆ ReSort()
Definition at line 10354 of file z3py.py.
10357 if s
is None or isinstance(s, Context):
10360 raise Z3Exception(
"Regular expression sort constructor expects either a string or a context or no argument")
◆ RNA()
def z3py.RNA |
( |
|
ctx = None | ) |
|
◆ RNE()
def z3py.RNE |
( |
|
ctx = None | ) |
|
◆ RotateLeft()
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 4085 of file z3py.py.
4086 """Return an expression representing `a` rotated to the left `b` times.
4088 >>> a, b = BitVecs('a b', 16)
4089 >>> RotateLeft(a, b)
4091 >>> simplify(RotateLeft(a, 0))
4093 >>> simplify(RotateLeft(a, 16))
4096 _check_bv_args(a, b)
4097 a, b = _coerce_exprs(a, b)
◆ RotateRight()
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 4100 of file z3py.py.
4101 """Return an expression representing `a` rotated to the right `b` times.
4103 >>> a, b = BitVecs('a b', 16)
4104 >>> RotateRight(a, b)
4106 >>> simplify(RotateRight(a, 0))
4108 >>> simplify(RotateRight(a, 16))
4111 _check_bv_args(a, b)
4112 a, b = _coerce_exprs(a, b)
◆ RoundNearestTiesToAway()
def z3py.RoundNearestTiesToAway |
( |
|
ctx = None | ) |
|
◆ RoundNearestTiesToEven()
def z3py.RoundNearestTiesToEven |
( |
|
ctx = None | ) |
|
◆ RoundTowardNegative()
def z3py.RoundTowardNegative |
( |
|
ctx = None | ) |
|
◆ RoundTowardPositive()
def z3py.RoundTowardPositive |
( |
|
ctx = None | ) |
|
◆ RoundTowardZero()
def z3py.RoundTowardZero |
( |
|
ctx = None | ) |
|
◆ RTN()
def z3py.RTN |
( |
|
ctx = None | ) |
|
◆ RTP()
def z3py.RTP |
( |
|
ctx = None | ) |
|
◆ RTZ()
def z3py.RTZ |
( |
|
ctx = None | ) |
|
◆ Select()
Return a Z3 select array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> i = Int('i')
>>> Select(a, i)
a[i]
>>> eq(Select(a, i), a[i])
True
Definition at line 4505 of file z3py.py.
4506 """Return a Z3 select array expression.
4508 >>> a = Array('a', IntSort(), IntSort())
4512 >>> eq(Select(a, i), a[i])
4516 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
◆ SeqSort()
Create a sequence sort over elements provided in the argument
>>> s = SeqSort(IntSort())
>>> s == Unit(IntVal(1)).sort()
True
Definition at line 10037 of file z3py.py.
10038 """Create a sequence sort over elements provided in the argument
10039 >>> s = SeqSort(IntSort())
10040 >>> s == Unit(IntVal(1)).sort()
◆ set_default_fp_sort()
def z3py.set_default_fp_sort |
( |
|
ebits, |
|
|
|
sbits, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 8713 of file z3py.py.
8714 global _dflt_fpsort_ebits
8715 global _dflt_fpsort_sbits
8716 _dflt_fpsort_ebits = ebits
8717 _dflt_fpsort_sbits = sbits
◆ set_default_rounding_mode()
def z3py.set_default_rounding_mode |
( |
|
rm, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 8697 of file z3py.py.
8698 global _dflt_rounding_mode
8700 _dflt_rounding_mode = rm.decl().kind()
8702 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO
or
8703 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE
or
8704 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE
or
8705 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
or
8706 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
8707 "illegal rounding mode")
8708 _dflt_rounding_mode = rm
◆ set_option()
def z3py.set_option |
( |
* |
args, |
|
|
** |
kws |
|
) |
| |
Alias for 'set_param' for backward compatibility.
Definition at line 268 of file z3py.py.
269 """Alias for 'set_param' for backward compatibility.
◆ set_param()
def z3py.set_param |
( |
* |
args, |
|
|
** |
kws |
|
) |
| |
Set Z3 global (or module) parameters.
>>> set_param(precision=10)
Definition at line 240 of file z3py.py.
241 """Set Z3 global (or module) parameters.
243 >>> set_param(precision=10)
246 _z3_assert(len(args) % 2 == 0,
"Argument list must have an even number of elements.")
250 if not set_pp_option(k, v):
Referenced by set_option().
◆ SetAdd()
Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)
Definition at line 4653 of file z3py.py.
4654 """ Add element e to set s
4655 >>> a = Const('a', SetSort(IntSort()))
4659 ctx = _ctx_from_ast_arg_list([s,e])
4660 e = _py2expr(e, ctx)
4661 return ArrayRef(
Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
◆ SetComplement()
def z3py.SetComplement |
( |
|
s | ) |
|
The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)
Definition at line 4673 of file z3py.py.
4674 """ The complement of set s
4675 >>> a = Const('a', SetSort(IntSort()))
4676 >>> SetComplement(a)
◆ SetDel()
Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
Definition at line 4663 of file z3py.py.
4664 """ Remove element e to set s
4665 >>> a = Const('a', SetSort(IntSort()))
4669 ctx = _ctx_from_ast_arg_list([s,e])
4670 e = _py2expr(e, ctx)
4671 return ArrayRef(
Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
◆ SetDifference()
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 4682 of file z3py.py.
4683 """ The set difference of a and b
4684 >>> a = Const('a', SetSort(IntSort()))
4685 >>> b = Const('b', SetSort(IntSort()))
4686 >>> SetDifference(a, b)
4689 ctx = _ctx_from_ast_arg_list([a, b])
◆ SetHasSize()
def z3py.SetHasSize |
( |
|
a, |
|
|
|
k |
|
) |
| |
Definition at line 4574 of file z3py.py.
4576 k = _py2expr(k, ctx)
◆ SetIntersect()
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 4641 of file z3py.py.
4642 """ Take the union of sets
4643 >>> a = Const('a', SetSort(IntSort()))
4644 >>> b = Const('b', SetSort(IntSort()))
4645 >>> SetIntersect(a, b)
4648 args = _get_args(args)
4649 ctx = _ctx_from_ast_arg_list(args)
4650 _args, sz = _to_ast_array(args)
◆ SetSort()
Sets.
Create a set sort over element sort s
Definition at line 4609 of file z3py.py.
4610 """ Create a set sort over element sort s"""
◆ SetUnion()
def z3py.SetUnion |
( |
* |
args | ) |
|
Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetUnion(a, b)
union(a, b)
Definition at line 4629 of file z3py.py.
4630 """ Take the union of sets
4631 >>> a = Const('a', SetSort(IntSort()))
4632 >>> b = Const('b', SetSort(IntSort()))
4636 args = _get_args(args)
4637 ctx = _ctx_from_ast_arg_list(args)
4638 _args, sz = _to_ast_array(args)
◆ SignExt()
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 4115 of file z3py.py.
4116 """Return a bit-vector expression with `n` extra sign-bits.
4118 >>> x = BitVec('x', 16)
4119 >>> n = SignExt(8, x)
4126 >>> v0 = BitVecVal(2, 2)
4131 >>> v = simplify(SignExt(6, v0))
4136 >>> print("%.x" % v.as_long())
4140 _z3_assert(_is_int(n),
"First argument must be an integer")
4141 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4142 return BitVecRef(
Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
◆ SimpleSolver()
def z3py.SimpleSolver |
( |
|
ctx = None , |
|
|
|
logFile = None |
|
) |
| |
Return a simple general purpose solver with limited amount of preprocessing.
>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
Definition at line 6988 of file z3py.py.
6989 """Return a simple general purpose solver with limited amount of preprocessing.
6991 >>> s = SimpleSolver()
◆ simplify()
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 8239 of file z3py.py.
8239 def simplify(a, *arguments, **keywords):
8240 """Simplify the expression `a` using the given options.
8242 This function has many options. Use `help_simplify` to obtain the complete list.
8246 >>> simplify(x + 1 + y + x + 1)
8248 >>> simplify((x + 1)*(y + 1), som=True)
8250 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
8251 And(Not(x == y), Not(x == 1), Not(y == 1))
8252 >>> simplify(And(x == 0, y == 1), elim_and=True)
8253 Not(Or(Not(x == 0), Not(y == 1)))
8256 _z3_assert(
is_expr(a),
"Z3 expression expected")
8257 if len(arguments) > 0
or len(keywords) > 0:
8259 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8261 return _to_expr_ref(
Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
Referenced by Q(), and RatVal().
◆ simplify_param_descrs()
def z3py.simplify_param_descrs |
( |
| ) |
|
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 8267 of file z3py.py.
8268 """Return the set of parameter descriptions for Z3 `simplify` procedure."""
◆ solve()
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 8458 of file z3py.py.
8458 def solve(*args, **keywords):
8459 """Solve the constraints `*args`.
8461 This is a simple function for creating demonstrations. It creates a solver,
8462 configure it using the options in `keywords`, adds the constraints
8463 in `args`, and invokes check.
8466 >>> solve(a > 0, a < 2)
8472 if keywords.get(
'show',
False):
8476 print(
"no solution")
8478 print(
"failed to solve")
◆ solve_using()
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 8486 of file z3py.py.
8487 """Solve the constraints `*args` using solver `s`.
8489 This is a simple function for creating demonstrations. It is similar to `solve`,
8490 but it uses the given solver `s`.
8491 It configures solver `s` using the options in `keywords`, adds the constraints
8492 in `args`, and invokes check.
8495 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8498 if keywords.get(
'show',
False):
8503 print(
"no solution")
8505 print(
"failed to solve")
8511 if keywords.get(
'show',
False):
◆ SolverFor()
def z3py.SolverFor |
( |
|
logic, |
|
|
|
ctx = None , |
|
|
|
logFile = None |
|
) |
| |
Create a solver customized for the given logic.
The parameter `logic` is a string. It should be contains
the name of a SMT-LIB logic.
See http://www.smtlib.org/ for the name of all available logics.
>>> s = SolverFor("QF_LIA")
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> s.check()
sat
>>> s.model()
[x = 1]
Definition at line 6968 of file z3py.py.
6968 def SolverFor(logic, ctx=None, logFile=None):
6969 """Create a solver customized for the given logic.
6971 The parameter `logic` is a string. It should be contains
6972 the name of a SMT-LIB logic.
6973 See http://www.smtlib.org/ for the name of all available logics.
6975 >>> s = SolverFor("QF_LIA")
◆ Sqrt()
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 3197 of file z3py.py.
3197 def Sqrt(a, ctx=None):
3198 """ Return a Z3 expression which represents the square root of a.
◆ SRem()
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 4034 of file z3py.py.
4035 """Create the Z3 expression signed remainder.
4037 Use the operator % for signed modulus, and URem() for unsigned remainder.
4039 >>> x = BitVec('x', 32)
4040 >>> y = BitVec('y', 32)
4043 >>> SRem(x, y).sort()
4047 >>> SRem(x, y).sexpr()
4050 _check_bv_args(a, b)
4051 a, b = _coerce_exprs(a, b)
4052 return BitVecRef(
Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ Star()
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 10450 of file z3py.py.
10451 """Create the regular expression accepting zero or more repetitions of argument.
10452 >>> re = Star(Re("a"))
10453 >>> print(simplify(InRe("aa", re)))
10455 >>> print(simplify(InRe("ab", re)))
10457 >>> print(simplify(InRe("", re)))
10460 return ReRef(
Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
◆ Store()
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 4489 of file z3py.py.
4490 """Return a Z3 store array expression.
4492 >>> a = Array('a', IntSort(), IntSort())
4493 >>> i, v = Ints('i v')
4494 >>> s = Store(a, i, v)
4497 >>> prove(s[i] == v)
4500 >>> prove(Implies(i != j, s[j] == a[j]))
◆ String()
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 10145 of file z3py.py.
10145 def String(name, ctx=None):
10146 """Return a string constant named `name`. If `ctx=None`, then the global context is used.
10148 >>> x = String('x')
10150 ctx = _get_ctx(ctx)
Referenced by Strings(), and SubSeq().
◆ Strings()
def Strings |
( |
|
names, |
|
|
|
ctx = None |
|
) |
| |
Return string constants
Return a tuple of String constants.
Definition at line 10153 of file z3py.py.
10153 def Strings(names, ctx=None):
10154 """Return string constants"""
10155 ctx = _get_ctx(ctx)
10156 if isinstance(names, str):
10157 names = names.split(
" ")
10158 return [
String(name, ctx)
for name
in names]
Referenced by SubSeq().
◆ StringSort()
def z3py.StringSort |
( |
|
ctx = None | ) |
|
Create a string sort
>>> s = StringSort()
>>> print(s)
String
Definition at line 10027 of file z3py.py.
10028 """Create a string sort
10029 >>> s = StringSort()
10033 ctx = _get_ctx(ctx)
Referenced by String().
◆ StringVal()
def z3py.StringVal |
( |
|
s, |
|
|
|
ctx = None |
|
) |
| |
◆ StrToInt()
Convert string expression to integer
>>> a = StrToInt("1")
>>> simplify(1 == a)
True
>>> b = StrToInt("2")
>>> simplify(1 == b)
False
>>> c = StrToInt(IntToStr(2))
>>> simplify(1 == c)
False
Definition at line 10311 of file z3py.py.
10312 """Convert string expression to integer
10313 >>> a = StrToInt("1")
10314 >>> simplify(1 == a)
10316 >>> b = StrToInt("2")
10317 >>> simplify(1 == b)
10319 >>> c = StrToInt(IntToStr(2))
10320 >>> simplify(1 == c)
◆ SubSeq()
def z3py.SubSeq |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10164 of file z3py.py.
10164 def SubSeq(s, offset, length):
10165 """Extract substring or subsequence starting at offset"""
10166 return Extract(s, offset, length)
◆ substitute()
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 8271 of file z3py.py.
8272 """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.
8276 >>> substitute(x + 1, (x, y + 1))
8278 >>> f = Function('f', IntSort(), IntSort())
8279 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
8282 if isinstance(m, tuple):
8284 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8287 _z3_assert(
is_expr(t),
"Z3 expression expected")
8288 _z3_assert(all([isinstance(p, tuple)
and is_expr(p[0])
and is_expr(p[1])
and p[0].sort().
eq(p[1].sort())
for p
in m]),
"Z3 invalid substitution, expression pairs expected.")
8290 _from = (Ast * num)()
8292 for i
in range(num):
8293 _from[i] = m[i][0].as_ast()
8294 _to[i] = m[i][1].as_ast()
8295 return _to_expr_ref(
Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
◆ substitute_vars()
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 8297 of file z3py.py.
8298 """Substitute the free variables in t with the expression in m.
8300 >>> v0 = Var(0, IntSort())
8301 >>> v1 = Var(1, IntSort())
8303 >>> f = Function('f', IntSort(), IntSort(), IntSort())
8304 >>> # replace v0 with x+1 and v1 with x
8305 >>> substitute_vars(f(v0, v1), x + 1, x)
8309 _z3_assert(
is_expr(t),
"Z3 expression expected")
8310 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8313 for i
in range(num):
8314 _to[i] = m[i].as_ast()
◆ SubString()
def z3py.SubString |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10160 of file z3py.py.
10161 """Extract substring or subsequence starting at offset"""
10162 return Extract(s, offset, length)
◆ SuffixOf()
def z3py.SuffixOf |
( |
|
a, |
|
|
|
b |
|
) |
| |
Check if 'a' is a suffix of 'b'
>>> s1 = SuffixOf("ab", "abc")
>>> simplify(s1)
False
>>> s2 = SuffixOf("bc", "abc")
>>> simplify(s2)
True
Definition at line 10226 of file z3py.py.
10227 """Check if 'a' is a suffix of 'b'
10228 >>> s1 = SuffixOf("ab", "abc")
10231 >>> s2 = SuffixOf("bc", "abc")
10235 ctx = _get_ctx2(a, b)
10236 a = _coerce_seq(a, ctx)
10237 b = _coerce_seq(b, ctx)
10238 return BoolRef(
Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ Sum()
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 8317 of file z3py.py.
8318 """Create the sum of the Z3 expressions.
8320 >>> a, b, c = Ints('a b c')
8325 >>> A = IntVector('a', 5)
8327 a__0 + a__1 + a__2 + a__3 + a__4
8329 args = _get_args(args)
8332 ctx = _ctx_from_ast_arg_list(args)
8334 return _reduce(
lambda a, b: a + b, args, 0)
8335 args = _coerce_expr_list(args, ctx)
8337 return _reduce(
lambda a, b: a + b, args, 0)
8339 _args, sz = _to_ast_array(args)
8340 return ArithRef(
Z3_mk_add(ctx.ref(), sz, _args), ctx)
◆ tactic_description()
def z3py.tactic_description |
( |
|
name, |
|
|
|
ctx = None |
|
) |
| |
Return a short description for the tactic named `name`.
>>> d = tactic_description('simplify')
Definition at line 7954 of file z3py.py.
7955 """Return a short description for the tactic named `name`.
7957 >>> d = tactic_description('simplify')
Referenced by describe_tactics().
◆ 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 7944 of file z3py.py.
7945 """Return a list of all available tactics in Z3.
7948 >>> l.count('simplify') == 1
Referenced by describe_tactics(), and z3.par_or().
◆ Then()
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 7823 of file z3py.py.
7823 def Then(*ts, **ks):
7824 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
7826 >>> x, y = Ints('x y')
7827 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
7828 >>> t(And(x == 0, y > x + 1))
7830 >>> t(And(x == 0, y > x + 1)).as_expr()
◆ to_symbol()
def z3py.to_symbol |
( |
|
s, |
|
|
|
ctx = None |
|
) |
| |
Convert an integer or string into a Z3 symbol.
Definition at line 109 of file z3py.py.
110 """Convert an integer or string into a Z3 symbol."""
Referenced by Fixedpoint.add_rule(), Optimize.add_soft(), Array(), BitVec(), Bool(), Const(), CreateDatatypes(), DeclareSort(), EnumSort(), FiniteDomainSort(), FP(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), is_quantifier(), prove(), Real(), RecFunction(), ParamsRef.set(), Fixedpoint.set_predicate_representation(), SolverFor(), String(), and Fixedpoint.update_rule().
◆ ToInt()
Return the Z3 expression ToInt(a).
>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int
Definition at line 3164 of file z3py.py.
3165 """ Return the Z3 expression ToInt(a).
3177 _z3_assert(a.is_real(),
"Z3 real expression expected.")
◆ ToReal()
Return the Z3 expression ToReal(a).
>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real
Definition at line 3147 of file z3py.py.
3148 """ Return the Z3 expression ToReal(a).
3160 _z3_assert(a.is_int(),
"Z3 integer expression expected.")
◆ TransitiveClosure()
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 10500 of file z3py.py.
10501 """Given a binary relation R, such that the two arguments have the same sort
10502 create the transitive closure relation R+.
10503 The transitive closure R+ is a new relation.
◆ TreeOrder()
def z3py.TreeOrder |
( |
|
a, |
|
|
|
index |
|
) |
| |
◆ TryFor()
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 7936 of file z3py.py.
7936 def TryFor(t, ms, ctx=None):
7937 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
7939 If `t` does not terminate in `ms` milliseconds, then it fails.
7941 t = _to_tactic(t, ctx)
◆ TupleSort()
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 5012 of file z3py.py.
5013 """Create a named tuple sort base on a set of underlying sorts
5015 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
5017 tuple = Datatype(name, ctx)
5018 projects = [ (
'project%d' % i, sorts[i])
for i
in range(len(sorts)) ]
5019 tuple.declare(name, *projects)
5020 tuple = tuple.create()
5021 return tuple, tuple.constructor(0), [tuple.accessor(0, i)
for i
in range(len(sorts))]
◆ UDiv()
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 3994 of file z3py.py.
3995 """Create the Z3 expression (unsigned) division `self / other`.
3997 Use the operator / for signed division.
3999 >>> x = BitVec('x', 32)
4000 >>> y = BitVec('y', 32)
4003 >>> UDiv(x, y).sort()
4007 >>> UDiv(x, y).sexpr()
4010 _check_bv_args(a, b)
4011 a, b = _coerce_exprs(a, b)
4012 return BitVecRef(
Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ UGE()
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 3960 of file z3py.py.
3961 """Create the Z3 expression (unsigned) `other >= self`.
3963 Use the operator >= for signed greater than or equal to.
3965 >>> x, y = BitVecs('x y', 32)
3968 >>> (x >= y).sexpr()
3970 >>> UGE(x, y).sexpr()
3973 _check_bv_args(a, b)
3974 a, b = _coerce_exprs(a, b)
3975 return BoolRef(
Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ UGT()
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 3977 of file z3py.py.
3978 """Create the Z3 expression (unsigned) `other > self`.
3980 Use the operator > for signed greater than.
3982 >>> x, y = BitVecs('x y', 32)
3987 >>> UGT(x, y).sexpr()
3990 _check_bv_args(a, b)
3991 a, b = _coerce_exprs(a, b)
3992 return BoolRef(
Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ ULE()
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 3926 of file z3py.py.
3927 """Create the Z3 expression (unsigned) `other <= self`.
3929 Use the operator <= for signed less than or equal to.
3931 >>> x, y = BitVecs('x y', 32)
3934 >>> (x <= y).sexpr()
3936 >>> ULE(x, y).sexpr()
3939 _check_bv_args(a, b)
3940 a, b = _coerce_exprs(a, b)
3941 return BoolRef(
Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ ULT()
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 3943 of file z3py.py.
3944 """Create the Z3 expression (unsigned) `other < self`.
3946 Use the operator < for signed less than.
3948 >>> x, y = BitVecs('x y', 32)
3953 >>> ULT(x, y).sexpr()
3956 _check_bv_args(a, b)
3957 a, b = _coerce_exprs(a, b)
3958 return BoolRef(
Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ Union()
Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> print (simplify(InRe("d", re)))
False
Definition at line 10386 of file z3py.py.
10387 """Create union of regular expressions.
10388 >>> re = Union(Re("a"), Re("b"), Re("c"))
10389 >>> print (simplify(InRe("d", re)))
10392 args = _get_args(args)
10395 _z3_assert(sz > 0,
"At least one argument expected.")
10396 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10401 for i
in range(sz):
10402 v[i] = args[i].as_ast()
Referenced by ReRef.__add__().
◆ Unit()
Create a singleton sequence
Definition at line 10208 of file z3py.py.
10209 """Create a singleton sequence"""
◆ Update()
def z3py.Update |
( |
|
a, |
|
|
|
i, |
|
|
|
v |
|
) |
| |
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 4457 of file z3py.py.
4458 """Return a Z3 store array expression.
4460 >>> a = Array('a', IntSort(), IntSort())
4461 >>> i, v = Ints('i v')
4462 >>> s = Update(a, i, v)
4465 >>> prove(s[i] == v)
4468 >>> prove(Implies(i != j, s[j] == a[j]))
4472 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4473 i = a.sort().domain().cast(i)
4474 v = a.sort().
range().cast(v)
4476 return _to_expr_ref(
Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
Referenced by Store().
◆ URem()
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 4014 of file z3py.py.
4015 """Create the Z3 expression (unsigned) remainder `self % other`.
4017 Use the operator % for signed modulus, and SRem() for signed remainder.
4019 >>> x = BitVec('x', 32)
4020 >>> y = BitVec('y', 32)
4023 >>> URem(x, y).sort()
4027 >>> URem(x, y).sexpr()
4030 _check_bv_args(a, b)
4031 a, b = _coerce_exprs(a, b)
4032 return BitVecRef(
Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ user_prop_diseq()
def z3py.user_prop_diseq |
( |
|
ctx, |
|
|
|
cb, |
|
|
|
x, |
|
|
|
y |
|
) |
| |
Definition at line 10574 of file z3py.py.
10575 prop = _prop_closures.get(ctx)
◆ user_prop_eq()
def z3py.user_prop_eq |
( |
|
ctx, |
|
|
|
cb, |
|
|
|
x, |
|
|
|
y |
|
) |
| |
Definition at line 10568 of file z3py.py.
10569 prop = _prop_closures.get(ctx)
◆ user_prop_final()
def z3py.user_prop_final |
( |
|
ctx, |
|
|
|
cb |
|
) |
| |
Definition at line 10562 of file z3py.py.
10563 prop = _prop_closures.get(ctx)
◆ user_prop_fixed()
def z3py.user_prop_fixed |
( |
|
ctx, |
|
|
|
cb, |
|
|
|
id, |
|
|
|
value |
|
) |
| |
Definition at line 10556 of file z3py.py.
10557 prop = _prop_closures.get(ctx)
10559 prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
◆ user_prop_fresh()
def z3py.user_prop_fresh |
( |
|
id, |
|
|
|
ctx |
|
) |
| |
Definition at line 10549 of file z3py.py.
10550 prop = _prop_closures.get(id)
10551 _prop_closures.set_threaded()
10552 new_prop = UsePropagateBase(
None, ctx)
10553 _prop_closures.set(new_prop.id, new_prop.fresh())
10554 return ctypes.c_void_p(new_prop.id)
◆ user_prop_pop()
def z3py.user_prop_pop |
( |
|
ctx, |
|
|
|
num_scopes |
|
) |
| |
Definition at line 10546 of file z3py.py.
10547 _prop_closures.get(ctx).
pop(num_scopes)
◆ user_prop_push()
def z3py.user_prop_push |
( |
|
ctx | ) |
|
◆ Var()
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 1351 of file z3py.py.
1352 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1354 >>> Var(0, IntSort())
1356 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1360 _z3_assert(
is_sort(s),
"Z3 sort expected")
1361 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
Referenced by RealVar().
◆ When()
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 8205 of file z3py.py.
8205 def When(p, t, ctx=None):
8206 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8208 >>> t = When(Probe('size') > 2, Tactic('simplify'))
8209 >>> x, y = Ints('x y')
8215 >>> g.add(x == y + 1)
8217 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8219 p = _to_probe(p, ctx)
8220 t = _to_tactic(t, ctx)
8221 return Tactic(
Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
◆ With()
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 7891 of file z3py.py.
7891 def With(t, *args, **keys):
7892 """Return a tactic that applies tactic `t` using the given configuration options.
7894 >>> x, y = Ints('x y')
7895 >>> t = With(Tactic('simplify'), som=True)
7896 >>> t((x + 1)*(y + 2) == 0)
7897 [[2*x + y + x*y == -2]]
7899 ctx = keys.pop(
'ctx',
None)
7900 t = _to_tactic(t, ctx)
◆ WithParams()
def z3py.WithParams |
( |
|
t, |
|
|
|
p |
|
) |
| |
Return a tactic that applies tactic `t` using the given configuration options.
>>> x, y = Ints('x y')
>>> p = ParamsRef()
>>> p.set("som", True)
>>> t = WithParams(Tactic('simplify'), p)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]
Definition at line 7904 of file z3py.py.
7905 """Return a tactic that applies tactic `t` using the given configuration options.
7907 >>> x, y = Ints('x y')
7909 >>> p.set("som", True)
7910 >>> t = WithParams(Tactic('simplify'), p)
7911 >>> t((x + 1)*(y + 2) == 0)
7912 [[2*x + y + x*y == -2]]
7914 t = _to_tactic(t,
None)
◆ Xor()
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 1654 of file z3py.py.
1654 def Xor(a, b, ctx=None):
1655 """Create a Z3 Xor expression.
1657 >>> p, q = Bools('p q')
1660 >>> simplify(Xor(p, q))
1663 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1667 return BoolRef(
Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
◆ z3_debug()
Definition at line 56 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AtLeast(), AtMost(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), ExprRef.children(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), describe_probes(), Distinct(), FuncDeclRef.domain(), EnumSort(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), AlgebraicNumRef.index(), Intersect(), is_quantifier(), is_sort(), IsInt(), K(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), OrElse(), Tactic.param_descrs(), ParOr(), ParThen(), QuantifierRef.pattern(), prove(), RatVal(), RealSort(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), simplify(), solve_using(), substitute(), substitute_vars(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Union(), Update(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
◆ z3_error_handler()
def z3py.z3_error_handler |
( |
|
c, |
|
|
|
e |
|
) |
| |
◆ 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 4144 of file z3py.py.
4145 """Return a bit-vector expression with `n` extra zero-bits.
4147 >>> x = BitVec('x', 16)
4148 >>> n = ZeroExt(8, x)
4155 >>> v0 = BitVecVal(2, 2)
4160 >>> v = simplify(ZeroExt(6, v0))
4167 _z3_assert(_is_int(n),
"First argument must be an integer")
4168 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4169 return BitVecRef(
Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
◆ sat
◆ unknown
◆ unsat
◆ Z3_DEBUG
Z3_ast Z3_API Z3_mk_re_plus(Z3_context c, Z3_ast re)
Create the regular language re+.
def Reals(names, ctx=None)
void Z3_API Z3_global_param_reset_all(void)
Restore the value of all global (and module) parameters. This command will not affect already created...
def fpInfinity(s, negative)
def fpRoundToIntegral(rm, a, ctx=None)
Z3_symbol Z3_API Z3_mk_string_symbol(Z3_context c, Z3_string s)
Create a Z3 symbol using a C string.
Z3_ast Z3_API Z3_mk_re_option(Z3_context c, Z3_ast re)
Create the regular language [re].
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a)
Convert an AST into a FUNC_DECL_AST. This is just type casting.
Z3_tactic Z3_API Z3_tactic_par_and_then(Z3_context c, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1....
def RoundTowardPositive(ctx=None)
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s)
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
def FreshReal(prefix='b', ctx=None)
Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s)
Integer to string conversion.
Z3_ast Z3_API Z3_mk_re_complement(Z3_context c, Z3_ast re)
Create the complement of the regular language re.
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i)
Return the name of the i probe.
void Z3_API Z3_get_version(unsigned *major, unsigned *minor, unsigned *build_number, unsigned *revision_number)
Return Z3 version number information.
Z3_ast Z3_API Z3_mk_ext_rotate_left(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the left t2 times.
def TupleSort(name, sorts, ctx=None)
Z3_ast Z3_API Z3_mk_true(Z3_context c)
Create an AST node representing true.
def fpBVToFP(v, sort, ctx=None)
Z3_ast_vector Z3_API Z3_parse_smtlib2_file(Z3_context c, Z3_string file_name, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflo...
def FPs(names, fpsort, ctx=None)
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_fresh_const(Z3_context c, Z3_string prefix, Z3_sort ty)
Declare and create a fresh constant.
Z3_ast Z3_API Z3_mk_zero_ext(Z3_context c, unsigned i, Z3_ast t1)
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i,...
Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a)
Return the function declaration f associated with a (_ as_array f) node.
def DisjointSum(name, sorts, ctx=None)
def Strings(names, ctx=None)
def user_prop_fixed(ctx, cb, id, value)
Z3_ast Z3_API Z3_mk_seq_concat(Z3_context c, unsigned n, Z3_ast const args[])
Concatenate sequences.
Z3_tactic Z3_API Z3_tactic_fail_if(Z3_context c, Z3_probe p)
Return a tactic that fails if the probe p evaluates to false.
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into an unsigned bit-vector.
def FPVal(sig, exp=None, fps=None, ctx=None)
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
def RealVarVector(n, ctx=None)
def fpToUBV(rm, x, s, ctx=None)
Z3_tactic Z3_API Z3_tactic_try_for(Z3_context c, Z3_tactic t, unsigned ms)
Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms mil...
Z3_ast Z3_API Z3_get_decl_ast_parameter(Z3_context c, Z3_func_decl d, unsigned idx)
Return the expression value associated with an expression parameter.
def user_prop_fresh(id, ctx)
void Z3_API Z3_append_log(Z3_string string)
Append user-defined string to interaction log.
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative)
Create a floating-point zero of sort s.
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
expr range(expr const &lo, expr const &hi)
def BVSubNoOverflow(a, b)
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re)
Create an universal regular expression of sort re.
def parse_smt2_string(s, sorts={}, decls={}, ctx=None)
Z3_ast Z3_API Z3_mk_bv2int(Z3_context c, Z3_ast t1, bool is_signed)
Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 is t...
def RoundTowardNegative(ctx=None)
Z3_ast Z3_API Z3_mk_and(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] and ... and args[num_args-1].
def set_param(*args, **kws)
def RatVal(a, b, ctx=None)
def IntVal(val, ctx=None)
void Z3_API Z3_add_rec_def(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast args[], Z3_ast body)
Define the body of a recursive function.
def fpToFP(a1, a2=None, a3=None, ctx=None)
Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k)
Create predicate that holds if Boolean array set has k elements set to true.
def fpUnsignedToFP(rm, v, sort, ctx=None)
Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem)
Remove an element to a set.
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3_ast Z3_API Z3_mk_seq_suffix(Z3_context c, Z3_ast suffix, Z3_ast s)
Check if suffix is a suffix of s.
def BoolVector(prefix, sz, ctx=None)
Z3_ast Z3_API Z3_mk_xor(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 xor t2.
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t1)
Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
def SubSeq(s, offset, length)
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig)
Create an expression of FloatingPoint sort from three bit-vector expressions.
def ensure_prop_closures()
def SimpleSolver(ctx=None, logFile=None)
def With(t, *args, **keys)
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain)
Create the full set.
def simplify(a, *arguments, **keywords)
Utils.
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic)
Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unkn...
Z3_string Z3_API Z3_simplify_get_help(Z3_context c)
Return a string describing all available parameters.
Z3_ast Z3_API Z3_mk_or(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] or ... or args[num_args-1].
Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size)
Create a named finite domain sort.
Z3_ast Z3_API Z3_mk_set_union(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the union of a list of sets.
def pop(self, num_scopes)
Z3_ast Z3_API Z3_mk_set_intersect(Z3_context c, unsigned num_args, Z3_ast const args[])
Take the intersection of a list of sets.
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
def to_symbol(s, ctx=None)
def fpMul(rm, a, b, ctx=None)
Z3_ast Z3_API Z3_mk_distinct(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing distinct(args[0], ..., args[num_args-1]).
Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p)
Interface to simplifier.
def fpGEQ(a, b, ctx=None)
Z3_func_decl Z3_API Z3_mk_rec_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a recursive function.
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain)
Create the empty set.
def fpRem(a, b, ctx=None)
def FiniteDomainSort(name, sz, ctx=None)
Z3_model Z3_API Z3_mk_model(Z3_context c)
Create a fresh model object. It has reference count 0.
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi)
Create a regular expression loop. The supplied regular expression r is repeated between lo and hi tim...
Z3_func_decl Z3_API Z3_mk_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a linear ordering relation over signature a. The relation is identified by the index id.
bool Z3_API Z3_is_as_array(Z3_context c, Z3_ast a)
The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3....
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz)
Conversion of a floating-point term into a signed bit-vector.
Z3_ast Z3_API Z3_mk_add(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] + ... + args[num_args-1].
def z3_error_handler(c, e)
def BitVecVal(val, bv, ctx=None)
Z3_ast Z3_API Z3_mk_bvugt(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than.
Z3_ast Z3_API Z3_mk_seq_prefix(Z3_context c, Z3_ast prefix, Z3_ast s)
Check if prefix is a prefix of s.
def Range(lo, hi, ctx=None)
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[])
Create a pattern for quantifier instantiation.
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
def Cond(p, t1, t2, ctx=None)
def is_finite_domain_sort(s)
Z3_ast Z3_API Z3_mk_concat(Z3_context c, Z3_ast t1, Z3_ast t2)
Concatenate the given bit-vectors.
Z3_ast Z3_API Z3_mk_implies(Z3_context c, Z3_ast t1, Z3_ast t2)
Create an AST node representing t1 implies t2.
def fpMax(a, b, ctx=None)
def RealVal(val, ctx=None)
def solve(*args, **keywords)
def RoundNearestTiesToEven(ctx=None)
Z3_ast Z3_API Z3_mk_seq_unit(Z3_context c, Z3_ast a)
Create a unit sequence of a.
Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t)
Return the sort kind (e.g., array, tuple, int, bool, etc).
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty)
Create a numeral of a given sort.
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
def fpToFPUnsigned(rm, x, s, ctx=None)
Z3_ast Z3_API Z3_mk_real2int(Z3_context c, Z3_ast t1)
Coerce a real to an integer.
def FloatQuadruple(ctx=None)
Z3_ast Z3_API Z3_mk_bvredor(Z3_context c, Z3_ast t1)
Take disjunction of bits in vector, return vector of length 1.
def If(a, b, c, ctx=None)
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits)
Create a FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
def set_default_rounding_mode(rm, ctx=None)
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a term of real sort into a term of FloatingPoint sort.
Z3_ast Z3_API Z3_mk_seq_length(Z3_context c, Z3_ast s)
Return the length of the sequence s.
Z3_ast Z3_API Z3_mk_re_star(Z3_context c, Z3_ast re)
Create the regular language re*.
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Create array extensionality index given two arrays with the same sort. The meaning is given by the ax...
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const *args)
Map f on the argument arrays.
def fpFMA(rm, a, b, c, ctx=None)
Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c)
Return the parameter description set for the simplify procedure.
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a real-numbered term.
def simplify_param_descrs()
def user_prop_eq(ctx, cb, x, y)
def fpSignedToFP(rm, v, sort, ctx=None)
def get_default_rounding_mode(ctx=None)
Z3_ast Z3_API Z3_mk_set_complement(Z3_context c, Z3_ast arg)
Take the complement of a set.
def PbEq(args, k, ctx=None)
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t)
Floating-point negation.
def user_prop_diseq(ctx, cb, x, y)
Z3_tactic Z3_API Z3_tactic_using_params(Z3_context c, Z3_tactic t, Z3_params p)
Return a tactic that applies t using the given set of parameters.
Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast, Z3_ast substr)
Return the last occurrence of substr in s. If s does not contain substr, then the value is -1,...
def BVAddNoOverflow(a, b, signed)
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c, Z3_symbol name, Z3_symbol recognizer, unsigned num_fields, Z3_symbol const field_names[], Z3_sort_opt const sorts[], unsigned sort_refs[])
Create a constructor.
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c)
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t)
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
def Ints(names, ctx=None)
def Extract(high, low, a)
Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s)
Convert string to integer.
def FreshBool(prefix='b', ctx=None)
def Array(name, dom, rng)
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i)
Return the name of the idx tactic.
Z3_ast Z3_API Z3_mk_repeat(Z3_context c, unsigned i, Z3_ast t1)
Repeat the given bit-vector up length i.
def ParAndThen(t1, t2, ctx=None)
def BVAddNoUnderflow(a, b)
def FloatDouble(ctx=None)
Z3_func_decl Z3_API Z3_mk_func_decl(Z3_context c, Z3_symbol s, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a constant or function.
def Bools(names, ctx=None)
def RoundNearestTiesToAway(ctx=None)
Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi)
Create the range regular expression over two sequences of length 1.
def parse_smt2_file(f, sorts={}, decls={}, ctx=None)
def substitute_vars(t, *m)
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
def Implies(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
def BVSDivNoOverflow(a, b)
def BitVec(name, bv, ctx=None)
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
def BitVecs(names, bv, ctx=None)
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
def LastIndexOf(s, substr)
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
def fpIsNormal(a, ctx=None)
def FreshConst(sort, prefix='c')
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
def probe_description(name, ctx=None)
def tactic_description(name, ctx=None)
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
def StringVal(s, ctx=None)
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
def fpFP(sgn, exp, sig, ctx=None)
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
def FPSort(ebits, sbits, ctx=None)
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
def DeclareSort(name, ctx=None)
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
def fpSqrt(rm, a, ctx=None)
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
def RealVar(idx, ctx=None)
def FP(name, fpsort, ctx=None)
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
def fpDiv(rm, a, b, ctx=None)
def set_default_fp_sort(ebits, sbits, ctx=None)
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a bound variable.
def PiecewiseLinearOrder(a, index)
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
def RecAddDefinition(f, args, body)
def fpToSBV(rm, x, s, ctx=None)
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
def FreshInt(prefix='x', ctx=None)
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
def solve_using(s, *args, **keywords)
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
def FiniteDomainVal(val, sort, ctx=None)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
def LinearOrder(a, index)
def BitVecSort(sz, ctx=None)
def fpAdd(rm, a, b, ctx=None)
def is_finite_domain_value(a)
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
def fpSub(rm, a, b, ctx=None)
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
def TryFor(t, ms, ctx=None)
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
def user_prop_final(ctx, cb)
def fpLEQ(a, b, ctx=None)
def EnumSort(name, values, ctx=None)
def BoolVal(val, ctx=None)
def get_default_fp_sort(ctx=None)
Z3_ast Z3_API Z3_mk_re_union(Z3_context c, unsigned n, Z3_ast const args[])
Create the union of the regular languages.
Z3_ast Z3_API Z3_mk_bvudiv(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned division.
Z3_sort Z3_API Z3_mk_re_sort(Z3_context c, Z3_sort seq)
Create a regular expression sort out of a sequence sort.
Z3_ast Z3_API Z3_mk_sign_ext(Z3_context c, unsigned i, Z3_ast t1)
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i,...
Z3_func_decl Z3_API Z3_mk_tree_order(Z3_context c, Z3_sort a, unsigned id)
create a tree ordering relation over signature a identified using index id.
Z3_sort Z3_API Z3_mk_seq_sort(Z3_context c, Z3_sort s)
Create a sequence sort out of the sort for the elements.
def SolverFor(logic, ctx=None, logFile=None)
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_substitute(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const from[], Z3_ast const to[])
Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs....
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c)
Create a new incremental solver.
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, bool is_signed)
Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
bool Z3_API Z3_open_log(Z3_string filename)
Log interaction to a file.
Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v)
Array update.
Z3_ast Z3_API Z3_mk_bvredand(Z3_context c, Z3_ast t1)
Take conjunction of bits in vector, return vector of length 1.
def IntVector(prefix, sz, ctx=None)
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_not(Z3_context c, Z3_ast a)
Create an AST node representing not(a).
def user_prop_pop(ctx, num_scopes)
def fpIsZero(a, ctx=None)
def PartialOrder(a, index)
void Z3_API Z3_enable_trace(Z3_string tag)
Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem)
Add an element to a set.
Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset)
Return index of first occurrence of substr in s starting from offset offset. If s does not contain su...
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v)
Create the constant array.
Z3_ast Z3_API Z3_substitute_vars(Z3_context c, Z3_ast a, unsigned num_exprs, Z3_ast const to[])
Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs,...
Z3_ast Z3_API Z3_mk_int2real(Z3_context c, Z3_ast t1)
Coerce an integer to a real.
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative)
Create a floating-point infinity of sort s.
Z3_ast Z3_API Z3_mk_re_intersect(Z3_context c, unsigned n, Z3_ast const args[])
Create the intersection of the regular languages.
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s)
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
def BV2Int(a, is_signed=False)
def RoundTowardZero(ctx=None)
def RecFunction(name, *sig)
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c)
Create the half-precision (16-bit) FloatingPoint sort.
def is_algebraic_value(a)
def BVMulNoUnderflow(a, b)
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t)
Floating-point absolute value.
Z3_ast Z3_API Z3_mk_is_int(Z3_context c, Z3_ast t1)
Check if a real number is an integer.
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s)
Create a floating-point NaN of sort s.
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value)
Set a global (or module) parameter. This setting is shared by all Z3 contexts.
def prove(claim, **keywords)
def fpMin(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
Z3_ast Z3_API Z3_mk_bvuge(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned greater than or equal to.
Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const *domain, Z3_sort range)
Create an array type with N arguments.
def BVMulNoOverflow(a, b, signed)
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a)
Return the sort of an AST node.
def Repeat(t, max=4294967295, ctx=None)
def fpToReal(x, ctx=None)
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
Z3_ast Z3_API Z3_mk_bvsrem(Z3_context c, Z3_ast t1, Z3_ast t2)
Two's complement signed remainder (sign follows dividend).
Z3_sort Z3_API Z3_mk_uninterpreted_sort(Z3_context c, Z3_symbol s)
Create a free (uninterpreted) type using the given name (symbol).
def fpIsSubnormal(a, ctx=None)
Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, unsigned num_bound, Z3_app const bound[], Z3_ast body)
Create a lambda expression using a list of constants that form the set of bound variables.
def fpIsNegative(a, ctx=None)
def fpFPToFP(rm, v, sort, ctx=None)
def fpNEQ(a, b, ctx=None)
def BVSubNoUnderflow(a, b, signed)
Z3_ast Z3_API Z3_mk_set_subset(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Check for subsetness of sets.
def ParThen(t1, t2, ctx=None)
Z3_ast Z3_API Z3_mk_bvlshr(Z3_context c, Z3_ast t1, Z3_ast t2)
Logical shift right.
def args2params(arguments, keywords, ctx=None)
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, Z3_ast const args[], int const coeffs[], int k)
Pseudo-Boolean relations.
def FloatSingle(ctx=None)
Z3_sort Z3_API Z3_mk_real_sort(Z3_context c)
Create the real type.
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_re_empty(Z3_context c, Z3_sort re)
Create an empty regular expression of sort re.
def fpRealToFP(rm, v, sort, ctx=None)
def RealVector(prefix, sz, ctx=None)
Z3_tactic Z3_API Z3_tactic_when(Z3_context c, Z3_probe p, Z3_tactic t)
Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to fa...
def fpIsPositive(a, ctx=None)
Z3_ast Z3_API Z3_mk_re_concat(Z3_context c, unsigned n, Z3_ast const args[])
Create the concatenation of the regular languages.
Z3_ast Z3_API Z3_mk_mul(Z3_context c, unsigned num_args, Z3_ast const args[])
Create an AST node representing args[0] * ... * args[num_args-1].
Z3_ast Z3_API Z3_mk_seq_extract(Z3_context c, Z3_ast s, Z3_ast offset, Z3_ast length)
Extract subsequence starting at offset of length.
def set_option(*args, **kws)
def SubString(s, offset, length)
Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c, Z3_func_decl f)
create transitive closure of binary relation.
Z3_symbol Z3_API Z3_mk_int_symbol(Z3_context c, int i)
Create a Z3 symbol using an integer.
def fpToIEEEBV(x, ctx=None)
def String(name, ctx=None)
Z3_func_decl Z3_API Z3_mk_partial_order(Z3_context c, Z3_sort a, unsigned id)
create a partial ordering relation over signature a and index id.
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c)
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3_func_decl Z3_API Z3_mk_piecewise_linear_order(Z3_context c, Z3_sort a, unsigned id)
create a piecewise linear ordering relation over signature a and index id.