Module Smtml.ExprSource

Term definitions of the abstract syntax

Sourceand expr =
  1. | Val of Value.t
  2. | Ptr of int32 * t
  3. | Symbol of Symbol.t
  4. | List of t list
  5. | Array of t array
  6. | Tuple of t list
  7. | App : [> `Op of string ] * t list -> expr
  8. | Unop of Ty.t * Ty.unop * t
  9. | Binop of Ty.t * Ty.binop * t * t
  10. | Triop of Ty.t * Ty.triop * t * t * t
  11. | Relop of Ty.t * Ty.relop * t * t
  12. | Cvtop of Ty.t * Ty.cvtop * t
  13. | Extract of t * int * int
  14. | Concat of t * t
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval make : expr -> t
Sourceval (@:) : expr -> Ty.t -> t
  • deprecated Please use 'make' instead
Sourceval view : t -> expr
Sourceval ty : t -> Ty.t
Sourceval mk_symbol : Symbol.t -> t
Sourceval is_symbolic : t -> bool
Sourceval get_symbols : t list -> Symbol.t list
Sourceval negate_relop : t -> (t, string) Result.t
Sourceval pp : Format.formatter -> t -> unit
Sourceval pp_smt : Format.formatter -> t list -> unit
Sourceval pp_list : Format.formatter -> t list -> unit
Sourceval to_string : t -> string
Sourceval value : Value.t -> t
Sourceval symbol : Symbol.t -> t
Sourceval unop : Ty.t -> Ty.unop -> t -> t

Smart unop constructor, applies simplifications at constructor level

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

Dumb unop constructor, no simplifications

Sourceval binop : Ty.t -> Ty.binop -> t -> t -> t

Smart binop constructor, applies simplifications at constructor level

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

Dumb binop constructor, no simplifications

Sourceval triop : Ty.t -> Ty.triop -> t -> t -> t -> t

Smart triop constructor, applies simplifications at constructor level

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

Dumb triop constructor, no simplifications

Sourceval relop : Ty.t -> Ty.relop -> t -> t -> t

Smart relop constructor, applies simplifications at constructor level

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

Dumb relop constructor, no simplifications

Sourceval cvtop : Ty.t -> Ty.cvtop -> t -> t

Smart relop constructor, applies simplifications at constructor level

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

Dumb cvtop constructor, no simplifications

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

Smart extract constructor, applies simplifications at constructor level

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

Dumb extract constructor, no simplifications

Sourceval concat : t -> t -> t

Smart concat constructor, applies simplifications at constructor level

Sourceval concat' : t -> t -> t

Dumb concat constructor, no simplifications

Sourceval simplify : t -> t

Applies expression simplifications until a fixpoint

Sourcemodule Hc : sig ... end
Sourcemodule Bool : sig ... end
Sourcemodule Bitv : sig ... end
Sourcemodule Fpa : sig ... end