|
def | z3_debug () |
|
def | enable_trace (msg) |
|
def | disable_trace (msg) |
|
def | get_version_string () |
|
def | get_version () |
|
def | get_full_version () |
|
def | open_log (fname) |
|
def | append_log (s) |
|
def | to_symbol (s, ctx=None) |
|
def | z3_error_handler (c, e) |
|
def | main_ctx () |
|
def | get_ctx (ctx) |
|
def | set_param (*args, **kws) |
|
def | reset_params () |
|
def | set_option (*args, **kws) |
|
def | get_param (name) |
|
def | is_ast (a) |
|
def | eq (a, b) |
|
def | is_sort (s) |
|
def | DeclareSort (name, ctx=None) |
|
def | is_func_decl (a) |
|
def | Function (name, *sig) |
|
def | FreshFunction (*sig) |
|
def | RecFunction (name, *sig) |
|
def | RecAddDefinition (f, args, body) |
|
def | is_expr (a) |
|
def | is_app (a) |
|
def | is_const (a) |
|
def | is_var (a) |
|
def | get_var_index (a) |
|
def | is_app_of (a, k) |
|
def | If (a, b, c, ctx=None) |
|
def | Distinct (*args) |
|
def | Const (name, sort) |
|
def | Consts (names, sort) |
|
def | FreshConst (sort, prefix='c') |
|
def | Var (idx, s) |
|
def | RealVar (idx, ctx=None) |
|
def | RealVarVector (n, ctx=None) |
|
def | is_bool (a) |
|
def | is_true (a) |
|
def | is_false (a) |
|
def | is_and (a) |
|
def | is_or (a) |
|
def | is_implies (a) |
|
def | is_not (a) |
|
def | is_eq (a) |
|
def | is_distinct (a) |
|
def | BoolSort (ctx=None) |
|
def | BoolVal (val, ctx=None) |
|
def | Bool (name, ctx=None) |
|
def | Bools (names, ctx=None) |
|
def | BoolVector (prefix, sz, ctx=None) |
|
def | FreshBool (prefix='b', ctx=None) |
|
def | Implies (a, b, ctx=None) |
|
def | Xor (a, b, ctx=None) |
|
def | Not (a, ctx=None) |
|
def | mk_not (a) |
|
def | And (*args) |
|
def | Or (*args) |
|
def | is_pattern (a) |
|
def | MultiPattern (*args) |
|
def | is_quantifier (a) |
|
def | ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
|
def | Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
|
def | Lambda (vs, body) |
|
def | is_arith_sort (s) |
|
def | is_arith (a) |
|
def | is_int (a) |
|
def | is_real (a) |
|
def | is_int_value (a) |
|
def | is_rational_value (a) |
|
def | is_algebraic_value (a) |
|
def | is_add (a) |
|
def | is_mul (a) |
|
def | is_sub (a) |
|
def | is_div (a) |
|
def | is_idiv (a) |
|
def | is_mod (a) |
|
def | is_le (a) |
|
def | is_lt (a) |
|
def | is_ge (a) |
|
def | is_gt (a) |
|
def | is_is_int (a) |
|
def | is_to_real (a) |
|
def | is_to_int (a) |
|
def | IntSort (ctx=None) |
|
def | RealSort (ctx=None) |
|
def | IntVal (val, ctx=None) |
|
def | RealVal (val, ctx=None) |
|
def | RatVal (a, b, ctx=None) |
|
def | Q (a, b, ctx=None) |
|
def | Int (name, ctx=None) |
|
def | Ints (names, ctx=None) |
|
def | IntVector (prefix, sz, ctx=None) |
|
def | FreshInt (prefix='x', ctx=None) |
|
def | Real (name, ctx=None) |
|
def | Reals (names, ctx=None) |
|
def | RealVector (prefix, sz, ctx=None) |
|
def | FreshReal (prefix='b', ctx=None) |
|
def | ToReal (a) |
|
def | ToInt (a) |
|
def | IsInt (a) |
|
def | Sqrt (a, ctx=None) |
|
def | Cbrt (a, ctx=None) |
|
def | is_bv_sort (s) |
|
def | is_bv (a) |
|
def | is_bv_value (a) |
|
def | BV2Int (a, is_signed=False) |
|
def | Int2BV (a, num_bits) |
|
def | BitVecSort (sz, ctx=None) |
|
def | BitVecVal (val, bv, ctx=None) |
|
def | BitVec (name, bv, ctx=None) |
|
def | BitVecs (names, bv, ctx=None) |
|
def | Concat (*args) |
|
def | Extract (high, low, a) |
|
def | ULE (a, b) |
|
def | ULT (a, b) |
|
def | UGE (a, b) |
|
def | UGT (a, b) |
|
def | UDiv (a, b) |
|
def | URem (a, b) |
|
def | SRem (a, b) |
|
def | LShR (a, b) |
|
def | RotateLeft (a, b) |
|
def | RotateRight (a, b) |
|
def | SignExt (n, a) |
|
def | ZeroExt (n, a) |
|
def | RepeatBitVec (n, a) |
|
def | BVRedAnd (a) |
|
def | BVRedOr (a) |
|
def | BVAddNoOverflow (a, b, signed) |
|
def | BVAddNoUnderflow (a, b) |
|
def | BVSubNoOverflow (a, b) |
|
def | BVSubNoUnderflow (a, b, signed) |
|
def | BVSDivNoOverflow (a, b) |
|
def | BVSNegNoOverflow (a) |
|
def | BVMulNoOverflow (a, b, signed) |
|
def | BVMulNoUnderflow (a, b) |
|
def | is_array_sort (a) |
|
def | is_array (a) |
|
def | is_const_array (a) |
|
def | is_K (a) |
|
def | is_map (a) |
|
def | is_default (a) |
|
def | get_map_func (a) |
|
def | ArraySort (*sig) |
|
def | Array (name, dom, rng) |
|
def | Update (a, i, v) |
|
def | Default (a) |
|
def | Store (a, i, v) |
|
def | Select (a, i) |
|
def | Map (f, *args) |
|
def | K (dom, v) |
|
def | Ext (a, b) |
|
def | SetHasSize (a, k) |
|
def | is_select (a) |
|
def | is_store (a) |
|
def | SetSort (s) |
| Sets. More...
|
|
def | EmptySet (s) |
|
def | FullSet (s) |
|
def | SetUnion (*args) |
|
def | SetIntersect (*args) |
|
def | SetAdd (s, e) |
|
def | SetDel (s, e) |
|
def | SetComplement (s) |
|
def | SetDifference (a, b) |
|
def | IsMember (e, s) |
|
def | IsSubset (a, b) |
|
def | CreateDatatypes (*ds) |
|
def | TupleSort (name, sorts, ctx=None) |
|
def | DisjointSum (name, sorts, ctx=None) |
|
def | EnumSort (name, values, ctx=None) |
|
def | args2params (arguments, keywords, ctx=None) |
|
def | Model (ctx=None) |
|
def | is_as_array (n) |
|
def | get_as_array_func (n) |
|
def | SolverFor (logic, ctx=None, logFile=None) |
|
def | SimpleSolver (ctx=None, logFile=None) |
|
def | FiniteDomainSort (name, sz, ctx=None) |
|
def | is_finite_domain_sort (s) |
|
def | is_finite_domain (a) |
|
def | FiniteDomainVal (val, sort, ctx=None) |
|
def | is_finite_domain_value (a) |
|
def | AndThen (*ts, **ks) |
|
def | Then (*ts, **ks) |
|
def | OrElse (*ts, **ks) |
|
def | ParOr (*ts, **ks) |
|
def | ParThen (t1, t2, ctx=None) |
|
def | ParAndThen (t1, t2, ctx=None) |
|
def | With (t, *args, **keys) |
|
def | WithParams (t, p) |
|
def | Repeat (t, max=4294967295, ctx=None) |
|
def | TryFor (t, ms, ctx=None) |
|
def | tactics (ctx=None) |
|
def | tactic_description (name, ctx=None) |
|
def | describe_tactics () |
|
def | is_probe (p) |
|
def | probes (ctx=None) |
|
def | probe_description (name, ctx=None) |
|
def | describe_probes () |
|
def | FailIf (p, ctx=None) |
|
def | When (p, t, ctx=None) |
|
def | Cond (p, t1, t2, ctx=None) |
|
def | simplify (a, *arguments, **keywords) |
| Utils. More...
|
|
def | help_simplify () |
|
def | simplify_param_descrs () |
|
def | substitute (t, *m) |
|
def | substitute_vars (t, *m) |
|
def | Sum (*args) |
|
def | Product (*args) |
|
def | AtMost (*args) |
|
def | AtLeast (*args) |
|
def | PbLe (args, k) |
|
def | PbGe (args, k) |
|
def | PbEq (args, k, ctx=None) |
|
def | solve (*args, **keywords) |
|
def | solve_using (s, *args, **keywords) |
|
def | prove (claim, **keywords) |
|
def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
|
def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
|
def | get_default_rounding_mode (ctx=None) |
|
def | set_default_rounding_mode (rm, ctx=None) |
|
def | get_default_fp_sort (ctx=None) |
|
def | set_default_fp_sort (ebits, sbits, ctx=None) |
|
def | Float16 (ctx=None) |
|
def | FloatHalf (ctx=None) |
|
def | Float32 (ctx=None) |
|
def | FloatSingle (ctx=None) |
|
def | Float64 (ctx=None) |
|
def | FloatDouble (ctx=None) |
|
def | Float128 (ctx=None) |
|
def | FloatQuadruple (ctx=None) |
|
def | is_fp_sort (s) |
|
def | is_fprm_sort (s) |
|
def | RoundNearestTiesToEven (ctx=None) |
|
def | RNE (ctx=None) |
|
def | RoundNearestTiesToAway (ctx=None) |
|
def | RNA (ctx=None) |
|
def | RoundTowardPositive (ctx=None) |
|
def | RTP (ctx=None) |
|
def | RoundTowardNegative (ctx=None) |
|
def | RTN (ctx=None) |
|
def | RoundTowardZero (ctx=None) |
|
def | RTZ (ctx=None) |
|
def | is_fprm (a) |
|
def | is_fprm_value (a) |
|
def | is_fp (a) |
|
def | is_fp_value (a) |
|
def | FPSort (ebits, sbits, ctx=None) |
|
def | fpNaN (s) |
|
def | fpPlusInfinity (s) |
|
def | fpMinusInfinity (s) |
|
def | fpInfinity (s, negative) |
|
def | fpPlusZero (s) |
|
def | fpMinusZero (s) |
|
def | fpZero (s, negative) |
|
def | FPVal (sig, exp=None, fps=None, ctx=None) |
|
def | FP (name, fpsort, ctx=None) |
|
def | FPs (names, fpsort, ctx=None) |
|
def | fpAbs (a, ctx=None) |
|
def | fpNeg (a, ctx=None) |
|
def | fpAdd (rm, a, b, ctx=None) |
|
def | fpSub (rm, a, b, ctx=None) |
|
def | fpMul (rm, a, b, ctx=None) |
|
def | fpDiv (rm, a, b, ctx=None) |
|
def | fpRem (a, b, ctx=None) |
|
def | fpMin (a, b, ctx=None) |
|
def | fpMax (a, b, ctx=None) |
|
def | fpFMA (rm, a, b, c, ctx=None) |
|
def | fpSqrt (rm, a, ctx=None) |
|
def | fpRoundToIntegral (rm, a, ctx=None) |
|
def | fpIsNaN (a, ctx=None) |
|
def | fpIsInf (a, ctx=None) |
|
def | fpIsZero (a, ctx=None) |
|
def | fpIsNormal (a, ctx=None) |
|
def | fpIsSubnormal (a, ctx=None) |
|
def | fpIsNegative (a, ctx=None) |
|
def | fpIsPositive (a, ctx=None) |
|
def | fpLT (a, b, ctx=None) |
|
def | fpLEQ (a, b, ctx=None) |
|
def | fpGT (a, b, ctx=None) |
|
def | fpGEQ (a, b, ctx=None) |
|
def | fpEQ (a, b, ctx=None) |
|
def | fpNEQ (a, b, ctx=None) |
|
def | fpFP (sgn, exp, sig, ctx=None) |
|
def | fpToFP (a1, a2=None, a3=None, ctx=None) |
|
def | fpBVToFP (v, sort, ctx=None) |
|
def | fpFPToFP (rm, v, sort, ctx=None) |
|
def | fpRealToFP (rm, v, sort, ctx=None) |
|
def | fpSignedToFP (rm, v, sort, ctx=None) |
|
def | fpUnsignedToFP (rm, v, sort, ctx=None) |
|
def | fpToFPUnsigned (rm, x, s, ctx=None) |
|
def | fpToSBV (rm, x, s, ctx=None) |
|
def | fpToUBV (rm, x, s, ctx=None) |
|
def | fpToReal (x, ctx=None) |
|
def | fpToIEEEBV (x, ctx=None) |
|
def | StringSort (ctx=None) |
|
def | SeqSort (s) |
|
def | is_seq (a) |
|
def | is_string (a) |
|
def | is_string_value (a) |
|
def | StringVal (s, ctx=None) |
|
def | String (name, ctx=None) |
|
def | Strings (names, ctx=None) |
|
def | SubString (s, offset, length) |
|
def | SubSeq (s, offset, length) |
|
def | Empty (s) |
|
def | Full (s) |
|
def | Unit (a) |
|
def | PrefixOf (a, b) |
|
def | SuffixOf (a, b) |
|
def | Contains (a, b) |
|
def | Replace (s, src, dst) |
|
def | IndexOf (s, substr) |
|
def | IndexOf (s, substr, offset) |
|
def | LastIndexOf (s, substr) |
|
def | Length (s) |
|
def | StrToInt (s) |
|
def | IntToStr (s) |
|
def | Re (s, ctx=None) |
|
def | ReSort (s) |
|
def | is_re (s) |
|
def | InRe (s, re) |
|
def | Union (*args) |
|
def | Intersect (*args) |
|
def | Plus (re) |
|
def | Option (re) |
|
def | Complement (re) |
|
def | Star (re) |
|
def | Loop (re, lo, hi=0) |
|
def | Range (lo, hi, ctx=None) |
|
def | PartialOrder (a, index) |
|
def | LinearOrder (a, index) |
|
def | TreeOrder (a, index) |
|
def | PiecewiseLinearOrder (a, index) |
|
def | TransitiveClosure (f) |
|
◆ And()
Create a Z3 and-expression or and-probe.
>>> p, q, r = Bools('p q r')
>>> And(p, q, r)
And(p, q, r)
>>> P = BoolVector('p', 5)
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)
Definition at line 1700 of file z3py.py.
1701 """Create a Z3 and-expression or and-probe.
1703 >>> p, q, r = Bools('p q r')
1706 >>> P = BoolVector('p', 5)
1708 And(p__0, p__1, p__2, p__3, p__4)
1712 last_arg = args[len(args)-1]
1713 if isinstance(last_arg, Context):
1714 ctx = args[len(args)-1]
1715 args = args[:len(args)-1]
1716 elif len(args) == 1
and isinstance(args[0], AstVector):
1718 args = [a
for a
in args[0]]
1721 args = _get_args(args)
1722 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1724 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1725 if _has_probe(args):
1726 return _probe_and(args, ctx)
1728 args = _coerce_expr_list(args, ctx)
1729 _args, sz = _to_ast_array(args)
1730 return BoolRef(
Z3_mk_and(ctx.ref(), sz, _args), ctx)
Referenced by Fixedpoint.add_rule(), Goal.as_expr(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().
◆ AndThen()
def z3py.AndThen |
( |
* |
ts, |
|
|
** |
ks |
|
) |
| |
Return a tactic that applies the tactics in `*ts` in sequence.
>>> x, y = Ints('x y')
>>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
>>> t(And(x == 0, y > x + 1))
[[Not(y <= 1)]]
>>> t(And(x == 0, y > x + 1)).as_expr()
Not(y <= 1)
Definition at line 7770 of file z3py.py.
7771 """Return a tactic that applies the tactics in `*ts` in sequence.
7773 >>> x, y = Ints('x y')
7774 >>> t = AndThen(Tactic('simplify'), Tactic('solve-eqs'))
7775 >>> t(And(x == 0, y > x + 1))
7777 >>> t(And(x == 0, y > x + 1)).as_expr()
7781 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7782 ctx = ks.get(
'ctx',
None)
7785 for i
in range(num - 1):
7786 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 5093 of file z3py.py.
5094 """Convert python arguments into a Z3_params object.
5095 A ':' is added to the keywords, and '_' is replaced with '-'
5097 >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
5098 (params model true relevancy 2 elim_and true)
5101 _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 4426 of file z3py.py.
4426 def Array(name, dom, rng):
4427 """Return an array constant named `name` with the given domain and range sorts.
4429 >>> 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 4394 of file z3py.py.
4395 """Return the Z3 array sort with the given domain and range sorts.
4397 >>> A = ArraySort(IntSort(), BoolSort())
4404 >>> AA = ArraySort(IntSort(), A)
4406 Array(Int, Array(Int, Bool))
4408 sig = _get_args(sig)
4410 _z3_assert(len(sig) > 1,
"At least two arguments expected")
4411 arity = len(sig) - 1
4416 _z3_assert(
is_sort(s),
"Z3 sort expected")
4417 _z3_assert(s.ctx == r.ctx,
"Context mismatch")
4421 dom = (Sort * arity)()
4422 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 8351 of file z3py.py.
8352 """Create an at-most Pseudo-Boolean k constraint.
8354 >>> a, b, c = Bools('a b c')
8355 >>> f = AtLeast(a, b, c, 2)
8357 args = _get_args(args)
8359 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8360 ctx = _ctx_from_ast_arg_list(args)
8362 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8363 args1 = _coerce_expr_list(args[:-1], ctx)
8365 _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 8334 of file z3py.py.
8335 """Create an at-most Pseudo-Boolean k constraint.
8337 >>> a, b, c = Bools('a b c')
8338 >>> f = AtMost(a, b, c, 2)
8340 args = _get_args(args)
8342 _z3_assert(len(args) > 1,
"Non empty list of arguments expected")
8343 ctx = _ctx_from_ast_arg_list(args)
8345 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
8346 args1 = _coerce_expr_list(args[:-1], ctx)
8348 _args, sz = _to_ast_array(args1)
8349 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 3793 of file z3py.py.
3793 def BitVec(name, bv, ctx=None):
3794 """Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
3795 If `ctx=None`, then the global context is used.
3797 >>> x = BitVec('x', 16)
3804 >>> word = BitVecSort(16)
3805 >>> x2 = BitVec('x', word)
3809 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 3816 of file z3py.py.
3816 def BitVecs(names, bv, ctx=None):
3817 """Return a tuple of bit-vector constants of size bv.
3819 >>> x, y, z = BitVecs('x y z', 16)
3826 >>> Product(x, y, z)
3828 >>> simplify(Product(x, y, z))
3832 if isinstance(names, str):
3833 names = names.split(
" ")
3834 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 3763 of file z3py.py.
3764 """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
3766 >>> Byte = BitVecSort(8)
3767 >>> Word = BitVecSort(16)
3770 >>> x = Const('x', Byte)
3771 >>> 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 3777 of file z3py.py.
3778 """Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
3780 >>> v = BitVecVal(10, 32)
3783 >>> print("0x%.8x" % v.as_long())
3788 return BitVecNumRef(
Z3_mk_numeral(ctx.ref(), _to_int_str(val), bv.ast), ctx)
◆ Bool()
def z3py.Bool |
( |
|
name, |
|
|
|
ctx = None |
|
) |
| |
◆ Bools()
def z3py.Bools |
( |
|
names, |
|
|
|
ctx = None |
|
) |
| |
Return a tuple of Boolean constants.
`names` is a single string containing all names separated by blank spaces.
If `ctx=None`, then the global context is used.
>>> p, q, r = Bools('p q r')
>>> And(p, Or(q, r))
And(p, Or(q, r))
Definition at line 1599 of file z3py.py.
1599 def Bools(names, ctx=None):
1600 """Return a tuple of Boolean constants.
1602 `names` is a single string containing all names separated by blank spaces.
1603 If `ctx=None`, then the global context is used.
1605 >>> p, q, r = Bools('p q r')
1606 >>> And(p, Or(q, r))
1610 if isinstance(names, str):
1611 names = names.split(
" ")
1612 return [
Bool(name, ctx)
for name
in names]
◆ BoolSort()
def z3py.BoolSort |
( |
|
ctx = None | ) |
|
Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
>>> BoolSort()
Bool
>>> p = Const('p', BoolSort())
>>> is_bool(p)
True
>>> r = Function('r', IntSort(), IntSort(), BoolSort())
>>> r(0, 1)
r(0, 1)
>>> is_bool(r(0, 1))
True
Definition at line 1553 of file z3py.py.
1554 """Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
1558 >>> p = Const('p', BoolSort())
1561 >>> r = Function('r', IntSort(), IntSort(), BoolSort())
1564 >>> is_bool(r(0, 1))
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Bool(), 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 1614 of file z3py.py.
1615 """Return a list of Boolean constants of size `sz`.
1617 The constants are named using the given prefix.
1618 If `ctx=None`, then the global context is used.
1620 >>> P = BoolVector('p', 3)
1624 And(p__0, p__1, p__2)
1626 return [
Bool(
'%s__%s' % (prefix, i))
for i
in range(sz) ]
◆ BV2Int()
def z3py.BV2Int |
( |
|
a, |
|
|
|
is_signed = False |
|
) |
| |
Return the Z3 expression BV2Int(a).
>>> b = BitVec('b', 3)
>>> BV2Int(b).sort()
Int
>>> x = Int('x')
>>> x > BV2Int(b)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=False)
x > BV2Int(b)
>>> x > BV2Int(b, is_signed=True)
x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
>>> solve(x > BV2Int(b), b == 1, x < 3)
[x = 2, b = 1]
Definition at line 3733 of file z3py.py.
3733 def BV2Int(a, is_signed=False):
3734 """Return the Z3 expression BV2Int(a).
3736 >>> b = BitVec('b', 3)
3737 >>> BV2Int(b).sort()
3742 >>> x > BV2Int(b, is_signed=False)
3744 >>> x > BV2Int(b, is_signed=True)
3745 x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
3746 >>> solve(x > BV2Int(b), b == 1, x < 3)
3750 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
3753 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 4188 of file z3py.py.
4189 """A predicate the determines that bit-vector addition does not overflow"""
4190 _check_bv_args(a, b)
4191 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 4194 of file z3py.py.
4195 """A predicate the determines that signed bit-vector addition does not underflow"""
4196 _check_bv_args(a, b)
4197 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 4225 of file z3py.py.
4226 """A predicate the determines that bit-vector multiplication does not overflow"""
4227 _check_bv_args(a, b)
4228 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 4232 of file z3py.py.
4233 """A predicate the determines that bit-vector signed multiplication does not underflow"""
4234 _check_bv_args(a, b)
4235 a, b = _coerce_exprs(a, b)
◆ BVRedAnd()
Return the reduction-and expression of `a`.
Definition at line 4176 of file z3py.py.
4177 """Return the reduction-and expression of `a`."""
4179 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
◆ BVRedOr()
Return the reduction-or expression of `a`.
Definition at line 4182 of file z3py.py.
4183 """Return the reduction-or expression of `a`."""
4185 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
4186 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 4213 of file z3py.py.
4214 """A predicate the determines that bit-vector signed division does not overflow"""
4215 _check_bv_args(a, b)
4216 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 4219 of file z3py.py.
4220 """A predicate the determines that bit-vector unary negation does not overflow"""
4222 _z3_assert(
is_bv(a),
"First argument must be a Z3 bit-vector expression")
◆ BVSubNoOverflow()
def z3py.BVSubNoOverflow |
( |
|
a, |
|
|
|
b |
|
) |
| |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4200 of file z3py.py.
4201 """A predicate the determines that bit-vector subtraction does not overflow"""
4202 _check_bv_args(a, b)
4203 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 4207 of file z3py.py.
4208 """A predicate the determines that bit-vector subtraction does not underflow"""
4209 _check_bv_args(a, b)
4210 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 3195 of file z3py.py.
3195 def Cbrt(a, ctx=None):
3196 """ Return a Z3 expression which represents the cubic root of a.
◆ Complement()
def z3py.Complement |
( |
|
re | ) |
|
Create the complement regular expression.
Definition at line 10412 of file z3py.py.
10413 """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 3836 of file z3py.py.
3837 """Create a Z3 bit-vector concatenation expression.
3839 >>> v = BitVecVal(1, 4)
3840 >>> Concat(v, v+1, v)
3841 Concat(Concat(1, 1 + 1), 1)
3842 >>> simplify(Concat(v, v+1, v))
3844 >>> print("%.3x" % simplify(Concat(v, v+1, v)).as_long())
3847 args = _get_args(args)
3850 _z3_assert(sz >= 2,
"At least two arguments expected.")
3857 if is_seq(args[0])
or isinstance(args[0], str):
3858 args = [_coerce_seq(s, ctx)
for s
in args]
3860 _z3_assert(all([
is_seq(a)
for a
in args]),
"All arguments must be sequence expressions.")
3863 v[i] = args[i].as_ast()
3868 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
3871 v[i] = args[i].as_ast()
3875 _z3_assert(all([
is_bv(a)
for a
in args]),
"All arguments must be Z3 bit-vector expressions.")
3877 for i
in range(sz - 1):
3878 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 8189 of file z3py.py.
8189 def Cond(p, t1, t2, ctx=None):
8190 """Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
8192 >>> t = Cond(Probe('is-qfnra'), Tactic('qfnra'), Tactic('smt'))
8194 p = _to_probe(p, ctx)
8195 t1 = _to_tactic(t1, ctx)
8196 t2 = _to_tactic(t2, ctx)
8197 return Tactic(
Z3_tactic_cond(t1.ctx.ref(), p.probe, t1.tactic, t2.tactic), t1.ctx)
Referenced by If().
◆ Const()
def z3py.Const |
( |
|
name, |
|
|
|
sort |
|
) |
| |
Create a constant of the given sort.
>>> Const('x', IntSort())
x
Definition at line 1321 of file z3py.py.
1321 def Const(name, sort):
1322 """Create a constant of the given sort.
1324 >>> Const('x', IntSort())
1328 _z3_assert(isinstance(sort, SortRef),
"Z3 sort expected")
Referenced by Consts().
◆ Consts()
def z3py.Consts |
( |
|
names, |
|
|
|
sort |
|
) |
| |
Create several constants of the given sort.
`names` is a string containing the names of all constants to be created.
Blank spaces separate the names of different constants.
>>> x, y, z = Consts('x y z', IntSort())
>>> x + y + z
x + y + z
Definition at line 1332 of file z3py.py.
1333 """Create several constants of the given sort.
1335 `names` is a string containing the names of all constants to be created.
1336 Blank spaces separate the names of different constants.
1338 >>> x, y, z = Consts('x y z', IntSort())
1342 if isinstance(names, str):
1343 names = names.split(
" ")
1344 return [
Const(name, sort)
for name
in names]
◆ Contains()
def z3py.Contains |
( |
|
a, |
|
|
|
b |
|
) |
| |
Check if 'a' contains 'b'
>>> s1 = Contains("abc", "ab")
>>> simplify(s1)
True
>>> s2 = Contains("abc", "bc")
>>> simplify(s2)
True
>>> x, y, z = Strings('x y z')
>>> s3 = Contains(Concat(x,y,z), y)
>>> simplify(s3)
True
Definition at line 10206 of file z3py.py.
10207 """Check if 'a' contains 'b'
10208 >>> s1 = Contains("abc", "ab")
10211 >>> s2 = Contains("abc", "bc")
10214 >>> x, y, z = Strings('x y z')
10215 >>> s3 = Contains(Concat(x,y,z), y)
10219 ctx = _get_ctx2(a, b)
10220 a = _coerce_seq(a, ctx)
10221 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 4805 of file z3py.py.
4806 """Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
4808 In the following example we define a Tree-List using two mutually recursive datatypes.
4810 >>> TreeList = Datatype('TreeList')
4811 >>> Tree = Datatype('Tree')
4812 >>> # Tree has two constructors: leaf and node
4813 >>> Tree.declare('leaf', ('val', IntSort()))
4814 >>> # a node contains a list of trees
4815 >>> Tree.declare('node', ('children', TreeList))
4816 >>> TreeList.declare('nil')
4817 >>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
4818 >>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
4819 >>> Tree.val(Tree.leaf(10))
4821 >>> simplify(Tree.val(Tree.leaf(10)))
4823 >>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
4825 node(cons(leaf(10), cons(leaf(20), nil)))
4826 >>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
4827 >>> simplify(n2 == n1)
4829 >>> simplify(TreeList.car(Tree.children(n2)) == n1)
4834 _z3_assert(len(ds) > 0,
"At least one Datatype must be specified")
4835 _z3_assert(all([isinstance(d, Datatype)
for d
in ds]),
"Arguments must be Datatypes")
4836 _z3_assert(all([d.ctx == ds[0].ctx
for d
in ds]),
"Context mismatch")
4837 _z3_assert(all([d.constructors != []
for d
in ds]),
"Non-empty Datatypes expected")
4840 names = (Symbol * num)()
4841 out = (Sort * num)()
4842 clists = (ConstructorList * num)()
4844 for i
in range(num):
4847 num_cs = len(d.constructors)
4848 cs = (Constructor * num_cs)()
4849 for j
in range(num_cs):
4850 c = d.constructors[j]
4855 fnames = (Symbol * num_fs)()
4856 sorts = (Sort * num_fs)()
4857 refs = (ctypes.c_uint * num_fs)()
4858 for k
in range(num_fs):
4862 if isinstance(ftype, Datatype):
4864 _z3_assert(ds.count(ftype) == 1,
"One and only one occurrence of each datatype is expected")
4866 refs[k] = ds.index(ftype)
4869 _z3_assert(
is_sort(ftype),
"Z3 sort expected")
4870 sorts[k] = ftype.ast
4873 to_delete.append(ScopedConstructor(cs[j], ctx))
4875 to_delete.append(ScopedConstructorList(clists[i], ctx))
4879 for i
in range(num):
4880 dref = DatatypeSortRef(out[i], ctx)
4881 num_cs = dref.num_constructors()
4882 for j
in range(num_cs):
4883 cref = dref.constructor(j)
4884 cref_name = cref.name()
4885 cref_arity = cref.arity()
4886 if cref.arity() == 0:
4888 setattr(dref, cref_name, cref)
4889 rref = dref.recognizer(j)
4890 setattr(dref,
"is_" + cref_name, rref)
4891 for k
in range(cref_arity):
4892 aref = dref.accessor(j, k)
4893 setattr(dref, aref.name(), aref)
4895 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 4460 of file z3py.py.
4461 """ Return a default value for array expression.
4462 >>> b = K(IntSort(), 1)
4463 >>> prove(Default(b) == 1)
4467 _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 8119 of file z3py.py.
8120 """Display a (tabular) description of all available probes in Z3."""
8123 print(
'<table border="1" cellpadding="2" cellspacing="0">')
8126 print(
'<tr style="background-color:#CFCFCF">')
8131 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 7928 of file z3py.py.
7929 """Display a (tabular) description of all available tactics in Z3."""
7932 print(
'<table border="1" cellpadding="2" cellspacing="0">')
7935 print(
'<tr style="background-color:#CFCFCF">')
7940 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 5005 of file z3py.py.
5006 """Create a named tagged union sort base on a set of underlying sorts
5008 >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), StringSort()])
5010 sum = Datatype(name, ctx)
5011 for i
in range(len(sorts)):
5012 sum.declare(
"inject%d" % i, (
"project%d" % i, sorts[i]))
5014 return sum, [(sum.constructor(i), sum.accessor(i, 0))
for i
in range(len(sorts))]
◆ Distinct()
def z3py.Distinct |
( |
* |
args | ) |
|
Create a Z3 distinct expression.
>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z))
Distinct(x, y, z)
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))
Definition at line 1290 of file z3py.py.
1291 """Create a Z3 distinct expression.
1298 >>> Distinct(x, y, z)
1300 >>> simplify(Distinct(x, y, z))
1302 >>> simplify(Distinct(x, y, z), blast_distinct=True)
1303 And(Not(x == y), Not(x == z), Not(y == z))
1305 args = _get_args(args)
1306 ctx = _ctx_from_ast_arg_list(args)
1308 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression")
1309 args = _coerce_expr_list(args, ctx)
1310 _args, sz = _to_ast_array(args)
◆ Empty()
Create the empty sequence of the given sort
>>> e = Empty(StringSort())
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
Empty(Seq(Int))
>>> e4 = Empty(ReSort(SeqSort(IntSort())))
>>> print(e4)
Empty(ReSort(Seq(Int)))
Definition at line 10141 of file z3py.py.
10142 """Create the empty sequence of the given sort
10143 >>> e = Empty(StringSort())
10144 >>> e2 = StringVal("")
10145 >>> print(e.eq(e2))
10147 >>> e3 = Empty(SeqSort(IntSort()))
10150 >>> e4 = Empty(ReSort(SeqSort(IntSort())))
10152 Empty(ReSort(Seq(Int)))
10154 if isinstance(s, SeqSortRef):
10156 if isinstance(s, ReSortRef):
10158 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Empty")
◆ EmptySet()
Create the empty set
>>> EmptySet(IntSort())
K(Int, False)
Definition at line 4595 of file z3py.py.
4596 """Create the empty set
4597 >>> 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 5017 of file z3py.py.
5017 def EnumSort(name, values, ctx=None):
5018 """Return a new enumeration sort named `name` containing the given values.
5020 The result is a pair (sort, list of constants).
5022 >>> Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
5025 _z3_assert(isinstance(name, str),
"Name must be a string")
5026 _z3_assert(all([isinstance(v, str)
for v
in values]),
"Eumeration sort values must be strings")
5027 _z3_assert(len(values) > 0,
"At least one value expected")
5030 _val_names = (Symbol * num)()
5031 for i
in range(num):
5033 _values = (FuncDecl * num)()
5034 _testers = (FuncDecl * num)()
5038 for i
in range(num):
5039 V.append(FuncDeclRef(_values[i], ctx))
5040 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 2082 of file z3py.py.
2082 def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2083 """Create a Z3 exists formula.
2085 The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
2088 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2091 >>> q = Exists([x, y], f(x, y) >= x, skid="foo")
2093 Exists([x, y], f(x, y) >= x)
2094 >>> is_quantifier(q)
2096 >>> r = Tactic('nnf')(q).as_expr()
2097 >>> is_quantifier(r)
2100 return _mk_quantifier(
False, vs, body, weight, qid, skid, patterns, no_patterns)
Referenced by Fixedpoint.abstract().
◆ Ext()
Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
>> Ext(a, b)
Ext(a, b)
Definition at line 4545 of file z3py.py.
4546 """Return extensionality index for one-dimensional arrays.
4547 >> a, b = Consts('a b', SetSort(IntSort()))
4554 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 3881 of file z3py.py.
3882 """Create a Z3 bit-vector extraction expression, or create a string extraction expression.
3884 >>> x = BitVec('x', 8)
3885 >>> Extract(6, 2, x)
3887 >>> Extract(6, 2, x).sort()
3889 >>> simplify(Extract(StringVal("abcd"),2,1))
3892 if isinstance(high, str):
3896 offset, length = _coerce_exprs(low, a, s.ctx)
3897 return SeqRef(
Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
3899 _z3_assert(low <= high,
"First argument must be greater than or equal to second argument")
3900 _z3_assert(_is_int(high)
and high >= 0
and _is_int(low)
and low >= 0,
"First and second arguments must be non negative integers")
3901 _z3_assert(
is_bv(a),
"Third argument must be a Z3 bit-vector expression")
3902 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 8152 of file z3py.py.
8153 """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8155 In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
8157 >>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
8158 >>> x, y = Ints('x y')
8164 >>> g.add(x == y + 1)
8166 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8168 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 7244 of file z3py.py.
7245 """Create a named finite domain sort of a given size sz"""
7246 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 7312 of file z3py.py.
7313 """Return a Z3 finite-domain value. If `ctx=None`, then the global context is used.
7315 >>> s = FiniteDomainSort('S', 256)
7316 >>> FiniteDomainVal(255, s)
7318 >>> FiniteDomainVal('100', s)
7324 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 8782 of file z3py.py.
8783 """Floating-point 128-bit (quadruple) sort."""
◆ Float16()
def z3py.Float16 |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8752 of file z3py.py.
8753 """Floating-point 16-bit (half) sort."""
◆ Float32()
def z3py.Float32 |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8762 of file z3py.py.
8763 """Floating-point 32-bit (single) sort."""
◆ Float64()
def z3py.Float64 |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8772 of file z3py.py.
8773 """Floating-point 64-bit (double) sort."""
◆ FloatDouble()
def z3py.FloatDouble |
( |
|
ctx = None | ) |
|
Floating-point 64-bit (double) sort.
Definition at line 8777 of file z3py.py.
8778 """Floating-point 64-bit (double) sort."""
◆ FloatHalf()
def z3py.FloatHalf |
( |
|
ctx = None | ) |
|
Floating-point 16-bit (half) sort.
Definition at line 8757 of file z3py.py.
8758 """Floating-point 16-bit (half) sort."""
◆ FloatQuadruple()
def z3py.FloatQuadruple |
( |
|
ctx = None | ) |
|
Floating-point 128-bit (quadruple) sort.
Definition at line 8787 of file z3py.py.
8788 """Floating-point 128-bit (quadruple) sort."""
◆ FloatSingle()
def z3py.FloatSingle |
( |
|
ctx = None | ) |
|
Floating-point 32-bit (single) sort.
Definition at line 8767 of file z3py.py.
8768 """Floating-point 32-bit (single) sort."""
◆ ForAll()
def z3py.ForAll |
( |
|
vs, |
|
|
|
body, |
|
|
|
weight = 1 , |
|
|
|
qid = "" , |
|
|
|
skid = "" , |
|
|
|
patterns = [] , |
|
|
|
no_patterns = [] |
|
) |
| |
Create a Z3 forall formula.
The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> ForAll([x, y], f(x, y) >= x)
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
ForAll([x, y], f(x, y) >= x)
>>> ForAll([x, y], f(x, y) >= x, weight=10)
ForAll([x, y], f(x, y) >= x)
Definition at line 2065 of file z3py.py.
2065 def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
2066 """Create a Z3 forall formula.
2068 The parameters `weight`, `qid`, `skid`, `patterns` and `no_patterns` are optional annotations.
2070 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2073 >>> ForAll([x, y], f(x, y) >= x)
2074 ForAll([x, y], f(x, y) >= x)
2075 >>> ForAll([x, y], f(x, y) >= x, patterns=[ f(x, y) ])
2076 ForAll([x, y], f(x, y) >= x)
2077 >>> ForAll([x, y], f(x, y) >= x, weight=10)
2078 ForAll([x, y], f(x, y) >= x)
2080 return _mk_quantifier(
True, vs, body, weight, qid, skid, patterns, no_patterns)
Referenced by Fixedpoint.abstract().
◆ FP()
def z3py.FP |
( |
|
name, |
|
|
|
fpsort, |
|
|
|
ctx = None |
|
) |
| |
Return a floating-point constant named `name`.
`fpsort` is the floating-point sort.
If `ctx=None`, then the global context is used.
>>> x = FP('x', FPSort(8, 24))
>>> is_fp(x)
True
>>> x.ebits()
8
>>> x.sort()
FPSort(8, 24)
>>> word = FPSort(8, 24)
>>> x2 = FP('x', word)
>>> eq(x, x2)
True
Definition at line 9367 of file z3py.py.
9367 def FP(name, fpsort, ctx=None):
9368 """Return a floating-point constant named `name`.
9369 `fpsort` is the floating-point sort.
9370 If `ctx=None`, then the global context is used.
9372 >>> x = FP('x', FPSort(8, 24))
9379 >>> word = FPSort(8, 24)
9380 >>> x2 = FP('x', word)
9384 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 9408 of file z3py.py.
9408 def fpAbs(a, ctx=None):
9409 """Create a Z3 floating-point absolute value expression.
9411 >>> s = FPSort(8, 24)
9413 >>> x = FPVal(1.0, s)
9416 >>> y = FPVal(-20.0, s)
9421 >>> fpAbs(-1.25*(2**4))
9427 [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 9490 of file z3py.py.
9490 def fpAdd(rm, a, b, ctx=None):
9491 """Create a Z3 floating-point addition expression.
9493 >>> s = FPSort(8, 24)
9499 >>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
9501 >>> fpAdd(rm, x, y).sort()
9504 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 9786 of file z3py.py.
9787 """Create a Z3 floating-point conversion expression that represents the
9788 conversion from a bit-vector term to a floating-point term.
9790 >>> x_bv = BitVecVal(0x3F800000, 32)
9791 >>> x_fp = fpBVToFP(x_bv, Float32())
9797 _z3_assert(
is_bv(v),
"First argument must be a Z3 bit-vector expression")
9798 _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 9534 of file z3py.py.
9534 def fpDiv(rm, a, b, ctx=None):
9535 """Create a Z3 floating-point division expression.
9537 >>> s = FPSort(8, 24)
9543 >>> fpDiv(rm, x, y).sort()
9546 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 9698 of file z3py.py.
9698 def fpEQ(a, b, ctx=None):
9699 """Create the Z3 floating-point expression `fpEQ(other, self)`.
9701 >>> x, y = FPs('x y', FPSort(8, 24))
9704 >>> fpEQ(x, y).sexpr()
9707 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 9589 of file z3py.py.
9589 def fpFMA(rm, a, b, c, ctx=None):
9590 """Create a Z3 floating-point fused multiply-add expression.
9592 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 9720 of file z3py.py.
9720 def fpFP(sgn, exp, sig, ctx=None):
9721 """Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
9723 >>> s = FPSort(8, 24)
9724 >>> x = fpFP(BitVecVal(1, 1), BitVecVal(2**7-1, 8), BitVecVal(2**22, 23))
9726 fpFP(1, 127, 4194304)
9727 >>> xv = FPVal(-1.5, s)
9731 >>> slvr.add(fpEQ(x, xv))
9734 >>> xv = FPVal(+1.5, s)
9738 >>> slvr.add(fpEQ(x, xv))
9743 _z3_assert(sgn.sort().size() == 1,
"sort mismatch")
9745 _z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx,
"context mismatch")
9746 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 9802 of file z3py.py.
9802 def fpFPToFP(rm, v, sort, ctx=None):
9803 """Create a Z3 floating-point conversion expression that represents the
9804 conversion from a floating-point term to a floating-point term of different precision.
9806 >>> x_sgl = FPVal(1.0, Float32())
9807 >>> x_dbl = fpFPToFP(RNE(), x_sgl, Float64())
9815 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9816 _z3_assert(
is_fp(v),
"Second argument must be a Z3 floating-point expression.")
9817 _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 9687 of file z3py.py.
9687 def fpGEQ(a, b, ctx=None):
9688 """Create the Z3 floating-point expression `other >= self`.
9690 >>> x, y = FPs('x y', FPSort(8, 24))
9693 >>> (x >= y).sexpr()
9696 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 9676 of file z3py.py.
9676 def fpGT(a, b, ctx=None):
9677 """Create the Z3 floating-point expression `other > self`.
9679 >>> x, y = FPs('x y', FPSort(8, 24))
9685 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 9301 of file z3py.py.
9302 """Create a Z3 floating-point +oo or -oo term."""
9303 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9304 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9305 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 9615 of file z3py.py.
9616 """Create a Z3 floating-point isInfinite expression.
9618 >>> s = FPSort(8, 24)
9623 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 9604 of file z3py.py.
9605 """Create a Z3 floating-point isNaN expression.
9607 >>> s = FPSort(8, 24)
9613 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 9640 of file z3py.py.
9641 """Create a Z3 floating-point isNegative expression.
9643 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 9630 of file z3py.py.
9631 """Create a Z3 floating-point isNormal expression.
9633 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 9645 of file z3py.py.
9646 """Create a Z3 floating-point isPositive expression.
9648 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 9635 of file z3py.py.
9636 """Create a Z3 floating-point isSubnormal expression.
9638 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 9625 of file z3py.py.
9626 """Create a Z3 floating-point isZero expression.
9628 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 9665 of file z3py.py.
9665 def fpLEQ(a, b, ctx=None):
9666 """Create the Z3 floating-point expression `other <= self`.
9668 >>> x, y = FPs('x y', FPSort(8, 24))
9671 >>> (x <= y).sexpr()
9674 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 9654 of file z3py.py.
9654 def fpLT(a, b, ctx=None):
9655 """Create the Z3 floating-point expression `other < self`.
9657 >>> x, y = FPs('x y', FPSort(8, 24))
9663 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 9575 of file z3py.py.
9575 def fpMax(a, b, ctx=None):
9576 """Create a Z3 floating-point maximum expression.
9578 >>> s = FPSort(8, 24)
9584 >>> fpMax(x, y).sort()
9587 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 9561 of file z3py.py.
9561 def fpMin(a, b, ctx=None):
9562 """Create a Z3 floating-point minimum expression.
9564 >>> s = FPSort(8, 24)
9570 >>> fpMin(x, y).sort()
9573 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 9296 of file z3py.py.
9297 """Create a Z3 floating-point -oo term."""
9298 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9299 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 9312 of file z3py.py.
9313 """Create a Z3 floating-point -0.0 term."""
9314 _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 9520 of file z3py.py.
9520 def fpMul(rm, a, b, ctx=None):
9521 """Create a Z3 floating-point multiplication expression.
9523 >>> s = FPSort(8, 24)
9529 >>> fpMul(rm, x, y).sort()
9532 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 9264 of file z3py.py.
9265 """Create a Z3 floating-point NaN term.
9267 >>> s = FPSort(8, 24)
9268 >>> set_fpa_pretty(True)
9271 >>> pb = get_fpa_pretty()
9272 >>> set_fpa_pretty(False)
9274 fpNaN(FPSort(8, 24))
9275 >>> set_fpa_pretty(pb)
9277 _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 9430 of file z3py.py.
9430 def fpNeg(a, ctx=None):
9431 """Create a Z3 floating-point addition expression.
9433 >>> s = FPSort(8, 24)
9442 [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 9709 of file z3py.py.
9709 def fpNEQ(a, b, ctx=None):
9710 """Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
9712 >>> x, y = FPs('x y', FPSort(8, 24))
9715 >>> (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 9280 of file z3py.py.
9281 """Create a Z3 floating-point +oo term.
9283 >>> s = FPSort(8, 24)
9284 >>> pb = get_fpa_pretty()
9285 >>> set_fpa_pretty(True)
9286 >>> fpPlusInfinity(s)
9288 >>> set_fpa_pretty(False)
9289 >>> fpPlusInfinity(s)
9290 fpPlusInfinity(FPSort(8, 24))
9291 >>> set_fpa_pretty(pb)
9293 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9294 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 9307 of file z3py.py.
9308 """Create a Z3 floating-point +0.0 term."""
9309 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9310 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 9821 of file z3py.py.
9822 """Create a Z3 floating-point conversion expression that represents the
9823 conversion from a real term to a floating-point term.
9825 >>> x_r = RealVal(1.5)
9826 >>> x_fp = fpRealToFP(RNE(), x_r, Float32())
9832 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9833 _z3_assert(
is_real(v),
"Second argument must be a Z3 expression or real sort.")
9834 _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 9548 of file z3py.py.
9548 def fpRem(a, b, ctx=None):
9549 """Create a Z3 floating-point remainder expression.
9551 >>> s = FPSort(8, 24)
9556 >>> fpRem(x, y).sort()
9559 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 9599 of file z3py.py.
9600 """Create a Z3 floating-point roundToIntegral expression.
9602 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 9390 of file z3py.py.
9390 def FPs(names, fpsort, ctx=None):
9391 """Return an array of floating-point constants.
9393 >>> x, y, z = FPs('x y z', FPSort(8, 24))
9400 >>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
9401 fpMul(RNE(), fpAdd(RNE(), x, y), z)
9404 if isinstance(names, str):
9405 names = names.split(
" ")
9406 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 9838 of file z3py.py.
9839 """Create a Z3 floating-point conversion expression that represents the
9840 conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
9842 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9843 >>> x_fp = fpSignedToFP(RNE(), x_signed, Float32())
9845 fpToFP(RNE(), 4294967291)
9849 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9850 _z3_assert(
is_bv(v),
"Second argument must be a Z3 bit-vector expression")
9851 _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 9206 of file z3py.py.
9206 def FPSort(ebits, sbits, ctx=None):
9207 """Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
9209 >>> Single = FPSort(8, 24)
9210 >>> Double = FPSort(11, 53)
9213 >>> x = Const('x', Single)
9214 >>> 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 9594 of file z3py.py.
9594 def fpSqrt(rm, a, ctx=None):
9595 """Create a Z3 floating-point square root expression.
9597 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 9506 of file z3py.py.
9506 def fpSub(rm, a, b, ctx=None):
9507 """Create a Z3 floating-point subtraction expression.
9509 >>> s = FPSort(8, 24)
9515 >>> fpSub(rm, x, y).sort()
9518 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 9748 of file z3py.py.
9748 def fpToFP(a1, a2=None, a3=None, ctx=None):
9749 """Create a Z3 floating-point conversion expression from other term sorts
9752 From a bit-vector term in IEEE 754-2008 format:
9753 >>> x = FPVal(1.0, Float32())
9754 >>> x_bv = fpToIEEEBV(x)
9755 >>> simplify(fpToFP(x_bv, Float32()))
9758 From a floating-point term with different precision:
9759 >>> x = FPVal(1.0, Float32())
9760 >>> x_db = fpToFP(RNE(), x, Float64())
9765 >>> x_r = RealVal(1.5)
9766 >>> simplify(fpToFP(RNE(), x_r, Float32()))
9769 From a signed bit-vector term:
9770 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9771 >>> simplify(fpToFP(RNE(), x_signed, Float32()))
9784 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 9872 of file z3py.py.
9873 """Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
9875 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9876 _z3_assert(
is_bv(x),
"Second argument must be a Z3 bit-vector expression")
9877 _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 9942 of file z3py.py.
9943 """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
9945 The size of the resulting bit-vector is automatically determined.
9947 Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
9948 knows only one NaN and it will always produce the same bit-vector representation of
9951 >>> x = FP('x', FPSort(8, 24))
9952 >>> y = fpToIEEEBV(x)
9963 _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 9923 of file z3py.py.
9924 """Create a Z3 floating-point conversion expression, from floating-point expression to real.
9926 >>> x = FP('x', FPSort(8, 24))
9930 >>> print(is_real(y))
9934 >>> print(is_real(x))
9938 _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 9881 of file z3py.py.
9881 def fpToSBV(rm, x, s, ctx=None):
9882 """Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
9884 >>> x = FP('x', FPSort(8, 24))
9885 >>> y = fpToSBV(RTZ(), x, BitVecSort(32))
9896 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9897 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9898 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9900 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 9902 of file z3py.py.
9902 def fpToUBV(rm, x, s, ctx=None):
9903 """Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
9905 >>> x = FP('x', FPSort(8, 24))
9906 >>> y = fpToUBV(RTZ(), x, BitVecSort(32))
9917 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression")
9918 _z3_assert(
is_fp(x),
"Second argument must be a Z3 floating-point expression")
9919 _z3_assert(
is_bv_sort(s),
"Third argument must be Z3 bit-vector sort")
9921 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 9855 of file z3py.py.
9856 """Create a Z3 floating-point conversion expression that represents the
9857 conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
9859 >>> x_signed = BitVecVal(-5, BitVecSort(32))
9860 >>> x_fp = fpUnsignedToFP(RNE(), x_signed, Float32())
9862 fpToFPUnsigned(RNE(), 4294967291)
9866 _z3_assert(
is_fprm(rm),
"First argument must be a Z3 floating-point rounding mode expression.")
9867 _z3_assert(
is_bv(v),
"Second argument must be a Z3 bit-vector expression")
9868 _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 9323 of file z3py.py.
9323 def FPVal(sig, exp=None, fps=None, ctx=None):
9324 """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
9326 >>> v = FPVal(20.0, FPSort(8, 24))
9329 >>> print("0x%.8x" % v.exponent_as_long(False))
9331 >>> v = FPVal(2.25, FPSort(8, 24))
9334 >>> v = FPVal(-2.25, FPSort(8, 24))
9337 >>> FPVal(-0.0, FPSort(8, 24))
9339 >>> FPVal(0.0, FPSort(8, 24))
9341 >>> FPVal(+0.0, FPSort(8, 24))
9349 fps = _dflt_fps(ctx)
9353 val = _to_float_str(sig)
9354 if val ==
"NaN" or val ==
"nan":
9358 elif val ==
"0.0" or val ==
"+0.0":
9360 elif val ==
"+oo" or val ==
"+inf" or val ==
"+Inf":
9362 elif val ==
"-oo" or val ==
"-inf" or val ==
"-Inf":
9365 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 9317 of file z3py.py.
9318 """Create a Z3 floating-point +0.0 or -0.0 term."""
9319 _z3_assert(isinstance(s, FPSortRef),
"sort mismatch")
9320 _z3_assert(isinstance(negative, bool),
"expected Boolean flag")
9321 return FPNumRef(
Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
◆ FreshBool()
def z3py.FreshBool |
( |
|
prefix = 'b' , |
|
|
|
ctx = None |
|
) |
| |
Return a fresh Boolean constant in the given context using the given prefix.
If `ctx=None`, then the global context is used.
>>> b1 = FreshBool()
>>> b2 = FreshBool()
>>> eq(b1, b2)
False
Definition at line 1628 of file z3py.py.
1629 """Return a fresh Boolean constant in the given context using the given prefix.
1631 If `ctx=None`, then the global context is used.
1633 >>> b1 = FreshBool()
1634 >>> b2 = FreshBool()
◆ FreshConst()
def z3py.FreshConst |
( |
|
sort, |
|
|
|
prefix = 'c' |
|
) |
| |
Create a fresh constant of a specified sort
Definition at line 1346 of file z3py.py.
1347 """Create a fresh constant of a specified sort"""
1348 ctx = _get_ctx(sort.ctx)
◆ FreshFunction()
def z3py.FreshFunction |
( |
* |
sig | ) |
|
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 821 of file z3py.py.
822 """Create a new fresh Z3 uninterpreted function with the given sorts.
826 _z3_assert(len(sig) > 0,
"At least two arguments expected")
830 _z3_assert(
is_sort(rng),
"Z3 sort expected")
831 dom = (z3.Sort * arity)()
832 for i
in range(arity):
834 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
◆ FreshInt()
def z3py.FreshInt |
( |
|
prefix = 'x' , |
|
|
|
ctx = None |
|
) |
| |
Return a fresh integer constant in the given context using the given prefix.
>>> x = FreshInt()
>>> y = FreshInt()
>>> eq(x, y)
False
>>> x.sort()
Int
Definition at line 3067 of file z3py.py.
3067 def FreshInt(prefix='x', ctx=None):
3068 """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 3120 of file z3py.py.
3121 """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 10160 of file z3py.py.
10161 """Create the regular expression that accepts the universal language
10162 >>> e = Full(ReSort(SeqSort(IntSort())))
10164 Full(ReSort(Seq(Int)))
10165 >>> e1 = Full(ReSort(StringSort()))
10167 Full(ReSort(String))
10169 if isinstance(s, ReSortRef):
10171 raise Z3Exception(
"Non-sequence, non-regular expression sort passed to Full")
◆ FullSet()
Create the full set
>>> FullSet(IntSort())
K(Int, True)
Definition at line 4603 of file z3py.py.
4604 """Create the full set
4605 >>> 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 6267 of file z3py.py.
6268 """Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
6270 _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 8649 of file z3py.py.
8650 """Retrieves the global default rounding mode."""
8651 global _dflt_rounding_mode
8652 if _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO:
8654 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE:
8656 elif _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE:
8658 elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN:
8660 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 4377 of file z3py.py.
4378 """Return the function declaration associated with a Z3 map array expression.
4380 >>> f = Function('f', IntSort(), IntSort())
4381 >>> b = Array('b', IntSort(), IntSort())
4383 >>> eq(f, get_map_func(a))
4387 >>> get_map_func(a)(0)
4391 _z3_assert(
is_map(a),
"Z3 array map expression expected.")
◆ get_param()
def z3py.get_param |
( |
|
name | ) |
|
Return the value of a Z3 global (or module) parameter
>>> get_param('nlsat.reorder')
'true'
Definition at line 273 of file z3py.py.
274 """Return the value of a Z3 global (or module) parameter
276 >>> get_param('nlsat.reorder')
279 ptr = (ctypes.c_char_p * 1)()
281 r = z3core._to_pystr(ptr[0])
283 raise Z3Exception(
"failed to retrieve value for '%s'" % name)
◆ get_var_index()
def z3py.get_var_index |
( |
|
a | ) |
|
Return the de-Bruijn index of the Z3 bounded variable `a`.
>>> x = Int('x')
>>> y = Int('y')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> # Z3 replaces x and y with bound variables when ForAll is executed.
>>> q = ForAll([x, y], f(x, y) == x + y)
>>> q.body()
f(Var(1), Var(0)) == Var(1) + Var(0)
>>> b = q.body()
>>> b.arg(0)
f(Var(1), Var(0))
>>> v1 = b.arg(0).arg(0)
>>> v2 = b.arg(0).arg(1)
>>> v1
Var(1)
>>> v2
Var(0)
>>> get_var_index(v1)
1
>>> get_var_index(v2)
0
Definition at line 1224 of file z3py.py.
1225 """Return the de-Bruijn index of the Z3 bounded variable `a`.
1233 >>> f = Function('f', IntSort(), IntSort(), IntSort())
1234 >>> # Z3 replaces x and y with bound variables when ForAll is executed.
1235 >>> q = ForAll([x, y], f(x, y) == x + y)
1237 f(Var(1), Var(0)) == Var(1) + Var(0)
1241 >>> v1 = b.arg(0).arg(0)
1242 >>> v2 = b.arg(0).arg(1)
1247 >>> get_var_index(v1)
1249 >>> get_var_index(v2)
1253 _z3_assert(
is_var(a),
"Z3 bound variable expected")
◆ get_version()
Definition at line 81 of file z3py.py.
82 major = ctypes.c_uint(0)
83 minor = ctypes.c_uint(0)
84 build = ctypes.c_uint(0)
85 rev = ctypes.c_uint(0)
87 return (major.value, minor.value, build.value, rev.value)
◆ get_version_string()
def z3py.get_version_string |
( |
| ) |
|
Definition at line 73 of file z3py.py.
74 major = ctypes.c_uint(0)
75 minor = ctypes.c_uint(0)
76 build = ctypes.c_uint(0)
77 rev = ctypes.c_uint(0)
79 return "%s.%s.%s" % (major.value, minor.value, build.value)
◆ help_simplify()
def z3py.help_simplify |
( |
| ) |
|
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 8229 of file z3py.py.
8230 """Return a string describing all options available for Z3 `simplify` procedure."""
◆ If()
def z3py.If |
( |
|
a, |
|
|
|
b, |
|
|
|
c, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 if-then-else expression.
>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> simplify(max)
If(x <= y, y, x)
Definition at line 1268 of file z3py.py.
1268 def If(a, b, c, ctx=None):
1269 """Create a Z3 if-then-else expression.
1273 >>> max = If(x > y, x, y)
1279 if isinstance(a, Probe)
or isinstance(b, Tactic)
or isinstance(c, Tactic):
1280 return Cond(a, b, c, ctx)
1282 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b, c], ctx))
1285 b, c = _coerce_exprs(b, c, ctx)
1287 _z3_assert(a.ctx == b.ctx,
"Context mismatch")
1288 return _to_expr_ref(
Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
Referenced by BoolRef.__mul__(), and ArithRef.__mul__().
◆ Implies()
def z3py.Implies |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 implies expression.
>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
Definition at line 1641 of file z3py.py.
1642 """Create a Z3 implies expression.
1644 >>> p, q = Bools('p q')
1648 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1652 return BoolRef(
Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
Referenced by Fixedpoint.add_rule(), and Fixedpoint.update_rule().
◆ IndexOf() [1/2]
def z3py.IndexOf |
( |
|
s, |
|
|
|
substr |
|
) |
| |
◆ IndexOf() [2/2]
def z3py.IndexOf |
( |
|
s, |
|
|
|
substr, |
|
|
|
offset |
|
) |
| |
Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4
Definition at line 10242 of file z3py.py.
10242 def IndexOf(s, substr, offset):
10243 """Retrieve the index of substring within a string starting at a specified offset.
10244 >>> simplify(IndexOf("abcabc", "bc", 0))
10246 >>> simplify(IndexOf("abcabc", "bc", 2))
10252 ctx = _get_ctx2(s, substr, ctx)
10253 s = _coerce_seq(s, ctx)
10254 substr = _coerce_seq(substr, ctx)
10255 if _is_int(offset):
10256 offset =
IntVal(offset, ctx)
10257 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 10339 of file z3py.py.
10340 """Create regular expression membership test
10341 >>> re = Union(Re("a"),Re("b"))
10342 >>> print (simplify(InRe("a", re)))
10344 >>> print (simplify(InRe("b", re)))
10346 >>> print (simplify(InRe("c", re)))
10349 s = _coerce_seq(s, re.ctx)
10350 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 3031 of file z3py.py.
3031 def Int(name, ctx=None):
3032 """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 3755 of file z3py.py.
3756 """Return the z3 expression Int2BV(a, num_bits).
3757 It is a bit-vector of width num_bits and represents the
3758 modulo of a by 2^num_bits
3761 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 10371 of file z3py.py.
10372 """Create intersection of regular expressions.
10373 >>> re = Intersect(Re("a"), Re("b"), Re("c"))
10375 args = _get_args(args)
10378 _z3_assert(sz > 0,
"At least one argument expected.")
10379 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10384 for i
in range(sz):
10385 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 3043 of file z3py.py.
3043 def Ints(names, ctx=None):
3044 """Return a tuple of Integer constants.
3046 >>> x, y, z = Ints('x y z')
3051 if isinstance(names, str):
3052 names = names.split(
" ")
3053 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 2928 of file z3py.py.
2929 """Return the integer sort in the given context. If `ctx=None`, then the global context is used.
2933 >>> x = Const('x', IntSort())
2936 >>> x.sort() == IntSort()
2938 >>> x.sort() == BoolSort()
Referenced by FreshInt(), Context.getIntSort(), Int(), IntVal(), and Context.mkIntSort().
◆ IntToStr()
Convert integer expression to string
Definition at line 10293 of file z3py.py.
10294 """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 3055 of file z3py.py.
3056 """Return a list of integer constants of size `sz`.
3058 >>> X = IntVector('x', 3)
3065 return [
Int(
'%s__%s' % (prefix, i), ctx)
for i
in range(sz) ]
◆ is_add()
Return `True` if `a` is an expression of the form b + c.
>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False
Definition at line 2617 of file z3py.py.
2618 """Return `True` if `a` is an expression of the form b + c.
2620 >>> x, y = Ints('x y')
◆ is_algebraic_value()
def z3py.is_algebraic_value |
( |
|
a | ) |
|
Return `True` if `a` is an algebraic value of sort Real.
>>> is_algebraic_value(RealVal("3/5"))
False
>>> n = simplify(Sqrt(2))
>>> n
1.4142135623?
>>> is_algebraic_value(n)
True
Definition at line 2604 of file z3py.py.
2605 """Return `True` if `a` is an algebraic value of sort Real.
2607 >>> is_algebraic_value(RealVal("3/5"))
2609 >>> n = simplify(Sqrt(2))
2612 >>> is_algebraic_value(n)
2615 return is_arith(a)
and a.is_real()
and _is_algebraic(a.ctx, a.as_ast())
◆ is_and()
Return `True` if `a` is a Z3 and expression.
>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False
Definition at line 1489 of file z3py.py.
1490 """Return `True` if `a` is a Z3 and expression.
1492 >>> p, q = Bools('p q')
1493 >>> is_and(And(p, q))
1495 >>> is_and(Or(p, q))
◆ is_app()
Return `True` if `a` is a Z3 function application.
Note that, constants are function applications with 0 arguments.
>>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')
>>> is_app(ForAll(x, x >= 0))
False
Definition at line 1157 of file z3py.py.
1158 """Return `True` if `a` is a Z3 function application.
1160 Note that, constants are function applications with 0 arguments.
1167 >>> is_app(IntSort())
1171 >>> is_app(IntVal(1))
1174 >>> is_app(ForAll(x, x >= 0))
1177 if not isinstance(a, ExprRef):
1179 k = _ast_kind(a.ctx, a)
1180 return k == Z3_NUMERAL_AST
or k == Z3_APP_AST
Referenced by ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), is_quantifier(), Lambda(), ExprRef.num_args(), and RecAddDefinition().
◆ is_app_of()
def z3py.is_app_of |
( |
|
a, |
|
|
|
k |
|
) |
| |
Return `True` if `a` is an application of the given kind `k`.
>>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Z3_OP_ADD)
True
>>> is_app_of(n, Z3_OP_MUL)
False
Definition at line 1256 of file z3py.py.
1257 """Return `True` if `a` is an application of the given kind `k`.
1261 >>> is_app_of(n, Z3_OP_ADD)
1263 >>> is_app_of(n, Z3_OP_MUL)
1266 return is_app(a)
and a.decl().kind() == k
Referenced by is_add(), is_and(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
◆ is_arith()
Return `True` if `a` is an arithmetical expression.
>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True
Definition at line 2498 of file z3py.py.
2499 """Return `True` if `a` is an arithmetical expression.
2508 >>> is_arith(IntVal(1))
2516 return isinstance(a, ArithRef)
Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().
◆ is_arith_sort()
def z3py.is_arith_sort |
( |
|
s | ) |
|
Return `True` if s is an arithmetical sort (type).
>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True
Definition at line 2199 of file z3py.py.
2200 """Return `True` if s is an arithmetical sort (type).
2202 >>> is_arith_sort(IntSort())
2204 >>> is_arith_sort(RealSort())
2206 >>> is_arith_sort(BoolSort())
2208 >>> n = Int('x') + 1
2209 >>> is_arith_sort(n.sort())
2212 return isinstance(s, ArithSortRef)
Referenced by ArithSortRef.subsort().
◆ is_array()
Return `True` if `a` is a Z3 array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False
Definition at line 4317 of file z3py.py.
4318 """Return `True` if `a` is a Z3 array expression.
4320 >>> a = Array('a', IntSort(), IntSort())
4323 >>> is_array(Store(a, 0, 1))
4328 return isinstance(a, ArrayRef)
Referenced by Ext(), and Map().
◆ is_array_sort()
def z3py.is_array_sort |
( |
|
a | ) |
|
◆ is_as_array()
def z3py.is_as_array |
( |
|
n | ) |
|
◆ is_ast()
Return `True` if `a` is an AST node.
>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False
Definition at line 412 of file z3py.py.
413 """Return `True` if `a` is an AST node.
417 >>> is_ast(IntVal(10))
421 >>> is_ast(BoolSort())
423 >>> is_ast(Function('f', IntSort(), IntSort()))
430 return isinstance(a, AstRef)
Referenced by eq(), AstRef.eq(), and ReSort().
◆ is_bool()
Return `True` if `a` is a Z3 Boolean expression.
>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True
Definition at line 1442 of file z3py.py.
1443 """Return `True` if `a` is a Z3 Boolean expression.
1449 >>> is_bool(And(p, q))
1457 return isinstance(a, BoolRef)
Referenced by is_quantifier(), and prove().
◆ is_bv()
Return `True` if `a` is a Z3 bit-vector expression.
>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False
Definition at line 3706 of file z3py.py.
3707 """Return `True` if `a` is a Z3 bit-vector expression.
3709 >>> b = BitVec('b', 32)
3717 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 3245 of file z3py.py.
3246 """Return True if `s` is a Z3 bit-vector sort.
3248 >>> is_bv_sort(BitVecSort(32))
3250 >>> is_bv_sort(IntSort())
3253 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 3719 of file z3py.py.
3720 """Return `True` if `a` is a Z3 bit-vector numeral value.
3722 >>> b = BitVec('b', 32)
3725 >>> b = BitVecVal(10, 32)
3731 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 4330 of file z3py.py.
4331 """Return `True` if `a` is a Z3 constant array.
4333 >>> a = K(IntSort(), 10)
4334 >>> is_const_array(a)
4336 >>> a = Array('a', IntSort(), IntSort())
4337 >>> 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 4369 of file z3py.py.
4370 """Return `True` if `a` is a Z3 default array expression.
4371 >>> d = Default(K(IntSort(), 10))
4375 return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
◆ is_distinct()
def z3py.is_distinct |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 distinct expression.
>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True
Definition at line 1542 of file z3py.py.
1543 """Return `True` if `a` is a Z3 distinct expression.
1545 >>> x, y, z = Ints('x y z')
1546 >>> is_distinct(x == y)
1548 >>> is_distinct(Distinct(x, y, z))
◆ is_div()
Return `True` if `a` is an expression of the form b / c.
>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True
Definition at line 2650 of file z3py.py.
2651 """Return `True` if `a` is an expression of the form b / c.
2653 >>> x, y = Reals('x y')
2658 >>> x, y = Ints('x y')
◆ is_eq()
Return `True` if `a` is a Z3 equality expression.
>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
Definition at line 1533 of file z3py.py.
1534 """Return `True` if `a` is a Z3 equality expression.
1536 >>> x, y = Ints('x y')
Referenced by AstRef.__bool__().
◆ is_expr()
Return `True` if `a` is a Z3 expression.
>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True
>>> is_expr(FPVal(1.0))
True
Definition at line 1135 of file z3py.py.
1136 """Return `True` if `a` is a Z3 expression.
1143 >>> is_expr(IntSort())
1147 >>> is_expr(IntVal(1))
1150 >>> is_expr(ForAll(x, x >= 0))
1152 >>> is_expr(FPVal(1.0))
1155 return isinstance(a, ExprRef)
Referenced by SeqRef.__gt__(), 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 1476 of file z3py.py.
1477 """Return `True` if `a` is the Z3 false expression.
1484 >>> is_false(BoolVal(False))
Referenced by AstRef.__bool__().
◆ is_finite_domain()
def z3py.is_finite_domain |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 finite-domain expression.
>>> s = FiniteDomainSort('S', 100)
>>> b = Const('b', s)
>>> is_finite_domain(b)
True
>>> is_finite_domain(Int('x'))
False
Definition at line 7273 of file z3py.py.
7274 """Return `True` if `a` is a Z3 finite-domain expression.
7276 >>> s = FiniteDomainSort('S', 100)
7277 >>> b = Const('b', s)
7278 >>> is_finite_domain(b)
7280 >>> is_finite_domain(Int('x'))
7283 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 7251 of file z3py.py.
7252 """Return True if `s` is a Z3 finite-domain sort.
7254 >>> is_finite_domain_sort(FiniteDomainSort('S', 100))
7256 >>> is_finite_domain_sort(IntSort())
7259 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 7326 of file z3py.py.
7327 """Return `True` if `a` is a Z3 finite-domain value.
7329 >>> s = FiniteDomainSort('S', 100)
7330 >>> b = Const('b', s)
7331 >>> is_finite_domain_value(b)
7333 >>> b = FiniteDomainVal(10, s)
7336 >>> 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 9179 of file z3py.py.
9180 """Return `True` if `a` is a Z3 floating-point expression.
9182 >>> b = FP('b', FPSort(8, 24))
9190 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 8796 of file z3py.py.
8797 """Return True if `s` is a Z3 floating-point sort.
8799 >>> is_fp_sort(FPSort(8, 24))
8801 >>> is_fp_sort(IntSort())
8804 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 9192 of file z3py.py.
9193 """Return `True` if `a` is a Z3 floating-point numeral value.
9195 >>> b = FP('b', FPSort(8, 24))
9198 >>> b = FPVal(1.0, FPSort(8, 24))
9204 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 9043 of file z3py.py.
9044 """Return `True` if `a` is a Z3 floating-point rounding mode expression.
9053 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 8806 of file z3py.py.
8807 """Return True if `s` is a Z3 floating-point rounding mode sort.
8809 >>> is_fprm_sort(FPSort(8, 24))
8811 >>> is_fprm_sort(RNE().sort())
8814 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 9055 of file z3py.py.
9056 """Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
9057 return is_fprm(a)
and _is_numeral(a.ctx, a.ast)
Referenced by set_default_rounding_mode().
◆ is_func_decl()
def z3py.is_func_decl |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 function declaration.
>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False
Definition at line 787 of file z3py.py.
788 """Return `True` if `a` is a Z3 function declaration.
790 >>> f = Function('f', IntSort(), IntSort())
797 return isinstance(a, FuncDeclRef)
Referenced by Map(), and prove().
◆ is_ge()
Return `True` if `a` is an expression of the form b >= c.
>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False
Definition at line 2710 of file z3py.py.
2711 """Return `True` if `a` is an expression of the form b >= c.
2713 >>> x, y = Ints('x y')
◆ is_gt()
Return `True` if `a` is an expression of the form b > c.
>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False
Definition at line 2721 of file z3py.py.
2722 """Return `True` if `a` is an expression of the form b > c.
2724 >>> x, y = Ints('x y')
◆ is_idiv()
Return `True` if `a` is an expression of the form b div c.
>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False
Definition at line 2666 of file z3py.py.
2667 """Return `True` if `a` is an expression of the form b div c.
2669 >>> x, y = Ints('x y')
◆ is_implies()
Return `True` if `a` is a Z3 implication expression.
>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False
Definition at line 1511 of file z3py.py.
1512 """Return `True` if `a` is a Z3 implication expression.
1514 >>> p, q = Bools('p q')
1515 >>> is_implies(Implies(p, q))
1517 >>> is_implies(And(p, q))
◆ is_int()
Return `True` if `a` is an integer expression.
>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False
Definition at line 2518 of file z3py.py.
2519 """Return `True` if `a` is an integer expression.
2526 >>> is_int(IntVal(1))
◆ is_int_value()
def z3py.is_int_value |
( |
|
a | ) |
|
Return `True` if `a` is an integer value of sort Int.
>>> is_int_value(IntVal(1))
True
>>> is_int_value(1)
False
>>> is_int_value(Int('x'))
False
>>> n = Int('x') + 1
>>> n
x + 1
>>> n.arg(1)
1
>>> is_int_value(n.arg(1))
True
>>> is_int_value(RealVal("1/3"))
False
>>> is_int_value(RealVal(1))
False
Definition at line 2560 of file z3py.py.
2561 """Return `True` if `a` is an integer value of sort Int.
2563 >>> is_int_value(IntVal(1))
2567 >>> is_int_value(Int('x'))
2569 >>> n = Int('x') + 1
2574 >>> is_int_value(n.arg(1))
2576 >>> is_int_value(RealVal("1/3"))
2578 >>> is_int_value(RealVal(1))
2581 return is_arith(a)
and a.is_int()
and _is_numeral(a.ctx, a.as_ast())
◆ is_is_int()
Return `True` if `a` is an expression of the form IsInt(b).
>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False
Definition at line 2732 of file z3py.py.
2733 """Return `True` if `a` is an expression of the form IsInt(b).
2736 >>> is_is_int(IsInt(x))
◆ is_K()
Return `True` if `a` is a Z3 constant array.
>>> a = K(IntSort(), 10)
>>> is_K(a)
True
>>> a = Array('a', IntSort(), IntSort())
>>> is_K(a)
False
Definition at line 4342 of file z3py.py.
4343 """Return `True` if `a` is a Z3 constant array.
4345 >>> a = K(IntSort(), 10)
4348 >>> a = Array('a', IntSort(), IntSort())
◆ is_le()
Return `True` if `a` is an expression of the form b <= c.
>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False
Definition at line 2688 of file z3py.py.
2689 """Return `True` if `a` is an expression of the form b <= c.
2691 >>> x, y = Ints('x y')
◆ is_lt()
Return `True` if `a` is an expression of the form b < c.
>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False
Definition at line 2699 of file z3py.py.
2700 """Return `True` if `a` is an expression of the form b < c.
2702 >>> x, y = Ints('x y')
◆ is_map()
Return `True` if `a` is a Z3 map array expression.
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False
Definition at line 4354 of file z3py.py.
4355 """Return `True` if `a` is a Z3 map array expression.
4357 >>> f = Function('f', IntSort(), IntSort())
4358 >>> b = Array('b', IntSort(), IntSort())
Referenced by get_map_func().
◆ is_mod()
Return `True` if `a` is an expression of the form b % c.
>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False
Definition at line 2677 of file z3py.py.
2678 """Return `True` if `a` is an expression of the form b % c.
2680 >>> x, y = Ints('x y')
◆ is_mul()
Return `True` if `a` is an expression of the form b * c.
>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False
Definition at line 2628 of file z3py.py.
2629 """Return `True` if `a` is an expression of the form b * c.
2631 >>> x, y = Ints('x y')
◆ is_not()
Return `True` if `a` is a Z3 not expression.
>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True
Definition at line 1522 of file z3py.py.
1523 """Return `True` if `a` is a Z3 not expression.
Referenced by mk_not().
◆ is_or()
Return `True` if `a` is a Z3 or expression.
>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False
Definition at line 1500 of file z3py.py.
1501 """Return `True` if `a` is a Z3 or expression.
1503 >>> p, q = Bools('p q')
1506 >>> is_or(And(p, q))
◆ is_pattern()
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
>>> q
ForAll(x, f(x) == 0)
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
f(Var(0))
Definition at line 1780 of file z3py.py.
1781 """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
1783 >>> f = Function('f', IntSort(), IntSort())
1785 >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
1787 ForAll(x, f(x) == 0)
1788 >>> q.num_patterns()
1790 >>> is_pattern(q.pattern(0))
1795 return isinstance(a, PatternRef)
Referenced by is_quantifier(), and MultiPattern().
◆ is_probe()
Return `True` if `p` is a Z3 probe.
>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True
Definition at line 8085 of file z3py.py.
8086 """Return `True` if `p` is a Z3 probe.
8088 >>> is_probe(Int('x'))
8090 >>> is_probe(Probe('memory'))
8093 return isinstance(p, Probe)
Referenced by eq(), mk_not(), and Not().
◆ is_quantifier()
def z3py.is_quantifier |
( |
|
a | ) |
|
Return `True` if `a` is a Z3 quantifier.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(f(x))
False
Definition at line 2018 of file z3py.py.
2019 """Return `True` if `a` is a Z3 quantifier.
2021 >>> f = Function('f', IntSort(), IntSort())
2023 >>> q = ForAll(x, f(x) == 0)
2024 >>> is_quantifier(q)
2026 >>> is_quantifier(f(x))
2029 return isinstance(a, QuantifierRef)
◆ is_rational_value()
def z3py.is_rational_value |
( |
|
a | ) |
|
Return `True` if `a` is rational value of sort Real.
>>> is_rational_value(RealVal(1))
True
>>> is_rational_value(RealVal("3/5"))
True
>>> is_rational_value(IntVal(1))
False
>>> is_rational_value(1)
False
>>> n = Real('x') + 1
>>> n.arg(1)
1
>>> is_rational_value(n.arg(1))
True
>>> is_rational_value(Real('x'))
False
Definition at line 2583 of file z3py.py.
2584 """Return `True` if `a` is rational value of sort Real.
2586 >>> is_rational_value(RealVal(1))
2588 >>> is_rational_value(RealVal("3/5"))
2590 >>> is_rational_value(IntVal(1))
2592 >>> is_rational_value(1)
2594 >>> n = Real('x') + 1
2597 >>> is_rational_value(n.arg(1))
2599 >>> is_rational_value(Real('x'))
2602 return is_arith(a)
and a.is_real()
and _is_numeral(a.ctx, a.as_ast())
◆ is_re()
◆ is_real()
Return `True` if `a` is a real expression.
>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True
Definition at line 2536 of file z3py.py.
2537 """Return `True` if `a` is a real expression.
2549 >>> is_real(RealVal(1))
Referenced by fpRealToFP(), and fpToFP().
◆ is_select()
Return `True` if `a` is a Z3 array select application.
>>> a = Array('a', IntSort(), IntSort())
>>> is_select(a)
False
>>> i = Int('i')
>>> is_select(a[i])
True
Definition at line 4561 of file z3py.py.
4562 """Return `True` if `a` is a Z3 array select application.
4564 >>> 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 10080 of file z3py.py.
10081 """Return `True` if `a` is a Z3 sequence expression.
10082 >>> print (is_seq(Unit(IntVal(0))))
10084 >>> print (is_seq(StringVal("abc")))
10087 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 4573 of file z3py.py.
4574 """Return `True` if `a` is a Z3 array store application.
4576 >>> a = Array('a', IntSort(), IntSort())
4579 >>> 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 10089 of file z3py.py.
10090 """Return `True` if `a` is a Z3 string expression.
10091 >>> print (is_string(StringVal("ab")))
10094 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 10096 of file z3py.py.
10097 """return 'True' if 'a' is a Z3 string constant expression.
10098 >>> print (is_string_value(StringVal("a")))
10100 >>> print (is_string_value(StringVal("a") + StringVal("b")))
10103 return isinstance(a, SeqRef)
and a.is_string_value()
◆ is_sub()
Return `True` if `a` is an expression of the form b - c.
>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False
Definition at line 2639 of file z3py.py.
2640 """Return `True` if `a` is an expression of the form b - c.
2642 >>> x, y = Ints('x y')
◆ is_to_int()
Return `True` if `a` is an expression of the form ToInt(b).
>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False
Definition at line 2757 of file z3py.py.
2758 """Return `True` if `a` is an expression of the form ToInt(b).
◆ is_to_real()
Return `True` if `a` is an expression of the form ToReal(b).
>>> x = Int('x')
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> is_to_real(n)
True
>>> is_to_real(x)
False
Definition at line 2743 of file z3py.py.
2744 """Return `True` if `a` is an expression of the form ToReal(b).
◆ is_true()
Return `True` if `a` is the Z3 true expression.
>>> p = Bool('p')
>>> is_true(p)
False
>>> is_true(simplify(p == p))
True
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False
Definition at line 1459 of file z3py.py.
1460 """Return `True` if `a` is the Z3 true expression.
1465 >>> is_true(simplify(p == p))
1470 >>> # True is a Python Boolean expression
Referenced by AstRef.__bool__().
◆ is_var()
Return `True` if `a` is variable.
Z3 uses de-Bruijn indices for representing bound variables in
quantifiers.
>>> x = Int('x')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort())
>>> # Z3 replaces x with bound variables when ForAll is executed.
>>> q = ForAll(x, f(x) == x)
>>> b = q.body()
>>> b
f(Var(0)) == Var(0)
>>> b.arg(1)
Var(0)
>>> is_var(b.arg(1))
True
Definition at line 1200 of file z3py.py.
1201 """Return `True` if `a` is variable.
1203 Z3 uses de-Bruijn indices for representing bound variables in
1211 >>> f = Function('f', IntSort(), IntSort())
1212 >>> # Z3 replaces x with bound variables when ForAll is executed.
1213 >>> q = ForAll(x, f(x) == x)
1219 >>> is_var(b.arg(1))
1222 return is_expr(a)
and _ast_kind(a.ctx, a) == Z3_VAR_AST
Referenced by get_var_index().
◆ IsInt()
Return the Z3 predicate IsInt(a).
>>> x = Real('x')
>>> IsInt(x + "1/2")
IsInt(x + 1/2)
>>> solve(IsInt(x + "1/2"), x > 0, x < 1)
[x = 1/2]
>>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
no solution
Definition at line 3167 of file z3py.py.
3168 """ Return the Z3 predicate IsInt(a).
3171 >>> IsInt(x + "1/2")
3173 >>> solve(IsInt(x + "1/2"), x > 0, x < 1)
3175 >>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
3179 _z3_assert(a.is_real(),
"Z3 real expression expected.")
3181 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 4674 of file z3py.py.
4675 """ Check if e is a member of set s
4676 >>> a = Const('a', SetSort(IntSort()))
4680 ctx = _ctx_from_ast_arg_list([s,e])
4681 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 4684 of file z3py.py.
4685 """ Check if a is a subset of b
4686 >>> a = Const('a', SetSort(IntSort()))
4687 >>> b = Const('b', SetSort(IntSort()))
4691 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 4524 of file z3py.py.
4525 """Return a Z3 constant array expression.
4527 >>> a = K(IntSort(), 10)
4539 _z3_assert(
is_sort(dom),
"Z3 sort expected")
4542 v = _py2expr(v, ctx)
◆ Lambda()
def z3py.Lambda |
( |
|
vs, |
|
|
|
body |
|
) |
| |
Create a Z3 lambda expression.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> mem0 = Array('mem0', IntSort(), IntSort())
>>> lo, hi, e, i = Ints('lo hi e i')
>>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
>>> mem1
Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
Definition at line 2102 of file z3py.py.
2103 """Create a Z3 lambda expression.
2105 >>> f = Function('f', IntSort(), IntSort(), IntSort())
2106 >>> mem0 = Array('mem0', IntSort(), IntSort())
2107 >>> lo, hi, e, i = Ints('lo hi e i')
2108 >>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
2110 Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))
2116 _vs = (Ast * num_vars)()
2117 for i
in range(num_vars):
2119 _vs[i] = vs[i].as_ast()
2120 return QuantifierRef(
Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
◆ LastIndexOf()
def z3py.LastIndexOf |
( |
|
s, |
|
|
|
substr |
|
) |
| |
Retrieve the last index of substring within a string
Definition at line 10259 of file z3py.py.
10260 """Retrieve the last index of substring within a string"""
10262 ctx = _get_ctx2(s, substr, ctx)
10263 s = _coerce_seq(s, ctx)
10264 substr = _coerce_seq(substr, ctx)
◆ Length()
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
Definition at line 10268 of file z3py.py.
10269 """Obtain the length of a sequence 's'
10270 >>> 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 10428 of file z3py.py.
10428 def Loop(re, lo, hi=0):
10429 """Create the regular expression accepting between a lower and upper bound repetitions
10430 >>> re = Loop(Re("a"), 1, 3)
10431 >>> print(simplify(InRe("aa", re)))
10433 >>> print(simplify(InRe("aaaa", re)))
10435 >>> print(simplify(InRe("", re)))
10438 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 4036 of file z3py.py.
4037 """Create the Z3 expression logical right shift.
4039 Use the operator >> for the arithmetical right shift.
4041 >>> x, y = BitVecs('x y', 32)
4044 >>> (x >> y).sexpr()
4046 >>> LShR(x, y).sexpr()
4050 >>> BitVecVal(4, 3).as_signed_long()
4052 >>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
4054 >>> simplify(BitVecVal(4, 3) >> 1)
4056 >>> simplify(LShR(BitVecVal(4, 3), 1))
4058 >>> simplify(BitVecVal(2, 3) >> 1)
4060 >>> simplify(LShR(BitVecVal(2, 3), 1))
4063 _check_bv_args(a, b)
4064 a, b = _coerce_exprs(a, b)
4065 return BitVecRef(
Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
◆ main_ctx()
Return a reference to the global Z3 context.
>>> x = Real('x')
>>> x.ctx == main_ctx()
True
>>> c = Context()
>>> c == main_ctx()
False
>>> x2 = Real('x', c)
>>> x2.ctx == c
True
>>> eq(x, x2)
False
Definition at line 211 of file z3py.py.
212 """Return a reference to the global Z3 context.
215 >>> x.ctx == main_ctx()
220 >>> x2 = Real('x', c)
227 if _main_ctx
is None:
228 _main_ctx = Context()
Referenced by SeqRef.__gt__(), help_simplify(), and simplify_param_descrs().
◆ Map()
def z3py.Map |
( |
|
f, |
|
|
* |
args |
|
) |
| |
Return a Z3 map array expression.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> a1 = Array('a1', IntSort(), IntSort())
>>> a2 = Array('a2', IntSort(), IntSort())
>>> b = Map(f, a1, a2)
>>> b
Map(f, a1, a2)
>>> prove(b[0] == f(a1[0], a2[0]))
proved
Definition at line 4502 of file z3py.py.
4503 """Return a Z3 map array expression.
4505 >>> f = Function('f', IntSort(), IntSort(), IntSort())
4506 >>> a1 = Array('a1', IntSort(), IntSort())
4507 >>> a2 = Array('a2', IntSort(), IntSort())
4508 >>> b = Map(f, a1, a2)
4511 >>> prove(b[0] == f(a1[0], a2[0]))
4514 args = _get_args(args)
4516 _z3_assert(len(args) > 0,
"At least one Z3 array expression expected")
4517 _z3_assert(
is_func_decl(f),
"First argument must be a Z3 function declaration")
4518 _z3_assert(all([
is_array(a)
for a
in args]),
"Z3 array expected expected")
4519 _z3_assert(len(args) == f.arity(),
"Number of arguments mismatch")
4520 _args, sz = _to_ast_array(args)
4522 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 1797 of file z3py.py.
1798 """Create a Z3 multi-pattern using the given expressions `*args`
1800 >>> f = Function('f', IntSort(), IntSort())
1801 >>> g = Function('g', IntSort(), IntSort())
1803 >>> q = ForAll(x, f(x) != g(x), patterns = [ MultiPattern(f(x), g(x)) ])
1805 ForAll(x, f(x) != g(x))
1806 >>> q.num_patterns()
1808 >>> is_pattern(q.pattern(0))
1811 MultiPattern(f(Var(0)), g(Var(0)))
1814 _z3_assert(len(args) > 0,
"At least one argument expected")
1815 _z3_assert(all([
is_expr(a)
for a
in args ]),
"Z3 expressions expected")
1817 args, sz = _to_ast_array(args)
◆ Not()
def z3py.Not |
( |
|
a, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 not expression or probe.
>>> p = Bool('p')
>>> Not(Not(p))
Not(Not(p))
>>> simplify(Not(Not(p)))
p
Definition at line 1669 of file z3py.py.
1669 def Not(a, ctx=None):
1670 """Create a Z3 not expression or probe.
1675 >>> simplify(Not(Not(p)))
1678 ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
1685 return BoolRef(
Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
Referenced by fpNEQ(), mk_not(), and prove().
◆ open_log()
def z3py.open_log |
( |
|
fname | ) |
|
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 101 of file z3py.py.
102 """Log interaction to a file. This function must be invoked immediately after init(). """
◆ Option()
Create the regular expression that optionally accepts the argument.
>>> re = Option(Re("a"))
>>> print(simplify(InRe("a", re)))
True
>>> print(simplify(InRe("", re)))
True
>>> print(simplify(InRe("aa", re)))
False
Definition at line 10400 of file z3py.py.
10401 """Create the regular expression that optionally accepts the argument.
10402 >>> re = Option(Re("a"))
10403 >>> print(simplify(InRe("a", re)))
10405 >>> print(simplify(InRe("", re)))
10407 >>> print(simplify(InRe("aa", re)))
◆ Or()
Create a Z3 or-expression or or-probe.
>>> p, q, r = Bools('p q r')
>>> Or(p, q, r)
Or(p, q, r)
>>> P = BoolVector('p', 5)
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 1732 of file z3py.py.
1733 """Create a Z3 or-expression or or-probe.
1735 >>> p, q, r = Bools('p q r')
1738 >>> P = BoolVector('p', 5)
1740 Or(p__0, p__1, p__2, p__3, p__4)
1744 last_arg = args[len(args)-1]
1745 if isinstance(last_arg, Context):
1746 ctx = args[len(args)-1]
1747 args = args[:len(args)-1]
1748 elif len(args) == 1
and isinstance(args[0], AstVector):
1750 args = [a
for a
in args[0]]
1753 args = _get_args(args)
1754 ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
1756 _z3_assert(ctx
is not None,
"At least one of the arguments must be a Z3 expression or probe")
1757 if _has_probe(args):
1758 return _probe_or(args, ctx)
1760 args = _coerce_expr_list(args, ctx)
1761 _args, sz = _to_ast_array(args)
1762 return BoolRef(
Z3_mk_or(ctx.ref(), sz, _args), ctx)
Referenced by ApplyResult.as_expr().
◆ OrElse()
def z3py.OrElse |
( |
* |
ts, |
|
|
** |
ks |
|
) |
| |
Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
>>> x = Int('x')
>>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
>>> # Tactic split-clause fails if there is no clause in the given goal.
>>> t(x == 0)
[[x == 0]]
>>> t(Or(x == 0, x == 1))
[[x == 0], [x == 1]]
Definition at line 7801 of file z3py.py.
7802 """Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
7805 >>> t = OrElse(Tactic('split-clause'), Tactic('skip'))
7806 >>> # Tactic split-clause fails if there is no clause in the given goal.
7809 >>> t(Or(x == 0, x == 1))
7810 [[x == 0], [x == 1]]
7813 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7814 ctx = ks.get(
'ctx',
None)
7817 for i
in range(num - 1):
7818 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 7853 of file z3py.py.
7854 """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 7821 of file z3py.py.
7821 def ParOr(*ts, **ks):
7822 """Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
7825 >>> t = ParOr(Tactic('simplify'), Tactic('fail'))
7830 _z3_assert(len(ts) >= 2,
"At least two arguments expected")
7831 ctx = _get_ctx(ks.get(
'ctx',
None))
7832 ts = [ _to_tactic(t, ctx)
for t
in ts ]
7834 _args = (TacticObj * sz)()
7836 _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 8626 of file z3py.py.
8627 """Parse a file in SMT 2.0 format using the given sorts and decls.
8629 This function is similar to parse_smt2_string().
8632 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8633 dsz, dnames, ddecls = _dict2darray(decls, ctx)
8634 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 8606 of file z3py.py.
8607 """Parse a string in SMT 2.0 format using the given sorts and decls.
8609 The arguments sorts and decls are Python dictionaries used to initialize
8610 the symbol table used for the SMT 2.0 parser.
8612 >>> parse_smt2_string('(declare-const x Int) (assert (> x 0)) (assert (< x 10))')
8614 >>> x, y = Ints('x y')
8615 >>> f = Function('f', IntSort(), IntSort())
8616 >>> parse_smt2_string('(assert (> (+ foo (g bar)) 0))', decls={ 'foo' : x, 'bar' : y, 'g' : f})
8618 >>> parse_smt2_string('(declare-const a U) (assert (> a 0))', sorts={ 'U' : IntSort() })
8622 ssz, snames, ssorts = _dict2sarray(sorts, ctx)
8623 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 7839 of file z3py.py.
7839 def ParThen(t1, t2, ctx=None):
7840 """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
7842 >>> x, y = Ints('x y')
7843 >>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
7844 >>> t(And(Or(x == 1, x == 2), y == x + 1))
7845 [[x == 1, y == 2], [x == 2, y == 3]]
7847 t1 = _to_tactic(t1, ctx)
7848 t2 = _to_tactic(t2, ctx)
7850 _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 8413 of file z3py.py.
8413 def PbEq(args, k, ctx = None):
8414 """Create a Pseudo-Boolean inequality k constraint.
8416 >>> a, b, c = Bools('a b c')
8417 >>> f = PbEq(((a,1),(b,3),(c,2)), 3)
8419 _z3_check_cint_overflow(k,
"k")
8420 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8421 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 8403 of file z3py.py.
8404 """Create a Pseudo-Boolean inequality k constraint.
8406 >>> a, b, c = Bools('a b c')
8407 >>> f = PbGe(((a,1),(b,3),(c,2)), 3)
8409 _z3_check_cint_overflow(k,
"k")
8410 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8411 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 8393 of file z3py.py.
8394 """Create a Pseudo-Boolean inequality k constraint.
8396 >>> a, b, c = Bools('a b c')
8397 >>> f = PbLe(((a,1),(b,3),(c,2)), 3)
8399 _z3_check_cint_overflow(k,
"k")
8400 ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
8401 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 10388 of file z3py.py.
10389 """Create the regular expression accepting one or more repetitions of argument.
10390 >>> re = Plus(Re("a"))
10391 >>> print(simplify(InRe("aa", re)))
10393 >>> print(simplify(InRe("ab", re)))
10395 >>> print(simplify(InRe("", re)))
10398 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 10178 of file z3py.py.
10179 """Check if 'a' is a prefix of 'b'
10180 >>> s1 = PrefixOf("ab", "abc")
10183 >>> s2 = PrefixOf("bc", "abc")
10187 ctx = _get_ctx2(a, b)
10188 a = _coerce_seq(a, ctx)
10189 b = _coerce_seq(b, ctx)
10190 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 8111 of file z3py.py.
8112 """Return a short description for the probe named `name`.
8114 >>> 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 8101 of file z3py.py.
8102 """Return a list of all available probes in Z3.
8105 >>> 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 8309 of file z3py.py.
8310 """Create the product of the Z3 expressions.
8312 >>> a, b, c = Ints('a b c')
8313 >>> Product(a, b, c)
8315 >>> Product([a, b, c])
8317 >>> A = IntVector('a', 5)
8319 a__0*a__1*a__2*a__3*a__4
8321 args = _get_args(args)
8324 ctx = _ctx_from_ast_arg_list(args)
8326 return _reduce(
lambda a, b: a * b, args, 1)
8327 args = _coerce_expr_list(args, ctx)
8329 return _reduce(
lambda a, b: a * b, args, 1)
8331 _args, sz = _to_ast_array(args)
8332 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 8481 of file z3py.py.
8481 def prove(claim, **keywords):
8482 """Try to prove the given claim.
8484 This is a simple function for creating demonstrations. It tries to prove
8485 `claim` by showing the negation is unsatisfiable.
8487 >>> p, q = Bools('p q')
8488 >>> prove(Not(And(p, q)) == Or(Not(p), Not(q)))
8492 _z3_assert(
is_bool(claim),
"Z3 Boolean expression expected")
8496 if keywords.get(
'show',
False):
8502 print(
"failed to prove")
8505 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 3019 of file z3py.py.
3019 def Q(a, b, ctx=None):
3020 """Return a Z3 rational a/b.
3022 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 10440 of file z3py.py.
10440 def Range(lo, hi, ctx = None):
10441 """Create the range regular expression over two sequences of length 1
10442 >>> range = Range("a","z")
10443 >>> print(simplify(InRe("b", range)))
10445 >>> print(simplify(InRe("bb", range)))
10448 lo = _coerce_seq(lo, ctx)
10449 hi = _coerce_seq(hi, ctx)
10450 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 3004 of file z3py.py.
3004 def RatVal(a, b, ctx=None):
3005 """Return a Z3 rational a/b.
3007 If `ctx=None`, then the global context is used.
3011 >>> RatVal(3,5).sort()
3015 _z3_assert(_is_int(a)
or isinstance(a, str),
"First argument cannot be converted into an integer")
3016 _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 10300 of file z3py.py.
10300 def Re(s, ctx=None):
10301 """The regular expression that accepts sequence 's'
10303 >>> s2 = Re(StringVal("ab"))
10304 >>> s3 = Re(Unit(BoolVal(True)))
10306 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 3080 of file z3py.py.
3080 def Real(name, ctx=None):
3081 """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 3092 of file z3py.py.
3092 def Reals(names, ctx=None):
3093 """Return a tuple of real constants.
3095 >>> x, y, z = Reals('x y z')
3098 >>> Sum(x, y, z).sort()
3102 if isinstance(names, str):
3103 names = names.split(
" ")
3104 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 2944 of file z3py.py.
2945 """Return the real sort in the given context. If `ctx=None`, then the global context is used.
2949 >>> x = Const('x', RealSort())
2954 >>> 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 2986 of file z3py.py.
2987 """Return a Z3 real value.
2989 `val` may be a Python int, long, float or string representing a number in decimal or rational notation.
2990 If `ctx=None`, then the global context is used.
2994 >>> 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 1363 of file z3py.py.
1365 Create a real free variable. Free variables are used to create quantified formulas.
1366 They are also used to create polynomials.
Referenced by RealVarVector().
◆ RealVarVector()
def z3py.RealVarVector |
( |
|
n, |
|
|
|
ctx = None |
|
) |
| |
Create a list of Real free variables.
The variables have ids: 0, 1, ..., n-1
>>> x0, x1, x2, x3 = RealVarVector(4)
>>> x2
Var(2)
Definition at line 1373 of file z3py.py.
1375 Create a list of Real free variables.
1376 The variables have ids: 0, 1, ..., n-1
1378 >>> x0, x1, x2, x3 = RealVarVector(4)
◆ RealVector()
def z3py.RealVector |
( |
|
prefix, |
|
|
|
sz, |
|
|
|
ctx = None |
|
) |
| |
Return a list of real constants of size `sz`.
>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real
Definition at line 3106 of file z3py.py.
3107 """Return a list of real constants of size `sz`.
3109 >>> X = RealVector('x', 3)
3118 return [
Real(
'%s__%s' % (prefix, i), ctx)
for i
in range(sz) ]
◆ RecAddDefinition()
def z3py.RecAddDefinition |
( |
|
f, |
|
|
|
args, |
|
|
|
body |
|
) |
| |
Set the body of a recursive function.
Recursive definitions can be simplified if they are applied to ground
arguments.
>>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx)
>>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
>>> simplify(fac(5))
120
>>> s = Solver(ctx=ctx)
>>> s.add(fac(n) < 3)
>>> s.check()
sat
>>> s.model().eval(fac(5))
120
Definition at line 860 of file z3py.py.
861 """Set the body of a recursive function.
862 Recursive definitions can be simplified if they are applied to ground
865 >>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
866 >>> n = Int('n', ctx)
867 >>> RecAddDefinition(fac, n, If(n == 0, 1, n*fac(n-1)))
870 >>> s = Solver(ctx=ctx)
871 >>> s.add(fac(n) < 3)
874 >>> s.model().eval(fac(5))
880 args = _get_args(args)
884 _args[i] = args[i].ast
◆ RecFunction()
def z3py.RecFunction |
( |
|
name, |
|
|
* |
sig |
|
) |
| |
Create a new Z3 recursive with the given sorts.
Definition at line 843 of file z3py.py.
844 """Create a new Z3 recursive with the given sorts."""
847 _z3_assert(len(sig) > 0,
"At least two arguments expected")
851 _z3_assert(
is_sort(rng),
"Z3 sort expected")
852 dom = (Sort * arity)()
853 for i
in range(arity):
855 _z3_assert(
is_sort(sig[i]),
"Z3 sort expected")
◆ Repeat()
def z3py.Repeat |
( |
|
t, |
|
|
|
max = 4294967295 , |
|
|
|
ctx = None |
|
) |
| |
Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
>>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
>>> r = t(c)
>>> for subgoal in r: print(subgoal)
[x == 0, y == 0, x > y]
[x == 0, y == 1, x > y]
[x == 1, y == 0, x > y]
[x == 1, y == 1, x > y]
>>> t = Then(t, Tactic('propagate-values'))
>>> t(c)
[[x == 1, y == 0]]
Definition at line 7883 of file z3py.py.
7883 def Repeat(t, max=4294967295, ctx=None):
7884 """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
7886 >>> x, y = Ints('x y')
7887 >>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
7888 >>> t = Repeat(OrElse(Tactic('split-clause'), Tactic('skip')))
7890 >>> for subgoal in r: print(subgoal)
7891 [x == 0, y == 0, x > y]
7892 [x == 0, y == 1, x > y]
7893 [x == 1, y == 0, x > y]
7894 [x == 1, y == 1, x > y]
7895 >>> t = Then(t, Tactic('propagate-values'))
7899 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 4153 of file z3py.py.
4154 """Return an expression representing `n` copies of `a`.
4156 >>> x = BitVec('x', 8)
4157 >>> n = RepeatBitVec(4, x)
4162 >>> v0 = BitVecVal(10, 4)
4163 >>> print("%.x" % v0.as_long())
4165 >>> v = simplify(RepeatBitVec(4, v0))
4168 >>> print("%.x" % v.as_long())
4172 _z3_assert(_is_int(n),
"First argument must be an integer")
4173 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4174 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 10225 of file z3py.py.
10226 """Replace the first occurrence of 'src' by 'dst' in 's'
10227 >>> r = Replace("aaa", "a", "b")
10231 ctx = _get_ctx2(dst, s)
10232 if ctx
is None and is_expr(src):
10234 src = _coerce_seq(src, ctx)
10235 dst = _coerce_seq(dst, ctx)
10236 s = _coerce_seq(s, ctx)
10237 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 10320 of file z3py.py.
10323 if s
is None or isinstance(s, Context):
10326 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 4067 of file z3py.py.
4068 """Return an expression representing `a` rotated to the left `b` times.
4070 >>> a, b = BitVecs('a b', 16)
4071 >>> RotateLeft(a, b)
4073 >>> simplify(RotateLeft(a, 0))
4075 >>> simplify(RotateLeft(a, 16))
4078 _check_bv_args(a, b)
4079 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 4082 of file z3py.py.
4083 """Return an expression representing `a` rotated to the right `b` times.
4085 >>> a, b = BitVecs('a b', 16)
4086 >>> RotateRight(a, b)
4088 >>> simplify(RotateRight(a, 0))
4090 >>> simplify(RotateRight(a, 16))
4093 _check_bv_args(a, b)
4094 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 4487 of file z3py.py.
4488 """Return a Z3 select array expression.
4490 >>> a = Array('a', IntSort(), IntSort())
4494 >>> eq(Select(a, i), a[i])
4498 _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 10003 of file z3py.py.
10004 """Create a sequence sort over elements provided in the argument
10005 >>> s = SeqSort(IntSort())
10006 >>> 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 8679 of file z3py.py.
8680 global _dflt_fpsort_ebits
8681 global _dflt_fpsort_sbits
8682 _dflt_fpsort_ebits = ebits
8683 _dflt_fpsort_sbits = sbits
◆ set_default_rounding_mode()
def z3py.set_default_rounding_mode |
( |
|
rm, |
|
|
|
ctx = None |
|
) |
| |
Definition at line 8663 of file z3py.py.
8664 global _dflt_rounding_mode
8666 _dflt_rounding_mode = rm.decl().kind()
8668 _z3_assert(_dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_ZERO
or
8669 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_NEGATIVE
or
8670 _dflt_rounding_mode == Z3_OP_FPA_RM_TOWARD_POSITIVE
or
8671 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN
or
8672 _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY,
8673 "illegal rounding mode")
8674 _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 4635 of file z3py.py.
4636 """ Add element e to set s
4637 >>> a = Const('a', SetSort(IntSort()))
4641 ctx = _ctx_from_ast_arg_list([s,e])
4642 e = _py2expr(e, ctx)
4643 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 4655 of file z3py.py.
4656 """ The complement of set s
4657 >>> a = Const('a', SetSort(IntSort()))
4658 >>> SetComplement(a)
◆ SetDel()
Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
Definition at line 4645 of file z3py.py.
4646 """ Remove element e to set s
4647 >>> a = Const('a', SetSort(IntSort()))
4651 ctx = _ctx_from_ast_arg_list([s,e])
4652 e = _py2expr(e, ctx)
4653 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 4664 of file z3py.py.
4665 """ The set difference of a and b
4666 >>> a = Const('a', SetSort(IntSort()))
4667 >>> b = Const('b', SetSort(IntSort()))
4668 >>> SetDifference(a, b)
4671 ctx = _ctx_from_ast_arg_list([a, b])
◆ SetHasSize()
def z3py.SetHasSize |
( |
|
a, |
|
|
|
k |
|
) |
| |
Definition at line 4556 of file z3py.py.
4558 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 4623 of file z3py.py.
4624 """ Take the union of sets
4625 >>> a = Const('a', SetSort(IntSort()))
4626 >>> b = Const('b', SetSort(IntSort()))
4627 >>> SetIntersect(a, b)
4630 args = _get_args(args)
4631 ctx = _ctx_from_ast_arg_list(args)
4632 _args, sz = _to_ast_array(args)
◆ SetSort()
Sets.
Create a set sort over element sort s
Definition at line 4591 of file z3py.py.
4592 """ 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 4611 of file z3py.py.
4612 """ Take the union of sets
4613 >>> a = Const('a', SetSort(IntSort()))
4614 >>> b = Const('b', SetSort(IntSort()))
4618 args = _get_args(args)
4619 ctx = _ctx_from_ast_arg_list(args)
4620 _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 4097 of file z3py.py.
4098 """Return a bit-vector expression with `n` extra sign-bits.
4100 >>> x = BitVec('x', 16)
4101 >>> n = SignExt(8, x)
4108 >>> v0 = BitVecVal(2, 2)
4113 >>> v = simplify(SignExt(6, v0))
4118 >>> print("%.x" % v.as_long())
4122 _z3_assert(_is_int(n),
"First argument must be an integer")
4123 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4124 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 6954 of file z3py.py.
6955 """Return a simple general purpose solver with limited amount of preprocessing.
6957 >>> 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 8205 of file z3py.py.
8205 def simplify(a, *arguments, **keywords):
8206 """Simplify the expression `a` using the given options.
8208 This function has many options. Use `help_simplify` to obtain the complete list.
8212 >>> simplify(x + 1 + y + x + 1)
8214 >>> simplify((x + 1)*(y + 1), som=True)
8216 >>> simplify(Distinct(x, y, 1), blast_distinct=True)
8217 And(Not(x == y), Not(x == 1), Not(y == 1))
8218 >>> simplify(And(x == 0, y == 1), elim_and=True)
8219 Not(Or(Not(x == 0), Not(y == 1)))
8222 _z3_assert(
is_expr(a),
"Z3 expression expected")
8223 if len(arguments) > 0
or len(keywords) > 0:
8225 return _to_expr_ref(
Z3_simplify_ex(a.ctx_ref(), a.as_ast(), p.params), a.ctx)
8227 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 8233 of file z3py.py.
8234 """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 8424 of file z3py.py.
8424 def solve(*args, **keywords):
8425 """Solve the constraints `*args`.
8427 This is a simple function for creating demonstrations. It creates a solver,
8428 configure it using the options in `keywords`, adds the constraints
8429 in `args`, and invokes check.
8432 >>> solve(a > 0, a < 2)
8438 if keywords.get(
'show',
False):
8442 print(
"no solution")
8444 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 8452 of file z3py.py.
8453 """Solve the constraints `*args` using solver `s`.
8455 This is a simple function for creating demonstrations. It is similar to `solve`,
8456 but it uses the given solver `s`.
8457 It configures solver `s` using the options in `keywords`, adds the constraints
8458 in `args`, and invokes check.
8461 _z3_assert(isinstance(s, Solver),
"Solver object expected")
8464 if keywords.get(
'show',
False):
8469 print(
"no solution")
8471 print(
"failed to solve")
8477 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 6934 of file z3py.py.
6934 def SolverFor(logic, ctx=None, logFile=None):
6935 """Create a solver customized for the given logic.
6937 The parameter `logic` is a string. It should be contains
6938 the name of a SMT-LIB logic.
6939 See http://www.smtlib.org/ for the name of all available logics.
6941 >>> 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 3183 of file z3py.py.
3183 def Sqrt(a, ctx=None):
3184 """ 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 4016 of file z3py.py.
4017 """Create the Z3 expression signed remainder.
4019 Use the operator % for signed modulus, and URem() for unsigned remainder.
4021 >>> x = BitVec('x', 32)
4022 >>> y = BitVec('y', 32)
4025 >>> SRem(x, y).sort()
4029 >>> SRem(x, y).sexpr()
4032 _check_bv_args(a, b)
4033 a, b = _coerce_exprs(a, b)
4034 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 10416 of file z3py.py.
10417 """Create the regular expression accepting zero or more repetitions of argument.
10418 >>> re = Star(Re("a"))
10419 >>> print(simplify(InRe("aa", re)))
10421 >>> print(simplify(InRe("ab", re)))
10423 >>> print(simplify(InRe("", re)))
10426 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 4471 of file z3py.py.
4472 """Return a Z3 store array expression.
4474 >>> a = Array('a', IntSort(), IntSort())
4475 >>> i, v = Ints('i v')
4476 >>> s = Store(a, i, v)
4479 >>> prove(s[i] == v)
4482 >>> 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 10111 of file z3py.py.
10111 def String(name, ctx=None):
10112 """Return a string constant named `name`. If `ctx=None`, then the global context is used.
10114 >>> x = String('x')
10116 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.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 10119 of file z3py.py.
10119 def Strings(names, ctx=None):
10120 """Return string constants"""
10121 ctx = _get_ctx(ctx)
10122 if isinstance(names, str):
10123 names = names.split(
" ")
10124 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 9993 of file z3py.py.
9994 """Create a string sort
9995 >>> 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 10277 of file z3py.py.
10278 """Convert string expression to integer
10279 >>> a = StrToInt("1")
10280 >>> simplify(1 == a)
10282 >>> b = StrToInt("2")
10283 >>> simplify(1 == b)
10285 >>> c = StrToInt(IntToStr(2))
10286 >>> simplify(1 == c)
◆ SubSeq()
def z3py.SubSeq |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10130 of file z3py.py.
10130 def SubSeq(s, offset, length):
10131 """Extract substring or subsequence starting at offset"""
10132 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 8237 of file z3py.py.
8238 """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.
8242 >>> substitute(x + 1, (x, y + 1))
8244 >>> f = Function('f', IntSort(), IntSort())
8245 >>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
8248 if isinstance(m, tuple):
8250 if isinstance(m1, list)
and all(isinstance(p, tuple)
for p
in m1):
8253 _z3_assert(
is_expr(t),
"Z3 expression expected")
8254 _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.")
8256 _from = (Ast * num)()
8258 for i
in range(num):
8259 _from[i] = m[i][0].as_ast()
8260 _to[i] = m[i][1].as_ast()
8261 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 8263 of file z3py.py.
8264 """Substitute the free variables in t with the expression in m.
8266 >>> v0 = Var(0, IntSort())
8267 >>> v1 = Var(1, IntSort())
8269 >>> f = Function('f', IntSort(), IntSort(), IntSort())
8270 >>> # replace v0 with x+1 and v1 with x
8271 >>> substitute_vars(f(v0, v1), x + 1, x)
8275 _z3_assert(
is_expr(t),
"Z3 expression expected")
8276 _z3_assert(all([
is_expr(n)
for n
in m]),
"Z3 invalid substitution, list of expressions expected.")
8279 for i
in range(num):
8280 _to[i] = m[i].as_ast()
◆ SubString()
def z3py.SubString |
( |
|
s, |
|
|
|
offset, |
|
|
|
length |
|
) |
| |
Extract substring or subsequence starting at offset
Definition at line 10126 of file z3py.py.
10127 """Extract substring or subsequence starting at offset"""
10128 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 10192 of file z3py.py.
10193 """Check if 'a' is a suffix of 'b'
10194 >>> s1 = SuffixOf("ab", "abc")
10197 >>> s2 = SuffixOf("bc", "abc")
10201 ctx = _get_ctx2(a, b)
10202 a = _coerce_seq(a, ctx)
10203 b = _coerce_seq(b, ctx)
10204 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 8283 of file z3py.py.
8284 """Create the sum of the Z3 expressions.
8286 >>> a, b, c = Ints('a b c')
8291 >>> A = IntVector('a', 5)
8293 a__0 + a__1 + a__2 + a__3 + a__4
8295 args = _get_args(args)
8298 ctx = _ctx_from_ast_arg_list(args)
8300 return _reduce(
lambda a, b: a + b, args, 0)
8301 args = _coerce_expr_list(args, ctx)
8303 return _reduce(
lambda a, b: a + b, args, 0)
8305 _args, sz = _to_ast_array(args)
8306 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 7920 of file z3py.py.
7921 """Return a short description for the tactic named `name`.
7923 >>> 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 7910 of file z3py.py.
7911 """Return a list of all available tactics in Z3.
7914 >>> 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 7789 of file z3py.py.
7789 def Then(*ts, **ks):
7790 """Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
7792 >>> x, y = Ints('x y')
7793 >>> t = Then(Tactic('simplify'), Tactic('solve-eqs'))
7794 >>> t(And(x == 0, y > x + 1))
7796 >>> 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 3150 of file z3py.py.
3151 """ Return the Z3 expression ToInt(a).
3163 _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 3133 of file z3py.py.
3134 """ Return the Z3 expression ToReal(a).
3146 _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 10466 of file z3py.py.
10467 """Given a binary relation R, such that the two arguments have the same sort
10468 create the transitive closure relation R+.
10469 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 7902 of file z3py.py.
7902 def TryFor(t, ms, ctx=None):
7903 """Return a tactic that applies `t` to a given goal for `ms` milliseconds.
7905 If `t` does not terminate in `ms` milliseconds, then it fails.
7907 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 4994 of file z3py.py.
4995 """Create a named tuple sort base on a set of underlying sorts
4997 >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
4999 tuple = Datatype(name, ctx)
5000 projects = [ (
'project%d' % i, sorts[i])
for i
in range(len(sorts)) ]
5001 tuple.declare(name, *projects)
5002 tuple = tuple.create()
5003 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 3976 of file z3py.py.
3977 """Create the Z3 expression (unsigned) division `self / other`.
3979 Use the operator / for signed division.
3981 >>> x = BitVec('x', 32)
3982 >>> y = BitVec('y', 32)
3985 >>> UDiv(x, y).sort()
3989 >>> UDiv(x, y).sexpr()
3992 _check_bv_args(a, b)
3993 a, b = _coerce_exprs(a, b)
3994 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 3942 of file z3py.py.
3943 """Create the Z3 expression (unsigned) `other >= self`.
3945 Use the operator >= for signed greater than or equal to.
3947 >>> x, y = BitVecs('x y', 32)
3950 >>> (x >= y).sexpr()
3952 >>> UGE(x, y).sexpr()
3955 _check_bv_args(a, b)
3956 a, b = _coerce_exprs(a, b)
3957 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 3959 of file z3py.py.
3960 """Create the Z3 expression (unsigned) `other > self`.
3962 Use the operator > for signed greater than.
3964 >>> x, y = BitVecs('x y', 32)
3969 >>> UGT(x, y).sexpr()
3972 _check_bv_args(a, b)
3973 a, b = _coerce_exprs(a, b)
3974 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 3908 of file z3py.py.
3909 """Create the Z3 expression (unsigned) `other <= self`.
3911 Use the operator <= for signed less than or equal to.
3913 >>> x, y = BitVecs('x y', 32)
3916 >>> (x <= y).sexpr()
3918 >>> ULE(x, y).sexpr()
3921 _check_bv_args(a, b)
3922 a, b = _coerce_exprs(a, b)
3923 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 3925 of file z3py.py.
3926 """Create the Z3 expression (unsigned) `other < self`.
3928 Use the operator < for signed less than.
3930 >>> x, y = BitVecs('x y', 32)
3935 >>> ULT(x, y).sexpr()
3938 _check_bv_args(a, b)
3939 a, b = _coerce_exprs(a, b)
3940 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 10352 of file z3py.py.
10353 """Create union of regular expressions.
10354 >>> re = Union(Re("a"), Re("b"), Re("c"))
10355 >>> print (simplify(InRe("d", re)))
10358 args = _get_args(args)
10361 _z3_assert(sz > 0,
"At least one argument expected.")
10362 _z3_assert(all([
is_re(a)
for a
in args]),
"All arguments must be regular expressions.")
10367 for i
in range(sz):
10368 v[i] = args[i].as_ast()
Referenced by ReRef.__add__().
◆ Unit()
Create a singleton sequence
Definition at line 10174 of file z3py.py.
10175 """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 4439 of file z3py.py.
4440 """Return a Z3 store array expression.
4442 >>> a = Array('a', IntSort(), IntSort())
4443 >>> i, v = Ints('i v')
4444 >>> s = Update(a, i, v)
4447 >>> prove(s[i] == v)
4450 >>> prove(Implies(i != j, s[j] == a[j]))
4454 _z3_assert(
is_array_sort(a),
"First argument must be a Z3 array expression")
4455 i = a.sort().domain().cast(i)
4456 v = a.sort().
range().cast(v)
4458 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 3996 of file z3py.py.
3997 """Create the Z3 expression (unsigned) remainder `self % other`.
3999 Use the operator % for signed modulus, and SRem() for signed remainder.
4001 >>> x = BitVec('x', 32)
4002 >>> y = BitVec('y', 32)
4005 >>> URem(x, y).sort()
4009 >>> URem(x, y).sexpr()
4012 _check_bv_args(a, b)
4013 a, b = _coerce_exprs(a, b)
4014 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 1351 of file z3py.py.
1352 """Create a Z3 free variable. Free variables are used to create quantified formulas.
1354 >>> Var(0, IntSort())
1356 >>> eq(Var(0, IntSort()), Var(0, BoolSort()))
1360 _z3_assert(
is_sort(s),
"Z3 sort expected")
1361 return _to_expr_ref(
Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
Referenced by RealVar().
◆ When()
def z3py.When |
( |
|
p, |
|
|
|
t, |
|
|
|
ctx = None |
|
) |
| |
Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
>>> t = When(Probe('size') > 2, Tactic('simplify'))
>>> x, y = Ints('x y')
>>> g = Goal()
>>> g.add(x > 0)
>>> g.add(y > 0)
>>> t(g)
[[x > 0, y > 0]]
>>> g.add(x == y + 1)
>>> t(g)
[[Not(x <= 0), Not(y <= 0), x == 1 + y]]
Definition at line 8171 of file z3py.py.
8171 def When(p, t, ctx=None):
8172 """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
8174 >>> t = When(Probe('size') > 2, Tactic('simplify'))
8175 >>> x, y = Ints('x y')
8181 >>> g.add(x == y + 1)
8183 [[Not(x <= 0), Not(y <= 0), x == 1 + y]]
8185 p = _to_probe(p, ctx)
8186 t = _to_tactic(t, ctx)
8187 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 7857 of file z3py.py.
7857 def With(t, *args, **keys):
7858 """Return a tactic that applies tactic `t` using the given configuration options.
7860 >>> x, y = Ints('x y')
7861 >>> t = With(Tactic('simplify'), som=True)
7862 >>> t((x + 1)*(y + 2) == 0)
7863 [[2*x + y + x*y == -2]]
7865 ctx = keys.pop(
'ctx',
None)
7866 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 7870 of file z3py.py.
7871 """Return a tactic that applies tactic `t` using the given configuration options.
7873 >>> x, y = Ints('x y')
7875 >>> p.set("som", True)
7876 >>> t = WithParams(Tactic('simplify'), p)
7877 >>> t((x + 1)*(y + 2) == 0)
7878 [[2*x + y + x*y == -2]]
7880 t = _to_tactic(t,
None)
◆ Xor()
def z3py.Xor |
( |
|
a, |
|
|
|
b, |
|
|
|
ctx = None |
|
) |
| |
Create a Z3 Xor expression.
>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)
>>> simplify(Xor(p, q))
Not(p) == q
Definition at line 1654 of file z3py.py.
1654 def Xor(a, b, ctx=None):
1655 """Create a Z3 Xor expression.
1657 >>> p, q = Bools('p q')
1660 >>> simplify(Xor(p, q))
1663 ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
1667 return BoolRef(
Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
◆ z3_debug()
Definition at line 56 of file z3py.py.
Referenced by FuncDeclRef.__call__(), Probe.__call__(), QuantifierRef.__getitem__(), ModelRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), DatatypeSortRef.accessor(), And(), AndThen(), Tactic.apply(), ExprRef.arg(), args2params(), ArraySort(), 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(), eq(), AstRef.eq(), Ext(), Extract(), FiniteDomainVal(), fpIsPositive(), fpNeg(), FPSort(), fpToFPUnsigned(), fpToIEEEBV(), fpToReal(), fpToSBV(), fpToUBV(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), 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 4126 of file z3py.py.
4127 """Return a bit-vector expression with `n` extra zero-bits.
4129 >>> x = BitVec('x', 16)
4130 >>> n = ZeroExt(8, x)
4137 >>> v0 = BitVecVal(2, 2)
4142 >>> v = simplify(ZeroExt(6, v0))
4149 _z3_assert(_is_int(n),
"First argument must be an integer")
4150 _z3_assert(
is_bv(a),
"Second argument must be a Z3 bit-vector expression")
4151 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_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, Z3_string prefix, unsigned domain_size, Z3_sort const domain[], Z3_sort range)
Declare a fresh constant or function.
Z3_ast Z3_API Z3_mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3)
Create an AST node representing an if-then-else: ite(t1, t2, t3).
Z3_ast Z3_API Z3_mk_extract(Z3_context c, unsigned high, unsigned low, Z3_ast t1)
Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n,...
def Implies(a, b, ctx=None)
Z3_ast Z3_API Z3_mk_seq_in_re(Z3_context c, Z3_ast seq, Z3_ast re)
Check if seq is in the language generated by the regular expression re.
Z3_ast Z3_API Z3_mk_set_difference(Z3_context c, Z3_ast arg1, Z3_ast arg2)
Take the set difference between two sets.
Z3_ast Z3_API Z3_mk_bvule(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than or equal to.
def BVSDivNoOverflow(a, b)
def BitVec(name, bv, ctx=None)
Z3_sort Z3_API Z3_mk_bool_sort(Z3_context c)
Create the Boolean type.
unsigned Z3_API Z3_get_num_tactics(Z3_context c)
Return the number of builtin tactics available in Z3.
def BitVecs(names, bv, ctx=None)
Z3_tactic Z3_API Z3_tactic_cond(Z3_context c, Z3_probe p, Z3_tactic t1, Z3_tactic t2)
Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluat...
def LastIndexOf(s, substr)
Z3_ast Z3_API Z3_mk_lstring(Z3_context c, unsigned len, Z3_string s)
Create a string constant out of the string that is passed in It takes the length of the string as wel...
Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value)
Get a global (or module) parameter.
def fpIsNormal(a, ctx=None)
def FreshConst(sort, prefix='c')
Z3_tactic Z3_API Z3_tactic_repeat(Z3_context c, Z3_tactic t, unsigned max)
Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of...
Z3_ast Z3_API Z3_mk_ext_rotate_right(Z3_context c, Z3_ast t1, Z3_ast t2)
Rotate bits of t1 to the right t2 times.
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c)
Create the single-precision (32-bit) FloatingPoint sort.
Z3_ast Z3_API Z3_mk_const(Z3_context c, Z3_symbol s, Z3_sort ty)
Declare and create a constant.
void Z3_API Z3_disable_trace(Z3_string tag)
Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise.
def probe_description(name, ctx=None)
def tactic_description(name, ctx=None)
Z3_sort Z3_API Z3_mk_bv_sort(Z3_context c, unsigned sz)
Create a bit-vector type of the given size.
def StringVal(s, ctx=None)
unsigned Z3_API Z3_get_index_value(Z3_context c, Z3_ast a)
Return index of de-Bruijn bound variable.
Z3_ast Z3_API Z3_mk_seq_to_re(Z3_context c, Z3_ast seq)
Create a regular expression that accepts the sequence seq.
def fpFP(sgn, exp, sig, ctx=None)
Z3_sort Z3_API Z3_mk_int_sort(Z3_context c)
Create the integer type.
Z3_string Z3_API Z3_probe_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the probe with the given name.
Z3_sort Z3_API Z3_mk_enumeration_sort(Z3_context c, Z3_symbol name, unsigned n, Z3_symbol const enum_names[], Z3_func_decl enum_consts[], Z3_func_decl enum_testers[])
Create a enumeration sort.
def FPSort(ebits, sbits, ctx=None)
Z3_string Z3_API Z3_get_full_version(void)
Return a string that fully describes the version of Z3 in use.
Z3_ast Z3_API Z3_mk_bvurem(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned remainder.
def DeclareSort(name, ctx=None)
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, unsigned num_constructors, Z3_constructor const constructors[])
Create list of constructors.
def fpSqrt(rm, a, ctx=None)
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst)
Replace the first occurrence of src with dst in s.
def RealVar(idx, ctx=None)
def FP(name, fpsort, ctx=None)
Z3_ast Z3_API Z3_mk_seq_contains(Z3_context c, Z3_ast container, Z3_ast containee)
Check if container contains containee.
def fpDiv(rm, a, b, ctx=None)
def set_default_fp_sort(ebits, sbits, ctx=None)
Z3_ast Z3_API Z3_mk_bound(Z3_context c, unsigned index, Z3_sort ty)
Create a bound variable.
def PiecewiseLinearOrder(a, index)
void Z3_API Z3_mk_datatypes(Z3_context c, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort sorts[], Z3_constructor_list constructor_lists[])
Create mutually recursive datatypes.
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2)
Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
Z3_ast Z3_API Z3_mk_seq_empty(Z3_context c, Z3_sort seq)
Create an empty sequence of the sequence sort seq.
def RecAddDefinition(f, args, body)
def fpToSBV(rm, x, s, ctx=None)
Z3_sort Z3_API Z3_mk_string_sort(Z3_context c)
Create a sort for 8 bit strings.
Z3_probe Z3_API Z3_probe_not(Z3_context x, Z3_probe p)
Return a probe that evaluates to "true" when p does not evaluate to true.
Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range)
Create an array type.
Z3_ast Z3_API Z3_mk_int2bv(Z3_context c, unsigned n, Z3_ast t1)
Create an n bit bit-vector from the integer argument t1.
def FreshInt(prefix='x', ctx=None)
Z3_ast Z3_API Z3_mk_false(Z3_context c)
Create an AST node representing false.
def solve_using(s, *args, **keywords)
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c)
Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
def FiniteDomainVal(val, sort, ctx=None)
unsigned Z3_API Z3_get_num_probes(Z3_context c)
Return the number of builtin probes available in Z3.
Z3_ast_vector Z3_API Z3_parse_smtlib2_string(Z3_context c, Z3_string str, unsigned num_sorts, Z3_symbol const sort_names[], Z3_sort const sorts[], unsigned num_decls, Z3_symbol const decl_names[], Z3_func_decl const decls[])
Parse the given string using the SMT-LIB2 parser.
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, Z3_ast const args[], unsigned k)
Pseudo-Boolean relations.
def LinearOrder(a, index)
def BitVecSort(sz, ctx=None)
def fpAdd(rm, a, b, ctx=None)
def is_finite_domain_value(a)
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c)
Create the double-precision (64-bit) FloatingPoint sort.
Z3_string Z3_API Z3_tactic_get_descr(Z3_context c, Z3_string name)
Return a string containing a description of the tactic with the given name.
def fpSub(rm, a, b, ctx=None)
Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set)
Check for set membership.
Z3_tactic Z3_API Z3_tactic_par_or(Z3_context c, unsigned num, Z3_tactic const ts[])
Return a tactic that applies the given tactics in parallel.
def TryFor(t, ms, ctx=None)
Z3_ast Z3_API Z3_mk_bvult(Z3_context c, Z3_ast t1, Z3_ast t2)
Unsigned less than.
Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a)
Interface to simplifier.
def 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.