|
| 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) |
|
| main_ctx () |
|
| _get_ctx (ctx) |
|
| get_ctx (ctx) |
|
| set_param (*args, **kws) |
|
| reset_params () |
|
| set_option (*args, **kws) |
|
| get_param (name) |
|
| is_ast (a) |
|
| eq (a, b) |
|
| _ast_kind (ctx, 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.
|
|
| is_sort (s) |
|
| _to_sort_ref (s, ctx) |
|
| _sort (ctx, a) |
|
| 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) |
|
| _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") |
|
| Var (idx, s) |
|
| RealVar (idx, ctx=None) |
|
| RealVarVector (n, ctx=None) |
|
| is_bool (a) |
|
| is_true (a) |
|
| is_false (a) |
|
| is_and (a) |
|
| is_or (a) |
|
| is_implies (a) |
|
| is_not (a) |
|
| is_eq (a) |
|
| is_distinct (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) |
|
| is_arith_sort (s) |
|
| is_arith (a) |
|
| 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) |
|
| is_add (a) |
|
| is_mul (a) |
|
| is_sub (a) |
|
| is_div (a) |
|
| is_idiv (a) |
|
| is_mod (a) |
|
| is_le (a) |
|
| is_lt (a) |
|
| is_ge (a) |
|
| is_gt (a) |
|
| is_is_int (a) |
|
| is_to_real (a) |
|
| is_to_int (a) |
|
| _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) |
|
| 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) |
|
| is_array (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) |
|
| SetHasSize (a, k) |
|
| 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) |
|
| _valid_accessor (acc) |
| Datatypes.
|
|
| CreateDatatypes (*ds) |
|
| DatatypeSort (name, 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) |
|
| 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) |
|
| _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) |
|
| is_string (a) |
|
| is_string_value (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) |
|
| 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, idx, phase) |
|
| PropagateFunction (name, *sig) |
|