package smtml

  1. Overview
  2. Docs
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.