- s -
- sbits() : FPRef, FPSortRef
- seq_sort() : context
- set() : ASTVector, ast_vector_tpl< T >::iterator, ast_vector_tpl< T >, config, context, fixedpoint, optimize, params, solver, Fixedpoint, Optimize, ParamsRef, Solver
- set_cutoff() : solver::cube_generator
- set_else() : func_interp
- set_enable_exceptions() : context
- set_predicate_representation() : Fixedpoint
- set_rounding_mode() : context
- setAstPrintMode() : Native
- setError() : Native
- setInternalErrorHandler() : Native
- setParameter() : Global
- setParameters() : Fixedpoint, Optimize, Solver
- setParamValue() : Native
- setPredicateRepresentation() : Fixedpoint
- setPrintMode() : Context
- sexpr() : ApplyResult, AstRef, AstVector, Fixedpoint, Goal, ModelRef, Optimize, Solver
- sign() : FPNumRef
- sign_as_bv() : FPNumRef
- significand() : FPNumRef
- significand_as_bv() : FPNumRef
- significand_as_long() : FPNumRef
- simplify() : Expr, Goal, Native, 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
- solver() : solver, Tactic
- solverAssert() : Native
- solverAssertAndTrack() : Native
- solverCheck() : Native
- solverCheckAssumptions() : Native
- solverCube() : Native
- solverDecRef() : Native
- solverFromFile() : Native
- solverFromString() : Native
- solverGetAssertions() : Native
- solverGetConsequences() : Native
- solverGetHelp() : Native
- solverGetLevels() : Native
- solverGetModel() : Native
- solverGetNonUnits() : Native
- solverGetNumScopes() : Native
- solverGetParamDescrs() : Native
- solverGetProof() : Native
- solverGetReasonUnknown() : Native
- solverGetStatistics() : Native
- solverGetTrail() : Native
- solverGetUnits() : Native
- solverGetUnsatCore() : Native
- solverImportModelConverter() : Native
- solverIncRef() : Native
- solverInterrupt() : Native
- solverPop() : Native
- solverPush() : Native
- solverReset() : Native
- solverSetParams() : Native
- solverToDimacsString() : 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
- statistics() : fixedpoint, 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
- stoi() : expr
- storeReference() : IDecRefQueue< T extends Z3Object >
- str() : symbol
- str_symbol() : context
- string_sort() : context
- string_val() : context
- stringToInt() : Context
- subsort() : ArithSortRef, BitVecSortRef, BoolSortRef, SortRef
- substitute() : Expr, Native, expr
- substituteVars() : Expr, Native
- Symbol() : Symbol
- symbol() : symbol