|
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 | 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) |
|
◆ 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 1680 of file z3py.py.
1681 """Create a Z3 and-expression or and-probe.
1683 >>> p, q, r = Bools('p q r')
1686 >>> P = BoolVector('p', 5)
1688 And(p__0, p__1, p__2, p__3, p__4)
1692 last_arg = args[len(args)-1]
1693 if isinstance(last_arg, Context):
1694 ctx = args[len(args)-1]
1695 args = args[:len(args)-1]
1696 elif len(args) == 1
and isinstance(args[0], AstVector):
1698 args = [a
for a
in args[0]]
1701 args = _get_args(args)
1702 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1704 _z3_assert(ctx_args
is None or ctx_args == ctx,
"context mismatch")
1705 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1706 if _has_probe(args):
1707 return _probe_and(args, ctx)
1709 args = _coerce_expr_list(args, ctx)
1710 _args, sz = _to_ast_array(args)
1711 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 7747 of file z3py.py.
7748 """Return a tactic that applies the tactics in `*ts` in sequence.
7750 >>> x, y = Ints('x y')
7751 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7752 >>> t(And(x == 0, y > x + 1))
7754 >>> t(And(x == 0, y > x + 1)).as_expr()
7758 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7759 ctx = ks.get(
'ctx',
None)
7762 for i
in range(num - 1):
7763 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 5070 of file z3py.py.
5071 """Convert python arguments into a Z3_params object.
5072 A ':' is added to the keywords, and '_' is replaced with '-'
5074 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5075 (params model true relevancy 2 elim_and true)
5078 _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 4403 of file z3py.py.
4403 def Array(name, dom, rng):
4404 """Return an array constant named `name` with the given domain and range sorts.
4406 >>> 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 4371 of file z3py.py.
4372 """Return the Z3 array sort with the given domain and range sorts.
4374 >>> A = ArraySort(IntSort(), BoolSort())
4381 >>> AA = ArraySort(IntSort(), A)
4383 Array(Int, Array(Int, Bool))
4385 sig = _get_args(sig)
4387 _z3_assert(len(sig) > 1,
"At least two arguments expected")
4388 arity = len(sig) - 1
4393 _z3_assert(
is_sort(s),
"Z3 sort expected")
4394 _z3_assert(s.ctx == r.ctx,
"Context mismatch")
4398 dom = (Sort * arity)()
4399 for i
in range(arity):
Referenced by Array(), Context.mkArraySort(), 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 8328 of file z3py.py.
8329 """Create an at-most Pseudo-Boolean k constraint.
8331 >>> a, b, c = Bools('a b c')
8332 >>> f = AtLeast(a, b, c, 2)
8334 args = _get_args(args)
8336 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8337 ctx = _ctx_from_ast_arg_list(args)
8339 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8340 args1 = _coerce_expr_list(args[:-1], ctx)
8342 _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 8311 of file z3py.py.
8312 """Create an at-most Pseudo-Boolean k constraint.
8314 >>> a, b, c = Bools('a b c')
8315 >>> f = AtMost(a, b, c, 2)
8317 args = _get_args(args)
8319 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8320 ctx = _ctx_from_ast_arg_list(args)
8322 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8323 args1 = _coerce_expr_list(args[:-1], ctx)
8325 _args, sz = _to_ast_array(args1)
8326 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 3770 of file z3py.py.
3770 def BitVec(name, bv, ctx=None):
3771 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3772 If `ctx=None`, then the global context is used.
3774 >>> x = BitVec('x', 16)
3781 >>> word = BitVecSort(16)
3782 >>> x2 = BitVec('x', word)
3786 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 3793 of file z3py.py.
3793 def BitVecs(names, bv, ctx=None):
3794 """Return a tuple of bit-vector constants of size bv.
3796 >>> x, y, z = BitVecs('x y z', 16)
3803 >>> Product(x, y, z)
3805 >>> simplify(Product(x, y, z))
3809 if isinstance(names, str):
3810 names = names.split(
" ")
3811 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 3740 of file z3py.py.
3741 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3743 >>> Byte = BitVecSort(8)
3744 >>> Word = BitVecSort(16)
3747 >>> x = Const('x', Byte)
3748 >>> eq(x, BitVec('x', 8))
Referenced by BitVec(), BitVecVal(), and Context.mkBitVecSort().
◆ 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 3754 of file z3py.py.
3755 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3757 >>> v = BitVecVal(10, 32)
3760 >>> print("0x%.8x" % v.as_long())
3765 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 1579 of file z3py.py.
1579 def Bools(names, ctx=None):
1580 """Return a tuple of Boolean constants.
1582 `names` is a single string containing all names separated by blank spaces.
1583 If `ctx=None`, then the global context is used.
1585 >>> p, q, r = Bools('p q r')
1586 >>> And(p, Or(q, r))
1590 if isinstance(names, str):
1591 names = names.split(
" ")
1592 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 1533 of file z3py.py.
1534 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1538 >>> p = Const('p', BoolSort())
1541 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1544 >>> is_bool(r(0, 1))
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), FreshBool(), Context.getBoolSort(), If(), Implies(), Context.mkBoolSort(), 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 1594 of file z3py.py.
1595 """Return a list of Boolean constants of size `sz`.
1597 The constants are named using the given prefix.
1598 If `ctx=None`, then the global context is used.
1600 >>> P = BoolVector('p', 3)
1604 And(p__0, p__1, p__2)
1606 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 3710 of file z3py.py.
3710 def BV2Int(a, is_signed=False):
3711 """Return the Z3 expression BV2Int(a).
3713 >>> b = BitVec('b', 3)
3714 >>> BV2Int(b).sort()
3719 >>> x > BV2Int(b, is_signed=False)
3721 >>> x > BV2Int(b, is_signed=True)
3722 x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3723 >>> solve(x > BV2Int(b), b == 1, x < 3)
3727 _z3_assert(
is_bv(a),
"Z3 bit-vector expression expected")
3730 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 4165 of file z3py.py.
4166 """A predicate the determines that bit-vector addition does not overflow"""
4167 _check_bv_args(a, b)
4168 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 4171 of file z3py.py.
4172 """A predicate the determines that signed bit-vector addition does not underflow"""
4173 _check_bv_args(a, b)
4174 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 4202 of file z3py.py.
4203 """A predicate the determines that bit-vector multiplication does not overflow"""
4204 _check_bv_args(a, b)
4205 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 4209 of file z3py.py.
4210 """A predicate the determines that bit-vector signed multiplication does not underflow"""
4211 _check_bv_args(a, b)
4212 a, b = _coerce_exprs(a, b)
◆ BVRedAnd()
Return the reduction-and expression of `a`.
Definition at line 4153 of file z3py.py.
4154 """Return the reduction-and expression of `a`."""
4156 _z3_assert(
is_bv(a),
"First argument must be a Z3 Bitvector expression")
◆ BVRedOr()
Return the reduction-or expression of `a`.
Definition at line 4159 of file z3py.py.
4160 """Return the reduction-or expression of `a`."""
4162 _z3_assert(
is_bv(a),
"First argument must be a Z3 Bitvector expression")
4163 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 4190 of file z3py.py.
4191 """A predicate the determines that bit-vector signed division does not overflow"""
4192 _check_bv_args(a, b)
4193 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 4196 of file z3py.py.
4197 """A predicate the determines that bit-vector unary negation does not overflow"""
4199 _z3_assert(
is_bv(a),
"Argument should be a bit-vector")
◆ BVSubNoOverflow()
def z3py.BVSubNoOverflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4177 of file z3py.py.
4178 """A predicate the determines that bit-vector subtraction does not overflow"""
4179 _check_bv_args(a, b)
4180 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 4184 of file z3py.py.
4185 """A predicate the determines that bit-vector subtraction does not underflow"""
4186 _check_bv_args(a, b)
4187 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 3172 of file z3py.py.
3172 def Cbrt(a, ctx=None):
3173 """ Return a Z3 expression which represents the cubic root of a.
◆ Complement()
def z3py.Complement |
( |
|
re | ) |
|
Create the complement regular expression.
Definition at line 10386 of file z3py.py.
10387 """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 3813 of file z3py.py.
3814 """Create a Z3 bit-vector concatenation expression.
3816 >>> v = BitVecVal(1, 4)
3817 >>> Concat(v, v+1, v)
3818 Concat(Concat(1, 1 + 1), 1)
3819 >>> simplify(Concat(v, v+1, v))
3821 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3824 args = _get_args(args)
3827 _z3_assert(sz >= 2,
"At least two arguments expected.")
3834 if is_seq(args[0])
or isinstance(args[0], str):
3835 args = [_coerce_seq(s, ctx)
for s
in args]
3837 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
3840 v[i] = args[i].as_ast()
3845 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
3848 v[i] = args[i].as_ast()
3852 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
3854 for i
in range(sz - 1):
3855 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 8166 of file z3py.py.
8166 def Cond(p, t1, t2, ctx=None):
8167 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8169 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8171 p = _to_probe(p, ctx)
8172 t1 = _to_tactic(t1, ctx)
8173 t2 = _to_tactic(t2, ctx)
8174 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 1301 of file z3py.py.
1301 def Const(name, sort):
1302 """Create a constant of the given sort.
1304 >>> Const('x', IntSort())
1308 _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 1312 of file z3py.py.
1313 """Create several constants of the given sort.
1315 `names` is a string containing the names of all constants to be created.
1316 Blank spaces separate the names of different constants.
1318 >>> x, y, z = Consts('x y z', IntSort())
1322 if isinstance(names, str):
1323 names = names.split(
" ")
1324 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 10180 of file z3py.py.
10181 """Check if 'a' contains 'b'
10182 >>> s1 = Contains("abc", "ab")
10185 >>> s2 = Contains("abc", "bc")
10188 >>> x, y, z = Strings('x y z')
10189 >>> s3 = Contains(Concat(x,y,z), y)
10193 ctx = _get_ctx2(a, b)
10194 a = _coerce_seq(a, ctx)
10195 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 4782 of file z3py.py.
4783 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4785 In the following example we define a Tree-List using two mutually recursive datatypes.
4787 >>> TreeList = Datatype('TreeList')
4788 >>> Tree = Datatype('Tree')
4789 >>> # Tree has two constructors: leaf and node
4790 >>> Tree.declare('leaf', ('val', IntSort()))
4791 >>> # a node contains a list of trees
4792 >>> Tree.declare('node', ('children', TreeList))
4793 >>> TreeList.declare('nil')
4794 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4795 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4796 >>> Tree.val(Tree.leaf(10))
4798 >>> simplify(Tree.val(Tree.leaf(10)))
4800 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4802 node(cons(leaf(10), cons(leaf(20), nil)))
4803 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4804 >>> simplify(n2 == n1)
4806 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4811 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
4812 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
4813 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
4814 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
4817 names = (Symbol * num)()
4818 out = (Sort * num)()
4819 clists = (ConstructorList * num)()
4821 for i
in range(num):
4824 num_cs = len(d.constructors)
4825 cs = (Constructor * num_cs)()
4826 for j
in range(num_cs):
4827 c = d.constructors[j]
4832 fnames = (Symbol * num_fs)()
4833 sorts = (Sort * num_fs)()
4834 refs = (ctypes.c_uint * num_fs)()
4835 for k
in range(num_fs):
4839 if isinstance(ftype, Datatype):
4841 _z3_assert(ds.count(ftype) == 1,
"One and only one occurrence of each datatype is expected")
4843 refs[k] = ds.index(ftype)
4846 _z3_assert(
is_sort(ftype),
"Z3 sort expected")
4847 sorts[k] = ftype.ast
4850 to_delete.append(ScopedConstructor(cs[j], ctx))
4852 to_delete.append(ScopedConstructorList(clists[i], ctx))
4856 for i
in range(num):
4857 dref = DatatypeSortRef(out[i], ctx)
4858 num_cs = dref.num_constructors()
4859 for j
in range(num_cs):
4860 cref = dref.constructor(j)
4861 cref_name = cref.name()
4862 cref_arity = cref.arity()
4863 if cref.arity() == 0:
4865 setattr(dref, cref_name, cref)
4866 rref = dref.recognizer(j)
4867 setattr(dref,
"is_" + cref_name, rref)
4868 for k
in range(cref_arity):
4869 aref = dref.accessor(j, k)
4870 setattr(dref, aref.name(), aref)
4872 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 4437 of file z3py.py.
4438 """ Return a default value for array expression.
4439 >>> b = K(IntSort(), 1)
4440 >>> prove(Default(b) == 1)
4444 _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 8096 of file z3py.py.
8097 """Display a (tabular) description of all available probes in Z3."""
8100 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8103 print(
'<tr style="background-color:#CFCFCF">')
8108 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 7905 of file z3py.py.
7906 """Display a (tabular) description of all available tactics in Z3."""
7909 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7912 print(
'<tr style="background-color:#CFCFCF">')
7917 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 4982 of file z3py.py.
4983 """Create a named tagged union sort base on a set of underlying sorts
4985 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
4987 sum = Datatype(name, ctx)
4988 for i
in range(len(sorts)):
4989 sum.declare(
"inject%d" % i, (
"project%d" % i, sorts[i]))
4991 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 1270 of file z3py.py.
1271 """Create a Z3 distinct expression.
1278 >>> Distinct(x, y, z)
1280 >>> simplify(Distinct(x, y, z))
1282 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1283 And(Not(x == y), Not(x == z), Not(y == z))
1285 args = _get_args(args)
1286 ctx = _ctx_from_ast_arg_list(args)
1288 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1289 args = _coerce_expr_list(args, ctx)
1290 _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 10115 of file z3py.py.
10116 """Create the empty sequence of the given sort
10117 >>> e = Empty(StringSort())
10118 >>> e2 = StringVal("")
10119 >>> print(e.eq(e2))
10121 >>> e3 = Empty(SeqSort(IntSort()))
10124 >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10126 Empty(ReSort(Seq(Int)))
10128 if isinstance(s, SeqSortRef):
10130 if isinstance(s, ReSortRef):
10132 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Empty")
◆ EmptySet()
Create the empty set
>>> EmptySet(IntSort())
K(Int, False)
Definition at line 4572 of file z3py.py.
4573 """Create the empty set
4574 >>> EmptySet(IntSort())
◆ enable_trace()
def z3py.enable_trace |
( |
|
msg | ) |
|
◆ 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 4994 of file z3py.py.
4994 def EnumSort(name, values, ctx=None):
4995 """Return a new enumeration sort named `name` containing the given values.
4997 The result is a pair (sort, list of constants).
4999 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5002 _z3_assert(isinstance(name, str),
"Name must be a string")
5003 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Eumeration sort values must be strings")
5004 _z3_assert(len(values) > 0,
"At least one value expected")
5007 _val_names = (Symbol * num)()
5008 for i
in range(num):
5010 _values = (FuncDecl * num)()
5011 _testers = (FuncDecl * num)()
5015 for i
in range(num):
5016 V.append(FuncDeclRef(_values[i], ctx))
5017 V = [a()
for a
in V]
Referenced by Context.mkEnumSort().
◆ 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 2061 of file z3py.py.
2061 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2062 """Create a Z3 exists formula.
2064 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2067 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2070 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2072 Exists([x, y], f(x, y) >= x)
2073 >>> is_quantifier(q)
2075 >>> r = Tactic('nnf')(q).as_expr()
2076 >>> is_quantifier(r)
2079 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 4522 of file z3py.py.
4523 """Return extensionality index for one-dimensional arrays.
4524 >> a, b = Consts('a b', SetSort(IntSort()))
4531 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 3858 of file z3py.py.
3859 """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3861 >>> x = BitVec('x', 8)
3862 >>> Extract(6, 2, x)
3864 >>> Extract(6, 2, x).sort()
3866 >>> simplify(Extract(StringVal("abcd"),2,1))
3869 if isinstance(high, str):
3873 offset, length = _coerce_exprs(low, a, s.ctx)
3874 return SeqRef(
Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3876 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
3877 _z3_assert(_is_int(high)
and high >= 0
and _is_int(low)
and low >= 0,
"First and second arguments must be non negative integers")
3878 _z3_assert(
is_bv(a),
"Third argument must be a Z3 Bitvector expression")
3879 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 8129 of file z3py.py.
8130 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8132 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8134 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8135 >>> x, y = Ints('x y')
8141 >>> g.add(x == y + 1)
8143 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8145 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 7221 of file z3py.py.
7222 """Create a named finite domain sort of a given size sz"""
7223 if not isinstance(name, Symbol):
Referenced by Context.mkFiniteDomainSort().
◆ 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 7289 of file z3py.py.
7290 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7292 >>> s = FiniteDomainSort('S', 256)
7293 >>> FiniteDomainVal(255, s)
7295 >>> FiniteDomainVal('100', s)
7301 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 8759 of file z3py.py.
8760 """Floating-point 128-bit (quadruple) sort."""
◆ Float16()
def z3py.Float16 |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8729 of file z3py.py.
8730 """Floating-point 16-bit (half) sort."""
◆ Float32()
def z3py.Float32 |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8739 of file z3py.py.
8740 """Floating-point 32-bit (single) sort."""
◆ Float64()
def z3py.Float64 |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8749 of file z3py.py.
8750 """Floating-point 64-bit (double) sort."""
◆ FloatDouble()
def z3py.FloatDouble |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8754 of file z3py.py.
8755 """Floating-point 64-bit (double) sort."""
◆ FloatHalf()
def z3py.FloatHalf |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8734 of file z3py.py.
8735 """Floating-point 16-bit (half) sort."""
◆ FloatQuadruple()
def z3py.FloatQuadruple |
( |
|
ctx = None | ) |
|
Floating-point 128-bit (quadruple) sort.
Definition at line 8764 of file z3py.py.
8765 """Floating-point 128-bit (quadruple) sort."""
◆ FloatSingle()
def z3py.FloatSingle |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8744 of file z3py.py.
8745 """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 2044 of file z3py.py.
2044 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2045 """Create a Z3 forall formula.
2047 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2049 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2052 >>> ForAll([x, y], f(x, y) >= x)
2053 ForAll([x, y], f(x, y) >= x)
2054 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2055 ForAll([x, y], f(x, y) >= x)
2056 >>> ForAll([x, y], f(x, y) >= x, weight=10)
2057 ForAll([x, y], f(x, y) >= x)
2059 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 9344 of file z3py.py.
9344 def FP(name, fpsort, ctx=None):
9345 """Return a floating-point constant named `name`.
9346 `fpsort` is the floating-point sort.
9347 If `ctx=None`, then the global context is used.
9349 >>> x = FP('x', FPSort(8, 24))
9356 >>> word = FPSort(8, 24)
9357 >>> x2 = FP('x', word)
9361 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 9385 of file z3py.py.
9385 def fpAbs(a, ctx=None):
9386 """Create a Z3 floating-point absolute value expression.
9388 >>> s = FPSort(8, 24)
9390 >>> x = FPVal(1.0, s)
9393 >>> y = FPVal(-20.0, s)
9398 >>> fpAbs(-1.25*(2**4))
9404 [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 9467 of file z3py.py.
9467 def fpAdd(rm, a, b, ctx=None):
9468 """Create a Z3 floating-point addition expression.
9470 >>> s = FPSort(8, 24)
9476 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9478 >>> fpAdd(rm, x, y).sort()
9481 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 9763 of file z3py.py.
9764 """Create a Z3 floating-point conversion expression that represents the
9765 conversion from a bit-vector term to a floating-point term.
9767 >>> x_bv = BitVecVal(0x3F800000, 32)
9768 >>> x_fp = fpBVToFP(x_bv, Float32())
9774 _z3_assert(
is_bv(v),
"First argument must be a Z3 floating-point rounding mode expression.")
9775 _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 9511 of file z3py.py.
9511 def fpDiv(rm, a, b, ctx=None):
9512 """Create a Z3 floating-point division expression.
9514 >>> s = FPSort(8, 24)
9520 >>> fpDiv(rm, x, y).sort()
9523 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 9675 of file z3py.py.
9675 def fpEQ(a, b, ctx=None):
9676 """Create the Z3 floating-point expression `fpEQ(other, self)`.
9678 >>> x, y = FPs('x y', FPSort(8, 24))
9681 >>> fpEQ(x, y).sexpr()
9684 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 9566 of file z3py.py.
9566 def fpFMA(rm, a, b, c, ctx=None):
9567 """Create a Z3 floating-point fused multiply-add expression.
9569 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 9697 of file z3py.py.
9697 def fpFP(sgn, exp, sig, ctx=None):
9698 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9700 >>> s = FPSort(8, 24)
9701 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9703 fpFP(1, 127, 4194304)
9704 >>> xv = FPVal(-1.5, s)
9708 >>> slvr.add(fpEQ(x, xv))
9711 >>> xv = FPVal(+1.5, s)
9715 >>> slvr.add(fpEQ(x, xv))
9720 _z3_assert(sgn.sort().size() == 1,
"sort mismatch")
9722 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,
"context mismatch")
9723 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 9779 of file z3py.py.
9779 def fpFPToFP(rm, v, sort, ctx=None):
9780 """Create a Z3 floating-point conversion expression that represents the
9781 conversion from a floating-point term to a floating-point term of different precision.
9783 >>> x_sgl = FPVal(1.0, Float32())
9784 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9792 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9793 _z3_assert(
is_fp(v),
"Second argument must be a Z3 floating-point expression.")
9794 _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 9664 of file z3py.py.
9664 def fpGEQ(a, b, ctx=None):
9665 """Create the Z3 floating-point expression `other >= self`.
9667 >>> x, y = FPs('x y', FPSort(8, 24))
9670 >>> (x >= y).sexpr()
9673 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 9653 of file z3py.py.
9653 def fpGT(a, b, ctx=None):
9654 """Create the Z3 floating-point expression `other > self`.
9656 >>> x, y = FPs('x y', FPSort(8, 24))
9662 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 9278 of file z3py.py.
9279 """Create a Z3 floating-point +oo or -oo term."""
9280 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9281 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9282 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 9592 of file z3py.py.
9593 """Create a Z3 floating-point isInfinite expression.
9595 >>> s = FPSort(8, 24)
9600 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 9581 of file z3py.py.
9582 """Create a Z3 floating-point isNaN expression.
9584 >>> s = FPSort(8, 24)
9590 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 9617 of file z3py.py.
9618 """Create a Z3 floating-point isNegative expression.
9620 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 9607 of file z3py.py.
9608 """Create a Z3 floating-point isNormal expression.
9610 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 9622 of file z3py.py.
9623 """Create a Z3 floating-point isPositive expression.
9625 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 9612 of file z3py.py.
9613 """Create a Z3 floating-point isSubnormal expression.
9615 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 9602 of file z3py.py.
9603 """Create a Z3 floating-point isZero expression.
9605 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 9642 of file z3py.py.
9642 def fpLEQ(a, b, ctx=None):
9643 """Create the Z3 floating-point expression `other <= self`.
9645 >>> x, y = FPs('x y', FPSort(8, 24))
9648 >>> (x <= y).sexpr()
9651 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 9631 of file z3py.py.
9631 def fpLT(a, b, ctx=None):
9632 """Create the Z3 floating-point expression `other < self`.
9634 >>> x, y = FPs('x y', FPSort(8, 24))
9640 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 9552 of file z3py.py.
9552 def fpMax(a, b, ctx=None):
9553 """Create a Z3 floating-point maximum expression.
9555 >>> s = FPSort(8, 24)
9561 >>> fpMax(x, y).sort()
9564 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 9538 of file z3py.py.
9538 def fpMin(a, b, ctx=None):
9539 """Create a Z3 floating-point minimum expression.
9541 >>> s = FPSort(8, 24)
9547 >>> fpMin(x, y).sort()
9550 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 9273 of file z3py.py.
9274 """Create a Z3 floating-point -oo term."""
9275 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9276 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 9289 of file z3py.py.
9290 """Create a Z3 floating-point -0.0 term."""
9291 _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 9497 of file z3py.py.
9497 def fpMul(rm, a, b, ctx=None):
9498 """Create a Z3 floating-point multiplication expression.
9500 >>> s = FPSort(8, 24)
9506 >>> fpMul(rm, x, y).sort()
9509 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 9241 of file z3py.py.
9242 """Create a Z3 floating-point NaN term.
9244 >>> s = FPSort(8, 24)
9245 >>> set_fpa_pretty(True)
9248 >>> pb = get_fpa_pretty()
9249 >>> set_fpa_pretty(False)
9251 fpNaN(FPSort(8, 24))
9252 >>> set_fpa_pretty(pb)
9254 _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 9407 of file z3py.py.
9407 def fpNeg(a, ctx=None):
9408 """Create a Z3 floating-point addition expression.
9410 >>> s = FPSort(8, 24)
9419 [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 9686 of file z3py.py.
9686 def fpNEQ(a, b, ctx=None):
9687 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9689 >>> x, y = FPs('x y', FPSort(8, 24))
9692 >>> (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 9257 of file z3py.py.
9258 """Create a Z3 floating-point +oo term.
9260 >>> s = FPSort(8, 24)
9261 >>> pb = get_fpa_pretty()
9262 >>> set_fpa_pretty(True)
9263 >>> fpPlusInfinity(s)
9265 >>> set_fpa_pretty(False)
9266 >>> fpPlusInfinity(s)
9267 fpPlusInfinity(FPSort(8, 24))
9268 >>> set_fpa_pretty(pb)
9270 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9271 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 9284 of file z3py.py.
9285 """Create a Z3 floating-point +0.0 term."""
9286 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9287 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 9798 of file z3py.py.
9799 """Create a Z3 floating-point conversion expression that represents the
9800 conversion from a real term to a floating-point term.
9802 >>> x_r = RealVal(1.5)
9803 >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9809 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9810 _z3_assert(
is_real(v),
"Second argument must be a Z3 expression or real sort.")
9811 _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 9525 of file z3py.py.
9525 def fpRem(a, b, ctx=None):
9526 """Create a Z3 floating-point remainder expression.
9528 >>> s = FPSort(8, 24)
9533 >>> fpRem(x, y).sort()
9536 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 9576 of file z3py.py.
9577 """Create a Z3 floating-point roundToIntegral expression.
9579 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 9367 of file z3py.py.
9367 def FPs(names, fpsort, ctx=None):
9368 """Return an array of floating-point constants.
9370 >>> x, y, z = FPs('x y z', FPSort(8, 24))
9377 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9378 fpMul(RNE(), fpAdd(RNE(), x, y), z)
9381 if isinstance(names, str):
9382 names = names.split(
" ")
9383 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 9815 of file z3py.py.
9816 """Create a Z3 floating-point conversion expression that represents the
9817 conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9819 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9820 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9822 fpToFP(RNE(), 4294967291)
9826 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9827 _z3_assert(
is_bv(v),
"Second argument must be a Z3 expression or real sort.")
9828 _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 9183 of file z3py.py.
9183 def FPSort(ebits, sbits, ctx=None):
9184 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9186 >>> Single = FPSort(8, 24)
9187 >>> Double = FPSort(11, 53)
9190 >>> x = Const('x', Single)
9191 >>> eq(x, FP('x', FPSort(8, 24)))
Referenced by get_default_fp_sort(), Context.mkFPSort(), Context.mkFPSort128(), Context.mkFPSort16(), Context.mkFPSort32(), Context.mkFPSort64(), Context.mkFPSortDouble(), Context.mkFPSortHalf(), Context.mkFPSortQuadruple(), and Context.mkFPSortSingle().
◆ fpSqrt()
def z3py.fpSqrt |
( |
|
rm, |
|
|
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 floating-point square root expression.
Definition at line 9571 of file z3py.py.
9571 def fpSqrt(rm, a, ctx=None):
9572 """Create a Z3 floating-point square root expression.
9574 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 9483 of file z3py.py.
9483 def fpSub(rm, a, b, ctx=None):
9484 """Create a Z3 floating-point subtraction expression.
9486 >>> s = FPSort(8, 24)
9492 >>> fpSub(rm, x, y).sort()
9495 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 9725 of file z3py.py.
9725 def fpToFP(a1, a2=None, a3=None, ctx=None):
9726 """Create a Z3 floating-point conversion expression from other term sorts
9729 From a bit-vector term in IEEE 754-2008 format:
9730 >>> x = FPVal(1.0, Float32())
9731 >>> x_bv = fpToIEEEBV(x)
9732 >>> simplify(fpToFP(x_bv, Float32()))
9735 From a floating-point term with different precision:
9736 >>> x = FPVal(1.0, Float32())
9737 >>> x_db = fpToFP(RNE(), x, Float64())
9742 >>> x_r = RealVal(1.5)
9743 >>> simplify(fpToFP(RNE(), x_r, Float32()))
9746 From a signed bit-vector term:
9747 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9748 >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9761 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 9849 of file z3py.py.
9850 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9852 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9853 _z3_assert(
is_bv(x),
"Second argument must be a Z3 bit-vector expression")
9854 _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 9919 of file z3py.py.
9920 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9922 The size of the resulting bit-vector is automatically determined.
9924 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9925 knows only one NaN and it will always produce the same bit-vector representation of
9928 >>> x = FP('x', FPSort(8, 24))
9929 >>> y = fpToIEEEBV(x)
9940 _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 9900 of file z3py.py.
9901 """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9903 >>> x = FP('x', FPSort(8, 24))
9907 >>> print(is_real(y))
9911 >>> print(is_real(x))
9915 _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 9858 of file z3py.py.
9858 def fpToSBV(rm, x, s, ctx=None):
9859 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9861 >>> x = FP('x', FPSort(8, 24))
9862 >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9873 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9874 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9875 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9877 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 9879 of file z3py.py.
9879 def fpToUBV(rm, x, s, ctx=None):
9880 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9882 >>> x = FP('x', FPSort(8, 24))
9883 >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9894 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9895 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9896 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9898 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 9832 of file z3py.py.
9833 """Create a Z3 floating-point conversion expression that represents the
9834 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9836 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9837 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9839 fpToFPUnsigned(RNE(), 4294967291)
9843 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9844 _z3_assert(
is_bv(v),
"Second argument must be a Z3 expression or real sort.")
9845 _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 9300 of file z3py.py.
9300 def FPVal(sig, exp=None, fps=None, ctx=None):
9301 """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9303 >>> v = FPVal(20.0, FPSort(8, 24))
9306 >>> print("0x%.8x" % v.exponent_as_long(False))
9308 >>> v = FPVal(2.25, FPSort(8, 24))
9311 >>> v = FPVal(-2.25, FPSort(8, 24))
9314 >>> FPVal(-0.0, FPSort(8, 24))
9316 >>> FPVal(0.0, FPSort(8, 24))
9318 >>> FPVal(+0.0, FPSort(8, 24))
9326 fps = _dflt_fps(ctx)
9330 val = _to_float_str(sig)
9331 if val ==
"NaN" or val ==
"nan":
9335 elif val ==
"0.0" or val ==
"+0.0":
9337 elif val ==
"+oo" or val ==
"+inf" or val ==
"+Inf":
9339 elif val ==
"-oo" or val ==
"-inf" or val ==
"-Inf":
9342 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 9294 of file z3py.py.
9295 """Create a Z3 floating-point +0.0 or -0.0 term."""
9296 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9297 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9298 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 1608 of file z3py.py.
1609 """Return a fresh Boolean constant in the given context using the given prefix.
1611 If `ctx=None`, then the global context is used.
1613 >>> b1 = FreshBool()
1614 >>> b2 = FreshBool()
◆ FreshConst()
def z3py.FreshConst |
( |
|
sort, |
|
|
|
prefix = 'c' |
|
) |
| |
Create a fresh constant of a specified sort
Definition at line 1326 of file z3py.py.
1327 """Create a fresh constant of a specified sort"""
1328 ctx = _get_ctx(sort.ctx)
◆ 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 3045 of file z3py.py.
3045 def FreshInt(prefix='x', ctx=None):
3046 """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 3097 of file z3py.py.
3098 """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 10134 of file z3py.py.
10135 """Create the regular expression that accepts the universal language
10136 >>> e = Full(ReSort(SeqSort(IntSort())))
10138 Full(ReSort(Seq(Int)))
10139 >>> e1 = Full(ReSort(StringSort()))
10141 Full(ReSort(String))
10143 if isinstance(s, ReSortRef):
10145 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Full")
◆ FullSet()
Create the full set
>>> FullSet(IntSort())
K(Int, True)
Definition at line 4580 of file z3py.py.
4581 """Create the full set
4582 >>> 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 6244 of file z3py.py.
6245 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6247 _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 8626 of file z3py.py.
8627 """Retrieves the global default rounding mode."""
8628 global _dflt_rounding_mode
8629 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8631 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8633 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8635 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8637 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 4354 of file z3py.py.
4355 """Return the function declaration associated with a Z3 map array expression.
4357 >>> f = Function('f', IntSort(), IntSort())
4358 >>> b = Array('b', IntSort(), IntSort())
4360 >>> eq(f, get_map_func(a))
4364 >>> get_map_func(a)(0)
4368 _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 1204 of file z3py.py.
1205 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1213 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1214 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1215 >>> q = ForAll([x, y], f(x, y) == x + y)
1217 f(Var(1), Var(0)) == Var(1) + Var(0)
1221 >>> v1 = b.arg(0).arg(0)
1222 >>> v2 = b.arg(0).arg(1)
1227 >>> get_var_index(v1)
1229 >>> get_var_index(v2)
1233 _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 8206 of file z3py.py.
8207 """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 1248 of file z3py.py.
1248 def If(a, b, c, ctx=None):
1249 """Create a Z3 if-then-else expression.
1253 >>> max = If(x > y, x, y)
1259 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1260 return Cond(a, b, c, ctx)
1262 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1265 b, c = _coerce_exprs(b, c, ctx)
1267 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1268 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 1621 of file z3py.py.
1622 """Create a Z3 implies expression.
1624 >>> p, q = Bools('p q')
1628 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1632 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 10216 of file z3py.py.
10216 def IndexOf(s, substr, offset):
10217 """Retrieve the index of substring within a string starting at a specified offset.
10218 >>> simplify(IndexOf("abcabc", "bc", 0))
10220 >>> simplify(IndexOf("abcabc", "bc", 2))
10226 ctx = _get_ctx2(s, substr, ctx)
10227 s = _coerce_seq(s, ctx)
10228 substr = _coerce_seq(substr, ctx)
10229 if _is_int(offset):
10230 offset =
IntVal(offset, ctx)
10231 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 10313 of file z3py.py.
10314 """Create regular expression membership test
10315 >>> re = Union(Re("a"),Re("b"))
10316 >>> print (simplify(InRe("a", re)))
10318 >>> print (simplify(InRe("b", re)))
10320 >>> print (simplify(InRe("c", re)))
10323 s = _coerce_seq(s, re.ctx)
10324 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 3010 of file z3py.py.
3010 def Int(name, ctx=None):
3011 """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 3732 of file z3py.py.
3733 """Return the z3 expression Int2BV(a, num_bits).
3734 It is a bit-vector of width num_bits and represents the
3735 modulo of a by 2^num_bits
3738 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 10345 of file z3py.py.
10346 """Create intersection of regular expressions.
10347 >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10349 args = _get_args(args)
10352 _z3_assert(sz > 0,
"At least one argument expected.")
10353 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10358 for i
in range(sz):
10359 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 3022 of file z3py.py.
3022 def Ints(names, ctx=None):
3023 """Return a tuple of Integer constants.
3025 >>> x, y, z = Ints('x y z')
3030 if isinstance(names, str):
3031 names = names.split(
" ")
3032 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 2907 of file z3py.py.
2908 """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2912 >>> x = Const('x', IntSort())
2915 >>> x.sort() == IntSort()
2917 >>> x.sort() == BoolSort()
Referenced by FreshInt(), Context.getIntSort(), Int(), IntVal(), and Context.mkIntSort().
◆ IntToStr()
Convert integer expression to string
Definition at line 10267 of file z3py.py.
10268 """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 3034 of file z3py.py.
3035 """Return a list of integer constants of size `sz`.
3037 >>> X = IntVector('x', 3)
3043 return [
Int(
'%s__%s' % (prefix, i))
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 2596 of file z3py.py.
2597 """Return `True` if `a` is an expression of the form b + c.
2599 >>> 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 2583 of file z3py.py.
2584 """Return `True` if `a` is an algebraic value of sort Real.
2586 >>> is_algebraic_value(RealVal("3/5"))
2588 >>> n = simplify(Sqrt(2))
2591 >>> is_algebraic_value(n)
2594 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 1469 of file z3py.py.
1470 """Return `True` if `a` is a Z3 and expression.
1472 >>> p, q = Bools('p q')
1473 >>> is_and(And(p, q))
1475 >>> 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 1137 of file z3py.py.
1138 """Return `True` if `a` is a Z3 function application.
1140 Note that, constants are function applications with 0 arguments.
1147 >>> is_app(IntSort())
1151 >>> is_app(IntVal(1))
1154 >>> is_app(ForAll(x, x >= 0))
1157 if not isinstance(a, ExprRef):
1159 k = _ast_kind(a.ctx, a)
1160 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 1236 of file z3py.py.
1237 """Return `True` if `a` is an application of the given kind `k`.
1241 >>> is_app_of(n, Z3_OP_ADD)
1243 >>> is_app_of(n, Z3_OP_MUL)
1246 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 2477 of file z3py.py.
2478 """Return `True` if `a` is an arithmetical expression.
2487 >>> is_arith(IntVal(1))
2495 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 2178 of file z3py.py.
2179 """Return `True` if s is an arithmetical sort (type).
2181 >>> is_arith_sort(IntSort())
2183 >>> is_arith_sort(RealSort())
2185 >>> is_arith_sort(BoolSort())
2187 >>> n = Int('x') + 1
2188 >>> is_arith_sort(n.sort())
2191 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 4294 of file z3py.py.
4295 """Return `True` if `a` is a Z3 array expression.
4297 >>> a = Array('a', IntSort(), IntSort())
4300 >>> is_array(Store(a, 0, 1))
4305 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 AstRef.eq(), 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 1422 of file z3py.py.
1423 """Return `True` if `a` is a Z3 Boolean expression.
1429 >>> is_bool(And(p, q))
1437 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 3683 of file z3py.py.
3684 """Return `True` if `a` is a Z3 bit-vector expression.
3686 >>> b = BitVec('b', 32)
3694 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 3222 of file z3py.py.
3223 """Return True if `s` is a Z3 bit-vector sort.
3225 >>> is_bv_sort(BitVecSort(32))
3227 >>> is_bv_sort(IntSort())
3230 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 3696 of file z3py.py.
3697 """Return `True` if `a` is a Z3 bit-vector numeral value.
3699 >>> b = BitVec('b', 32)
3702 >>> b = BitVecVal(10, 32)
3708 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 4307 of file z3py.py.
4308 """Return `True` if `a` is a Z3 constant array.
4310 >>> a = K(IntSort(), 10)
4311 >>> is_const_array(a)
4313 >>> a = Array('a', IntSort(), IntSort())
4314 >>> 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 4346 of file z3py.py.
4347 """Return `True` if `a` is a Z3 default array expression.
4348 >>> d = Default(K(IntSort(), 10))
4352 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 1522 of file z3py.py.
1523 """Return `True` if `a` is a Z3 distinct expression.
1525 >>> x, y, z = Ints('x y z')
1526 >>> is_distinct(x == y)
1528 >>> 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 2629 of file z3py.py.
2630 """Return `True` if `a` is an expression of the form b / c.
2632 >>> x, y = Reals('x y')
2637 >>> 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 1513 of file z3py.py.
1514 """Return `True` if `a` is a Z3 equality expression.
1516 >>> 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 1115 of file z3py.py.
1116 """Return `True` if `a` is a Z3 expression.
1123 >>> is_expr(IntSort())
1127 >>> is_expr(IntVal(1))
1130 >>> is_expr(ForAll(x, x >= 0))
1132 >>> is_expr(FPVal(1.0))
1135 return isinstance(a, ExprRef)
Referenced by SeqRef.__gt__(), AlgebraicNumRef.as_decimal(), SortRef.cast(), BoolSortRef.cast(), ArithSortRef.cast(), BitVecSortRef.cast(), FPSortRef.cast(), Cbrt(), ExprRef.children(), Concat(), 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 1456 of file z3py.py.
1457 """Return `True` if `a` is the Z3 false expression.
1464 >>> 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 7250 of file z3py.py.
7251 """Return `True` if `a` is a Z3 finite-domain expression.
7253 >>> s = FiniteDomainSort('S', 100)
7254 >>> b = Const('b', s)
7255 >>> is_finite_domain(b)
7257 >>> is_finite_domain(Int('x'))
7260 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 7228 of file z3py.py.
7229 """Return True if `s` is a Z3 finite-domain sort.
7231 >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7233 >>> is_finite_domain_sort(IntSort())
7236 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 7303 of file z3py.py.
7304 """Return `True` if `a` is a Z3 finite-domain value.
7306 >>> s = FiniteDomainSort('S', 100)
7307 >>> b = Const('b', s)
7308 >>> is_finite_domain_value(b)
7310 >>> b = FiniteDomainVal(10, s)
7313 >>> 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 9156 of file z3py.py.
9157 """Return `True` if `a` is a Z3 floating-point expression.
9159 >>> b = FP('b', FPSort(8, 24))
9167 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 8773 of file z3py.py.
8774 """Return True if `s` is a Z3 floating-point sort.
8776 >>> is_fp_sort(FPSort(8, 24))
8778 >>> is_fp_sort(IntSort())
8781 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 9169 of file z3py.py.
9170 """Return `True` if `a` is a Z3 floating-point numeral value.
9172 >>> b = FP('b', FPSort(8, 24))
9175 >>> b = FPVal(1.0, FPSort(8, 24))
9181 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 9020 of file z3py.py.
9021 """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9030 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 8783 of file z3py.py.
8784 """Return True if `s` is a Z3 floating-point rounding mode sort.
8786 >>> is_fprm_sort(FPSort(8, 24))
8788 >>> is_fprm_sort(RNE().sort())
8791 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 9032 of file z3py.py.
9033 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9034 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 2689 of file z3py.py.
2690 """Return `True` if `a` is an expression of the form b >= c.
2692 >>> 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 2700 of file z3py.py.
2701 """Return `True` if `a` is an expression of the form b > c.
2703 >>> 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 2645 of file z3py.py.
2646 """Return `True` if `a` is an expression of the form b div c.
2648 >>> 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 1491 of file z3py.py.
1492 """Return `True` if `a` is a Z3 implication expression.
1494 >>> p, q = Bools('p q')
1495 >>> is_implies(Implies(p, q))
1497 >>> 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 2497 of file z3py.py.
2498 """Return `True` if `a` is an integer expression.
2505 >>> 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 2539 of file z3py.py.
2540 """Return `True` if `a` is an integer value of sort Int.
2542 >>> is_int_value(IntVal(1))
2546 >>> is_int_value(Int('x'))
2548 >>> n = Int('x') + 1
2553 >>> is_int_value(n.arg(1))
2555 >>> is_int_value(RealVal("1/3"))
2557 >>> is_int_value(RealVal(1))
2560 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 2711 of file z3py.py.
2712 """Return `True` if `a` is an expression of the form IsInt(b).
2715 >>> 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 4319 of file z3py.py.
4320 """Return `True` if `a` is a Z3 constant array.
4322 >>> a = K(IntSort(), 10)
4325 >>> 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 2667 of file z3py.py.
2668 """Return `True` if `a` is an expression of the form b <= c.
2670 >>> 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 2678 of file z3py.py.
2679 """Return `True` if `a` is an expression of the form b < c.
2681 >>> 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 4331 of file z3py.py.
4332 """Return `True` if `a` is a Z3 map array expression.
4334 >>> f = Function('f', IntSort(), IntSort())
4335 >>> 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 2656 of file z3py.py.
2657 """Return `True` if `a` is an expression of the form b % c.
2659 >>> 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 2607 of file z3py.py.
2608 """Return `True` if `a` is an expression of the form b * c.
2610 >>> 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 1502 of file z3py.py.
1503 """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 1480 of file z3py.py.
1481 """Return `True` if `a` is a Z3 or expression.
1483 >>> p, q = Bools('p q')
1486 >>> 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 1759 of file z3py.py.
1760 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1762 >>> f = Function('f', IntSort(), IntSort())
1764 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1766 ForAll(x, f(x) == 0)
1767 >>> q.num_patterns()
1769 >>> is_pattern(q.pattern(0))
1774 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 8062 of file z3py.py.
8063 """Return `True` if `p` is a Z3 probe.
8065 >>> is_probe(Int('x'))
8067 >>> is_probe(Probe('memory'))
8070 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 1997 of file z3py.py.
1998 """Return `True` if `a` is a Z3 quantifier.
2000 >>> f = Function('f', IntSort(), IntSort())
2002 >>> q = ForAll(x, f(x) == 0)
2003 >>> is_quantifier(q)
2005 >>> is_quantifier(f(x))
2008 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 2562 of file z3py.py.
2563 """Return `True` if `a` is rational value of sort Real.
2565 >>> is_rational_value(RealVal(1))
2567 >>> is_rational_value(RealVal("3/5"))
2569 >>> is_rational_value(IntVal(1))
2571 >>> is_rational_value(1)
2573 >>> n = Real('x') + 1
2576 >>> is_rational_value(n.arg(1))
2578 >>> is_rational_value(Real('x'))
2581 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 2515 of file z3py.py.
2516 """Return `True` if `a` is a real expression.
2528 >>> 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 4538 of file z3py.py.
4539 """Return `True` if `a` is a Z3 array select application.
4541 >>> 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 10054 of file z3py.py.
10055 """Return `True` if `a` is a Z3 sequence expression.
10056 >>> print (is_seq(Unit(IntVal(0))))
10058 >>> print (is_seq(StringVal("abc")))
10061 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 4550 of file z3py.py.
4551 """Return `True` if `a` is a Z3 array store application.
4553 >>> a = Array('a', IntSort(), IntSort())
4556 >>> 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 10063 of file z3py.py.
10064 """Return `True` if `a` is a Z3 string expression.
10065 >>> print (is_string(StringVal("ab")))
10068 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 10070 of file z3py.py.
10071 """return 'True' if 'a' is a Z3 string constant expression.
10072 >>> print (is_string_value(StringVal("a")))
10074 >>> print (is_string_value(StringVal("a") + StringVal("b")))
10077 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 2618 of file z3py.py.
2619 """Return `True` if `a` is an expression of the form b - c.
2621 >>> 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 2736 of file z3py.py.
2737 """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 2722 of file z3py.py.
2723 """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 1439 of file z3py.py.
1440 """Return `True` if `a` is the Z3 true expression.
1445 >>> is_true(simplify(p == p))
1450 >>> # 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 1180 of file z3py.py.
1181 """Return `True` if `a` is variable.
1183 Z3 uses de-Bruijn indices for representing bound variables in
1191 >>> f = Function('f', IntSort(), IntSort())
1192 >>> # Z3 replaces x with bound variables when ForAll is executed.
1193 >>> q = ForAll(x, f(x) == x)
1199 >>> is_var(b.arg(1))
1202 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 3144 of file z3py.py.
3145 """ Return the Z3 predicate IsInt(a).
3148 >>> IsInt(x + "1/2")
3150 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3152 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3156 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3158 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 4651 of file z3py.py.
4652 """ Check if e is a member of set s
4653 >>> a = Const('a', SetSort(IntSort()))
4657 ctx = _ctx_from_ast_arg_list([s,e])
4658 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 4661 of file z3py.py.
4662 """ Check if a is a subset of b
4663 >>> a = Const('a', SetSort(IntSort()))
4664 >>> b = Const('b', SetSort(IntSort()))
4668 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 4501 of file z3py.py.
4502 """Return a Z3 constant array expression.
4504 >>> a = K(IntSort(), 10)
4516 _z3_assert(
is_sort(dom),
"Z3 sort expected")
4519 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 2081 of file z3py.py.
2082 """Create a Z3 lambda expression.
2084 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2085 >>> mem0 = Array('mem0', IntSort(), IntSort())
2086 >>> lo, hi, e, i = Ints('lo hi e i')
2087 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2089 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2095 _vs = (Ast * num_vars)()
2096 for i
in range(num_vars):
2098 _vs[i] = vs[i].as_ast()
2099 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 10233 of file z3py.py.
10234 """Retrieve the last index of substring within a string"""
10236 ctx = _get_ctx2(s, substr, ctx)
10237 s = _coerce_seq(s, ctx)
10238 substr = _coerce_seq(substr, ctx)
◆ Length()
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
Definition at line 10242 of file z3py.py.
10243 """Obtain the length of a sequence 's'
10244 >>> 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 10402 of file z3py.py.
10402 def Loop(re, lo, hi=0):
10403 """Create the regular expression accepting between a lower and upper bound repetitions
10404 >>> re = Loop(Re("a"), 1, 3)
10405 >>> print(simplify(InRe("aa", re)))
10407 >>> print(simplify(InRe("aaaa", re)))
10409 >>> print(simplify(InRe("", re)))
10412 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 4013 of file z3py.py.
4014 """Create the Z3 expression logical right shift.
4016 Use the operator >> for the arithmetical right shift.
4018 >>> x, y = BitVecs('x y', 32)
4021 >>> (x >> y).sexpr()
4023 >>> LShR(x, y).sexpr()
4027 >>> BitVecVal(4, 3).as_signed_long()
4029 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4031 >>> simplify(BitVecVal(4, 3) >> 1)
4033 >>> simplify(LShR(BitVecVal(4, 3), 1))
4035 >>> simplify(BitVecVal(2, 3) >> 1)
4037 >>> simplify(LShR(BitVecVal(2, 3), 1))
4040 _check_bv_args(a, b)
4041 a, b = _coerce_exprs(a, b)
4042 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__(), And(), help_simplify(), Or(), 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 4479 of file z3py.py.
4480 """Return a Z3 map array expression.
4482 >>> f = Function('f', IntSort(), IntSort(), IntSort())
4483 >>> a1 = Array('a1', IntSort(), IntSort())
4484 >>> a2 = Array('a2', IntSort(), IntSort())
4485 >>> b = Map(f, a1, a2)
4488 >>> prove(b[0] == f(a1[0], a2[0]))
4491 args = _get_args(args)
4493 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4494 _z3_assert(
is_func_decl(f),
"First argument must be a Z3 function declaration")
4495 _z3_assert(all([
is_array(a)
for a
in args]),
"Z3 array expected expected")
4496 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4497 _args, sz = _to_ast_array(args)
4499 return ArrayRef(
Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
Referenced by Context.Context().
◆ 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 1776 of file z3py.py.
1777 """Create a Z3 multi-pattern using the given expressions `*args`
1779 >>> f = Function('f', IntSort(), IntSort())
1780 >>> g = Function('g', IntSort(), IntSort())
1782 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1784 ForAll(x, f(x) != g(x))
1785 >>> q.num_patterns()
1787 >>> is_pattern(q.pattern(0))
1790 MultiPattern(f(Var(0)), g(Var(0)))
1793 _z3_assert(len(args) > 0,
"At least one argument expected")
1794 _z3_assert(all([
is_expr(a)
for a
in args ]),
"Z3 expressions expected")
1796 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 1649 of file z3py.py.
1649 def Not(a, ctx=None):
1650 """Create a Z3 not expression or probe.
1655 >>> simplify(Not(Not(p)))
1658 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1665 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 10374 of file z3py.py.
10375 """Create the regular expression that optionally accepts the argument.
10376 >>> re = Option(Re("a"))
10377 >>> print(simplify(InRe("a", re)))
10379 >>> print(simplify(InRe("", re)))
10381 >>> 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 1713 of file z3py.py.
1714 """Create a Z3 or-expression or or-probe.
1716 >>> p, q, r = Bools('p q r')
1719 >>> P = BoolVector('p', 5)
1721 Or(p__0, p__1, p__2, p__3, p__4)
1725 last_arg = args[len(args)-1]
1726 if isinstance(last_arg, Context):
1727 ctx = args[len(args)-1]
1728 args = args[:len(args)-1]
1731 args = _get_args(args)
1732 ctx_args = _ctx_from_ast_arg_list(args, ctx)
1734 _z3_assert(ctx_args
is None or ctx_args == ctx,
"context mismatch")
1735 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1736 if _has_probe(args):
1737 return _probe_or(args, ctx)
1739 args = _coerce_expr_list(args, ctx)
1740 _args, sz = _to_ast_array(args)
1741 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 7778 of file z3py.py.
7779 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
7782 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
7783 >>> # Tactic split-clause fails if there is no clause in the given goal.
7786 >>> t(Or(x == 0, x == 1))
7787 [[x == 0], [x == 1]]
7790 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7791 ctx = ks.get(
'ctx',
None)
7794 for i
in range(num - 1):
7795 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 7830 of file z3py.py.
7831 """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 7798 of file z3py.py.
7798 def ParOr(*ts, **ks):
7799 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
7802 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
7807 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7808 ctx = _get_ctx(ks.get(
'ctx',
None))
7809 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7811 _args = (TacticObj * sz)()
7813 _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 8603 of file z3py.py.
8604 """Parse a file in SMT 2.0 format using the given sorts and decls.
8606 This function is similar to parse_smt2_string().
8609 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8610 dsz, dnames, ddecls = _dict2darray(decls, ctx)
8611 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 8583 of file z3py.py.
8584 """Parse a string in SMT 2.0 format using the given sorts and decls.
8586 The arguments sorts and decls are Python dictionaries used to initialize
8587 the symbol table used for the SMT 2.0 parser.
8589 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
8591 >>> x, y = Ints('x y')
8592 >>> f = Function('f', IntSort(), IntSort())
8593 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
8595 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
8599 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8600 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 7816 of file z3py.py.
7816 def ParThen(t1, t2, ctx=None):
7817 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
7819 >>> x, y = Ints('x y')
7820 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
7821 >>> t(And(Or(x == 1, x == 2), y == x + 1))
7822 [[x == 1, y == 2], [x == 2, y == 3]]
7824 t1 = _to_tactic(t1, ctx)
7825 t2 = _to_tactic(t2, ctx)
7827 _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 8390 of file z3py.py.
8390 def PbEq(args, k, ctx = None):
8391 """Create a Pseudo-Boolean inequality k constraint.
8393 >>> a, b, c = Bools('a b c')
8394 >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
8396 _z3_check_cint_overflow(k,
"k")
8397 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8398 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 8380 of file z3py.py.
8381 """Create a Pseudo-Boolean inequality k constraint.
8383 >>> a, b, c = Bools('a b c')
8384 >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8386 _z3_check_cint_overflow(k,
"k")
8387 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8388 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 8370 of file z3py.py.
8371 """Create a Pseudo-Boolean inequality k constraint.
8373 >>> a, b, c = Bools('a b c')
8374 >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8376 _z3_check_cint_overflow(k,
"k")
8377 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8378 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 10362 of file z3py.py.
10363 """Create the regular expression accepting one or more repetitions of argument.
10364 >>> re = Plus(Re("a"))
10365 >>> print(simplify(InRe("aa", re)))
10367 >>> print(simplify(InRe("ab", re)))
10369 >>> print(simplify(InRe("", re)))
10372 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 10152 of file z3py.py.
10153 """Check if 'a' is a prefix of 'b'
10154 >>> s1 = PrefixOf("ab", "abc")
10157 >>> s2 = PrefixOf("bc", "abc")
10161 ctx = _get_ctx2(a, b)
10162 a = _coerce_seq(a, ctx)
10163 b = _coerce_seq(b, ctx)
10164 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 8088 of file z3py.py.
8089 """Return a short description for the probe named `name`.
8091 >>> 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 8078 of file z3py.py.
8079 """Return a list of all available probes in Z3.
8082 >>> 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 8286 of file z3py.py.
8287 """Create the product of the Z3 expressions.
8289 >>> a, b, c = Ints('a b c')
8290 >>> Product(a, b, c)
8292 >>> Product([a, b, c])
8294 >>> A = IntVector('a', 5)
8296 a__0*a__1*a__2*a__3*a__4
8298 args = _get_args(args)
8301 ctx = _ctx_from_ast_arg_list(args)
8303 return _reduce(
lambda a, b: a * b, args, 1)
8304 args = _coerce_expr_list(args, ctx)
8306 return _reduce(
lambda a, b: a * b, args, 1)
8308 _args, sz = _to_ast_array(args)
8309 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 8458 of file z3py.py.
8458 def prove(claim, **keywords):
8459 """Try to prove the given claim.
8461 This is a simple function for creating demonstrations. It tries to prove
8462 `claim` by showing the negation is unsatisfiable.
8464 >>> p, q = Bools('p q')
8465 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
8469 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8473 if keywords.get(
'show',
False):
8479 print(
"failed to prove")
8482 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 2998 of file z3py.py.
2998 def Q(a, b, ctx=None):
2999 """Return a Z3 rational a/b.
3001 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 10414 of file z3py.py.
10414 def Range(lo, hi, ctx = None):
10415 """Create the range regular expression over two sequences of length 1
10416 >>> range = Range("a","z")
10417 >>> print(simplify(InRe("b", range)))
10419 >>> print(simplify(InRe("bb", range)))
10422 lo = _coerce_seq(lo, ctx)
10423 hi = _coerce_seq(hi, ctx)
10424 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 2983 of file z3py.py.
2983 def RatVal(a, b, ctx=None):
2984 """Return a Z3 rational a/b.
2986 If `ctx=None`, then the global context is used.
2990 >>> RatVal(3,5).sort()
2994 _z3_assert(_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
2995 _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 10274 of file z3py.py.
10274 def Re(s, ctx=None):
10275 """The regular expression that accepts sequence 's'
10277 >>> s2 = Re(StringVal("ab"))
10278 >>> s3 = Re(Unit(BoolVal(True)))
10280 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 3058 of file z3py.py.
3058 def Real(name, ctx=None):
3059 """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 3070 of file z3py.py.
3070 def Reals(names, ctx=None):
3071 """Return a tuple of real constants.
3073 >>> x, y, z = Reals('x y z')
3076 >>> Sum(x, y, z).sort()
3080 if isinstance(names, str):
3081 names = names.split(
" ")
3082 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 2923 of file z3py.py.
2924 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2928 >>> x = Const('x', RealSort())
2933 >>> x.sort() == RealSort()
Referenced by FreshReal(), Context.getRealSort(), Context.mkRealSort(), 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 2965 of file z3py.py.
2966 """Return a Z3 real value.
2968 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2969 If `ctx=None`, then the global context is used.
2973 >>> RealVal(1).sort()
Referenced by AlgebraicNumRef.as_decimal(), Cbrt(), 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 1343 of file z3py.py.
1345 Create a real free variable. Free variables are used to create quantified formulas.
1346 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 1353 of file z3py.py.
1355 Create a list of Real free variables.
1356 The variables have ids: 0, 1, ..., n-1
1358 >>> 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 3084 of file z3py.py.
3085 """Return a list of real constants of size `sz`.
3087 >>> X = RealVector('x', 3)
3095 return [
Real(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
◆ RecAddDefinition()
def z3py.RecAddDefinition |
( |
|
f, |
|
|
|
args, |
|
|
|
body |
|
) |
| |
Set the body of a recursive function.
Recursive definitions are only unfolded during search.
>>> 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))
fac(5)
>>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3)
>>> s.check()
sat
>>> s.model().eval(fac(5))
120
Definition at line 841 of file z3py.py.
842 """Set the body of a recursive function.
843 Recursive definitions are only unfolded during search.
845 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
846 >>> n = Int('n', ctx)
847 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
850 >>> s = Solver(ctx=ctx)
851 >>> s.add(fac(n) < 3)
854 >>> s.model().eval(fac(5))
860 args = _get_args(args)
864 _args[i] = args[i].ast
◆ RecFunction()
def z3py.RecFunction |
( |
|
name, |
|
|
* |
sig |
|
) |
| |
Create a new Z3 recursive with the given sorts.
Definition at line 824 of file z3py.py.
825 """Create a new Z3 recursive with the given sorts."""
828 _z3_assert(len(sig) > 0,
"At least two arguments expected")
832 _z3_assert(
is_sort(rng),
"Z3 sort expected")
833 dom = (Sort * arity)()
834 for i
in range(arity):
836 _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 7860 of file z3py.py.
7860 def Repeat(t, max=4294967295, ctx=None):
7861 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
7863 >>> x, y = Ints('x y')
7864 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
7865 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
7867 >>> for subgoal in r: print(subgoal)
7868 [x == 0, y == 0, x > y]
7869 [x == 0, y == 1, x > y]
7870 [x == 1, y == 0, x > y]
7871 [x == 1, y == 1, x > y]
7872 >>> t = Then(t, Tactic('propagate-values'))
7876 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 4130 of file z3py.py.
4131 """Return an expression representing `n` copies of `a`.
4133 >>> x = BitVec('x', 8)
4134 >>> n = RepeatBitVec(4, x)
4139 >>> v0 = BitVecVal(10, 4)
4140 >>> print("%.x" % v0.as_long())
4142 >>> v = simplify(RepeatBitVec(4, v0))
4145 >>> print("%.x" % v.as_long())
4149 _z3_assert(_is_int(n),
"First argument must be an integer")
4150 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
4151 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 10199 of file z3py.py.
10200 """Replace the first occurrence of 'src' by 'dst' in 's'
10201 >>> r = Replace("aaa", "a", "b")
10205 ctx = _get_ctx2(dst, s)
10206 if ctx
is None and is_expr(src):
10208 src = _coerce_seq(src, ctx)
10209 dst = _coerce_seq(dst, ctx)
10210 s = _coerce_seq(s, ctx)
10211 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 10294 of file z3py.py.
10297 if s
is None or isinstance(s, Context):
10300 raise Z3Exception(
"Regular expression sort constructor expects either a string or a context or no argument")
Referenced by Context.mkReSort().
◆ 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 4044 of file z3py.py.
4045 """Return an expression representing `a` rotated to the left `b` times.
4047 >>> a, b = BitVecs('a b', 16)
4048 >>> RotateLeft(a, b)
4050 >>> simplify(RotateLeft(a, 0))
4052 >>> simplify(RotateLeft(a, 16))
4055 _check_bv_args(a, b)
4056 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 4059 of file z3py.py.
4060 """Return an expression representing `a` rotated to the right `b` times.
4062 >>> a, b = BitVecs('a b', 16)
4063 >>> RotateRight(a, b)
4065 >>> simplify(RotateRight(a, 0))
4067 >>> simplify(RotateRight(a, 16))
4070 _check_bv_args(a, b)
4071 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 4464 of file z3py.py.
4465 """Return a Z3 select array expression.
4467 >>> a = Array('a', IntSort(), IntSort())
4471 >>> eq(Select(a, i), a[i])
4475 _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 9980 of file z3py.py.
9981 """Create a sequence sort over elements provided in the argument
9982 >>> s = SeqSort(IntSort())
9983 >>> s == Unit(IntVal(1)).sort()
Referenced by Context.mkSeqSort(), and Context.mkStringSort().
◆ set_default_fp_sort()
def z3py.set_default_fp_sort |
( |
|
ebits, |
|
|
|
sbits, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 8656 of file z3py.py.
8657 global _dflt_fpsort_ebits
8658 global _dflt_fpsort_sbits
8659 _dflt_fpsort_ebits = ebits
8660 _dflt_fpsort_sbits = sbits
◆ set_default_rounding_mode()
def z3py.set_default_rounding_mode |
( |
|
rm, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 8640 of file z3py.py.
8641 global _dflt_rounding_mode
8643 _dflt_rounding_mode = rm.decl().kind()
8645 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO
or
8646 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE
or
8647 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE
or
8648 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
or
8649 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
8650 "illegal rounding mode")
8651 _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 4612 of file z3py.py.
4613 """ Add element e to set s
4614 >>> a = Const('a', SetSort(IntSort()))
4618 ctx = _ctx_from_ast_arg_list([s,e])
4619 e = _py2expr(e, ctx)
4620 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 4632 of file z3py.py.
4633 """ The complement of set s
4634 >>> a = Const('a', SetSort(IntSort()))
4635 >>> SetComplement(a)
◆ SetDel()
Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
Definition at line 4622 of file z3py.py.
4623 """ Remove element e to set s
4624 >>> a = Const('a', SetSort(IntSort()))
4628 ctx = _ctx_from_ast_arg_list([s,e])
4629 e = _py2expr(e, ctx)
4630 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 4641 of file z3py.py.
4642 """ The set difference of a and b
4643 >>> a = Const('a', SetSort(IntSort()))
4644 >>> b = Const('b', SetSort(IntSort()))
4645 >>> SetDifference(a, b)
4648 ctx = _ctx_from_ast_arg_list([a, b])
◆ SetHasSize()
def z3py.SetHasSize |
( |
|
a, |
|
|
|
k |
|
) |
| |
Definition at line 4533 of file z3py.py.
4535 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 4600 of file z3py.py.
4601 """ Take the union of sets
4602 >>> a = Const('a', SetSort(IntSort()))
4603 >>> b = Const('b', SetSort(IntSort()))
4604 >>> SetIntersect(a, b)
4607 args = _get_args(args)
4608 ctx = _ctx_from_ast_arg_list(args)
4609 _args, sz = _to_ast_array(args)
◆ SetSort()
Sets.
Create a set sort over element sort s
Definition at line 4568 of file z3py.py.
4569 """ Create a set sort over element sort s"""
Referenced by Context.mkSetSort().
◆ 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 4588 of file z3py.py.
4589 """ Take the union of sets
4590 >>> a = Const('a', SetSort(IntSort()))
4591 >>> b = Const('b', SetSort(IntSort()))
4595 args = _get_args(args)
4596 ctx = _ctx_from_ast_arg_list(args)
4597 _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 4074 of file z3py.py.
4075 """Return a bit-vector expression with `n` extra sign-bits.
4077 >>> x = BitVec('x', 16)
4078 >>> n = SignExt(8, x)
4085 >>> v0 = BitVecVal(2, 2)
4090 >>> v = simplify(SignExt(6, v0))
4095 >>> print("%.x" % v.as_long())
4099 _z3_assert(_is_int(n),
"First argument must be an integer")
4100 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
4101 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 6931 of file z3py.py.
6932 """Return a simple general purpose solver with limited amount of preprocessing.
6934 >>> 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 8182 of file z3py.py.
8182 def simplify(a, *arguments, **keywords):
8183 """Simplify the expression `a` using the given options.
8185 This function has many options. Use `help_simplify` to obtain the complete list.
8189 >>> simplify(x + 1 + y + x + 1)
8191 >>> simplify((x + 1)*(y + 1), som=True)
8193 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
8194 And(Not(x == y), Not(x == 1), Not(y == 1))
8195 >>> simplify(And(x == 0, y == 1), elim_and=True)
8196 Not(Or(Not(x == 0), Not(y == 1)))
8199 _z3_assert(
is_expr(a),
"Z3 expression expected")
8200 if len(arguments) > 0
or len(keywords) > 0:
8202 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8204 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 8210 of file z3py.py.
8211 """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 8401 of file z3py.py.
8401 def solve(*args, **keywords):
8402 """Solve the constraints `*args`.
8404 This is a simple function for creating demonstrations. It creates a solver,
8405 configure it using the options in `keywords`, adds the constraints
8406 in `args`, and invokes check.
8409 >>> solve(a > 0, a < 2)
8415 if keywords.get(
'show',
False):
8419 print(
"no solution")
8421 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 8429 of file z3py.py.
8430 """Solve the constraints `*args` using solver `s`.
8432 This is a simple function for creating demonstrations. It is similar to `solve`,
8433 but it uses the given solver `s`.
8434 It configures solver `s` using the options in `keywords`, adds the constraints
8435 in `args`, and invokes check.
8438 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8441 if keywords.get(
'show',
False):
8446 print(
"no solution")
8448 print(
"failed to solve")
8454 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 6911 of file z3py.py.
6911 def SolverFor(logic, ctx=None, logFile=None):
6912 """Create a solver customized for the given logic.
6914 The parameter `logic` is a string. It should be contains
6915 the name of a SMT-LIB logic.
6916 See http://www.smtlib.org/ for the name of all available logics.
6918 >>> 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 3160 of file z3py.py.
3160 def Sqrt(a, ctx=None):
3161 """ 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 3993 of file z3py.py.
3994 """Create the Z3 expression signed remainder.
3996 Use the operator % for signed modulus, and URem() for unsigned remainder.
3998 >>> x = BitVec('x', 32)
3999 >>> y = BitVec('y', 32)
4002 >>> SRem(x, y).sort()
4006 >>> SRem(x, y).sexpr()
4009 _check_bv_args(a, b)
4010 a, b = _coerce_exprs(a, b)
4011 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 10390 of file z3py.py.
10391 """Create the regular expression accepting zero or more repetitions of argument.
10392 >>> re = Star(Re("a"))
10393 >>> print(simplify(InRe("aa", re)))
10395 >>> print(simplify(InRe("ab", re)))
10397 >>> print(simplify(InRe("", re)))
10400 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 4448 of file z3py.py.
4449 """Return a Z3 store array expression.
4451 >>> a = Array('a', IntSort(), IntSort())
4452 >>> i, v = Ints('i v')
4453 >>> s = Store(a, i, v)
4456 >>> prove(s[i] == v)
4459 >>> 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 10085 of file z3py.py.
10085 def String(name, ctx=None):
10086 """Return a string constant named `name`. If `ctx=None`, then the global context is used.
10088 >>> x = String('x')
10090 ctx = _get_ctx(ctx)
Referenced by Native.applyResultToString(), Native.astMapToString(), Native.astToString(), Native.astVectorToString(), Native.benchmarkToSmtlibString(), Context.Context(), Native.evalSmtlib2String(), Native.fixedpointGetHelp(), Native.fixedpointGetReasonUnknown(), Native.fixedpointToString(), Native.fpaGetNumeralExponentString(), Native.fpaGetNumeralSignificandString(), Native.funcDeclToString(), Native.getDeclRationalParameter(), Statistics.getEntries(), Native.getErrorMsg(), Native.getFullVersion(), Statistics.getKeys(), Native.getLstring(), Native.getNumeralDecimalString(), Native.getNumeralString(), Native.getProbeName(), Context.getProbeNames(), Native.getString(), Native.getSymbolString(), Native.getTacticName(), Context.getTacticNames(), Native.goalToDimacsString(), Native.goalToString(), Native.modelToString(), Native.optimizeGetHelp(), Native.optimizeGetReasonUnknown(), Native.optimizeToString(), Native.paramDescrsGetDocumentation(), Native.paramDescrsToString(), Native.paramsToString(), Native.patternToString(), Native.probeGetDescr(), Native.rcfNumToDecimalString(), Native.rcfNumToString(), Native.simplifyGetHelp(), Native.solverGetHelp(), Native.solverGetReasonUnknown(), Native.solverToDimacsString(), Native.solverToString(), Native.sortToString(), Native.statsGetKey(), Native.statsToString(), Strings(), SubSeq(), Native.tacticGetDescr(), Native.tacticGetHelp(), and FuncInterp.toString().
◆ Strings()
def Strings |
( |
|
names, |
|
|
|
ctx = None |
|
) |
| |
Return string constants
Return a tuple of String constants.
Definition at line 10093 of file z3py.py.
10093 def Strings(names, ctx=None):
10094 """Return string constants"""
10095 ctx = _get_ctx(ctx)
10096 if isinstance(names, str):
10097 names = names.split(
" ")
10098 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 9970 of file z3py.py.
9971 """Create a string sort
9972 >>> s = StringSort()
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 10251 of file z3py.py.
10252 """Convert string expression to integer
10253 >>> a = StrToInt("1")
10254 >>> simplify(1 == a)
10256 >>> b = StrToInt("2")
10257 >>> simplify(1 == b)
10259 >>> c = StrToInt(IntToStr(2))
10260 >>> simplify(1 == c)
◆ SubSeq()
def z3py.SubSeq |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10104 of file z3py.py.
10104 def SubSeq(s, offset, length):
10105 """Extract substring or subsequence starting at offset"""
10106 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 8214 of file z3py.py.
8215 """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.
8219 >>> substitute(x + 1, (x, y + 1))
8221 >>> f = Function('f', IntSort(), IntSort())
8222 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
8225 if isinstance(m, tuple):
8227 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8230 _z3_assert(
is_expr(t),
"Z3 expression expected")
8231 _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.")
8233 _from = (Ast * num)()
8235 for i
in range(num):
8236 _from[i] = m[i][0].as_ast()
8237 _to[i] = m[i][1].as_ast()
8238 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 8240 of file z3py.py.
8241 """Substitute the free variables in t with the expression in m.
8243 >>> v0 = Var(0, IntSort())
8244 >>> v1 = Var(1, IntSort())
8246 >>> f = Function('f', IntSort(), IntSort(), IntSort())
8247 >>> # replace v0 with x+1 and v1 with x
8248 >>> substitute_vars(f(v0, v1), x + 1, x)
8252 _z3_assert(
is_expr(t),
"Z3 expression expected")
8253 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8256 for i
in range(num):
8257 _to[i] = m[i].as_ast()
◆ SubString()
def z3py.SubString |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10100 of file z3py.py.
10101 """Extract substring or subsequence starting at offset"""
10102 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 10166 of file z3py.py.
10167 """Check if 'a' is a suffix of 'b'
10168 >>> s1 = SuffixOf("ab", "abc")
10171 >>> s2 = SuffixOf("bc", "abc")
10175 ctx = _get_ctx2(a, b)
10176 a = _coerce_seq(a, ctx)
10177 b = _coerce_seq(b, ctx)
10178 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 8260 of file z3py.py.
8261 """Create the sum of the Z3 expressions.
8263 >>> a, b, c = Ints('a b c')
8268 >>> A = IntVector('a', 5)
8270 a__0 + a__1 + a__2 + a__3 + a__4
8272 args = _get_args(args)
8275 ctx = _ctx_from_ast_arg_list(args)
8277 return _reduce(
lambda a, b: a + b, args, 0)
8278 args = _coerce_expr_list(args, ctx)
8280 return _reduce(
lambda a, b: a + b, args, 0)
8282 _args, sz = _to_ast_array(args)
8283 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 7897 of file z3py.py.
7898 """Return a short description for the tactic named `name`.
7900 >>> 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 7887 of file z3py.py.
7888 """Return a list of all available tactics in Z3.
7891 >>> 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 7766 of file z3py.py.
7766 def Then(*ts, **ks):
7767 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
7769 >>> x, y = Ints('x y')
7770 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
7771 >>> t(And(x == 0, y > x + 1))
7773 >>> 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 3127 of file z3py.py.
3128 """ Return the Z3 expression ToInt(a).
3140 _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 3110 of file z3py.py.
3111 """ Return the Z3 expression ToReal(a).
3123 _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 10440 of file z3py.py.
10441 """Given a binary relation R, such that the two arguments have the same sort
10442 create the transitive closure relation R+.
10443 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 7879 of file z3py.py.
7879 def TryFor(t, ms, ctx=None):
7880 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
7882 If `t` does not terminate in `ms` milliseconds, then it fails.
7884 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 4971 of file z3py.py.
4972 """Create a named tuple sort base on a set of underlying sorts
4974 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
4976 tuple = Datatype(name, ctx)
4977 projects = [ (
'project%d' % i, sorts[i])
for i
in range(len(sorts)) ]
4978 tuple.declare(name, *projects)
4979 tuple = tuple.create()
4980 return tuple, tuple.constructor(0), [tuple.accessor(0, i)
for i
in range(len(sorts))]
Referenced by Context.mkTupleSort().
◆ 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 3953 of file z3py.py.
3954 """Create the Z3 expression (unsigned) division `self / other`.
3956 Use the operator / for signed division.
3958 >>> x = BitVec('x', 32)
3959 >>> y = BitVec('y', 32)
3962 >>> UDiv(x, y).sort()
3966 >>> UDiv(x, y).sexpr()
3969 _check_bv_args(a, b)
3970 a, b = _coerce_exprs(a, b)
3971 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 3919 of file z3py.py.
3920 """Create the Z3 expression (unsigned) `other >= self`.
3922 Use the operator >= for signed greater than or equal to.
3924 >>> x, y = BitVecs('x y', 32)
3927 >>> (x >= y).sexpr()
3929 >>> UGE(x, y).sexpr()
3932 _check_bv_args(a, b)
3933 a, b = _coerce_exprs(a, b)
3934 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 3936 of file z3py.py.
3937 """Create the Z3 expression (unsigned) `other > self`.
3939 Use the operator > for signed greater than.
3941 >>> x, y = BitVecs('x y', 32)
3946 >>> UGT(x, y).sexpr()
3949 _check_bv_args(a, b)
3950 a, b = _coerce_exprs(a, b)
3951 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 3885 of file z3py.py.
3886 """Create the Z3 expression (unsigned) `other <= self`.
3888 Use the operator <= for signed less than or equal to.
3890 >>> x, y = BitVecs('x y', 32)
3893 >>> (x <= y).sexpr()
3895 >>> ULE(x, y).sexpr()
3898 _check_bv_args(a, b)
3899 a, b = _coerce_exprs(a, b)
3900 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 3902 of file z3py.py.
3903 """Create the Z3 expression (unsigned) `other < self`.
3905 Use the operator < for signed less than.
3907 >>> x, y = BitVecs('x y', 32)
3912 >>> ULT(x, y).sexpr()
3915 _check_bv_args(a, b)
3916 a, b = _coerce_exprs(a, b)
3917 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 10326 of file z3py.py.
10327 """Create union of regular expressions.
10328 >>> re = Union(Re("a"), Re("b"), Re("c"))
10329 >>> print (simplify(InRe("d", re)))
10332 args = _get_args(args)
10335 _z3_assert(sz > 0,
"At least one argument expected.")
10336 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10341 for i
in range(sz):
10342 v[i] = args[i].as_ast()
Referenced by ReRef.__add__().
◆ Unit()
Create a singleton sequence
Definition at line 10148 of file z3py.py.
10149 """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 4416 of file z3py.py.
4417 """Return a Z3 store array expression.
4419 >>> a = Array('a', IntSort(), IntSort())
4420 >>> i, v = Ints('i v')
4421 >>> s = Update(a, i, v)
4424 >>> prove(s[i] == v)
4427 >>> prove(Implies(i != j, s[j] == a[j]))
4431 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4432 i = a.domain().cast(i)
4433 v = a.range().cast(v)
4435 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 3973 of file z3py.py.
3974 """Create the Z3 expression (unsigned) remainder `self % other`.
3976 Use the operator % for signed modulus, and SRem() for signed remainder.
3978 >>> x = BitVec('x', 32)
3979 >>> y = BitVec('y', 32)
3982 >>> URem(x, y).sort()
3986 >>> URem(x, y).sexpr()
3989 _check_bv_args(a, b)
3990 a, b = _coerce_exprs(a, b)
3991 return BitVecRef(
Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.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 1331 of file z3py.py.
1332 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1334 >>> Var(0, IntSort())
1336 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1340 _z3_assert(
is_sort(s),
"Z3 sort expected")
1341 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 8148 of file z3py.py.
8148 def When(p, t, ctx=None):
8149 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8151 >>> t = When(Probe('size') > 2, Tactic('simplify'))
8152 >>> x, y = Ints('x y')
8158 >>> g.add(x == y + 1)
8160 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8162 p = _to_probe(p, ctx)
8163 t = _to_tactic(t, ctx)
8164 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 7834 of file z3py.py.
7834 def With(t, *args, **keys):
7835 """Return a tactic that applies tactic `t` using the given configuration options.
7837 >>> x, y = Ints('x y')
7838 >>> t = With(Tactic('simplify'), som=True)
7839 >>> t((x + 1)*(y + 2) == 0)
7840 [[2*x + y + x*y == -2]]
7842 ctx = keys.pop(
'ctx',
None)
7843 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 7847 of file z3py.py.
7848 """Return a tactic that applies tactic `t` using the given configuration options.
7850 >>> x, y = Ints('x y')
7852 >>> p.set("som", True)
7853 >>> t = WithParams(Tactic('simplify'), p)
7854 >>> t((x + 1)*(y + 2) == 0)
7855 [[2*x + y + x*y == -2]]
7857 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 1634 of file z3py.py.
1634 def Xor(a, b, ctx=None):
1635 """Create a Z3 Xor expression.
1637 >>> p, q = Bools('p q')
1640 >>> simplify(Xor(p, q))
1643 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1647 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(), AlgebraicNumRef.as_decimal(), 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(), AstRef.eq(), eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), 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 4103 of file z3py.py.
4104 """Return a bit-vector expression with `n` extra zero-bits.
4106 >>> x = BitVec('x', 16)
4107 >>> n = ZeroExt(8, x)
4114 >>> v0 = BitVecVal(2, 2)
4119 >>> v = simplify(ZeroExt(6, v0))
4126 _z3_assert(_is_int(n),
"First argument must be an integer")
4127 _z3_assert(
is_bv(a),
"Second argument must be a Z3 Bitvector expression")
4128 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)
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.
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 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.
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 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.
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_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 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 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.