package libsail

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.Smt_expSource

Sourcemodule IntSet = Util.IntSet
Sourceval zencode_id : Ast.id -> string
Sourceval zencode_upper_id : Ast.id -> string
Sourceval zencode_name : Jib.name -> string
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 * Jib.ctyp
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. | Unit
  7. | Member of Ast.id
  8. | Fn of string * smt_exp list
  9. | Ite of smt_exp * smt_exp * smt_exp
  10. | SignExtend of int * int * smt_exp
  11. | ZeroExtend of int * int * smt_exp
  12. | Extract of int * int * int * smt_exp
  13. | Tester of Ast.id * smt_exp
  14. | Unwrap of Ast.id * bool * smt_exp
  15. | Field of Ast.id * Ast.id * smt_exp
  16. | Struct of Ast.id * (Ast.id * smt_exp) list
  17. | Store of smt_array_info * string * smt_exp * smt_exp * smt_exp
  18. | Empty_list
  19. | Hd of string * smt_exp
  20. | Tl of string * smt_exp
Sourceval pp_smt_exp : smt_exp -> PPrint.document
Sourceval var_id : Ast.id -> smt_exp
Sourceval fold_smt_exp : (smt_exp -> smt_exp) -> smt_exp -> smt_exp
Sourceval iter_smt_exp : (smt_exp -> 'a) -> smt_exp -> unit
Sourceval smt_exp_size : smt_exp -> int
Sourceval extract : from:int -> 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 bvsdiv : smt_exp -> smt_exp -> smt_exp
Sourceval bvsrem : 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 bvslt : smt_exp -> smt_exp -> smt_exp
Sourceval bvzero : int -> smt_exp
Sourceval bvones : int -> smt_exp
Sourceval bvone' : int -> Sail2_values.bitU list
Sourceval bvone : int -> smt_exp
Sourceval bv_is_zero : Sail2_values.bitU list -> bool
Sourceval smt_conj : smt_exp list -> smt_exp
Sourceval smt_disj : smt_exp list -> smt_exp
Sourceval is_literal : smt_exp -> bool
Sourcemodule SimpSet : sig ... end
Sourceval and_prefer : smt_exp -> int option
Sourceval and_order : smt_exp -> smt_exp -> int
Sourceval or_prefer : smt_exp -> int option
Sourceval or_order : smt_exp -> smt_exp -> int
Sourceval identical : smt_exp -> smt_exp -> bool
Sourceval simp_eq : smt_exp -> smt_exp -> bool option
Sourcemodule Simplifier : sig ... end
Sourceval count : int ref
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 Jib.name * smt_typ
  4. | Define_const of Jib.name * 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
Sourceval pp_sfun : string -> PPrint.document list -> PPrint.document
Sourceval pp_smt_typ : smt_typ -> PPrint.document
Sourceval pp_str_smt_typ : (string * smt_typ) -> PPrint.document
Sourceval pp_smt_def : smt_def -> PPrint.document
Sourceval string_of_smt_def : smt_def -> string
Sourcetype counterexample_solver =
  1. | Cvc5
  2. | Cvc4
  3. | Z3
Sourceval counterexample_command : counterexample_solver -> string
Sourceval counterexample_solver_from_name : string -> counterexample_solver option
Sourcemodule type COUNTEREXAMPLE_CONFIG = sig ... end
OCaml

Innovation. Community. Security.