package smtml

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package smtml

smtml
- Smtml
  - Ast
  - Cache
    
    Strong
  - Cache_intf
    
    Intf
    
    Strong
    
    S
  - Constructors_intf
    
    Infix
  - Eval
  - Expr
    
    Bitv
    
    I32
    
    I64
    
    I8
    
    Bool
    
    Fpa
    
    F32
    
    F64
    
    Hc
  - Interpret
    
    Make
    
    Solver
  - Interpret_intf
    
    Intf
    
    Make
    
    Solver
    
    S
  - Lexer
  - Log
  - Mappings
    
    Make
    
    Bitv_impl
    
    B
    
    Ixx
    
    Bitv_sig
    
    Ixx
    
    Bool_impl
    
    Float32_impl
    
    Float64_impl
    
    Float_impl
    
    F
    
    Float_sig
    
    I32
    
    Ixx
    
    I64
    
    Ixx
    
    I8
    
    Ixx
    
    Int_impl
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Real_impl
    
    Solver
    
    String_impl
    
    Make'
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    Optimizer
    
    Solver
  - Mappings_intf
    
    M
    
    Bitv
    
    Cont
    
    Float
    
    Rounding_mode
    
    Int
    
    Interp
    
    Model
    
    Optimizer
    
    Real
    
    Solver
    
    String
    
    Types
    
    S
    
    Optimizer
    
    Solver
  - Model
  - Num
  - Op_intf
    
    S
  - Optimizer
    
    Z3
  - Params
  - Parse
  - Parser
  - Solver
    
    Batch
    
    M
    
    Optimizer
    
    Solver
    
    Cached
    
    Cache
    
    M
    
    Optimizer
    
    Solver
    
    Incremental
    
    M
    
    Optimizer
    
    Solver
    
    Z3_batch
    
    Z3_incremental
  - Solver_intf
    
    Intf
    
    Batch
    
    M
    
    Optimizer
    
    Solver
    
    Cached
    
    Cache
    
    M
    
    Optimizer
    
    Solver
    
    Incremental
    
    M
    
    Optimizer
    
    Solver
    
    Z3_batch
    
    Z3_incremental
    
    S
  - Symbol
  - Ty
  - Utils
  - Value
  - Z3_mappings
    
    Fresh
    
    Make
    
    Optimizer
    
    Solver
    
    Optimizer
    
    Solver
  - Z3_mappings2
    
    Optimizer
    
    Solver

Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

module M : Mappings_intf.M

Signature

type 'a with_cont = {

node : 'a;
cont : M.cont;

}

type model = M.model with_cont

type solver = M.solver with_cont

type handle = M.handle

type optimize = M.optimizer with_cont

val err : ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

val get_type : Ty.t -> M.ty M.t

module Bool_impl : sig ... end

module Int_impl : sig ... end

module Real_impl : sig ... end

module String_impl : sig ... end

module type Bitv_sig = sig ... end

module Bitv_impl (B : Bitv_sig) : sig ... end

module I8 : sig ... end

module I32 : sig ... end

module I64 : sig ... end

module type Float_sig = sig ... end

module Float_impl (F : Float_sig) : sig ... end

module Float32_impl : sig ... end

module Float64_impl : sig ... end

val v : Value.t -> M.term M.t

val unop : Ty.t -> Ty.unop -> M.term -> M.term M.t

val binop : Ty.t -> Ty.binop -> M.term -> M.term -> M.term M.t

val triop : Ty.t -> Ty.triop -> M.term -> M.term -> M.term -> M.term M.t

val relop : Ty.t -> Ty.relop -> M.term -> M.term -> M.term M.t

val cvtop : Ty.t -> Ty.cvtop -> M.term -> M.term M.t

val encode_expr : Expr.t -> M.term M.t

val pp_smt : ?status:'a -> 'b -> 'c -> 'd

val value : model -> Expr.t -> Value.t

val values_of_model : 
  ?symbols:Symbol.t list ->
  M.model with_cont ->
  (Symbol.t, Value.t) Stdlib.Hashtbl.t

val set_debug : 'a -> unit

module Solver : sig ... end

module Optimizer : sig ... end