package libsail

  1. Overview
  2. Docs

Module Libsail.Smt_expSource

Sourcetype smt_typ =
  1. | Bitvec of int
  2. | Bool
  3. | String
  4. | Real
  5. | Datatype of string * (string * (string * smt_typ) list) list
  6. | Array of smt_typ * smt_typ
Sourceval mk_enum : string -> string list -> smt_typ
Sourceval mk_record : string -> (string * smt_typ) list -> smt_typ
Sourceval mk_variant : string -> (string * smt_typ) list -> smt_typ
Sourcetype smt_array_info =
  1. | Fixed of int
Sourcetype smt_exp =
  1. | Bool_lit of bool
  2. | Bitvec_lit of Sail2_values.bitU list
  3. | Real_lit of string
  4. | String_lit of string
  5. | Var of Jib.name
  6. | Enum of string
  7. | Fn of string * smt_exp list
  8. | Ite of smt_exp * smt_exp * smt_exp
  9. | SignExtend of int * int * smt_exp
  10. | ZeroExtend of int * int * smt_exp
  11. | Extract of int * int * smt_exp
  12. | Tester of string * smt_exp
  13. | Unwrap of Ast.id * bool * smt_exp
  14. | Field of Ast.id * Ast.id * smt_exp
  15. | Store of smt_array_info * string * smt_exp * smt_exp * smt_exp
  16. | Empty_list
  17. | Hd of string * smt_exp
  18. | Tl of string * smt_exp
Sourceval fold_smt_exp : (smt_exp -> smt_exp) -> smt_exp -> smt_exp
Sourceval smt_conj : smt_exp list -> smt_exp
Sourceval smt_disj : smt_exp list -> smt_exp
Sourceval extract : int -> int -> smt_exp -> smt_exp
Sourceval bvnot : smt_exp -> smt_exp
Sourceval bvand : smt_exp -> smt_exp -> smt_exp
Sourceval bvor : smt_exp -> smt_exp -> smt_exp
Sourceval bvneg : smt_exp -> smt_exp
Sourceval bvadd : smt_exp -> smt_exp -> smt_exp
Sourceval bvsub : smt_exp -> smt_exp -> smt_exp
Sourceval bvmul : smt_exp -> smt_exp -> smt_exp
Sourceval bvudiv : smt_exp -> smt_exp -> smt_exp
Sourceval bvurem : smt_exp -> smt_exp -> smt_exp
Sourceval bvshl : smt_exp -> smt_exp -> smt_exp
Sourceval bvlshr : smt_exp -> smt_exp -> smt_exp
Sourceval bvult : smt_exp -> smt_exp -> smt_exp
Sourceval bvzero : int -> smt_exp
Sourceval bvones : int -> smt_exp
Sourceval bvone : int -> smt_exp
Sourceval simp : smt_exp -> smt_exp
Sourcetype smt_def =
  1. | Define_fun of string * (string * smt_typ) list * smt_typ * smt_exp
  2. | Declare_fun of string * smt_typ list * smt_typ
  3. | Declare_const of string * smt_typ
  4. | Define_const of string * smt_typ * smt_exp
  5. | Declare_datatypes of string * (string * (string * smt_typ) list) list
  6. | Assert of smt_exp
Sourceval declare_datatypes : smt_typ -> smt_def