|
| def | z3_debug () |
| |
| def | enable_trace (msg) |
| |
| def | disable_trace (msg) |
| |
| def | get_version_string () |
| |
| def | get_version () |
| |
| def | get_full_version () |
| |
| def | open_log (fname) |
| |
| def | append_log (s) |
| |
| def | to_symbol (s, ctx=None) |
| |
| def | z3_error_handler (c, e) |
| |
| def | main_ctx () |
| |
| def | get_ctx (ctx) |
| |
| def | set_param (*args, **kws) |
| |
| def | reset_params () |
| |
| def | set_option (*args, **kws) |
| |
| def | get_param (name) |
| |
| def | is_ast (a) |
| |
| def | eq (a, b) |
| |
| def | is_sort (s) |
| |
| def | DeclareSort (name, ctx=None) |
| |
| def | is_func_decl (a) |
| |
| def | Function (name, *sig) |
| |
| def | FreshFunction (*sig) |
| |
| def | RecFunction (name, *sig) |
| |
| def | RecAddDefinition (f, args, body) |
| |
| def | deserialize (st) |
| |
| def | is_expr (a) |
| |
| def | is_app (a) |
| |
| def | is_const (a) |
| |
| def | is_var (a) |
| |
| def | get_var_index (a) |
| |
| def | is_app_of (a, k) |
| |
| def | If (a, b, c, ctx=None) |
| |
| def | Distinct (*args) |
| |
| def | Const (name, sort) |
| |
| def | Consts (names, sort) |
| |
| def | FreshConst (sort, prefix="c") |
| |
| def | Var (idx, s) |
| |
| def | RealVar (idx, ctx=None) |
| |
| def | RealVarVector (n, ctx=None) |
| |
| def | is_bool (a) |
| |
| def | is_true (a) |
| |
| def | is_false (a) |
| |
| def | is_and (a) |
| |
| def | is_or (a) |
| |
| def | is_implies (a) |
| |
| def | is_not (a) |
| |
| def | is_eq (a) |
| |
| def | is_distinct (a) |
| |
| def | BoolSort (ctx=None) |
| |
| def | BoolVal (val, ctx=None) |
| |
| def | Bool (name, ctx=None) |
| |
| def | Bools (names, ctx=None) |
| |
| def | BoolVector (prefix, sz, ctx=None) |
| |
| def | FreshBool (prefix="b", ctx=None) |
| |
| def | Implies (a, b, ctx=None) |
| |
| def | Xor (a, b, ctx=None) |
| |
| def | Not (a, ctx=None) |
| |
| def | mk_not (a) |
| |
| def | And (*args) |
| |
| def | Or (*args) |
| |
| def | is_pattern (a) |
| |
| def | MultiPattern (*args) |
| |
| def | is_quantifier (a) |
| |
| def | ForAll (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
| |
| def | Exists (vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]) |
| |
| def | Lambda (vs, body) |
| |
| def | is_arith_sort (s) |
| |
| def | is_arith (a) |
| |
| def | is_int (a) |
| |
| def | is_real (a) |
| |
| def | is_int_value (a) |
| |
| def | is_rational_value (a) |
| |
| def | is_algebraic_value (a) |
| |
| def | is_add (a) |
| |
| def | is_mul (a) |
| |
| def | is_sub (a) |
| |
| def | is_div (a) |
| |
| def | is_idiv (a) |
| |
| def | is_mod (a) |
| |
| def | is_le (a) |
| |
| def | is_lt (a) |
| |
| def | is_ge (a) |
| |
| def | is_gt (a) |
| |
| def | is_is_int (a) |
| |
| def | is_to_real (a) |
| |
| def | is_to_int (a) |
| |
| def | IntSort (ctx=None) |
| |
| def | RealSort (ctx=None) |
| |
| def | IntVal (val, ctx=None) |
| |
| def | RealVal (val, ctx=None) |
| |
| def | RatVal (a, b, ctx=None) |
| |
| def | Q (a, b, ctx=None) |
| |
| def | Int (name, ctx=None) |
| |
| def | Ints (names, ctx=None) |
| |
| def | IntVector (prefix, sz, ctx=None) |
| |
| def | FreshInt (prefix="x", ctx=None) |
| |
| def | Real (name, ctx=None) |
| |
| def | Reals (names, ctx=None) |
| |
| def | RealVector (prefix, sz, ctx=None) |
| |
| def | FreshReal (prefix="b", ctx=None) |
| |
| def | ToReal (a) |
| |
| def | ToInt (a) |
| |
| def | IsInt (a) |
| |
| def | Sqrt (a, ctx=None) |
| |
| def | Cbrt (a, ctx=None) |
| |
| def | is_bv_sort (s) |
| |
| def | is_bv (a) |
| |
| def | is_bv_value (a) |
| |
| def | BV2Int (a, is_signed=False) |
| |
| def | Int2BV (a, num_bits) |
| |
| def | BitVecSort (sz, ctx=None) |
| |
| def | BitVecVal (val, bv, ctx=None) |
| |
| def | BitVec (name, bv, ctx=None) |
| |
| def | BitVecs (names, bv, ctx=None) |
| |
| def | Concat (*args) |
| |
| def | Extract (high, low, a) |
| |
| def | ULE (a, b) |
| |
| def | ULT (a, b) |
| |
| def | UGE (a, b) |
| |
| def | UGT (a, b) |
| |
| def | UDiv (a, b) |
| |
| def | URem (a, b) |
| |
| def | SRem (a, b) |
| |
| def | LShR (a, b) |
| |
| def | RotateLeft (a, b) |
| |
| def | RotateRight (a, b) |
| |
| def | SignExt (n, a) |
| |
| def | ZeroExt (n, a) |
| |
| def | RepeatBitVec (n, a) |
| |
| def | BVRedAnd (a) |
| |
| def | BVRedOr (a) |
| |
| def | BVAddNoOverflow (a, b, signed) |
| |
| def | BVAddNoUnderflow (a, b) |
| |
| def | BVSubNoOverflow (a, b) |
| |
| def | BVSubNoUnderflow (a, b, signed) |
| |
| def | BVSDivNoOverflow (a, b) |
| |
| def | BVSNegNoOverflow (a) |
| |
| def | BVMulNoOverflow (a, b, signed) |
| |
| def | BVMulNoUnderflow (a, b) |
| |
| def | is_array_sort (a) |
| |
| def | is_array (a) |
| |
| def | is_const_array (a) |
| |
| def | is_K (a) |
| |
| def | is_map (a) |
| |
| def | is_default (a) |
| |
| def | get_map_func (a) |
| |
| def | ArraySort (*sig) |
| |
| def | Array (name, *sorts) |
| |
| def | Update (a, *args) |
| |
| def | Default (a) |
| |
| def | Store (a, *args) |
| |
| def | Select (a, *args) |
| |
| def | Map (f, *args) |
| |
| def | K (dom, v) |
| |
| def | Ext (a, b) |
| |
| def | SetHasSize (a, k) |
| |
| def | is_select (a) |
| |
| def | is_store (a) |
| |
| def | SetSort (s) |
| | Sets. More...
|
| |
| def | EmptySet (s) |
| |
| def | FullSet (s) |
| |
| def | SetUnion (*args) |
| |
| def | SetIntersect (*args) |
| |
| def | SetAdd (s, e) |
| |
| def | SetDel (s, e) |
| |
| def | SetComplement (s) |
| |
| def | SetDifference (a, b) |
| |
| def | IsMember (e, s) |
| |
| def | IsSubset (a, b) |
| |
| def | CreateDatatypes (*ds) |
| |
| def | DatatypeSort (name, ctx=None) |
| |
| def | TupleSort (name, sorts, ctx=None) |
| |
| def | DisjointSum (name, sorts, ctx=None) |
| |
| def | EnumSort (name, values, ctx=None) |
| |
| def | args2params (arguments, keywords, ctx=None) |
| |
| def | Model (ctx=None) |
| |
| def | is_as_array (n) |
| |
| def | get_as_array_func (n) |
| |
| def | SolverFor (logic, ctx=None, logFile=None) |
| |
| def | SimpleSolver (ctx=None, logFile=None) |
| |
| def | FiniteDomainSort (name, sz, ctx=None) |
| |
| def | is_finite_domain_sort (s) |
| |
| def | is_finite_domain (a) |
| |
| def | FiniteDomainVal (val, sort, ctx=None) |
| |
| def | is_finite_domain_value (a) |
| |
| def | AndThen (*ts, **ks) |
| |
| def | Then (*ts, **ks) |
| |
| def | OrElse (*ts, **ks) |
| |
| def | ParOr (*ts, **ks) |
| |
| def | ParThen (t1, t2, ctx=None) |
| |
| def | ParAndThen (t1, t2, ctx=None) |
| |
| def | With (t, *args, **keys) |
| |
| def | WithParams (t, p) |
| |
| def | Repeat (t, max=4294967295, ctx=None) |
| |
| def | TryFor (t, ms, ctx=None) |
| |
| def | tactics (ctx=None) |
| |
| def | tactic_description (name, ctx=None) |
| |
| def | describe_tactics () |
| |
| def | is_probe (p) |
| |
| def | probes (ctx=None) |
| |
| def | probe_description (name, ctx=None) |
| |
| def | describe_probes () |
| |
| def | FailIf (p, ctx=None) |
| |
| def | When (p, t, ctx=None) |
| |
| def | Cond (p, t1, t2, ctx=None) |
| |
| def | simplify (a, *arguments, **keywords) |
| | Utils. More...
|
| |
| def | help_simplify () |
| |
| def | simplify_param_descrs () |
| |
| def | substitute (t, *m) |
| |
| def | substitute_vars (t, *m) |
| |
| def | substitute_funs (t, *m) |
| |
| def | Sum (*args) |
| |
| def | Product (*args) |
| |
| def | Abs (arg) |
| |
| def | AtMost (*args) |
| |
| def | AtLeast (*args) |
| |
| def | PbLe (args, k) |
| |
| def | PbGe (args, k) |
| |
| def | PbEq (args, k, ctx=None) |
| |
| def | solve (*args, **keywords) |
| |
| def | solve_using (s, *args, **keywords) |
| |
| def | prove (claim, show=False, **keywords) |
| |
| def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
| |
| def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
| |
| def | get_default_rounding_mode (ctx=None) |
| |
| def | set_default_rounding_mode (rm, ctx=None) |
| |
| def | get_default_fp_sort (ctx=None) |
| |
| def | set_default_fp_sort (ebits, sbits, ctx=None) |
| |
| def | Float16 (ctx=None) |
| |
| def | FloatHalf (ctx=None) |
| |
| def | Float32 (ctx=None) |
| |
| def | FloatSingle (ctx=None) |
| |
| def | Float64 (ctx=None) |
| |
| def | FloatDouble (ctx=None) |
| |
| def | Float128 (ctx=None) |
| |
| def | FloatQuadruple (ctx=None) |
| |
| def | is_fp_sort (s) |
| |
| def | is_fprm_sort (s) |
| |
| def | RoundNearestTiesToEven (ctx=None) |
| |
| def | RNE (ctx=None) |
| |
| def | RoundNearestTiesToAway (ctx=None) |
| |
| def | RNA (ctx=None) |
| |
| def | RoundTowardPositive (ctx=None) |
| |
| def | RTP (ctx=None) |
| |
| def | RoundTowardNegative (ctx=None) |
| |
| def | RTN (ctx=None) |
| |
| def | RoundTowardZero (ctx=None) |
| |
| def | RTZ (ctx=None) |
| |
| def | is_fprm (a) |
| |
| def | is_fprm_value (a) |
| |
| def | is_fp (a) |
| |
| def | is_fp_value (a) |
| |
| def | FPSort (ebits, sbits, ctx=None) |
| |
| def | fpNaN (s) |
| |
| def | fpPlusInfinity (s) |
| |
| def | fpMinusInfinity (s) |
| |
| def | fpInfinity (s, negative) |
| |
| def | fpPlusZero (s) |
| |
| def | fpMinusZero (s) |
| |
| def | fpZero (s, negative) |
| |
| def | FPVal (sig, exp=None, fps=None, ctx=None) |
| |
| def | FP (name, fpsort, ctx=None) |
| |
| def | FPs (names, fpsort, ctx=None) |
| |
| def | fpAbs (a, ctx=None) |
| |
| def | fpNeg (a, ctx=None) |
| |
| def | fpAdd (rm, a, b, ctx=None) |
| |
| def | fpSub (rm, a, b, ctx=None) |
| |
| def | fpMul (rm, a, b, ctx=None) |
| |
| def | fpDiv (rm, a, b, ctx=None) |
| |
| def | fpRem (a, b, ctx=None) |
| |
| def | fpMin (a, b, ctx=None) |
| |
| def | fpMax (a, b, ctx=None) |
| |
| def | fpFMA (rm, a, b, c, ctx=None) |
| |
| def | fpSqrt (rm, a, ctx=None) |
| |
| def | fpRoundToIntegral (rm, a, ctx=None) |
| |
| def | fpIsNaN (a, ctx=None) |
| |
| def | fpIsInf (a, ctx=None) |
| |
| def | fpIsZero (a, ctx=None) |
| |
| def | fpIsNormal (a, ctx=None) |
| |
| def | fpIsSubnormal (a, ctx=None) |
| |
| def | fpIsNegative (a, ctx=None) |
| |
| def | fpIsPositive (a, ctx=None) |
| |
| def | fpLT (a, b, ctx=None) |
| |
| def | fpLEQ (a, b, ctx=None) |
| |
| def | fpGT (a, b, ctx=None) |
| |
| def | fpGEQ (a, b, ctx=None) |
| |
| def | fpEQ (a, b, ctx=None) |
| |
| def | fpNEQ (a, b, ctx=None) |
| |
| def | fpFP (sgn, exp, sig, ctx=None) |
| |
| def | fpToFP (a1, a2=None, a3=None, ctx=None) |
| |
| def | fpBVToFP (v, sort, ctx=None) |
| |
| def | fpFPToFP (rm, v, sort, ctx=None) |
| |
| def | fpRealToFP (rm, v, sort, ctx=None) |
| |
| def | fpSignedToFP (rm, v, sort, ctx=None) |
| |
| def | fpUnsignedToFP (rm, v, sort, ctx=None) |
| |
| def | fpToFPUnsigned (rm, x, s, ctx=None) |
| |
| def | fpToSBV (rm, x, s, ctx=None) |
| |
| def | fpToUBV (rm, x, s, ctx=None) |
| |
| def | fpToReal (x, ctx=None) |
| |
| def | fpToIEEEBV (x, ctx=None) |
| |
| def | StringSort (ctx=None) |
| |
| def | CharSort (ctx=None) |
| |
| def | SeqSort (s) |
| |
| def | CharVal (ch, ctx=None) |
| |
| def | CharFromBv (ch, ctx=None) |
| |
| def | CharToBv (ch, ctx=None) |
| |
| def | CharToInt (ch, ctx=None) |
| |
| def | CharIsDigit (ch, ctx=None) |
| |
| def | is_seq (a) |
| |
| def | is_string (a) |
| |
| def | is_string_value (a) |
| |
| def | StringVal (s, ctx=None) |
| |
| def | String (name, ctx=None) |
| |
| def | Strings (names, ctx=None) |
| |
| def | SubString (s, offset, length) |
| |
| def | SubSeq (s, offset, length) |
| |
| def | Empty (s) |
| |
| def | Full (s) |
| |
| def | Unit (a) |
| |
| def | PrefixOf (a, b) |
| |
| def | SuffixOf (a, b) |
| |
| def | Contains (a, b) |
| |
| def | Replace (s, src, dst) |
| |
| def | IndexOf (s, substr, offset=None) |
| |
| def | LastIndexOf (s, substr) |
| |
| def | Length (s) |
| |
| def | StrToInt (s) |
| |
| def | IntToStr (s) |
| |
| def | StrToCode (s) |
| |
| def | StrFromCode (c) |
| |
| def | Re (s, ctx=None) |
| |
| def | ReSort (s) |
| |
| def | is_re (s) |
| |
| def | InRe (s, re) |
| |
| def | Union (*args) |
| |
| def | Intersect (*args) |
| |
| def | Plus (re) |
| |
| def | Option (re) |
| |
| def | Complement (re) |
| |
| def | Star (re) |
| |
| def | Loop (re, lo, hi=0) |
| |
| def | Range (lo, hi, ctx=None) |
| |
| def | Diff (a, b, ctx=None) |
| |
| def | AllChar (regex_sort, ctx=None) |
| |
| def | PartialOrder (a, index) |
| |
| def | LinearOrder (a, index) |
| |
| def | TreeOrder (a, index) |
| |
| def | PiecewiseLinearOrder (a, index) |
| |
| def | TransitiveClosure (f) |
| |
| def | to_Ast (ptr) |
| |
| def | to_ContextObj (ptr) |
| |
| def | to_AstVectorObj (ptr) |
| |
| def | on_clause_eh (ctx, p, clause) |
| |
| def | ensure_prop_closures () |
| |
| def | user_prop_push (ctx, cb) |
| |
| def | user_prop_pop (ctx, cb, num_scopes) |
| |
| def | user_prop_fresh (ctx, _new_ctx) |
| |
| def | user_prop_fixed (ctx, cb, id, value) |
| |
| def | user_prop_created (ctx, cb, id) |
| |
| def | user_prop_final (ctx, cb) |
| |
| def | user_prop_eq (ctx, cb, x, y) |
| |
| def | user_prop_diseq (ctx, cb, x, y) |
| |
| def | user_prop_decide (ctx, cb, t_ref, idx_ref, phase_ref) |
| |
| def | PropagateFunction (name, *sig) |
| |
1.9.1