- a -
- abstract()
: Fixedpoint
- accessor()
: DatatypeSortRef
- accessors()
: func_decl
- add()
: goal
, optimize
, solver
, user_propagator_base
, Fixedpoint
, Goal
, Optimize
, Solver
, UserPropagateBase
- add_const_interp()
: model
- add_cover()
: fixedpoint
, Fixedpoint
- add_diseq()
: UserPropagateBase
- add_entry()
: func_interp
- add_eq()
: UserPropagateBase
- add_fact()
: fixedpoint
- add_final()
: UserPropagateBase
- add_fixed()
: UserPropagateBase
- add_func_interp()
: model
- add_rule()
: fixedpoint
, Fixedpoint
- add_soft()
: optimize
, Optimize
- algebraic_i()
: expr
- algebraic_lower()
: expr
- algebraic_poly()
: expr
- algebraic_upper()
: expr
- append()
: Fixedpoint
, Goal
, Solver
- apply()
: probe
, tactic
, Tactic
- apply_result()
: apply_result
- approx()
: AlgebraicNumRef
- arg()
: expr
, func_entry
, ExprRef
- arg_value()
: FuncEntry
- args()
: expr
- 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_binary()
: expr
- as_binary_string()
: BitVecNumRef
, IntNumRef
- as_decimal()
: AlgebraicNumRef
, RatNumRef
- as_double()
: expr
- as_expr()
: goal
, ApplyResult
, Goal
- as_fraction()
: RatNumRef
- as_func_decl()
: FuncDeclRef
- as_int64()
: expr
- 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
- as_uint64()
: expr
- assert_and_track()
: Optimize
, Solver
- assert_exprs()
: Fixedpoint
, Goal
, Optimize
, Solver
- assertions()
: fixedpoint
, optimize
, solver
, Optimize
, Solver
- ast()
: ast
- ast_vector_tpl()
: ast_vector_tpl< T >
- at()
: expr
, SeqRef