Functions | |
| z3_debug () | |
| _is_int (v) | |
| enable_trace (msg) | |
| disable_trace (msg) | |
| get_version_string () | |
| get_version () | |
| get_full_version () | |
| _z3_assert (cond, msg) | |
| _z3_check_cint_overflow (n, name) | |
| open_log (fname) | |
| append_log (s) | |
| to_symbol (s, ctx=None) | |
| _symbol2py (ctx, s) | |
| _get_args (args) | |
| _get_args_ast_list (args) | |
| _to_param_value (val) | |
| z3_error_handler (c, e) | |
| Context | main_ctx () |
| Context | _get_ctx (ctx) |
| Context | get_ctx (ctx) |
| set_param (*args, **kws) | |
| None | reset_params () |
| set_option (*args, **kws) | |
| get_param (name) | |
| bool | is_ast (Any a) |
| bool | eq (AstRef a, AstRef b) |
| int | _ast_kind (Context ctx, Any a) |
| _ctx_from_ast_arg_list (args, default_ctx=None) | |
| _ctx_from_ast_args (*args) | |
| _to_func_decl_array (args) | |
| _to_ast_array (args) | |
| _to_ref_array (ref, args) | |
| _to_ast_ref (a, ctx) | |
| _sort_kind (ctx, s) | |
| Sorts. | |
| bool | is_sort (Any s) |
| _to_sort_ref (s, ctx) | |
| SortRef | _sort (Context ctx, Any a) |
| SortRef | DeclareSort (name, ctx=None) |
| DeclareTypeVar (name, ctx=None) | |
| is_func_decl (a) | |
| Function (name, *sig) | |
| FreshFunction (*sig) | |
| _to_func_decl_ref (a, ctx) | |
| RecFunction (name, *sig) | |
| RecAddDefinition (f, args, body) | |
| deserialize (st) | |
| _to_expr_ref (a, ctx) | |
| _coerce_expr_merge (s, a) | |
| _check_same_sort (a, b, ctx=None) | |
| _coerce_exprs (a, b, ctx=None) | |
| _reduce (func, sequence, initial) | |
| _coerce_expr_list (alist, ctx=None) | |
| is_expr (a) | |
| is_app (a) | |
| is_const (a) | |
| is_var (a) | |
| get_var_index (a) | |
| is_app_of (a, k) | |
| If (a, b, c, ctx=None) | |
| Distinct (*args) | |
| _mk_bin (f, a, b) | |
| Const (name, sort) | |
| Consts (names, sort) | |
| FreshConst (sort, prefix="c") | |
| ExprRef | Var (int idx, SortRef s) |
| ExprRef | RealVar (int idx, ctx=None) |
| RealVarVector (int n, ctx=None) | |
| bool | is_bool (Any a) |
| bool | is_true (Any a) |
| bool | is_false (Any a) |
| bool | is_and (Any a) |
| bool | is_or (Any a) |
| bool | is_implies (Any a) |
| bool | is_not (Any a) |
| bool | is_eq (Any a) |
| bool | is_distinct (Any a) |
| BoolSort (ctx=None) | |
| BoolVal (val, ctx=None) | |
| Bool (name, ctx=None) | |
| Bools (names, ctx=None) | |
| BoolVector (prefix, sz, ctx=None) | |
| FreshBool (prefix="b", ctx=None) | |
| Implies (a, b, ctx=None) | |
| Xor (a, b, ctx=None) | |
| Not (a, ctx=None) | |
| mk_not (a) | |
| _has_probe (args) | |
| And (*args) | |
| Or (*args) | |
| is_pattern (a) | |
| MultiPattern (*args) | |
| _to_pattern (arg) | |
| is_quantifier (a) | |
| _mk_quantifier (is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) | |
| ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) | |
| Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) | |
| Lambda (vs, body) | |
| bool | is_arith_sort (Any s) |
| is_arith (a) | |
| bool | is_int (a) |
| is_real (a) | |
| _is_numeral (ctx, a) | |
| _is_algebraic (ctx, a) | |
| is_int_value (a) | |
| is_rational_value (a) | |
| is_algebraic_value (a) | |
| bool | is_add (Any a) |
| bool | is_mul (Any a) |
| bool | is_sub (Any a) |
| bool | is_div (Any a) |
| bool | is_idiv (Any a) |
| bool | is_mod (Any a) |
| bool | is_le (Any a) |
| bool | is_lt (Any a) |
| bool | is_ge (Any a) |
| bool | is_gt (Any a) |
| bool | is_is_int (Any a) |
| bool | is_to_real (Any a) |
| bool | is_to_int (Any a) |
| is_complex_sort (s) | |
| is_complex (a) | |
| ComplexSort (ctx=None) | |
| Complex (name, ctx=None) | |
| Complexes (names, ctx=None) | |
| ComplexVal (real, imag=0, ctx=None) | |
| RealPart (value) | |
| ImagPart (value) | |
| _py2expr (a, ctx=None) | |
| IntSort (ctx=None) | |
| RealSort (ctx=None) | |
| _to_int_str (val) | |
| IntVal (val, ctx=None) | |
| RealVal (val, ctx=None) | |
| RatVal (a, b, ctx=None) | |
| Q (a, b, ctx=None) | |
| Int (name, ctx=None) | |
| Ints (names, ctx=None) | |
| IntVector (prefix, sz, ctx=None) | |
| FreshInt (prefix="x", ctx=None) | |
| Real (name, ctx=None) | |
| Reals (names, ctx=None) | |
| RealVector (prefix, sz, ctx=None) | |
| FreshReal (prefix="b", ctx=None) | |
| ToReal (a) | |
| ToInt (a) | |
| IsInt (a) | |
| Sqrt (a, ctx=None) | |
| Cbrt (a, ctx=None) | |
| is_bv_sort (s) | |
| is_bv (a) | |
| is_bv_value (a) | |
| BV2Int (a, is_signed=False) | |
| Int2BV (a, num_bits) | |
| BitVecSort (sz, ctx=None) | |
| BitVecVal (val, bv, ctx=None) | |
| BitVec (name, bv, ctx=None) | |
| BitVecs (names, bv, ctx=None) | |
| Concat (*args) | |
| Extract (high, low, a) | |
| _check_bv_args (a, b) | |
| ULE (a, b) | |
| ULT (a, b) | |
| UGE (a, b) | |
| UGT (a, b) | |
| UDiv (a, b) | |
| URem (a, b) | |
| SRem (a, b) | |
| LShR (a, b) | |
| RotateLeft (a, b) | |
| RotateRight (a, b) | |
| SignExt (n, a) | |
| ZeroExt (n, a) | |
| RepeatBitVec (n, a) | |
| BVRedAnd (a) | |
| BVRedOr (a) | |
| BvNand (a, b) | |
| BvNor (a, b) | |
| BvXnor (a, b) | |
| BVAddNoOverflow (a, b, signed) | |
| BVAddNoUnderflow (a, b) | |
| BVSubNoOverflow (a, b) | |
| BVSubNoUnderflow (a, b, signed) | |
| BVSDivNoOverflow (a, b) | |
| BVSNegNoOverflow (a) | |
| BVMulNoOverflow (a, b, signed) | |
| BVMulNoUnderflow (a, b) | |
| _array_select (ar, arg) | |
| is_array_sort (a) | |
| bool | is_array (Any a) |
| is_const_array (a) | |
| is_K (a) | |
| is_map (a) | |
| is_default (a) | |
| get_map_func (a) | |
| ArraySort (*sig) | |
| Array (name, *sorts) | |
| Update (a, *args) | |
| Default (a) | |
| Store (a, *args) | |
| Select (a, *args) | |
| Map (f, *args) | |
| K (dom, v) | |
| Ext (a, b) | |
| AsArray (f) | |
| is_select (a) | |
| is_store (a) | |
| SetSort (s) | |
| Sets. | |
| EmptySet (s) | |
| FullSet (s) | |
| SetUnion (*args) | |
| SetIntersect (*args) | |
| SetAdd (s, e) | |
| SetDel (s, e) | |
| SetComplement (s) | |
| SetDifference (a, b) | |
| IsMember (e, s) | |
| IsSubset (a, b) | |
| is_finite_set (a) | |
| is_finite_set_sort (s) | |
| FiniteSetSort (elem_sort) | |
| FiniteSetEmpty (set_sort) | |
| Singleton (elem) | |
| FiniteSetUnion (s1, s2) | |
| FiniteSetIntersect (s1, s2) | |
| FiniteSetDifference (s1, s2) | |
| FiniteSetMember (elem, set) | |
| In (elem, set) | |
| FiniteSetSize (set) | |
| FiniteSetSubset (s1, s2) | |
| FiniteSetMap (f, set) | |
| FiniteSetFilter (f, set) | |
| FiniteSetRange (low, high) | |
| _valid_accessor (acc) | |
| Datatypes. | |
| CreateDatatypes (*ds) | |
| CreatePolymorphicDatatype (d, type_params) | |
| DatatypeSort (name, params=None, ctx=None) | |
| TupleSort (name, sorts, ctx=None) | |
| DisjointSum (name, sorts, ctx=None) | |
| EnumSort (name, values, ctx=None) | |
| args2params (arguments, keywords, ctx=None) | |
| Model (ctx=None, eval={}) | |
| is_as_array (n) | |
| get_as_array_func (n) | |
| SolverFor (logic, ctx=None, logFile=None) | |
| SimpleSolver (ctx=None, logFile=None) | |
| FiniteDomainSort (name, sz, ctx=None) | |
| is_finite_domain_sort (s) | |
| is_finite_domain (a) | |
| FiniteDomainVal (val, sort, ctx=None) | |
| is_finite_domain_value (a) | |
| _global_on_model (ctx) | |
| num_simplifiers (ctx=None) | |
| simplifier_name (i, ctx=None) | |
| simplifier_description (name, ctx=None) | |
| _to_goal (a) | |
| _to_tactic (t, ctx=None) | |
| _and_then (t1, t2, ctx=None) | |
| _or_else (t1, t2, ctx=None) | |
| AndThen (*ts, **ks) | |
| Then (*ts, **ks) | |
| OrElse (*ts, **ks) | |
| ParOr (*ts, **ks) | |
| ParThen (t1, t2, ctx=None) | |
| ParAndThen (t1, t2, ctx=None) | |
| With (t, *args, **keys) | |
| WithParams (t, p) | |
| Repeat (t, max=4294967295, ctx=None) | |
| TryFor (t, ms, ctx=None) | |
| tactics (ctx=None) | |
| tactic_description (name, ctx=None) | |
| describe_tactics () | |
| is_probe (p) | |
| _to_probe (p, ctx=None) | |
| probes (ctx=None) | |
| probe_description (name, ctx=None) | |
| describe_probes () | |
| _probe_nary (f, args, ctx) | |
| _probe_and (args, ctx) | |
| _probe_or (args, ctx) | |
| FailIf (p, ctx=None) | |
| When (p, t, ctx=None) | |
| Cond (p, t1, t2, ctx=None) | |
| simplify (a, *arguments, **keywords) | |
| Utils. | |
| help_simplify () | |
| simplify_param_descrs () | |
| substitute (t, *m) | |
| substitute_vars (t, *m) | |
| substitute_funs (t, *m) | |
| Sum (*args) | |
| Product (*args) | |
| Abs (arg) | |
| AtMost (*args) | |
| AtLeast (*args) | |
| _reorder_pb_arg (arg) | |
| _pb_args_coeffs (args, default_ctx=None) | |
| PbLe (args, k) | |
| PbGe (args, k) | |
| PbEq (args, k, ctx=None) | |
| solve (*args, **keywords) | |
| solve_using (s, *args, **keywords) | |
| prove (claim, show=False, **keywords) | |
| _solve_html (*args, **keywords) | |
| _solve_using_html (s, *args, **keywords) | |
| _prove_html (claim, show=False, **keywords) | |
| _dict2sarray (sorts, ctx) | |
| _dict2darray (decls, ctx) | |
| parse_smt2_string (s, sorts={}, decls={}, ctx=None) | |
| parse_smt2_file (f, sorts={}, decls={}, ctx=None) | |
| get_default_rounding_mode (ctx=None) | |
| set_default_rounding_mode (rm, ctx=None) | |
| get_default_fp_sort (ctx=None) | |
| set_default_fp_sort (ebits, sbits, ctx=None) | |
| _dflt_rm (ctx=None) | |
| _dflt_fps (ctx=None) | |
| _coerce_fp_expr_list (alist, ctx) | |
| Float16 (ctx=None) | |
| FloatHalf (ctx=None) | |
| Float32 (ctx=None) | |
| FloatSingle (ctx=None) | |
| Float64 (ctx=None) | |
| FloatDouble (ctx=None) | |
| Float128 (ctx=None) | |
| FloatQuadruple (ctx=None) | |
| is_fp_sort (s) | |
| is_fprm_sort (s) | |
| RoundNearestTiesToEven (ctx=None) | |
| RNE (ctx=None) | |
| RoundNearestTiesToAway (ctx=None) | |
| RNA (ctx=None) | |
| RoundTowardPositive (ctx=None) | |
| RTP (ctx=None) | |
| RoundTowardNegative (ctx=None) | |
| RTN (ctx=None) | |
| RoundTowardZero (ctx=None) | |
| RTZ (ctx=None) | |
| is_fprm (a) | |
| is_fprm_value (a) | |
| is_fp (a) | |
| is_fp_value (a) | |
| FPSort (ebits, sbits, ctx=None) | |
| _to_float_str (val, exp=0) | |
| fpNaN (s) | |
| fpPlusInfinity (s) | |
| fpMinusInfinity (s) | |
| fpInfinity (s, negative) | |
| fpPlusZero (s) | |
| fpMinusZero (s) | |
| fpZero (s, negative) | |
| FPVal (sig, exp=None, fps=None, ctx=None) | |
| FP (name, fpsort, ctx=None) | |
| FPs (names, fpsort, ctx=None) | |
| fpAbs (a, ctx=None) | |
| fpNeg (a, ctx=None) | |
| _mk_fp_unary (f, rm, a, ctx) | |
| _mk_fp_unary_pred (f, a, ctx) | |
| _mk_fp_bin (f, rm, a, b, ctx) | |
| _mk_fp_bin_norm (f, a, b, ctx) | |
| _mk_fp_bin_pred (f, a, b, ctx) | |
| _mk_fp_tern (f, rm, a, b, c, ctx) | |
| fpAdd (rm, a, b, ctx=None) | |
| fpSub (rm, a, b, ctx=None) | |
| fpMul (rm, a, b, ctx=None) | |
| fpDiv (rm, a, b, ctx=None) | |
| fpRem (a, b, ctx=None) | |
| fpMin (a, b, ctx=None) | |
| fpMax (a, b, ctx=None) | |
| fpFMA (rm, a, b, c, ctx=None) | |
| fpSqrt (rm, a, ctx=None) | |
| fpRoundToIntegral (rm, a, ctx=None) | |
| fpIsNaN (a, ctx=None) | |
| fpIsInf (a, ctx=None) | |
| fpIsZero (a, ctx=None) | |
| fpIsNormal (a, ctx=None) | |
| fpIsSubnormal (a, ctx=None) | |
| fpIsNegative (a, ctx=None) | |
| fpIsPositive (a, ctx=None) | |
| _check_fp_args (a, b) | |
| fpLT (a, b, ctx=None) | |
| fpLEQ (a, b, ctx=None) | |
| fpGT (a, b, ctx=None) | |
| fpGEQ (a, b, ctx=None) | |
| fpEQ (a, b, ctx=None) | |
| fpNEQ (a, b, ctx=None) | |
| fpFP (sgn, exp, sig, ctx=None) | |
| fpToFP (a1, a2=None, a3=None, ctx=None) | |
| fpBVToFP (v, sort, ctx=None) | |
| fpFPToFP (rm, v, sort, ctx=None) | |
| fpRealToFP (rm, v, sort, ctx=None) | |
| fpSignedToFP (rm, v, sort, ctx=None) | |
| fpUnsignedToFP (rm, v, sort, ctx=None) | |
| fpToFPUnsigned (rm, x, s, ctx=None) | |
| fpToSBV (rm, x, s, ctx=None) | |
| fpToUBV (rm, x, s, ctx=None) | |
| fpToReal (x, ctx=None) | |
| fpToIEEEBV (x, ctx=None) | |
| StringSort (ctx=None) | |
| CharSort (ctx=None) | |
| SeqSort (s) | |
| _coerce_char (ch, ctx=None) | |
| CharVal (ch, ctx=None) | |
| CharFromBv (bv) | |
| CharToBv (ch, ctx=None) | |
| CharToInt (ch, ctx=None) | |
| CharIsDigit (ch, ctx=None) | |
| _coerce_seq (s, ctx=None) | |
| _get_ctx2 (a, b, ctx=None) | |
| is_seq (a) | |
| bool | is_string (Any a) |
| bool | is_string_value (Any a) |
| StringVal (s, ctx=None) | |
| String (name, ctx=None) | |
| Strings (names, ctx=None) | |
| SubString (s, offset, length) | |
| SubSeq (s, offset, length) | |
| Empty (s) | |
| Full (s) | |
| Unit (a) | |
| PrefixOf (a, b) | |
| SuffixOf (a, b) | |
| Contains (a, b) | |
| Replace (s, src, dst) | |
| IndexOf (s, substr, offset=None) | |
| LastIndexOf (s, substr) | |
| Length (s) | |
| SeqPower (s, n) | |
| SeqMap (f, s) | |
| SeqMapI (f, i, s) | |
| SeqFoldLeft (f, a, s) | |
| SeqFoldLeftI (f, i, a, s) | |
| StrToInt (s) | |
| IntToStr (s) | |
| StrToCode (s) | |
| StrFromCode (c) | |
| Re (s, ctx=None) | |
| ReSort (s) | |
| is_re (s) | |
| InRe (s, re) | |
| Union (*args) | |
| Intersect (*args) | |
| Plus (re) | |
| Option (re) | |
| Complement (re) | |
| Star (re) | |
| Loop (re, lo, hi=0) | |
| Range (lo, hi, ctx=None) | |
| Diff (a, b, ctx=None) | |
| AllChar (regex_sort, ctx=None) | |
| PartialOrder (a, index) | |
| LinearOrder (a, index) | |
| TreeOrder (a, index) | |
| PiecewiseLinearOrder (a, index) | |
| TransitiveClosure (f) | |
| to_Ast (ptr) | |
| to_ContextObj (ptr) | |
| to_AstVectorObj (ptr) | |
| on_clause_eh (ctx, p, n, dep, clause) | |
| ensure_prop_closures () | |
| user_prop_push (ctx, cb) | |
| user_prop_pop (ctx, cb, num_scopes) | |
| user_prop_fresh (ctx, _new_ctx) | |
| user_prop_fixed (ctx, cb, id, value) | |
| user_prop_created (ctx, cb, id) | |
| user_prop_final (ctx, cb) | |
| user_prop_eq (ctx, cb, x, y) | |
| user_prop_diseq (ctx, cb, x, y) | |
| user_prop_decide (ctx, cb, t_ref, idx, phase) | |
| user_prop_binding (ctx, cb, q_ref, inst_ref) | |
| PropagateFunction (name, *sig) | |
| FiniteFieldSort (prime, ctx=None) | |
| FiniteFieldVal (value, field, ctx=None) | |
| FiniteFieldElem (name, field, ctx=None) | |
| FiniteFieldElems (names, field, ctx=None) | |
| FiniteFieldBitsum (*args) | |
Variables | |
| Z3_DEBUG = __debug__ | |
| _main_ctx = None | |
| sat = CheckSatResult(Z3_L_TRUE) | |
| unsat = CheckSatResult(Z3_L_FALSE) | |
| unknown = CheckSatResult(Z3_L_UNDEF) | |
| dict | _on_models = {} |
| _on_model_eh = on_model_eh_type(_global_on_model) | |
| _dflt_rounding_mode = Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN | |
| Floating-Point Arithmetic. | |
| int | _dflt_fpsort_ebits = 11 |
| int | _dflt_fpsort_sbits = 53 |
| _ROUNDING_MODES | |
| _my_hacky_class = None | |
| _on_clause_eh = Z3_on_clause_eh(on_clause_eh) | |
| _prop_closures = None | |
| _user_prop_push = Z3_push_eh(user_prop_push) | |
| _user_prop_pop = Z3_pop_eh(user_prop_pop) | |
| _user_prop_fresh = Z3_fresh_eh(user_prop_fresh) | |
| _user_prop_fixed = Z3_fixed_eh(user_prop_fixed) | |
| _user_prop_created = Z3_created_eh(user_prop_created) | |
| _user_prop_final = Z3_final_eh(user_prop_final) | |
| _user_prop_eq = Z3_eq_eh(user_prop_eq) | |
| _user_prop_diseq = Z3_eq_eh(user_prop_diseq) | |
| _user_prop_decide = Z3_decide_eh(user_prop_decide) | |
| _user_prop_binding = Z3_on_binding_eh(user_prop_binding) | |
|
protected |
Definition at line 9237 of file z3py.py.
|
protected |
Definition at line 4948 of file z3py.py.
Referenced by ArrayRef.__getitem__(), and QuantifierRef.__getitem__().
|
protected |
Definition at line 522 of file z3py.py.
Referenced by _to_ast_ref(), is_app(), and is_var().
|
protected |
Definition at line 4470 of file z3py.py.
Referenced by BVAddNoOverflow(), BVAddNoUnderflow(), BVMulNoOverflow(), BVMulNoUnderflow(), BvNand(), BvNor(), BVSDivNoOverflow(), BVSubNoOverflow(), BVSubNoUnderflow(), BvXnor(), LShR(), RotateLeft(), RotateRight(), SRem(), UDiv(), UGE(), UGT(), ULE(), ULT(), and URem().
|
protected |
|
protected |
Definition at line 1305 of file z3py.py.
Referenced by _coerce_exprs().
|
protected |
|
protected |
Definition at line 1357 of file z3py.py.
Referenced by And(), Distinct(), and Or().
|
protected |
Definition at line 1287 of file z3py.py.
Referenced by _coerce_exprs().
|
protected |
Definition at line 1318 of file z3py.py.
Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), ArithRef.__gt__(), BitVecRef.__gt__(), ArithRef.__le__(), BitVecRef.__le__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), BVAddNoOverflow(), BVAddNoUnderflow(), BVMulNoOverflow(), BVMulNoUnderflow(), BvNand(), BvNor(), BVSDivNoOverflow(), BVSubNoOverflow(), BVSubNoUnderflow(), BvXnor(), Extract(), If(), LShR(), RotateLeft(), RotateRight(), SRem(), UDiv(), UGE(), UGT(), ULE(), ULT(), and URem().
|
protected |
Definition at line 10298 of file z3py.py.
|
protected |
Definition at line 11877 of file z3py.py.
Referenced by Concat().
|
protected |
Definition at line 528 of file z3py.py.
Referenced by _coerce_expr_list(), _ctx_from_ast_args(), And(), ComplexVal(), Distinct(), FiniteSetDifference(), FiniteSetFilter(), FiniteSetIntersect(), FiniteSetMap(), FiniteSetMember(), FiniteSetRange(), FiniteSetSubset(), FiniteSetUnion(), If(), Implies(), IsMember(), IsSubset(), Not(), Or(), SetAdd(), SetDel(), SetDifference(), SetIntersect(), SetUnion(), and Xor().
|
protected |
|
protected |
|
protected |
|
protected |
Definition at line 10163 of file z3py.py.
|
protected |
Definition at line 10147 of file z3py.py.
|
protected |
Definition at line 152 of file z3py.py.
Referenced by FuncDeclRef.__call__(), And(), ArraySort(), Goal.assert_exprs(), Solver.assert_exprs(), Solver.check(), Concat(), CreateDatatypes(), Distinct(), FreshFunction(), Function(), Map(), Or(), RecAddDefinition(), RecFunction(), Select(), SetIntersect(), SetUnion(), and Update().
|
protected |
|
protected |
Definition at line 287 of file z3py.py.
Referenced by And(), BitVec(), BitVecs(), BitVecSort(), BitVecVal(), Bool(), Bools(), BoolSort(), BoolVal(), Cbrt(), Complex(), ComplexSort(), ComplexVal(), DatatypeSort(), DeclareSort(), DeclareTypeVar(), EnumSort(), FreshBool(), FreshConst(), FreshInt(), FreshReal(), get_ctx(), If(), Implies(), Int(), Ints(), IntSort(), IntVal(), IntVector(), Model(), Not(), Or(), Real(), Reals(), RealSort(), RealVal(), RealVector(), Sqrt(), to_symbol(), and Xor().
|
protected |
|
protected |
|
protected |
Return `True` if one of the elements of the given collection is a Z3 probe.
Definition at line 2001 of file z3py.py.
|
protected |
Definition at line 2910 of file z3py.py.
Referenced by _to_expr_ref(), and is_algebraic_value().
|
protected |
Definition at line 76 of file z3py.py.
Referenced by ModelRef.__getitem__(), ParamDescrsRef.__getitem__(), _py2expr(), Extract(), RatVal(), RepeatBitVec(), ParamsRef.set(), SignExt(), to_symbol(), and ZeroExt().
|
protected |
Definition at line 2906 of file z3py.py.
Referenced by _to_expr_ref(), is_bv_value(), is_int_value(), and is_rational_value().
|
protected |
Definition at line 1558 of file z3py.py.
Referenced by ArithRef.__add__(), ArithRef.__mul__(), ArithRef.__radd__(), ArithRef.__rmul__(), ArithRef.__rsub__(), and ArithRef.__sub__().
|
protected |
Definition at line 11169 of file z3py.py.
|
protected |
Definition at line 11178 of file z3py.py.
|
protected |
Definition at line 11186 of file z3py.py.
|
protected |
Definition at line 11194 of file z3py.py.
|
protected |
Definition at line 11152 of file z3py.py.
|
protected |
Definition at line 11161 of file z3py.py.
|
protected |
Definition at line 2358 of file z3py.py.
|
protected |
Definition at line 9245 of file z3py.py.
|
protected |
Definition at line 9936 of file z3py.py.
|
protected |
|
protected |
Definition at line 9650 of file z3py.py.
|
protected |
|
protected |
Version of function `prove` that renders HTML.
Definition at line 10127 of file z3py.py.
|
protected |
Definition at line 3402 of file z3py.py.
Referenced by _coerce_expr_list(), _coerce_exprs(), FiniteSetSortRef.cast(), IsMember(), K(), SetAdd(), SetDel(), and ModelRef.update_value().
|
protected |
Definition at line 1350 of file z3py.py.
Referenced by _coerce_expr_list().
|
protected |
|
protected |
Version of function `solve` that renders HTML output.
Definition at line 10078 of file z3py.py.
|
protected |
Version of function `solve_using` that renders HTML.
Definition at line 10102 of file z3py.py.
|
protected |
Sorts.
Definition at line 586 of file z3py.py.
Referenced by _to_sort_ref().
|
protected |
Convert a Z3 symbol back into a Python object.
Definition at line 140 of file z3py.py.
Referenced by ParamDescrsRef.get_name(), SortRef.name(), FuncDeclRef.params(), QuantifierRef.qid(), QuantifierRef.skolem_id(), and QuantifierRef.var_name().
|
protected |
Definition at line 554 of file z3py.py.
Referenced by ExprRef.__ne__(), _array_select(), _mk_quantifier(), And(), Distinct(), Map(), MultiPattern(), Or(), SetIntersect(), SetUnion(), and Update().
|
protected |
Definition at line 570 of file z3py.py.
Referenced by AstRef.__deepcopy__(), AstMap.__getitem__(), AstVector.__getitem__(), and AstRef.translate().
|
protected |
Definition at line 1229 of file z3py.py.
Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), ArithRef.__div__(), ArithRef.__mul__(), ArithRef.__neg__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmul__(), ArithRef.__rsub__(), ArithRef.__sub__(), _array_select(), _to_ast_ref(), ExprRef.arg(), FuncEntry.arg_value(), QuantifierRef.body(), Const(), ArrayRef.default(), FuncInterp.else_value(), ModelRef.eval(), Ext(), FreshConst(), Goal.get(), ModelRef.get_interp(), If(), ImagPart(), QuantifierRef.no_pattern(), ModelRef.project(), ModelRef.project_with_witness(), RealPart(), Update(), ExprRef.update(), DatatypeRef.update_field(), FuncEntry.value(), and Var().
|
protected |
Definition at line 10882 of file z3py.py.
|
protected |
|
protected |
Definition at line 970 of file z3py.py.
Referenced by _to_ast_ref().
|
protected |
|
protected |
Definition at line 3453 of file z3py.py.
Referenced by BitVecVal(), and IntVal().
|
protected |
Definition at line 178 of file z3py.py.
Referenced by Context.__init__(), and set_param().
|
protected |
Definition at line 2136 of file z3py.py.
Referenced by _mk_quantifier().
|
protected |
|
protected |
|
protected |
Definition at line 696 of file z3py.py.
Referenced by _sort(), _to_ast_ref(), FuncDeclRef.domain(), ArraySortRef.domain_n(), ModelRef.get_sort(), ArraySortRef.range(), FuncDeclRef.range(), and QuantifierRef.var_sort().
|
protected |
|
protected |
Datatypes.
Return `True` if acc is pair of the form (String, Datatype or Sort).
Definition at line 5636 of file z3py.py.
Referenced by Datatype.declare_core().
|
protected |
Definition at line 113 of file z3py.py.
Referenced by ModelRef.__getitem__(), QuantifierRef.__getitem__(), Context.__init__(), Goal.__init__(), ParamDescrsRef.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), _check_bv_args(), _coerce_expr_merge(), _coerce_exprs(), _ctx_from_ast_arg_list(), _mk_bin(), _mk_quantifier(), _py2expr(), _to_sort_ref(), _z3_check_cint_overflow(), DatatypeSortRef.accessor(), And(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), RatNumRef.as_long(), AsArray(), Solver.assert_and_track(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), FiniteSetSortRef.cast(), SortRef.cast(), ComplexVal(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), CreatePolymorphicDatatype(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), Distinct(), EnumSort(), AstRef.eq(), eq(), Ext(), Extract(), FreshConst(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), ImagPart(), IsInt(), K(), ExprRef.kind(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), QuantifierRef.pattern(), RatVal(), RealPart(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Update(), ExprRef.update(), DatatypeRef.update_field(), ParamsRef.validate(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
|
protected |
| Abs | ( | arg | ) |
Create the absolute value of an arithmetic expression
Definition at line 9888 of file z3py.py.
Referenced by ArithRef.__abs__().
| AllChar | ( | regex_sort, | |
| ctx = None ) |
Create a regular expression that accepts all single character strings
Definition at line 12386 of file z3py.py.
| And | ( | * | args | ) |
Create a Z3 and-expression or and-probe.
>>> p, q, r = Bools('p q r')
>>> And(p, q, r)
And(p, q, r)
>>> P = BoolVector('p', 5)
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)
Definition at line 2009 of file z3py.py.
Referenced by BoolRef.__and__(), and Goal.as_expr().
| 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 9253 of file z3py.py.
| append_log | ( | s | ) |
Append user-defined string to interaction log.
Definition at line 127 of file z3py.py.
| 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 6195 of file z3py.py.
Referenced by Solver.set().
| Array | ( | name, | |
| * | sorts ) |
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 5085 of file z3py.py.
| 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)) >>> ArraySort(IntSort(), BoolSort(), RealSort()) Array(Int, Bool, Real)
Definition at line 5050 of file z3py.py.
Referenced by SortRef.__gt__(), Array(), and SetSort().
| AsArray | ( | f | ) |
Return a Z3 as-array expression for the given function declaration.
>>> f = Function('f', IntSort(), IntSort())
>>> a = AsArray(f)
>>> a.sort()
Array(Int, Int)
>>> is_as_array(a)
True
>>> get_as_array_func(a) == f
True
Definition at line 5232 of file z3py.py.
Referenced by FiniteSetFilter(), and FiniteSetMap().
| AtLeast | ( | * | args | ) |
Create an at-least Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)
Definition at line 9911 of file z3py.py.
| 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 9893 of file z3py.py.
| 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 4325 of file z3py.py.
Referenced by BitVecs().
| 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 4349 of file z3py.py.
| 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 4293 of file z3py.py.
Referenced by BitVec(), and BitVecVal().
| 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 4308 of file z3py.py.
| Bool | ( | name, | |
| ctx = None ) |
Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
>>> p = Bool('p')
>>> q = Bool('q')
>>> And(p, q)
And(p, q)
Definition at line 1888 of file z3py.py.
Referenced by Solver.assert_and_track(), Bools(), and BoolVector().
| 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 1900 of file z3py.py.
| 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 1851 of file z3py.py.
Referenced by Goal.assert_exprs(), Solver.assert_exprs(), Bool(), Solver.check(), FreshBool(), If(), Implies(), Not(), SetSort(), and Xor().
| BoolVal | ( | val, | |
| ctx = None ) |
Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used. >>> BoolVal(True) True >>> is_true(BoolVal(True)) True >>> is_true(True) False >>> is_false(BoolVal(False)) True
Definition at line 1869 of file z3py.py.
Referenced by _mk_quantifier(), _py2expr(), and Goal.as_expr().
| 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 1916 of file z3py.py.
| 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 4261 of file z3py.py.
| BVAddNoOverflow | ( | a, | |
| b, | |||
| signed ) |
A predicate the determines that bit-vector addition does not overflow
Definition at line 4809 of file z3py.py.
| BVAddNoUnderflow | ( | a, | |
| b ) |
A predicate the determines that signed bit-vector addition does not underflow
Definition at line 4816 of file z3py.py.
| BVMulNoOverflow | ( | a, | |
| b, | |||
| signed ) |
A predicate the determines that bit-vector multiplication does not overflow
Definition at line 4851 of file z3py.py.
| BVMulNoUnderflow | ( | a, | |
| b ) |
A predicate the determines that bit-vector signed multiplication does not underflow
Definition at line 4858 of file z3py.py.
| BvNand | ( | a, | |
| b ) |
Return the bitwise NAND of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvNand(x, y)
bvnand(x, y)
Definition at line 4770 of file z3py.py.
| BvNor | ( | a, | |
| b ) |
Return the bitwise NOR of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvNor(x, y)
bvnor(x, y)
Definition at line 4783 of file z3py.py.
| BVRedAnd | ( | a | ) |
Return the reduction-and expression of `a`.
Definition at line 4756 of file z3py.py.
| BVRedOr | ( | a | ) |
Return the reduction-or expression of `a`.
Definition at line 4763 of file z3py.py.
| BVSDivNoOverflow | ( | a, | |
| b ) |
A predicate the determines that bit-vector signed division does not overflow
Definition at line 4837 of file z3py.py.
| BVSNegNoOverflow | ( | a | ) |
A predicate the determines that bit-vector unary negation does not overflow
Definition at line 4844 of file z3py.py.
| BVSubNoOverflow | ( | a, | |
| b ) |
A predicate the determines that bit-vector subtraction does not overflow
Definition at line 4823 of file z3py.py.
| BVSubNoUnderflow | ( | a, | |
| b, | |||
| signed ) |
A predicate the determines that bit-vector subtraction does not underflow
Definition at line 4830 of file z3py.py.
| BvXnor | ( | a, | |
| b ) |
Return the bitwise XNOR of `a` and `b`.
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> BvXnor(x, y)
bvxnor(x, y)
Definition at line 4796 of file z3py.py.
| 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 3707 of file z3py.py.
| CharFromBv | ( | bv | ) |
| CharIsDigit | ( | ch, | |
| ctx = None ) |
| CharSort | ( | ctx = None | ) |
| CharToBv | ( | ch, | |
| ctx = None ) |
| CharToInt | ( | ch, | |
| ctx = None ) |
| CharVal | ( | ch, | |
| ctx = None ) |
| Complement | ( | re | ) |
| Complex | ( | name, | |
| ctx = None ) |
Create a named Complex constant.
Definition at line 3357 of file z3py.py.
Referenced by Complexes().
| Complexes | ( | names, | |
| ctx = None ) |
Create Complex constants from a space-separated string or list of names.
Definition at line 3363 of file z3py.py.
| ComplexSort | ( | ctx = None | ) |
Return the Complex sort in the given context.
Definition at line 3351 of file z3py.py.
Referenced by Complex().
| ComplexVal | ( | real, | |
| imag = 0, | |||
| ctx = None ) |
Construct a Complex value or expression from Int or Real components.
A Python complex value may be passed as the sole component argument.
>>> z = ComplexVal("1/2", 2)
>>> simplify(RealPart(z))
1/2
>>> simplify(ImagPart(z))
2
Definition at line 3370 of file z3py.py.
Referenced by _coerce_expr_list(), _coerce_exprs(), and _py2expr().
| 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 4370 of file z3py.py.
| 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 9710 of file z3py.py.
Referenced by If().
| Const | ( | name, | |
| sort ) |
Create a constant of the given sort.
>>> Const('x', IntSort())
x
Definition at line 1567 of file z3py.py.
Referenced by Consts().
| 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 1579 of file z3py.py.
| 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 12047 of file z3py.py.
| 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 5771 of file z3py.py.
Referenced by Datatype.create().
| CreatePolymorphicDatatype | ( | d, | |
| type_params ) |
Create a single polymorphic Z3 datatype with explicit type parameters.
`d` is a `Datatype` helper object whose constructors have been declared.
`type_params` is a list of type variables created with `DeclareTypeVar`.
Constructor field sorts may reference these type variables, and self-recursive
fields may reference `d` directly.
>>> A = DeclareTypeVar('A')
>>> Pair = Datatype('Pair')
>>> Pair.declare('pair', ('fst', A), ('snd', A))
>>> Pair = CreatePolymorphicDatatype(Pair, [A])
Definition at line 5867 of file z3py.py.
Referenced by Datatype.create_polymorphic().
| DatatypeSort | ( | name, | |
| params = None, | |||
| ctx = None ) |
Create a reference to a sort that was declared, or will be declared, as a recursive datatype.
Args:
name: name of the datatype sort
params: optional list/tuple of sort parameters for parametric datatypes
ctx: Z3 context (optional)
Example:
>>> # Non-parametric datatype
>>> TreeRef = DatatypeSort('Tree')
>>> # Parametric datatype with one parameter
>>> ListIntRef = DatatypeSort('List', [IntSort()])
>>> # Parametric datatype with multiple parameters
>>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()])
Definition at line 6067 of file z3py.py.
| SortRef 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 737 of file z3py.py.
| DeclareTypeVar | ( | name, | |
| ctx = None ) |
Create a new type variable named `name`. If `ctx=None`, then the new sort is declared in the global Z3Py context.
Definition at line 765 of file z3py.py.
| Default | ( | a | ) |
Return a default value for array expression. >>> b = K(IntSort(), 1) >>> prove(Default(b) == 1) proved
Definition at line 5131 of file z3py.py.
| describe_probes | ( | ) |
Display a (tabular) description of all available probes in Z3.
Definition at line 9631 of file z3py.py.
| describe_tactics | ( | ) |
Display a (tabular) description of all available tactics in Z3.
Definition at line 9425 of file z3py.py.
| deserialize | ( | st | ) |
inverse function to the serialize method on ExprRef. It is made available to make it easier for users to serialize expressions back and forth between strings. Solvers can be serialized using the 'sexpr()' method.
Definition at line 1215 of file z3py.py.
| Diff | ( | a, | |
| b, | |||
| ctx = None ) |
Create the difference regular expression
Definition at line 12378 of file z3py.py.
| disable_trace | ( | msg | ) |
Definition at line 87 of file z3py.py.
| 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 6104 of file z3py.py.
| 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 1534 of file z3py.py.
| Empty | ( | s | ) |
Create the empty sequence of the given sort
>>> e = Empty(StringSort())
>>> e2 = StringVal("")
>>> print(e.eq(e2))
True
>>> e3 = Empty(SeqSort(IntSort()))
>>> print(e3)
Empty(Seq(Int))
>>> e4 = Empty(ReSort(SeqSort(IntSort())))
>>> print(e4)
Empty(ReSort(Seq(Int)))
Definition at line 11977 of file z3py.py.
| EmptySet | ( | s | ) |
| enable_trace | ( | msg | ) |
Definition at line 83 of file z3py.py.
| ensure_prop_closures | ( | ) |
| 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 6116 of file z3py.py.
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 503 of file z3py.py.
| 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 2411 of file z3py.py.
| Ext | ( | a, | |
| b ) |
Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
>> Ext(a, b)
Ext(a, b)
Definition at line 5220 of file z3py.py.
| Extract | ( | high, | |
| low, | |||
| a ) |
Create a Z3 bit-vector extraction expression or sequence extraction expression.
Extract is overloaded to work with both bit-vectors and sequences:
**Bit-vector extraction**: Extract(high, low, bitvector)
Extracts bits from position `high` down to position `low` (both inclusive).
- high: int - the highest bit position to extract (0-indexed from right)
- low: int - the lowest bit position to extract (0-indexed from right)
- bitvector: BitVecRef - the bit-vector to extract from
Returns a new bit-vector containing bits [high:low]
**Sequence extraction**: Extract(sequence, offset, length)
Extracts a subsequence starting at the given offset with the specified length.
The functions SubString and SubSeq are redirected to this form of Extract.
- sequence: SeqRef or str - the sequence to extract from
- offset: int - the starting position (0-indexed)
- length: int - the number of elements to extract
Returns a new sequence containing the extracted subsequence
>>> # Bit-vector extraction examples
>>> x = BitVec('x', 8)
>>> Extract(6, 2, x) # Extract bits 6 down to 2 (5 bits total)
Extract(6, 2, x)
>>> Extract(6, 2, x).sort() # Result is a 5-bit vector
BitVec(5)
>>> Extract(7, 0, x) # Extract all 8 bits
Extract(7, 0, x)
>>> Extract(3, 3, x) # Extract single bit at position 3
Extract(3, 3, x)
>>> # Sequence extraction examples
>>> s = StringVal("hello")
>>> Extract(s, 1, 3) # Extract 3 characters starting at position 1
str.substr("hello", 1, 3)
>>> simplify(Extract(StringVal("abcd"), 2, 1)) # Extract 1 character at position 2
"c"
>>> simplify(Extract(StringVal("abcd"), 0, 2)) # Extract first 2 characters
"ab"
Definition at line 4416 of file z3py.py.
| 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 9668 of file z3py.py.
| FiniteDomainSort | ( | name, | |
| sz, | |||
| ctx = None ) |
Create a named finite domain sort of a given size sz
Definition at line 8566 of file z3py.py.
| 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 8636 of file z3py.py.
| FiniteFieldBitsum | ( | * | args | ) |
Definition at line 12862 of file z3py.py.
| FiniteFieldElem | ( | name, | |
| field, | |||
| ctx = None ) |
| FiniteFieldElems | ( | names, | |
| field, | |||
| ctx = None ) |
| FiniteFieldSort | ( | prime, | |
| ctx = None ) |
| FiniteFieldVal | ( | value, | |
| field, | |||
| ctx = None ) |
Definition at line 12842 of file z3py.py.
| FiniteSetDifference | ( | s1, | |
| s2 ) |
Create the set difference of two finite sets.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> b = Const('b', FiniteSetSort(IntSort()))
>>> FiniteSetDifference(a, b)
set.difference(a, b)
Definition at line 5551 of file z3py.py.
Referenced by FiniteSetRef.__sub__(), and SetDifference().
| FiniteSetEmpty | ( | set_sort | ) |
Create an empty finite set of the given sort. >>> s = FiniteSetSort(IntSort()) >>> FiniteSetEmpty(s) set.empty
Definition at line 5510 of file z3py.py.
Referenced by FiniteSetSortRef.cast(), and EmptySet().
| FiniteSetFilter | ( | f, | |
| set ) |
Filter a finite set using predicate f.
>>> f = Array('f', IntSort(), BoolSort())
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetFilter(f, a)
set.filter(f, a)
Definition at line 5608 of file z3py.py.
| FiniteSetIntersect | ( | s1, | |
| s2 ) |
Create the intersection of two finite sets.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> b = Const('b', FiniteSetSort(IntSort()))
>>> FiniteSetIntersect(a, b)
set.intersect(a, b)
Definition at line 5540 of file z3py.py.
Referenced by FiniteSetRef.__and__().
| FiniteSetMap | ( | f, | |
| set ) |
Apply function f to all elements of the finite set.
>>> f = Array('f', IntSort(), IntSort())
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetMap(f, a)
set.map(f, a)
Definition at line 5595 of file z3py.py.
| FiniteSetMember | ( | elem, | |
| set ) |
Check if elem is a member of the finite set.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetMember(IntVal(1), a)
set.in(1, a)
Definition at line 5562 of file z3py.py.
Referenced by In().
| FiniteSetRange | ( | low, | |
| high ) |
Create a finite set of integers in the range [low, high). >>> FiniteSetRange(IntVal(0), IntVal(5)) set.range(0, 5)
Definition at line 5621 of file z3py.py.
| FiniteSetSize | ( | set | ) |
Get the size (cardinality) of a finite set.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> FiniteSetSize(a)
set.size(a)
Definition at line 5574 of file z3py.py.
| FiniteSetSort | ( | elem_sort | ) |
Create a finite set sort over element sort elem_sort. >>> s = FiniteSetSort(IntSort()) >>> s FiniteSet(Int)
Definition at line 5501 of file z3py.py.
| FiniteSetSubset | ( | s1, | |
| s2 ) |
Check if s1 is a subset of s2.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> b = Const('b', FiniteSetSort(IntSort()))
>>> FiniteSetSubset(a, b)
set.subset(a, b)
Definition at line 5584 of file z3py.py.
| FiniteSetUnion | ( | s1, | |
| s2 ) |
Create the union of two finite sets.
>>> a = Const('a', FiniteSetSort(IntSort()))
>>> b = Const('b', FiniteSetSort(IntSort()))
>>> FiniteSetUnion(a, b)
set.union(a, b)
Definition at line 5529 of file z3py.py.
Referenced by FiniteSetRef.__or__(), and FiniteSetSortRef.cast().
| Float128 | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 10396 of file z3py.py.
| Float16 | ( | ctx = None | ) |
| Float32 | ( | ctx = None | ) |
| Float64 | ( | ctx = None | ) |
| FloatDouble | ( | ctx = None | ) |
Floating-point 64-bit (double) sort.
Definition at line 10390 of file z3py.py.
| FloatHalf | ( | ctx = None | ) |
| FloatQuadruple | ( | ctx = None | ) |
Floating-point 128-bit (quadruple) sort.
Definition at line 10402 of file z3py.py.
| FloatSingle | ( | ctx = None | ) |
Floating-point 32-bit (single) sort.
Definition at line 10378 of file z3py.py.
| 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 2393 of file z3py.py.
| 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 11070 of file z3py.py.
| 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 11113 of file z3py.py.
| fpAdd | ( | rm, | |
| a, | |||
| b, | |||
| ctx = None ) |
Create a Z3 floating-point addition expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpAdd(rm, x, y)
x + y
>>> fpAdd(RTZ(), x, y) # default rounding mode is RTZ
fpAdd(RTZ(), x, y)
>>> fpAdd(rm, x, y).sort()
FPSort(8, 24)
Definition at line 11204 of file z3py.py.
| 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 11526 of file z3py.py.
| fpDiv | ( | rm, | |
| a, | |||
| b, | |||
| ctx = None ) |
Create a Z3 floating-point division expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpDiv(rm, x, y)
x / y
>>> fpDiv(rm, x, y).sort()
FPSort(8, 24)
Definition at line 11251 of file z3py.py.
| 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 11434 of file z3py.py.
| fpFMA | ( | rm, | |
| a, | |||
| b, | |||
| c, | |||
| ctx = None ) |
| 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 11458 of file z3py.py.
| 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 11543 of file z3py.py.
| 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 11422 of file z3py.py.
| 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 11410 of file z3py.py.
| fpInfinity | ( | s, | |
| negative ) |
Create a Z3 floating-point +oo or -oo term.
Definition at line 10971 of file z3py.py.
| 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 11340 of file z3py.py.
| 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 11328 of file z3py.py.
| fpIsNegative | ( | a, | |
| ctx = None ) |
| fpIsNormal | ( | a, | |
| ctx = None ) |
| fpIsPositive | ( | a, | |
| ctx = None ) |
| fpIsSubnormal | ( | a, | |
| ctx = None ) |
| fpIsZero | ( | a, | |
| ctx = None ) |
| 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 11398 of file z3py.py.
| 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 11386 of file z3py.py.
| 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 11295 of file z3py.py.
| 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 11280 of file z3py.py.
| fpMinusInfinity | ( | s | ) |
| fpMinusZero | ( | s | ) |
Create a Z3 floating-point -0.0 term.
Definition at line 10984 of file z3py.py.
| fpMul | ( | rm, | |
| a, | |||
| b, | |||
| ctx = None ) |
Create a Z3 floating-point multiplication expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpMul(rm, x, y)
x * y
>>> fpMul(rm, x, y).sort()
FPSort(8, 24)
Definition at line 11236 of file z3py.py.
| fpNaN | ( | s | ) |
Create a Z3 floating-point NaN term. >>> s = FPSort(8, 24) >>> set_fpa_pretty(True) >>> fpNaN(s) NaN >>> pb = get_fpa_pretty() >>> set_fpa_pretty(False) >>> fpNaN(s) fpNaN(FPSort(8, 24)) >>> set_fpa_pretty(pb)
Definition at line 10931 of file z3py.py.
| 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 11136 of file z3py.py.
| 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 11446 of file z3py.py.
| 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 10948 of file z3py.py.
| fpPlusZero | ( | s | ) |
| 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 11563 of file z3py.py.
| 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 11266 of file z3py.py.
| fpRoundToIntegral | ( | rm, | |
| a, | |||
| ctx = None ) |
| 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)
(x + y) * z
Definition at line 11094 of file z3py.py.
| 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 11581 of file z3py.py.
| 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 10867 of file z3py.py.
| fpSqrt | ( | rm, | |
| a, | |||
| ctx = None ) |
| fpSub | ( | rm, | |
| a, | |||
| b, | |||
| ctx = None ) |
Create a Z3 floating-point subtraction expression.
>>> s = FPSort(8, 24)
>>> rm = RNE()
>>> x = FP('x', s)
>>> y = FP('y', s)
>>> fpSub(rm, x, y)
x - y
>>> fpSub(rm, x, y).sort()
FPSort(8, 24)
Definition at line 11221 of file z3py.py.
| 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 11487 of file z3py.py.
| fpToFPUnsigned | ( | rm, | |
| x, | |||
| s, | |||
| ctx = None ) |
Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression.
Definition at line 11617 of file z3py.py.
| 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 11691 of file z3py.py.
| 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 11671 of file z3py.py.
| 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 11627 of file z3py.py.
| 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 11649 of file z3py.py.
| 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 11599 of file z3py.py.
| FPVal | ( | sig, | |
| exp = None, | |||
| fps = None, | |||
| ctx = None ) |
Return a floating-point value of value `sig * 2**exp` and sort `fps`.
If `exp=None`, then the exponent is zero.
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
>>> FPVal(1.0, 3, Float32())
1*(2**3)
>>> FPVal(1, 3, Float32())
1*(2**3)
>>> FPVal("1.5", -2, Float32())
1.5*(2**-2)
>>> FPVal("1.25*(2**4)", 1, Float32())
1.25*(2**5)
>>> FPVal("1.25*(2**4)", -4, Float32())
1.25
>>> FPVal("1p2", 3, Float32())
1*(2**5)
>>> FPVal("1P2", 3, Float32())
1*(2**5)
>>> FPVal("1.5p-2", 2, Float32())
1.5
>>> FPVal(1.5, 0, Float32())
1.5
>>> FPVal(1.5, fps=Float32())
1.5
>>> [FPVal(v, 3, Float32()) for v in
... [float("nan"), float("inf"), float("-inf"), 0.0, -0.0]]
[NaN, +oo, -oo, +0.0, -0.0]
>>> [FPVal(v, -2, Float32()) for v in
... ["NaN", "+oo", "-oo", "+0.0", "-0.0"]]
[NaN, +oo, -oo, +0.0, -0.0]
Definition at line 10997 of file z3py.py.
| fpZero | ( | s, | |
| negative ) |
Create a Z3 floating-point +0.0 or -0.0 term.
Definition at line 10990 of file z3py.py.
| 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 1931 of file z3py.py.
| FreshConst | ( | sort, | |
| prefix = "c" ) |
Create a fresh constant of a specified sort
Definition at line 1594 of file z3py.py.
| FreshFunction | ( | * | sig | ) |
Create a new fresh Z3 uninterpreted function with the given sorts.
Definition at line 951 of file z3py.py.
| 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 3568 of file z3py.py.
| 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 3625 of file z3py.py.
| Full | ( | s | ) |
Create the regular expression that accepts the universal language >>> e = Full(ReSort(SeqSort(IntSort()))) >>> print(e) Full(ReSort(Seq(Int))) >>> e1 = Full(ReSort(StringSort())) >>> print(e1) Full(ReSort(String))
Definition at line 11997 of file z3py.py.
| FullSet | ( | s | ) |
| 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 928 of file z3py.py.
| get_as_array_func | ( | n | ) |
Return the function declaration f associated with a Z3 expression of the form (_ as-array f).
Definition at line 7483 of file z3py.py.
Referenced by ModelRef.get_interp().
| Context get_ctx | ( | ctx | ) |
| get_default_fp_sort | ( | ctx = None | ) |
| get_default_rounding_mode | ( | ctx = None | ) |
Retrieves the global default rounding mode.
Definition at line 10246 of file z3py.py.
| get_full_version | ( | ) |
| 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 5026 of file z3py.py.
| get_param | ( | name | ) |
Return the value of a Z3 global (or module) parameter
>>> get_param('nlsat.reorder')
'true'
Definition at line 334 of file z3py.py.
| 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 1465 of file z3py.py.
| get_version | ( | ) |
Definition at line 100 of file z3py.py.
| get_version_string | ( | ) |
Definition at line 91 of file z3py.py.
| help_simplify | ( | ) |
Return a string describing all options available for Z3 `simplify` procedure.
Definition at line 9752 of file z3py.py.
| 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 1511 of file z3py.py.
Referenced by BoolRef.__add__(), ArithRef.__mul__(), BoolRef.__mul__(), and ToReal().
| ImagPart | ( | value | ) |
Return the Real-valued imaginary component of a Complex expression.
Definition at line 3396 of file z3py.py.
Referenced by ComplexRef.imag_part().
| Implies | ( | a, | |
| b, | |||
| ctx = None ) |
Create a Z3 implies expression.
>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
Definition at line 1945 of file z3py.py.
| In | ( | elem, | |
| set ) |
| IndexOf | ( | s, | |
| substr, | |||
| offset = None ) |
Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4
Definition at line 12081 of file z3py.py.
| InRe | ( | s, | |
| re ) |
Create regular expression membership test
>>> re = Union(Re("a"),Re("b"))
>>> print (simplify(InRe("a", re)))
True
>>> print (simplify(InRe("b", re)))
True
>>> print (simplify(InRe("c", re)))
False
Definition at line 12230 of file z3py.py.
| 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 3529 of file z3py.py.
Referenced by Ints(), and IntVector().
| 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 4284 of file z3py.py.
| Intersect | ( | * | args | ) |
Create intersection of regular expressions.
>>> re = Intersect(Re("a"), Re("b"), Re("c"))
Definition at line 12272 of file z3py.py.
| 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 3542 of file z3py.py.
| 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 3419 of file z3py.py.
Referenced by FreshInt(), and Int().
| IntToStr | ( | s | ) |
| IntVal | ( | val, | |
| ctx = None ) |
Return a Z3 integer value. If `ctx=None`, then the global context is used.
>>> IntVal(1)
1
>>> IntVal("100")
100
Definition at line 3465 of file z3py.py.
Referenced by BoolRef.__mul__(), and _py2expr().
| 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 3555 of file z3py.py.
| bool is_add | ( | Any | a | ) |
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 2974 of file z3py.py.
| 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 2960 of file z3py.py.
| bool is_and | ( | Any | a | ) |
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 1781 of file z3py.py.
| is_app | ( | a | ) |
Return `True` if `a` is a Z3 function application.
Note that, constants are function applications with 0 arguments.
>>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')
>>> is_app(ForAll(x, x >= 0))
False
Definition at line 1395 of file z3py.py.
Referenced by _mk_quantifier(), ExprRef.arg(), ExprRef.children(), ExprRef.decl(), is_app_of(), is_const(), ExprRef.kind(), Lambda(), ExprRef.num_args(), RecAddDefinition(), and ExprRef.update().
| 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 1498 of file z3py.py.
Referenced by is_add(), is_and(), is_const_array(), is_default(), is_distinct(), is_div(), is_eq(), is_false(), is_ge(), is_gt(), is_idiv(), is_implies(), is_is_int(), is_K(), is_le(), is_lt(), is_map(), is_mod(), is_mul(), is_not(), is_or(), is_select(), is_store(), is_sub(), is_to_int(), is_to_real(), and is_true().
| is_arith | ( | a | ) |
Return `True` if `a` is an arithmetical expression.
>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True
Definition at line 2847 of file z3py.py.
Referenced by is_algebraic_value(), is_int(), is_int_value(), is_rational_value(), and is_real().
| bool is_arith_sort | ( | Any | 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 2535 of file z3py.py.
Referenced by ArithSortRef.subsort().
| bool is_array | ( | Any | a | ) |
Return `True` if `a` is a Z3 array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> is_array(a)
True
>>> is_array(Store(a, 0, 1))
True
>>> is_array(a[0])
False
Definition at line 4961 of file z3py.py.
| is_as_array | ( | n | ) |
Return true if n is a Z3 expression of the form (_ as-array f).
Definition at line 7478 of file z3py.py.
Referenced by get_as_array_func(), and ModelRef.get_interp().
| bool is_ast | ( | Any | a | ) |
Return `True` if `a` is an AST node.
>>> is_ast(10)
False
>>> is_ast(IntVal(10))
True
>>> is_ast(Int('x'))
True
>>> is_ast(BoolSort())
True
>>> is_ast(Function('f', IntSort(), IntSort()))
True
>>> is_ast("x")
False
>>> is_ast(Solver())
False
Definition at line 482 of file z3py.py.
Referenced by _ast_kind(), _ctx_from_ast_arg_list(), AstRef.eq(), and eq().
| bool is_bool | ( | Any | a | ) |
Return `True` if `a` is a Z3 Boolean expression.
>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True
Definition at line 1731 of file z3py.py.
Referenced by _mk_quantifier().
| is_bv | ( | a | ) |
Return `True` if `a` is a Z3 bit-vector expression.
>>> b = BitVec('b', 32)
>>> is_bv(b)
True
>>> is_bv(b + 10)
True
>>> is_bv(Int('x'))
False
Definition at line 4232 of file z3py.py.
Referenced by _check_bv_args(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), Concat(), Extract(), is_bv_value(), RepeatBitVec(), SignExt(), and ZeroExt().
| is_bv_sort | ( | s | ) |
Return True if `s` is a Z3 bit-vector sort. >>> is_bv_sort(BitVecSort(32)) True >>> is_bv_sort(IntSort()) False
Definition at line 3759 of file z3py.py.
Referenced by BitVecVal(), and BitVecSortRef.subsort().
| 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 4246 of file z3py.py.
| is_complex | ( | a | ) |
Return whether `a` is a Complex expression.
Definition at line 3346 of file z3py.py.
Referenced by ImagPart(), and RealPart().
| is_complex_sort | ( | s | ) |
Return whether `s` is a Complex sort.
Definition at line 3341 of file z3py.py.
Referenced by ArithSortRef.subsort().
| is_const | ( | a | ) |
Return `True` if `a` is Z3 constant/variable expression.
>>> a = Int('a')
>>> is_const(a)
True
>>> is_const(a + 1)
False
>>> is_const(1)
False
>>> is_const(IntVal(1))
True
>>> x = Int('x')
>>> is_const(ForAll(x, x >= 0))
False
Definition at line 1421 of file z3py.py.
Referenced by ModelRef.__getitem__(), _mk_quantifier(), Solver.assert_and_track(), and ModelRef.get_interp().
| 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 4975 of file z3py.py.
| is_default | ( | a | ) |
Return `True` if `a` is a Z3 default array expression. >>> d = Default(K(IntSort(), 10)) >>> is_default(d) True
Definition at line 5017 of file z3py.py.
| bool is_distinct | ( | Any | 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 1839 of file z3py.py.
| bool is_div | ( | Any | a | ) |
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 3010 of file z3py.py.
| bool is_eq | ( | Any | a | ) |
Return `True` if `a` is a Z3 equality expression.
>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
Definition at line 1829 of file z3py.py.
Referenced by AstRef.__bool__().
| is_expr | ( | a | ) |
Return `True` if `a` is a Z3 expression.
>>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')
>>> is_expr(ForAll(x, x >= 0))
True
>>> is_expr(FPVal(1.0))
True
Definition at line 1372 of file z3py.py.
Referenced by _coerce_expr_list(), _coerce_expr_merge(), _coerce_exprs(), _mk_quantifier(), _py2expr(), ArithSortRef.cast(), BitVecSortRef.cast(), ComplexSortRef.cast(), FiniteSetSortRef.cast(), SortRef.cast(), Cbrt(), Concat(), is_var(), K(), MultiPattern(), Sqrt(), ExprRef.update(), DatatypeRef.update_field(), and ModelRef.update_value().
| bool is_false | ( | Any | a | ) |
Return `True` if `a` is the Z3 false expression.
>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True
Definition at line 1767 of file z3py.py.
Referenced by AstRef.__bool__(), and BoolRef.py_value().
| 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 8597 of file z3py.py.
| 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 8574 of file z3py.py.
| 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 8651 of file z3py.py.
| is_finite_set | ( | a | ) |
Return True if a is a Z3 finite set expression. >>> s = FiniteSetSort(IntSort()) >>> is_finite_set(FiniteSetEmpty(s)) True >>> is_finite_set(IntVal(1)) False
Definition at line 5461 of file z3py.py.
Referenced by IsMember(), IsSubset(), SetAdd(), SetDel(), SetDifference(), SetIntersect(), and SetUnion().
| is_finite_set_sort | ( | s | ) |
Return True if s is a Z3 finite set sort. >>> is_finite_set_sort(FiniteSetSort(IntSort())) True >>> is_finite_set_sort(IntSort()) False
Definition at line 5472 of file z3py.py.
Referenced by EmptySet().
| is_fp | ( | a | ) |
Return `True` if `a` is a Z3 floating-point expression.
>>> b = FP('b', FPSort(8, 24))
>>> is_fp(b)
True
>>> is_fp(b + 1.0)
True
>>> is_fp(Int('x'))
False
Definition at line 10838 of file z3py.py.
| is_fp_sort | ( | s | ) |
Return True if `s` is a Z3 floating-point sort. >>> is_fp_sort(FPSort(8, 24)) True >>> is_fp_sort(IntSort()) False
Definition at line 10412 of file z3py.py.
| 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 10852 of file z3py.py.
| is_fprm | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode expression. >>> rm = RNE() >>> is_fprm(rm) True >>> rm = 1.0 >>> is_fprm(rm) False
Definition at line 10672 of file z3py.py.
| 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 10423 of file z3py.py.
| is_fprm_value | ( | a | ) |
Return `True` if `a` is a Z3 floating-point rounding mode numeral value.
Definition at line 10685 of file z3py.py.
| 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 915 of file z3py.py.
Referenced by Map(), DatatypeRef.update_field(), and ModelRef.update_value().
| bool is_ge | ( | Any | a | ) |
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 3075 of file z3py.py.
| bool is_gt | ( | Any | a | ) |
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 3087 of file z3py.py.
| bool is_idiv | ( | Any | a | ) |
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 3027 of file z3py.py.
| bool is_implies | ( | Any | a | ) |
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 1805 of file z3py.py.
| bool is_int | ( | a | ) |
Return `True` if `a` is an integer expression.
>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False
Definition at line 2868 of file z3py.py.
| 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 2914 of file z3py.py.
| bool is_is_int | ( | Any | a | ) |
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 3099 of file z3py.py.
| is_K | ( | a | ) |
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 4988 of file z3py.py.
| bool is_le | ( | Any | a | ) |
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 3051 of file z3py.py.
| bool is_lt | ( | Any | a | ) |
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 3063 of file z3py.py.
| is_map | ( | a | ) |
Return `True` if `a` is a Z3 map array expression.
>>> f = Function('f', IntSort(), IntSort())
>>> b = Array('b', IntSort(), IntSort())
>>> a = Map(f, b)
>>> a
Map(f, b)
>>> is_map(a)
True
>>> is_map(b)
False
Definition at line 5001 of file z3py.py.
Referenced by get_map_func().
| bool is_mod | ( | Any | a | ) |
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 3039 of file z3py.py.
| bool is_mul | ( | Any | a | ) |
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 2986 of file z3py.py.
| bool is_not | ( | Any | a | ) |
Return `True` if `a` is a Z3 not expression.
>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True
Definition at line 1817 of file z3py.py.
Referenced by mk_not().
| bool is_or | ( | Any | a | ) |
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 1793 of file z3py.py.
| is_pattern | ( | a | ) |
Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
>>> q
ForAll(x, f(x) == 0)
>>> q.num_patterns()
1
>>> is_pattern(q.pattern(0))
True
>>> q.pattern(0)
f(Var(0))
Definition at line 2094 of file z3py.py.
Referenced by _mk_quantifier(), and _to_pattern().
| is_probe | ( | p | ) |
Return `True` if `p` is a Z3 probe.
>>> is_probe(Int('x'))
False
>>> is_probe(Probe('memory'))
True
Definition at line 9593 of file z3py.py.
Referenced by _ctx_from_ast_arg_list(), _has_probe(), and Not().
| 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 2344 of file z3py.py.
| 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 2938 of file z3py.py.
| is_re | ( | s | ) |
| is_real | ( | a | ) |
Return `True` if `a` is a real expression.
>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True
Definition at line 2887 of file z3py.py.
| is_select | ( | a | ) |
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 5250 of file z3py.py.
| is_seq | ( | a | ) |
Return `True` if `a` is a Z3 sequence expression.
>>> print (is_seq(Unit(IntVal(0))))
True
>>> print (is_seq(StringVal("abc")))
True
Definition at line 11898 of file z3py.py.
| bool is_sort | ( | Any | s | ) |
Return `True` if `s` is a Z3 sort.
>>> is_sort(IntSort())
True
>>> is_sort(Int('x'))
False
>>> is_expr(Int('x'))
True
Definition at line 683 of file z3py.py.
Referenced by _valid_accessor(), ArraySort(), CreateDatatypes(), CreatePolymorphicDatatype(), FreshConst(), FreshFunction(), Function(), K(), RecFunction(), and Var().
| is_store | ( | a | ) |
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 5263 of file z3py.py.
| bool is_string | ( | Any | a | ) |
Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
True
Definition at line 11908 of file z3py.py.
| bool is_string_value | ( | Any | 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 11916 of file z3py.py.
| bool is_sub | ( | Any | a | ) |
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 2998 of file z3py.py.
| bool is_to_int | ( | Any | a | ) |
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 3126 of file z3py.py.
| bool is_to_real | ( | Any | a | ) |
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 3111 of file z3py.py.
| bool is_true | ( | Any | a | ) |
Return `True` if `a` is the Z3 true expression.
>>> p = Bool('p')
>>> is_true(p)
False
>>> is_true(simplify(p == p))
True
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False
Definition at line 1749 of file z3py.py.
Referenced by AstRef.__bool__(), and BoolRef.py_value().
| is_var | ( | a | ) |
Return `True` if `a` is variable.
Z3 uses de-Bruijn indices for representing bound variables in
quantifiers.
>>> x = Int('x')
>>> is_var(x)
False
>>> is_const(x)
True
>>> f = Function('f', IntSort(), IntSort())
>>> # Z3 replaces x with bound variables when ForAll is executed.
>>> q = ForAll(x, f(x) == x)
>>> b = q.body()
>>> b
f(Var(0)) == Var(0)
>>> b.arg(1)
Var(0)
>>> is_var(b.arg(1))
True
Definition at line 1440 of file z3py.py.
Referenced by get_var_index().
| IsInt | ( | a | ) |
Return the Z3 predicate IsInt(a).
>>> x = Real('x')
>>> IsInt(x + "1/2")
IsInt(x + 1/2)
>>> solve(IsInt(x + "1/2"), x > 0, x < 1)
[x = 1/2]
>>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
no solution
Definition at line 3677 of file z3py.py.
| 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 5387 of file z3py.py.
| 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 5400 of file z3py.py.
| K | ( | dom, | |
| v ) |
Return a Z3 constant array expression.
>>> a = K(IntSort(), 10)
>>> a
K(Int, 10)
>>> a.sort()
Array(Int, Int)
>>> i = Int('i')
>>> a[i]
K(Int, 10)[i]
>>> simplify(a[i])
10
Definition at line 5198 of file z3py.py.
Referenced by ModelRef.get_interp().
| 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 2432 of file z3py.py.
| LastIndexOf | ( | s, | |
| substr ) |
Retrieve the last index of substring within a string
Definition at line 12101 of file z3py.py.
| Length | ( | s | ) |
Obtain the length of a sequence 's'
>>> l = Length(StringVal("abc"))
>>> simplify(l)
3
Definition at line 12110 of file z3py.py.
| LinearOrder | ( | a, | |
| index ) |
| 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 12348 of file z3py.py.
| LShR | ( | a, | |
| b ) |
Create the Z3 expression logical right shift.
Use the operator >> for the arithmetical right shift.
>>> x, y = BitVecs('x y', 32)
>>> LShR(x, y)
LShR(x, y)
>>> (x >> y).sexpr()
'(bvashr x y)'
>>> LShR(x, y).sexpr()
'(bvlshr x y)'
>>> BitVecVal(4, 3)
4
>>> BitVecVal(4, 3).as_signed_long()
-4
>>> simplify(BitVecVal(4, 3) >> 1).as_signed_long()
-2
>>> simplify(BitVecVal(4, 3) >> 1)
6
>>> simplify(LShR(BitVecVal(4, 3), 1))
2
>>> simplify(BitVecVal(2, 3) >> 1)
1
>>> simplify(LShR(BitVecVal(2, 3), 1))
1
Definition at line 4610 of file z3py.py.
| Context 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 266 of file z3py.py.
Referenced by _get_ctx().
| 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 5175 of file z3py.py.
| mk_not | ( | a | ) |
| Model | ( | ctx = None, | |
| eval = {} ) |
Definition at line 7470 of file z3py.py.
| 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 2112 of file z3py.py.
Referenced by _to_pattern().
| 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 1975 of file z3py.py.
Referenced by BoolRef.__invert__(), and mk_not().
| num_simplifiers | ( | ctx = None | ) |
Return the number of simplifiers supported by the given context.
Definition at line 9067 of file z3py.py.
| on_clause_eh | ( | ctx, | |
| p, | |||
| n, | |||
| dep, | |||
| clause ) |
Definition at line 12438 of file z3py.py.
| open_log | ( | fname | ) |
Log interaction to a file. This function must be invoked immediately after init().
Definition at line 122 of file z3py.py.
| Option | ( | re | ) |
Create the regular expression that optionally accepts the argument.
>>> re = Option(Re("a"))
>>> print(simplify(InRe("a", re)))
True
>>> print(simplify(InRe("", re)))
True
>>> print(simplify(InRe("aa", re)))
False
Definition at line 12313 of file z3py.py.
| Or | ( | * | args | ) |
Create a Z3 or-expression or or-probe.
>>> p, q, r = Bools('p q r')
>>> Or(p, q, r)
Or(p, q, r)
>>> P = BoolVector('p', 5)
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)
Definition at line 2042 of file z3py.py.
Referenced by BoolRef.__or__().
| 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 9286 of file z3py.py.
| ParAndThen | ( | t1, | |
| t2, | |||
| ctx = None ) |
| 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 9307 of file z3py.py.
| 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 10222 of file z3py.py.
| 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 10201 of file z3py.py.
| 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 9326 of file z3py.py.
| PartialOrder | ( | a, | |
| index ) |
| PbEq | ( | args, | |
| k, | |||
| ctx = None ) |
Create a Pseudo-Boolean equality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
Definition at line 9978 of file z3py.py.
| 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 9967 of file z3py.py.
| 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 9956 of file z3py.py.
| PiecewiseLinearOrder | ( | a, | |
| index ) |
| Plus | ( | re | ) |
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 12298 of file z3py.py.
| 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 12017 of file z3py.py.
| probe_description | ( | name, | |
| ctx = None ) |
Return a short description for the probe named `name`.
>>> d = probe_description('memory')
Definition at line 9622 of file z3py.py.
| probes | ( | ctx = None | ) |
Return a list of all available probes in Z3.
>>> l = probes()
>>> l.count('memory') == 1
True
Definition at line 9611 of file z3py.py.
| 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 9863 of file z3py.py.
| PropagateFunction | ( | name, | |
| * | sig ) |
Create a function that gets tracked by user propagator. Every term headed by this function symbol is tracked. If a term is fixed and the fixed callback is registered a callback is invoked that the term headed by this function is fixed.
Definition at line 12603 of file z3py.py.
| prove | ( | claim, | |
| show = False, | |||
| ** | 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 10050 of file z3py.py.
| 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 3516 of file z3py.py.
| 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 12363 of file z3py.py.
| RatVal | ( | a, | |
| b, | |||
| ctx = None ) |
Return a Z3 rational a/b. If `ctx=None`, then the global context is used. Note: Division by zero (b == 0) is allowed in Z3 symbolic expressions. Z3 can reason about such expressions symbolically. >>> RatVal(3,5) 3/5 >>> RatVal(3,5).sort() Real
Definition at line 3496 of file z3py.py.
Referenced by Q().
| 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 12191 of file z3py.py.
| 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 3582 of file z3py.py.
Referenced by Reals(), and RealVector().
| RealPart | ( | value | ) |
Return the Real-valued real component of a Complex expression.
Definition at line 3390 of file z3py.py.
Referenced by ComplexRef.real_part().
| 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 3595 of file z3py.py.
| 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 3436 of file z3py.py.
Referenced by ComplexVal(), FreshReal(), Real(), and RealVar().
| 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 3477 of file z3py.py.
Referenced by _coerce_exprs(), _py2expr(), Cbrt(), RatVal(), Sqrt(), and ToReal().
| ExprRef RealVar | ( | int | 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 1617 of file z3py.py.
Referenced by RealVarVector().
| RealVarVector | ( | int | 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 1627 of file z3py.py.
| 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 3610 of file z3py.py.
| 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 992 of file z3py.py.
| RecFunction | ( | name, | |
| * | sig ) |
Create a new Z3 recursive with the given sorts.
Definition at line 974 of file z3py.py.
| 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 9375 of file z3py.py.
| 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 4732 of file z3py.py.
| 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 12066 of file z3py.py.
| None reset_params | ( | ) |
Reset all global (or module) parameters.
Definition at line 322 of file z3py.py.
| ReSort | ( | s | ) |
Definition at line 12210 of file z3py.py.
| RNA | ( | ctx = None | ) |
| RNE | ( | ctx = None | ) |
| 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 4642 of file z3py.py.
| 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 4658 of file z3py.py.
| RoundNearestTiesToAway | ( | ctx = None | ) |
| RoundNearestTiesToEven | ( | ctx = None | ) |
| RoundTowardNegative | ( | ctx = None | ) |
| RoundTowardPositive | ( | ctx = None | ) |
| RoundTowardZero | ( | ctx = None | ) |
| RTN | ( | ctx = None | ) |
| RTP | ( | ctx = None | ) |
| RTZ | ( | ctx = None | ) |
| Select | ( | a, | |
| * | args ) |
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 5159 of file z3py.py.
| SeqFoldLeft | ( | f, | |
| a, | |||
| s ) |
Definition at line 12143 of file z3py.py.
| SeqFoldLeftI | ( | f, | |
| i, | |||
| a, | |||
| s ) |
Definition at line 12149 of file z3py.py.
| SeqMap | ( | f, | |
| s ) |
Map function 'f' over sequence 's'
Definition at line 12129 of file z3py.py.
| SeqMapI | ( | f, | |
| i, | |||
| s ) |
Map function 'f' over sequence 's' at index 'i'
Definition at line 12135 of file z3py.py.
| SeqPower | ( | s, | |
| n ) |
Concatenate the sequence 's' with itself 'n' times. It is the empty sequence for n <= 0
>>> p = SeqPower(StringVal("ab"), 2)
>>> simplify(p)
"abab"
Definition at line 12119 of file z3py.py.
| SeqSort | ( | s | ) |
Create a sequence sort over elements provided in the argument >>> s = SeqSort(IntSort()) >>> s == Unit(IntVal(1)).sort() True
Definition at line 11763 of file z3py.py.
| set_default_fp_sort | ( | ebits, | |
| sbits, | |||
| ctx = None ) |
| set_default_rounding_mode | ( | rm, | |
| ctx = None ) |
Definition at line 10270 of file z3py.py.
| set_option | ( | * | args, |
| ** | kws ) |
| set_param | ( | * | args, |
| ** | kws ) |
Set Z3 global (or module) parameters. >>> set_param(precision=10)
Definition at line 298 of file z3py.py.
Referenced by set_option().
| SetAdd | ( | s, | |
| e ) |
Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)
Definition at line 5338 of file z3py.py.
| SetComplement | ( | s | ) |
The complement of set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
complement(a)
Definition at line 5364 of file z3py.py.
| SetDel | ( | s, | |
| e ) |
Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
Definition at line 5351 of file z3py.py.
| 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 5374 of file z3py.py.
| 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 5322 of file z3py.py.
| SetSort | ( | s | ) |
| 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 5306 of file z3py.py.
| 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 4674 of file z3py.py.
| 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 8269 of file z3py.py.
| simplifier_description | ( | name, | |
| ctx = None ) |
Return the description of the simplifier identified by name.
Definition at line 9077 of file z3py.py.
| simplifier_name | ( | i, | |
| ctx = None ) |
Return the name of the i-th simplifier supported by the given context.
Definition at line 9072 of file z3py.py.
| 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 9727 of file z3py.py.
| simplify_param_descrs | ( | ) |
Return the set of parameter descriptions for Z3 `simplify` procedure.
Definition at line 9757 of file z3py.py.
| Singleton | ( | elem | ) |
Create a singleton finite set containing elem. >>> Singleton(IntVal(1)) set.singleton(1)
Definition at line 5520 of file z3py.py.
Referenced by FiniteSetSortRef.cast().
| 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 9989 of file z3py.py.
| 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 10019 of file z3py.py.
| 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 8248 of file z3py.py.
| 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 3694 of file z3py.py.
| SRem | ( | a, | |
| b ) |
Create the Z3 expression signed remainder.
Use the operator % for signed modulus, and URem() for unsigned remainder.
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> SRem(x, y)
SRem(x, y)
>>> SRem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> SRem(x, y).sexpr()
'(bvsrem x y)'
Definition at line 4589 of file z3py.py.
| Star | ( | re | ) |
Create the regular expression accepting zero or more repetitions of argument.
>>> re = Star(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
True
Definition at line 12333 of file z3py.py.
| Store | ( | a, | |
| * | args ) |
Return a Z3 store array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s = Store(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved
Definition at line 5142 of file z3py.py.
Referenced by ModelRef.get_interp().
| StrFromCode | ( | c | ) |
| 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 11932 of file z3py.py.
| Strings | ( | names, | |
| ctx = None ) |
Return a tuple of String constants.
Definition at line 11941 of file z3py.py.
| StringSort | ( | ctx = None | ) |
| StringVal | ( | s, | |
| ctx = None ) |
create a string expression
Definition at line 11925 of file z3py.py.
Referenced by _coerce_exprs(), _py2expr(), and Extract().
| StrToCode | ( | s | ) |
Convert a unit length string to integer code
Definition at line 12179 of file z3py.py.
| StrToInt | ( | s | ) |
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 12156 of file z3py.py.
| SubSeq | ( | s, | |
| offset, | |||
| length ) |
Extract substring or subsequence starting at offset.
This is a convenience function that redirects to Extract(s, offset, length).
>>> s = StringVal("hello world")
>>> SubSeq(s, 0, 5) # Extract "hello"
str.substr("hello world", 0, 5)
>>> simplify(SubSeq(StringVal("testing"), 2, 4))
"stin"
Definition at line 11963 of file z3py.py.
| 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 9762 of file z3py.py.
| substitute_funs | ( | t, | |
| * | m ) |
Apply substitution m on t, m is a list of pairs of a function and expression (from, to) Every occurrence in to of the function from is replaced with the expression to. The expression to can have free variables, that refer to the arguments of from. For examples, see
Definition at line 9815 of file z3py.py.
| 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 9795 of file z3py.py.
| SubString | ( | s, | |
| offset, | |||
| length ) |
Extract substring or subsequence starting at offset.
This is a convenience function that redirects to Extract(s, offset, length).
>>> s = StringVal("hello world")
>>> SubString(s, 6, 5) # Extract "world"
str.substr("hello world", 6, 5)
>>> simplify(SubString(StringVal("hello"), 1, 3))
"ell"
Definition at line 11949 of file z3py.py.
| 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 12032 of file z3py.py.
| Sum | ( | * | args | ) |
Create the sum of the Z3 expressions.
>>> a, b, c = Ints('a b c')
>>> Sum(a, b, c)
a + b + c
>>> Sum([a, b, c])
a + b + c
>>> A = IntVector('a', 5)
>>> Sum(A)
a__0 + a__1 + a__2 + a__3 + a__4
Definition at line 9837 of file z3py.py.
| tactic_description | ( | name, | |
| ctx = None ) |
Return a short description for the tactic named `name`.
>>> d = tactic_description('simplify')
Definition at line 9416 of file z3py.py.
| tactics | ( | ctx = None | ) |
Return a list of all available tactics in Z3.
>>> l = tactics()
>>> l.count('simplify') == 1
True
Definition at line 9405 of file z3py.py.
| 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 9273 of file z3py.py.
| to_Ast | ( | ptr | ) |
| to_AstVectorObj | ( | ptr | ) |
Definition at line 12427 of file z3py.py.
| to_ContextObj | ( | ptr | ) |
| to_symbol | ( | s, | |
| ctx = None ) |
Convert an integer or string into a Z3 symbol.
Definition at line 132 of file z3py.py.
Referenced by _mk_quantifier(), Array(), BitVec(), Bool(), Complex(), Const(), CreateDatatypes(), CreatePolymorphicDatatype(), DatatypeSort(), DeclareSort(), DeclareTypeVar(), EnumSort(), Function(), ParamDescrsRef.get_documentation(), ParamDescrsRef.get_kind(), Int(), Real(), RecFunction(), and ParamsRef.set().
| ToInt | ( | a | ) |
Return the Z3 expression ToInt(a).
>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int
Definition at line 3659 of file z3py.py.
| ToReal | ( | a | ) |
Return the Z3 expression ToReal(a).
>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real
Definition at line 3639 of file z3py.py.
| 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 12410 of file z3py.py.
| TreeOrder | ( | a, | |
| index ) |
| 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 9396 of file z3py.py.
| 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 6092 of file z3py.py.
| UDiv | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) division `self / other`.
Use the operator / for signed division.
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> UDiv(x, y)
UDiv(x, y)
>>> UDiv(x, y).sort()
BitVec(32)
>>> (x / y).sexpr()
'(bvsdiv x y)'
>>> UDiv(x, y).sexpr()
'(bvudiv x y)'
Definition at line 4547 of file z3py.py.
| UGE | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) `other >= self`.
Use the operator >= for signed greater than or equal to.
>>> x, y = BitVecs('x y', 32)
>>> UGE(x, y)
UGE(x, y)
>>> (x >= y).sexpr()
'(bvsge x y)'
>>> UGE(x, y).sexpr()
'(bvuge x y)'
Definition at line 4511 of file z3py.py.
| UGT | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) `other > self`.
Use the operator > for signed greater than.
>>> x, y = BitVecs('x y', 32)
>>> UGT(x, y)
UGT(x, y)
>>> (x > y).sexpr()
'(bvsgt x y)'
>>> UGT(x, y).sexpr()
'(bvugt x y)'
Definition at line 4529 of file z3py.py.
| ULE | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) `other <= self`.
Use the operator <= for signed less than or equal to.
>>> x, y = BitVecs('x y', 32)
>>> ULE(x, y)
ULE(x, y)
>>> (x <= y).sexpr()
'(bvsle x y)'
>>> ULE(x, y).sexpr()
'(bvule x y)'
Definition at line 4475 of file z3py.py.
| ULT | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) `other < self`.
Use the operator < for signed less than.
>>> x, y = BitVecs('x y', 32)
>>> ULT(x, y)
ULT(x, y)
>>> (x < y).sexpr()
'(bvslt x y)'
>>> ULT(x, y).sexpr()
'(bvult x y)'
Definition at line 4493 of file z3py.py.
| Union | ( | * | args | ) |
Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> print (simplify(InRe("d", re)))
False
Definition at line 12244 of file z3py.py.
| Unit | ( | a | ) |
| Update | ( | a, | |
| * | args ) |
Return a Z3 store array expression.
>>> a = Array('a', IntSort(), IntSort())
>>> i, v = Ints('i v')
>>> s = Update(a, i, v)
>>> s.sort()
Array(Int, Int)
>>> prove(s[i] == v)
proved
>>> j = Int('j')
>>> prove(Implies(i != j, s[j] == a[j]))
proved
Definition at line 5099 of file z3py.py.
Referenced by Store().
| URem | ( | a, | |
| b ) |
Create the Z3 expression (unsigned) remainder `self % other`.
Use the operator % for signed modulus, and SRem() for signed remainder.
>>> x = BitVec('x', 32)
>>> y = BitVec('y', 32)
>>> URem(x, y)
URem(x, y)
>>> URem(x, y).sort()
BitVec(32)
>>> (x % y).sexpr()
'(bvsmod x y)'
>>> URem(x, y).sexpr()
'(bvurem x y)'
Definition at line 4568 of file z3py.py.
| user_prop_binding | ( | ctx, | |
| cb, | |||
| q_ref, | |||
| inst_ref ) |
Definition at line 12580 of file z3py.py.
| user_prop_created | ( | ctx, | |
| cb, | |||
| id ) |
| user_prop_decide | ( | ctx, | |
| cb, | |||
| t_ref, | |||
| idx, | |||
| phase ) |
| user_prop_diseq | ( | ctx, | |
| cb, | |||
| x, | |||
| y ) |
Definition at line 12563 of file z3py.py.
| user_prop_eq | ( | ctx, | |
| cb, | |||
| x, | |||
| y ) |
| user_prop_final | ( | ctx, | |
| cb ) |
| user_prop_fixed | ( | ctx, | |
| cb, | |||
| id, | |||
| value ) |
Definition at line 12529 of file z3py.py.
| user_prop_fresh | ( | ctx, | |
| _new_ctx ) |
Definition at line 12515 of file z3py.py.
| user_prop_pop | ( | ctx, | |
| cb, | |||
| num_scopes ) |
| user_prop_push | ( | ctx, | |
| cb ) |
Create a Z3 free variable. Free variables are used to create quantified formulas. A free variable with index n is bound when it occurs within the scope of n+1 quantified declarations. >>> Var(0, IntSort()) Var(0) >>> eq(Var(0, IntSort()), Var(0, BoolSort())) False
Definition at line 1602 of file z3py.py.
Referenced by RealVar().
| 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 9690 of file z3py.py.
| 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 9347 of file z3py.py.
| 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 9361 of file z3py.py.
| 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 1959 of file z3py.py.
Referenced by BoolRef.__xor__().
| z3_debug | ( | ) |
Definition at line 70 of file z3py.py.
Referenced by ModelRef.__getitem__(), QuantifierRef.__getitem__(), Context.__init__(), Goal.__init__(), ArithRef.__mod__(), ArithRef.__rmod__(), _check_bv_args(), _coerce_expr_merge(), _coerce_exprs(), _ctx_from_ast_arg_list(), _mk_bin(), _mk_quantifier(), _py2expr(), _to_sort_ref(), DatatypeSortRef.accessor(), And(), ExprRef.arg(), args2params(), ArraySort(), IntNumRef.as_long(), AsArray(), BV2Int(), BVRedAnd(), BVRedOr(), BVSNegNoOverflow(), ArithSortRef.cast(), BitVecSortRef.cast(), SortRef.cast(), Concat(), Const(), DatatypeSortRef.constructor(), Goal.convert_model(), CreateDatatypes(), CreatePolymorphicDatatype(), ExprRef.decl(), Datatype.declare(), Datatype.declare_core(), Default(), Distinct(), EnumSort(), AstRef.eq(), eq(), Ext(), Extract(), FreshConst(), FreshFunction(), Function(), get_as_array_func(), ModelRef.get_interp(), get_map_func(), ModelRef.get_universe(), get_var_index(), If(), IsInt(), K(), ExprRef.kind(), Map(), MultiPattern(), QuantifierRef.no_pattern(), ExprRef.num_args(), Or(), QuantifierRef.pattern(), RatVal(), RecFunction(), DatatypeSortRef.recognizer(), RepeatBitVec(), Select(), ParamsRef.set(), set_param(), SignExt(), ToInt(), ToReal(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Update(), ExprRef.update(), DatatypeRef.update_field(), Var(), QuantifierRef.var_name(), QuantifierRef.var_sort(), and ZeroExt().
| z3_error_handler | ( | c, | |
| e ) |
| 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 4704 of file z3py.py.
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
| sat = CheckSatResult(Z3_L_TRUE) |
| unknown = CheckSatResult(Z3_L_UNDEF) |
| unsat = CheckSatResult(Z3_L_FALSE) |