package smtml

You can search for identifiers within the package.

in-package search v0.2.0

package smtml

smtml
- Smtml
  - Altergo_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Ast
  - Binder
  - Bitwuzla_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Cache
    
    Strong
  - Cache_intf
    
    Intf
    
    Strong
    
    S
  - Colibri2_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Compile
  - Constructors_intf
    
    Infix
  - Cvc5_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Dolmenexpr_to_expr
    
    Builtin
    
    SHT
  - Eval
  - Expr
    
    Bitv
    
    I32
    
    I64
    
    I8
    
    Bool
    
    Fpa
    
    F32
    
    F64
    
    Hc
    
    Set
    
    BaseMap
    
    WithForeign
    
    Map2
  - Interpret
    
    Make
    
    Solver
  - Interpret_intf
    
    Intf
    
    Make
    
    Solver
    
    S
  - Lexer
  - Log
  - Logic
  - Mappings
    
    Make
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    M_with_make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Smtlib
    
    Solver
  - Mappings_intf
    
    M
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    M_with_make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Make
    
    Bitv
    
    Float
    
    Rounding_mode
    
    Func
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    Model
    
    Optimizer
    
    Re
    
    Real
    
    Smtlib
    
    Solver
    
    String
    
    Types
    
    S
    
    Optimizer
    
    Smtlib
    
    Solver
    
    S_with_fresh
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
  - Model
    
    Parse
    
    Json
    
    Scfg
    
    Smtlib
  - Num
  - Op_intf
    
    S
  - Optimizer
    
    Make
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Z3
  - Optimizer_intf
    
    Intf
    
    Make
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Z3
    
    S
  - Params
  - Parse
    
    Smtlib
    
    Smtml
  - Parser
    
    Incremental
    
    MenhirInterpreter
  - Rewrite
    
    Symb_map
  - Smtlib
    
    Extension
    
    Lexer
    
    Parser
    
    Statement
    
    Term
  - Solver
    
    Batch
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Cached
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Incremental
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
  - Solver_dispatcher
  - Solver_intf
    
    Intf
    
    Batch
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Cached
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Incremental
    
    _
    
    Optimizer
    
    Smtlib
    
    Solver
    
    S
  - Solver_mode
  - Solver_type
  - Statistics
    
    Map
  - Symbol
  - Ty
    
    Binop
    
    Cvtop
    
    Naryop
    
    Relop
    
    Triop
    
    Unop
  - Utils
  - Value
  - Z3_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Smtlib
    
    Solver
    
    Optimizer
    
    Smtlib
    
    Solver
smtml.prelude
- Smtml_prelude
  - Option
  - Result

Legend:
Library
Module
Module type
Parameter
Class
Class type

Rounding modes for floating-point operations.

val rne : term

rne represents the "round nearest ties to even" rounding mode.

val rna : term

rna represents the "round nearest ties to away" rounding mode.

val rtp : term

rtp represents the "round toward positive" rounding mode.

val rtn : term

rtn represents the "round toward negative" rounding mode.

val rtz : term

rtz represents the "round toward zero" rounding mode.