- s -

• sbits() : FPRef , FPSortRef
• seq_sort() : context
• set() : ASTVector , config , context , optimize , params , solver , Fixedpoint , Optimize , ParamsRef , Solver
• set_predicate_representation() : Fixedpoint
• SetLimit() : IDecRefQueue
• setParameter() : Global
• setParameters() : Fixedpoint , Optimize , Solver
• setPredicateRepresentation() : Fixedpoint
• SetPredicateRepresentation() : Fixedpoint
• setPrintMode() : Context
• SExpr() : AST
• sexpr() : ApplyResult , AstRef , AstVector , Fixedpoint , Goal , ModelRef , Optimize , Solver
• sign() : FPNumRef
• significand() : FPNumRef
• simplify() : Expr , Goal
• Simplify() : Expr , Goal
• simplify() : expr , Goal
• simplify_param_descrs() : param_descrs
• 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
• sort() : sort , ArithRef , ArrayRef , BitVecRef , BoolRef , DatatypeRef , ExprRef , FiniteDomainRef , FPRef , QuantifierRef , SeqRef
• sort_kind() : sort , ExprRef
• sorts() : ModelRef
• SortUniverse() : Model
• statistics() : optimize , solver , Fixedpoint , Optimize , Solver
• stats() : stats
• 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
• Substitute() : Expr
• substitute() : expr
• substituteVars() : Expr
• SubstituteVars() : Expr
• Symbol() : Symbol
• symbol() : symbol