package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Library
Module
Module type
Parameter
Class
Class type
type binder =
  1. | Forall
  2. | Exists
  3. | Let_in

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 of Symbol.t * t list
  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
  14. | Binder of binder * t list * t
val make : expr -> t
val view : t -> expr
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val ty : t -> Ty.t

The return type of an expression

val is_symbolic : t -> bool
val get_symbols : t list -> Symbol.t list
val negate_relop : t -> (t, string) Smtml_prelude.Result.t
val pp_smt : t list Smtml_prelude.Fmt.t
val pp_list : t list Smtml_prelude.Fmt.t
val to_string : t -> string
val value : Value.t -> t
val ptr : int32 -> t -> t
val symbol : Symbol.t -> t
val app : Symbol.t -> t list -> t
val let_in : t list -> 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 Set : 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