- s -
- sbits()
: FPRef
, FPSortRef
- seq_sort()
: context
- set()
: ASTVector
, config
, context
, optimize
, params
, solver
, Fixedpoint
, Optimize
, ParamsRef
, Solver
- set_predicate_representation()
: Fixedpoint
- setAstPrintMode()
: Native
- setError()
: Native
- setInternalErrorHandler()
: Native
- SetLimit()
: IDecRefQueue
- setParameter()
: Global
- setParameters()
: Fixedpoint
, Optimize
, Solver
- setParamValue()
: Native
- setPredicateRepresentation()
: Fixedpoint
- SetPredicateRepresentation()
: Fixedpoint
- setPrintMode()
: Context
- SExpr()
: AST
- sexpr()
: ApplyResult
, AstRef
, AstVector
, Fixedpoint
, Goal
, ModelRef
, Optimize
, Solver
- sign()
: FPNumRef
- significand()
: FPNumRef
- simplify()
: Expr
, Goal
, Native
- Simplify()
: Expr
, Goal
- simplify()
: expr
, Goal
- simplify_param_descrs()
: param_descrs
- simplifyEx()
: Native
- simplifyGetHelp()
: Native
- simplifyGetParamDescrs()
: Native
- SimplifyHelp()
: Context
- size()
: ASTVector
, Goal
, ParamDescrs
, Statistics
, apply_result
, array< T >
, ast_vector_tpl< T >
, goal
, model
, param_descrs
, stats
, BitVecRef
, BitVecSortRef
, FiniteDomainSortRef
, Goal
, ParamDescrsRef
- skip()
: Context
- Skip()
: Context
- solver()
: solver
, Tactic
- solverAssert()
: Native
- solverAssertAndTrack()
: Native
- solverCheck()
: Native
- solverCheckAssumptions()
: Native
- solverDecRef()
: Native
- solverGetAssertions()
: Native
- solverGetConsequences()
: Native
- solverGetHelp()
: Native
- solverGetModel()
: Native
- solverGetNumScopes()
: Native
- solverGetParamDescrs()
: Native
- solverGetProof()
: Native
- solverGetReasonUnknown()
: Native
- solverGetStatistics()
: Native
- solverGetUnsatCore()
: Native
- solverIncRef()
: Native
- solverPop()
: Native
- solverPush()
: Native
- solverReset()
: Native
- solverSetParams()
: Native
- solverToString()
: Native
- solverTranslate()
: Native
- sort()
: sort
, ArithRef
, ArrayRef
, BitVecRef
, BoolRef
, DatatypeRef
, ExprRef
, FiniteDomainRef
, FPRef
, QuantifierRef
, SeqRef
- sort_kind()
: sort
, ExprRef
- sorts()
: ModelRef
- sortToAst()
: Native
- sortToString()
: Native
- SortUniverse()
: Model
- statistics()
: optimize
, solver
, Fixedpoint
, Optimize
, Solver
- stats()
: stats
- statsDecRef()
: Native
- statsGetDoubleValue()
: Native
- statsGetKey()
: Native
- statsGetUintValue()
: Native
- statsIncRef()
: Native
- statsIsDouble()
: Native
- statsIsUint()
: Native
- statsSize()
: Native
- statsToString()
: Native
- Status()
: Status
- storeReference()
: IDecRefQueue< T extends Z3Object >
- str()
: symbol
- str_symbol()
: context
- string_sort()
: context
- string_val()
: context
- subsort()
: ArithSortRef
, BitVecSortRef
, BoolSortRef
, SortRef
- substitute()
: Expr
, Native
- Substitute()
: Expr
- substitute()
: expr
- substituteVars()
: Expr
, Native
- SubstituteVars()
: Expr
- Symbol()
: Symbol
- symbol()
: symbol