- a -
- abstract() : Fixedpoint
- accessor() : DatatypeSortRef
- add() : Fixedpoint, Goal
- Add() : Optimize
- add() : Params, Solver, goal, optimize, solver, Fixedpoint, Goal, Optimize, Solver
- add_const_interp() : model
- add_cover() : fixedpoint, Fixedpoint
- add_entry() : func_interp
- add_fact() : fixedpoint
- add_func_interp() : model
- add_rule() : fixedpoint, Fixedpoint
- add_soft() : Optimize
- addConstInterp() : Native
- addCover() : Fixedpoint
- addFact() : Fixedpoint
- addFuncInterp() : Native
- addRecDef() : Native
- addRule() : Fixedpoint
- algebraicAdd() : Native
- algebraicDiv() : Native
- algebraicEq() : Native
- algebraicEval() : Native
- algebraicGe() : Native
- algebraicGt() : Native
- algebraicIsNeg() : Native
- algebraicIsPos() : Native
- algebraicIsValue() : Native
- algebraicIsZero() : Native
- algebraicLe() : Native
- algebraicLt() : Native
- algebraicMul() : Native
- algebraicNeq() : Native
- algebraicPower() : Native
- algebraicRoot() : Native
- algebraicRoots() : Native
- algebraicSign() : Native
- algebraicSub() : Native
- and() : Context
- andThen() : Context
- append() : Log, Fixedpoint, Goal, Solver
- appendLog() : Native
- apply() : FuncDecl, Probe, Tactic, probe, tactic, Tactic
- apply_result() : apply_result
- applyResultDecRef() : Native
- applyResultGetNumSubgoals() : Native
- applyResultGetSubgoal() : Native
- applyResultIncRef() : Native
- applyResultToString() : Native
- approx() : AlgebraicNumRef
- appToAst() : Native
- arg() : expr, func_entry, ExprRef
- arg_value() : FuncEntry
- arity() : func_decl, FuncDeclRef, FuncInterp
- array() : array< T >
- array_domain() : sort
- array_range() : sort
- array_sort() : context
- as_ast() : AstRef, ExprRef, FuncDeclRef, PatternRef, QuantifierRef, SortRef
- as_decimal() : AlgebraicNumRef, RatNumRef
- as_expr() : goal, ApplyResult, Goal
- as_fraction() : RatNumRef
- as_func_decl() : FuncDeclRef
- as_list() : FuncEntry, FuncInterp
- as_long() : BitVecNumRef, FiniteDomainNumRef, IntNumRef, RatNumRef
- as_signed_long() : BitVecNumRef
- as_string() : BitVecNumRef, FiniteDomainNumRef, FiniteDomainRef, FPNumRef, FPRef, FPRMRef, IntNumRef, RatNumRef, SeqRef
- AsBoolExpr() : Goal
- Assert() : Optimize
- assert_and_track() : Optimize, Solver
- assert_exprs() : Fixedpoint, Goal, Optimize, Solver
- assertAndTrack() : Solver
- assertions() : fixedpoint, optimize, solver, Optimize, Solver
- AssertSoft() : Optimize
- ast() : ast
- ast_vector_tpl() : ast_vector_tpl< T >
- astMapContains() : Native
- astMapDecRef() : Native
- astMapErase() : Native
- astMapFind() : Native
- astMapIncRef() : Native
- astMapInsert() : Native
- astMapKeys() : Native
- astMapReset() : Native
- astMapSize() : Native
- astMapToString() : Native
- astToString() : Native
- astVectorDecRef() : Native
- astVectorGet() : Native
- astVectorIncRef() : Native
- astVectorPush() : Native
- astVectorResize() : Native
- astVectorSet() : Native
- astVectorSize() : Native
- astVectorToString() : Native
- astVectorTranslate() : Native
- at() : expr, SeqRef