package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

alt-ergo-lib
- AltErgoLib
  - Ac
    
    Make
    
    X
    
    S
  - Adt
    
    ALIEN
    
    Shostak
    
    X
  - Adt_rel
  - Arith
    
    Shostak
    
    P
    
    X
    
    Type
    
    X
  - Arrays
    
    ALIEN
    
    Shostak
    
    X
  - Arrays_rel
  - Bitv
    
    ALIEN
    
    Shostak
    
    X
  - Bitv_rel
  - Ccx
    
    Main
    
    S
  - Cnf
  - Commands
  - Config
  - Emap
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Enum
    
    ALIEN
    
    Shostak
    
    X
  - Enum_rel
  - Errors
  - Explanation
    
    MI
  - Expr
    
    Map
    
    Set
  - Format_shims
  - Fpa_rounding
  - Frontend
    
    Make
    
    SAT
    
    S
  - Fun_sat
    
    Make
    
    Th
  - Gc_debug
  - Hconsing
    
    HASHED
    
    Make
    
    H
    
    S
  - Hstring
    
    Map
    
    Set
  - Iheap
  - Inequalities
    
    Container_SIG
    
    Make
    
    MINEQS
    
    MP
    
    P
    
    FM
    
    MINEQS
    
    MP
    
    P
    
    S
    
    MINEQS
    
    MP
    
    P
  - Input
    
    S
  - Instances
    
    Make
    
    X
    
    S
  - IntervalCalculus
  - Intervals
  - Ite
    
    ALIEN
    
    Shostak
    
    X
  - Ite_rel
  - Lists
  - Loc
  - Matching
    
    Arg
    
    Make
    
    X
    
    S
  - Matching_types
  - MyDynlink
  - MyUnix
  - Numbers
    
    Q
    
    Z
  - NumbersInterface
    
    QSig
    
    Z
    
    ZSig
  - NumsNumbers
    
    Q
    
    Z
  - Options
    
    Time
  - Parsed
  - Parsed_interface
  - Polynome
    
    EXTENDED_Polynome
    
    Make
    
    X
    
    S
    
    T
  - Printer
  - Profiling
  - Records
    
    ALIEN
    
    Shostak
    
    X
  - Records_rel
  - Relation
  - Sat_solver
  - Sat_solver_sig
    
    S
    
    SatContainer
    
    Make
    
    Th
  - Satml
    
    Make
    
    Th
    
    SAT_ML
  - Satml_frontend
    
    Make
    
    Th
  - Satml_frontend_hybrid
    
    Make
    
    Th
  - Satml_types
    
    ATOM
    
    Map
    
    Set
    
    Atom
    
    Map
    
    Set
    
    FLAT_FORMULA
    
    Map
    
    Set
    
    Flat_Formula
    
    Map
    
    Set
    
    Proxy_formula
  - Shostak
    
    Ac
    
    Adt
    
    Arith
    
    Arrays
    
    Bitv
    
    Combine
    
    Enum
    
    Ite
    
    MXH
    
    MXS
    
    Polynome
    
    Records
    
    SXH
    
    SXS
  - Sig
    
    SHOSTAK
    
    X
  - Sig_rel
    
    RELATION
  - Steps
  - Symbols
    
    Map
    
    Set
  - Th_util
  - Theory
    
    Main_Default
    
    Main_Empty
    
    S
  - Timers
  - Ty
    
    M
    
    Set
    
    Svty
  - Typechecker
  - Typed
  - Uf
    
    LX
    
    Map
    
    Set
  - Use
    
    SA
  - Util
    
    MI
    
    SI
    
    SS
  - Var
    
    Map
    
    Set
  - Vec
  - Version
  - Xliteral
    
    Make
    
    Map
    
    Set
    
    X
    
    OrderedType
    
    S
    
    Map
    
    Set
  - ZarithNumbers
    
    Q
    
    Z

Legend:
Library
Module
Module type
Parameter
Class
Class type

type constant =

| ConstBitv of string
| ConstInt of string
| ConstReal of Num.num
| ConstTrue
| ConstFalse
| ConstVoid

type pp_infix =

| PPand
| PPor
| PPxor
| PPimplies
| PPiff
| PPlt
| PPle
| PPgt
| PPge
| PPeq
| PPneq
| PPadd
| PPsub
| PPmul
| PPdiv
| PPmod
| PPpow_int
| PPpow_real

type pp_prefix =

| PPneg
| PPnot

type ppure_type =

| PPTint
| PPTbool
| PPTreal
| PPTunit
| PPTbitv of int
| PPTvarid of string * Loc.t
| PPTexternal of ppure_type list * string * Loc.t

type pattern = {

pat_loc : Loc.t;
pat_desc : string * string list;

}

type lexpr = {

pp_loc : Loc.t;
pp_desc : pp_desc;

}

and pp_desc =

| PPvar of string
| PPapp of string * lexpr list
| PPmapsTo of string * lexpr
| PPinInterval of lexpr * bool * lexpr * lexpr * bool
| PPdistinct of lexpr list
| PPconst of constant
| PPinfix of lexpr * pp_infix * lexpr
| PPprefix of pp_prefix * lexpr
| PPget of lexpr * lexpr
| PPset of lexpr * lexpr * lexpr
| PPdot of lexpr * string
| PPrecord of (string * lexpr) list
| PPwith of lexpr * (string * lexpr) list
| PPextract of lexpr * lexpr * lexpr
| PPconcat of lexpr * lexpr
| PPif of lexpr * lexpr * lexpr
| PPforall of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPexists of (string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPforall_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPexists_named of (string * string * ppure_type) list * (lexpr list * bool) list * lexpr list * lexpr
| PPnamed of string * lexpr
| PPlet of (string * lexpr) list * lexpr
| PPcheck of lexpr
| PPcut of lexpr
| PPcast of lexpr * ppure_type
| PPmatch of lexpr * (pattern * lexpr) list
| PPisConstr of lexpr * string
| PPproject of bool * lexpr * string

type plogic_type =

| PPredicate of ppure_type list
| PFunction of ppure_type list * ppure_type

type body_type_decl =

| Record of string * (string * ppure_type) list
| Enum of string list
| Algebraic of (string * (string * ppure_type) list) list
| Abstract

type type_decl = Loc.t * string list * string * body_type_decl

type decl =

| Theory of Loc.t * string * string * decl list
| Axiom of Loc.t * string * Util.axiom_kind * lexpr
| Rewriting of Loc.t * string * lexpr list
| Goal of Loc.t * string * lexpr
| Logic of Loc.t * Symbols.name_kind * (string * string) list * plogic_type
| Predicate_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * lexpr
| Function_def of Loc.t * string * string * (Loc.t * string * ppure_type) list * ppure_type * lexpr
| TypeDecl of type_decl list
| Push of Loc.t * int
| Pop of Loc.t * int

type file = decl list