Go to the source code of this file.
|
def | enable_trace (msg) |
|
def | disable_trace (msg) |
|
def | get_version_string () |
|
def | get_version () |
|
def | open_log (fname) |
|
def | append_log (s) |
|
def | to_symbol |
|
def | main_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 | is_func_decl (a) |
|
def | Function (name, sig) |
|
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 | 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_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 | And (args) |
|
def | Or (args) |
|
def | is_pattern (a) |
|
def | MultiPattern (args) |
|
def | is_quantifier (a) |
|
def | ForAll |
|
def | Exists |
|
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 (a) |
|
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 | is_array (a) |
|
def | is_const_array (a) |
|
def | is_K (a) |
|
def | is_map (a) |
|
def | get_map_func (a) |
|
def | ArraySort (d, r) |
|
def | Array (name, dom, rng) |
|
def | Update (a, i, v) |
|
def | Store (a, i, v) |
|
def | Select (a, i) |
|
def | Map (f, args) |
|
def | K (dom, v) |
|
def | is_select (a) |
|
def | is_store (a) |
|
def | CreateDatatypes (ds) |
|
def | EnumSort |
|
def | args2params |
|
def | is_as_array (n) |
|
def | get_as_array_func (n) |
|
def | SolverFor |
|
def | SimpleSolver |
|
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 | 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 | Sum (args) |
|
def | Product (args) |
|
def | solve (args, keywords) |
|
def | solve_using (s, args, keywords) |
|
def | prove (claim, keywords) |
|
def | parse_smt2_string |
|
def | parse_smt2_file |
|
def | Interpolant |
|
def | tree_interpolant |
|
def | binary_interpolant |
|
def | sequence_interpolant |
|
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 | Float128 |
|
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 (a) |
|
def | fpNeg (a) |
|
def | fpAdd (rm, a, b) |
|
def | fpSub (rm, a, b) |
|
def | fpMul (rm, a, b) |
|
def | fpDiv (rm, a, b) |
|
def | fpRem (a, b) |
|
def | fpMin (a, b) |
|
def | fpMax (a, b) |
|
def | fpFMA (rm, a, b, c) |
|
def | fpSqrt (rm, a) |
|
def | fpRoundToIntegral (rm, a) |
|
def | fpIsNaN (a) |
|
def | fpIsInfinite (a) |
|
def | fpIsZero (a) |
|
def | fpIsNormal (a) |
|
def | fpIsSubnormal (a) |
|
def | fpIsNegative (a) |
|
def | fpIsPositive (a) |
|
def | fpLT (a, b) |
|
def | fpLEQ (a, b) |
|
def | fpGT (a, b) |
|
def | fpGEQ (a, b) |
|
def | fpEQ (a, b) |
|
def | fpNEQ (a, b) |
|
def | fpFP (sgn, exp, sig) |
|
def | fpToFP |
|
def | fpToFPUnsigned (rm, x, s) |
|
def | fpToSBV (rm, x, s) |
|
def | fpToUBV (rm, x, s) |
|
def | fpToReal (x) |
|
def | fpToIEEEBV (x) |
|