package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type
type 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
val mk_enum : string -> string list -> smt_typ
val mk_record : string -> (string * smt_typ) list -> smt_typ
val mk_variant : string -> (string * smt_typ) list -> smt_typ
type smt_array_info =
  1. | Fixed of int
type 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
val fold_smt_exp : (smt_exp -> smt_exp) -> smt_exp -> smt_exp
val smt_conj : smt_exp list -> smt_exp
val smt_disj : smt_exp list -> smt_exp
val extract : int -> int -> smt_exp -> smt_exp
val bvnot : smt_exp -> smt_exp
val bvand : smt_exp -> smt_exp -> smt_exp
val bvor : smt_exp -> smt_exp -> smt_exp
val bvneg : smt_exp -> smt_exp
val bvadd : smt_exp -> smt_exp -> smt_exp
val bvsub : smt_exp -> smt_exp -> smt_exp
val bvmul : smt_exp -> smt_exp -> smt_exp
val bvudiv : smt_exp -> smt_exp -> smt_exp
val bvurem : smt_exp -> smt_exp -> smt_exp
val bvshl : smt_exp -> smt_exp -> smt_exp
val bvlshr : smt_exp -> smt_exp -> smt_exp
val bvult : smt_exp -> smt_exp -> smt_exp
val bvzero : int -> smt_exp
val bvones : int -> smt_exp
val bvone : int -> smt_exp
val simp : smt_exp -> smt_exp
type 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
val declare_datatypes : smt_typ -> smt_def