|
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 |
|
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 |
|
def | DeclareTypeVar |
|
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 |
|
def | Distinct (args) |
|
def | Const (name, sort) |
|
def | Consts (names, sort) |
|
def | FreshConst |
|
def | Var (idx, s) |
|
def | RealVar |
|
def | RealVarVector |
|
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 |
|
def | BoolVal |
|
def | Bool |
|
def | Bools |
|
def | BoolVector |
|
def | FreshBool |
|
def | Implies |
|
def | Xor |
|
def | Not |
|
def | mk_not (a) |
|
def | And (args) |
|
def | Or (args) |
|
def | is_pattern (a) |
|
def | MultiPattern (args) |
|
def | is_quantifier (a) |
|
def | ForAll |
|
def | Exists |
|
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 |
|
def | RealSort |
|
def | IntVal |
|
def | RealVal |
|
def | RatVal |
|
def | Q |
|
def | Int |
|
def | Ints |
|
def | IntVector |
|
def | FreshInt |
|
def | Real |
|
def | Reals |
|
def | RealVector |
|
def | FreshReal |
|
def | ToReal (a) |
|
def | ToInt (a) |
|
def | IsInt (a) |
|
def | Sqrt |
|
def | Cbrt |
|
def | is_bv_sort (s) |
|
def | is_bv (a) |
|
def | is_bv_value (a) |
|
def | BV2Int |
|
def | Int2BV (a, num_bits) |
|
def | BitVecSort |
|
def | BitVecVal |
|
def | BitVec |
|
def | BitVecs |
|
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 |
|
def | TupleSort |
|
def | DisjointSum |
|
def | EnumSort |
|
def | args2params |
|
def | Model |
|
def | is_as_array (n) |
|
def | get_as_array_func (n) |
|
def | SolverFor |
|
def | SimpleSolver |
|
def | FiniteDomainSort |
|
def | is_finite_domain_sort (s) |
|
def | is_finite_domain (a) |
|
def | FiniteDomainVal |
|
def | is_finite_domain_value (a) |
|
def | AndThen (ts, ks) |
|
def | Then (ts, ks) |
|
def | OrElse (ts, ks) |
|
def | ParOr (ts, ks) |
|
def | ParThen |
|
def | ParAndThen |
|
def | With (t, args, keys) |
|
def | WithParams (t, p) |
|
def | Repeat |
|
def | TryFor |
|
def | tactics |
|
def | tactic_description |
|
def | describe_tactics () |
|
def | is_probe (p) |
|
def | probes |
|
def | probe_description |
|
def | describe_probes () |
|
def | FailIf |
|
def | When |
|
def | Cond |
|
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 |
|
def | solve (args, keywords) |
|
def | solve_using (s, args, keywords) |
|
def | prove (claim, show=False, keywords) |
|
def | parse_smt2_string |
|
def | parse_smt2_file |
|
def | get_default_rounding_mode |
|
def | set_default_rounding_mode |
|
def | get_default_fp_sort |
|
def | set_default_fp_sort |
|
def | Float16 |
|
def | FloatHalf |
|
def | Float32 |
|
def | FloatSingle |
|
def | Float64 |
|
def | FloatDouble |
|
def | Float128 |
|
def | FloatQuadruple |
|
def | is_fp_sort (s) |
|
def | is_fprm_sort (s) |
|
def | RoundNearestTiesToEven |
|
def | RNE |
|
def | RoundNearestTiesToAway |
|
def | RNA |
|
def | RoundTowardPositive |
|
def | RTP |
|
def | RoundTowardNegative |
|
def | RTN |
|
def | RoundTowardZero |
|
def | RTZ |
|
def | is_fprm (a) |
|
def | is_fprm_value (a) |
|
def | is_fp (a) |
|
def | is_fp_value (a) |
|
def | FPSort |
|
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 |
|
def | FP |
|
def | FPs |
|
def | fpAbs |
|
def | fpNeg |
|
def | fpAdd |
|
def | fpSub |
|
def | fpMul |
|
def | fpDiv |
|
def | fpRem |
|
def | fpMin |
|
def | fpMax |
|
def | fpFMA |
|
def | fpSqrt |
|
def | fpRoundToIntegral |
|
def | fpIsNaN |
|
def | fpIsInf |
|
def | fpIsZero |
|
def | fpIsNormal |
|
def | fpIsSubnormal |
|
def | fpIsNegative |
|
def | fpIsPositive |
|
def | fpLT |
|
def | fpLEQ |
|
def | fpGT |
|
def | fpGEQ |
|
def | fpEQ |
|
def | fpNEQ |
|
def | fpFP |
|
def | fpToFP |
|
def | fpBVToFP |
|
def | fpFPToFP |
|
def | fpRealToFP |
|
def | fpSignedToFP |
|
def | fpUnsignedToFP |
|
def | fpToFPUnsigned |
|
def | fpToSBV |
|
def | fpToUBV |
|
def | fpToReal |
|
def | fpToIEEEBV |
|
def | StringSort |
|
def | CharSort |
|
def | SeqSort (s) |
|
def | CharVal |
|
def | CharFromBv (bv) |
|
def | CharToBv |
|
def | CharToInt |
|
def | CharIsDigit |
|
def | is_seq (a) |
|
def | is_string (a) |
|
def | is_string_value (a) |
|
def | StringVal |
|
def | String |
|
def | Strings |
|
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 |
|
def | LastIndexOf (s, substr) |
|
def | Length (s) |
|
def | StrToInt (s) |
|
def | IntToStr (s) |
|
def | StrToCode (s) |
|
def | StrFromCode (c) |
|
def | Re |
|
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 |
|
def | Range |
|
def | Diff |
|
def | AllChar |
|
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, n, dep, 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, idx, phase) |
|
def | PropagateFunction (name, sig) |
|