Module Smtml.Typed

type 'a ty = private Ty.t

The type of a type witness.

type 'a expr = private Expr.t

The type of a typed expression (term).

type real
type regexp
type bitv8
type bitv16
type bitv32
type bitv64
type bitv128
type float32
type float64
module Unsafe : sig ... end
val view : 'a expr -> Expr.expr

view e typed alias for Expr.view. Allows retrieving the underlying structure of the expression e.

val simplify : 'a expr -> 'a expr

simplify e typed alias for Expr.simplify. Performs algebraic simplifications on the expression e.

val symbol : 'a ty -> string -> 'a expr

symbol ty name creates a symbolic constant of type ty with the given name.

val get_symbols : 'a expr list -> Symbol.t list

get_symbols es returns a list of all unique symbols appearing in the list of expressions es.

val ptr : int32 -> bitv32 expr -> bitv32 expr

ptr value base creates a 32-bit pointer expression by adding value to the base address.

module Types : sig ... end
module Bool : sig ... end
module Int : sig ... end
module Real : sig ... end
module String : sig ... end
module Bitv : sig ... end
module Bitv8 : Bitv.S with type w = bitv8
module Bitv16 : Bitv.S with type w = bitv16
module Bitv32 : sig ... end
module Bitv64 : sig ... end
module Bitv128 : sig ... end
module Float32 : sig ... end
module Float64 : sig ... end
module Func : sig ... end

Typed function builders for SMT usage.