|
| 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) |
| _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) |
| _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) |
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) |
| 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, 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) |
| _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) |
| 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) |
| PropagateFunction (name, *sig) |