- a -
- abstract() : Fixedpoint
- accessor() : DatatypeSortRef
- add() : Fixedpoint, Goal
- Add() : Optimize
- add() : Params, Solver
- Add() : Fixedpoint, Goal, Optimize, Params, Solver
- 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
- addCover() : Fixedpoint
- AddCover() : Fixedpoint
- addFact() : Fixedpoint
- AddFact() : Fixedpoint
- AddRecDef() : Context
- addRule() : Fixedpoint
- AddRule() : Fixedpoint
- algebraic_i() : expr
- algebraic_lower() : expr
- algebraic_poly() : expr
- algebraic_upper() : expr
- and() : Context
- And() : Context
- andThen() : Context
- AndThen() : Context
- append() : Log, Fixedpoint, Goal, Solver
- apply() : FuncDecl< R extends Sort >, Probe, Tactic
- Apply() : FuncDecl, Probe, Tactic
- apply() : probe, tactic, Tactic
- apply_result() : apply_result
- approx() : AlgebraicNumRef
- Arg() : Expr
- 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
- arrayLength() : Z3Object
- arrayToNative() : Z3Object
- 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
- AsBoolExpr() : Goal
- Assert() : Optimize, Fixedpoint, Goal, Optimize, Solver
- assert_and_track() : Optimize, Solver
- assert_exprs() : Fixedpoint, Goal, Optimize, Solver
- AssertAndTrack() : Optimize
- assertAndTrack() : Solver
- AssertAndTrack() : Solver
- assertions() : fixedpoint, optimize, solver, Optimize, Solver
- AssertSoft() : Optimize
- ast() : ast
- ast_vector_tpl() : ast_vector_tpl< T >
- ASTVector() : ASTVector
- at() : expr, SeqRef