|
| 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 (s, ctx=None) |
| |
| 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 (name, ctx=None) |
| |
| 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 (a, b, c, ctx=None) |
| |
| def | Distinct (args) |
| |
| def | Const (name, sort) |
| |
| def | Consts (names, sort) |
| |
| 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_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 | 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 | 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) |
| |
| 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 | 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 (d, r) |
| |
| def | Array (name, dom, rng) |
| |
| def | Update (a, i, v) |
| |
| def | Default (a) |
| |
| 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 (name, values, ctx=None) |
| |
| def | args2params (arguments, keywords, ctx=None) |
| |
| def | is_as_array (n) |
| |
| def | get_as_array_func (n) |
| |
| def | SolverFor (logic, ctx=None) |
| |
| def | SimpleSolver (ctx=None) |
| |
| def | FiniteDomainSort (name, sz, ctx=None) |
| |
| 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 | 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 | Sum (args) |
| |
| def | Product (args) |
| |
| def | solve (args, keywords) |
| |
| def | solve_using (s, args, keywords) |
| |
| def | prove (claim, keywords) |
| |
| def | parse_smt2_string (s, sorts={}, decls={}, ctx=None) |
| |
| def | parse_smt2_file (f, sorts={}, decls={}, ctx=None) |
| |
| def | Interpolant (a, ctx=None) |
| |
| def | tree_interpolant (pat, p=None, ctx=None) |
| |
| def | binary_interpolant (a, b, p=None, ctx=None) |
| |
| def | sequence_interpolant (v, p=None, 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 | Float128 (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) |
| |
| 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 (a1, a2=None, a3=None) |
| |
| def | fpToFPUnsigned (rm, x, s) |
| |
| def | fpToSBV (rm, x, s) |
| |
| def | fpToUBV (rm, x, s) |
| |
| def | fpToReal (x) |
| |
| def | fpToIEEEBV (x) |
| |
1.8.11