package smtml

You can search for identifiers within the package.

in-package search v0.2.0

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

type t = expr Hc.hash_consed

Term definitions of the abstract syntax

and expr =

| Val of Value.t
| Ptr of int32 * t
| Symbol of Symbol.t
| List of t list
| Array of t array
| Tuple of t list
| App : [> `Op of string ] * t list -> expr
| Unop of Ty.t * Ty.unop * t
| Binop of Ty.t * Ty.binop * t * t
| Triop of Ty.t * Ty.triop * t * t * t
| Relop of Ty.t * Ty.relop * t * t
| Cvtop of Ty.t * Ty.cvtop * t
| Extract of t * int * int
| Concat of t * t

val equal : t -> t -> bool

val hash : t -> int

val make : expr -> t

val (@:) : expr -> Ty.t -> t

deprecated Please use 'make' instead

val view : t -> expr

val ty : t -> Ty.t

val mk_symbol : Symbol.t -> t

val is_symbolic : t -> bool

val get_symbols : t list -> Symbol.t list

val negate_relop : t -> (t, string) Result.t

val pp : Format.formatter -> t -> unit

val pp_smt : Format.formatter -> t list -> unit

val pp_list : Format.formatter -> t list -> unit

val to_string : t -> string

val value : Value.t -> t

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

Smart unop constructor, applies simplifications at constructor level

val unop' : Ty.t -> Ty.unop -> t -> t

Dumb unop constructor, no simplifications

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

Smart binop constructor, applies simplifications at constructor level

val binop' : Ty.t -> Ty.binop -> t -> t -> t

Dumb binop constructor, no simplifications

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

Smart triop constructor, applies simplifications at constructor level

val triop' : Ty.t -> Ty.triop -> t -> t -> t -> t

Dumb triop constructor, no simplifications

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

Smart relop constructor, applies simplifications at constructor level

val relop' : Ty.t -> Ty.relop -> t -> t -> t

Dumb relop constructor, no simplifications

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

Smart relop constructor, applies simplifications at constructor level

val cvtop' : Ty.t -> Ty.cvtop -> t -> t

Dumb cvtop constructor, no simplifications

val extract : t -> high:int -> low:int -> t

Smart extract constructor, applies simplifications at constructor level

val extract' : t -> high:int -> low:int -> t

Dumb extract constructor, no simplifications

val concat : t -> t -> t

Smart concat constructor, applies simplifications at constructor level

val concat' : t -> t -> t

Dumb concat constructor, no simplifications

val simplify : t -> t

Applies expression simplifications until a fixpoint

module Hc : sig ... end

module Bool : sig ... end

module Bitv : sig ... end

module Fpa : sig ... end