package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type constant =
  1. | ConstBitv of string
  2. | ConstInt of string
  3. | ConstReal of Numbers.Q.t
  4. | ConstTrue
  5. | ConstFalse
  6. | ConstVoid
type pp_infix =
  1. | PPand
  2. | PPor
  3. | PPxor
  4. | PPimplies
  5. | PPiff
  6. | PPlt
  7. | PPle
  8. | PPgt
  9. | PPge
  10. | PPeq
  11. | PPneq
  12. | PPadd
  13. | PPsub
  14. | PPmul
  15. | PPdiv
  16. | PPmod
  17. | PPpow_int
  18. | PPpow_real
type pp_prefix =
  1. | PPneg
  2. | PPnot
type ppure_type =
  1. | PPTint
  2. | PPTbool
  3. | PPTreal
  4. | PPTunit
  5. | PPTbitv of int
  6. | PPTvarid of string * Loc.t
  7. | PPTexternal of ppure_type list * string * Loc.t
val pp_ppure_type : Stdlib.Format.formatter -> ppure_type -> unit
val pp_ppure_type_list : Stdlib.Format.formatter -> ppure_type list -> unit
type pattern = {
  1. pat_loc : Loc.t;
  2. pat_desc : string * string list;
}
type lexpr = {
  1. pp_loc : Loc.t;
  2. pp_desc : pp_desc;
}
and pp_desc =
  1. | PPvar of string
  2. | PPapp of string * lexpr list
  3. | PPmapsTo of string * lexpr
  4. | PPinInterval of lexpr * bool * lexpr * lexpr * bool
  5. | PPdistinct of lexpr list
  6. | PPconst of constant
  7. | PPinfix of lexpr * pp_infix * lexpr
  8. | PPprefix of pp_prefix * lexpr
  9. | PPget of lexpr * lexpr
  10. | PPset of lexpr * lexpr * lexpr
  11. | PPdot of lexpr * string
  12. | PPrecord of (string * lexpr) list
  13. | PPwith of lexpr * (string * lexpr) list
  14. | PPextract of lexpr * int * int
  15. | PPconcat of lexpr * lexpr
  16. | PPif of lexpr * lexpr * lexpr
  17. | PPforall of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  18. | PPexists of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  19. | PPforall_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  20. | PPexists_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
  21. | PPnamed of string * lexpr
  22. | PPlet of (string * lexpr) list * lexpr
  23. | PPcheck of lexpr
  24. | PPcut of lexpr
  25. | PPcast of lexpr * ppure_type
  26. | PPmatch of lexpr * (pattern * lexpr) list
  27. | PPisConstr of lexpr * string
  28. | PPproject of lexpr * string
val pp_lexpr : Stdlib.Format.formatter -> lexpr -> unit
val pp_lexpr_list : Stdlib.Format.formatter -> lexpr list -> unit
type plogic_type =
  1. | PPredicate of ppure_type list
  2. | PFunction of ppure_type list * ppure_type
type body_type_decl =
  1. | Record of string * (string * ppure_type) list
  2. | Enum of string list
  3. | Algebraic of (string * (string * ppure_type) list) list
  4. | Abstract
type type_decl = Loc.t * string list * string * body_type_decl
type decl =
  1. | Theory of Loc.t * string * string * decl list
  2. | Axiom of Loc.t * string * Util.axiom_kind * lexpr
  3. | Rewriting of Loc.t * string * lexpr list
  4. | Goal of Loc.t * string * lexpr
  5. | Check_sat of Loc.t * string * lexpr
  6. | Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type
  7. | Predicate_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * lexpr
  8. | Function_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * ppure_type * lexpr
  9. | MutRecDefs of (Loc.t * (string * string) * (Loc.t * string * ppure_type) list * ppure_type option * lexpr) list
  10. | TypeDecl of type_decl list
  11. | Push of Loc.t * int
  12. | Pop of Loc.t * int
  13. | Reset of Loc.t
  14. | Exit of Loc.t
  15. | Optimize of Loc.t * lexpr * bool
type file = decl list
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct