package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Library
Module
Module type
Parameter
Class
Class type

Term definitions of the abstract syntax

and expr =
  1. | Val of Value.t
  2. | Ptr of {
    1. base : int32;
    2. offset : t;
    }
  3. | Symbol of Symbol.t
  4. | List of t list
  5. | App : [> `Op of string ] * t list -> expr
  6. | Unop of Ty.t * Ty.unop * t
  7. | Binop of Ty.t * Ty.binop * t * t
  8. | Triop of Ty.t * Ty.triop * t * t * t
  9. | Relop of Ty.t * Ty.relop * t * t
  10. | Cvtop of Ty.t * Ty.cvtop * t
  11. | Naryop of Ty.t * Ty.naryop * t list
  12. | Extract of t * int * int
  13. | 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 ptr : int32 -> t -> t
val symbol : Symbol.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 naryop : Ty.t -> Ty.naryop -> t list -> t

Smart naryop constructor, applies simplifications at constructor level

val naryop' : Ty.t -> Ty.naryop -> t list -> t

Dumb naryop 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct