package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Exceptions
Type comparison and coercion

package colibri2

colibri2.core
- Colibri2_core
  - Choice
    
    Group
  - Daemon
  - DaemonFixingModel
  - DaemonLastEffort
  - DaemonLastEffortUncontextual
  - DaemonWithFilter
  - DaemonWithKey
    
    Register
    
    S
    
    Key
    
    H
    
    M
    
    S
    
    M
    
    S
    
    Key
    
    H
    
    M
    
    S
    
    M
  - Datastructure
    
    Hashtbl
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Hashtbl2
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Memo
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Memo2
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Push
    
    Ref
    
    Sig
    
    Sig2
  - Debug
  - Dom
    
    Kind
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    Lattice
    
    L
    
    Make
    
    L
    
    S
  - Egraph
  - Env
    
    Saved
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    Unsaved
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
  - Events
    
    Dem
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    T
  - Expr
    
    Term
    
    Const
    
    D
    
    H
    
    M
    
    S
    
    M
    
    HC
    
    H
    
    M
    
    S
    
    M
    
    Var
    
    H
    
    M
    
    S
    
    M
    
    Ty
    
    Const
    
    H
    
    M
    
    S
    
    M
    
    H
    
    M
    
    S
    
    M
    
    Var
    
    H
    
    M
    
    S
    
    M
  - ForSchedulers
    
    Backtrackable
    
    Fix_model
    
    Options
  - Ground
    
    ClosedQuantifier
    
    H
    
    M
    
    S
    
    M
    
    Defs
    
    H
    
    M
    
    NotTotallyApplied
    
    S
    
    M
    
    Subst
    
    H
    
    M
    
    S
    
    M
    
    Term
    
    H
    
    M
    
    S
    
    M
    
    Ty
    
    H
    
    M
    
    S
    
    M
  - Init
  - Interp
    
    Register
    
    SeqLim
    
    WatchArgs
  - Monad
  - Node
    
    H
    
    HC
    
    M
    
    S
    
    M
  - Options
  - ThTerm
    
    H
    
    Kind
    
    Eq
    
    Make_Registry
    
    S
    
    MkVector
    
    D
    
    Vector
    
    M
    
    Register
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
    
    T
    
    H
    
    M
    
    S
    
    M
    
    S
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - Value
    
    H
    
    Kind
    
    Eq
    
    Make_Registry
    
    S
    
    MkVector
    
    D
    
    Vector
    
    M
    
    Register
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
    
    T
    
    H
    
    M
    
    S
    
    M
    
    S
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
colibri2.popop_lib
- Colibri2_popop_lib
  - Bag
  - Cmdline
  - Enum
  - Exn_printer
  - Exthtbl
    
    Hashtbl
    
    HashedType
    
    Make
    
    H
    
    Private
    
    S
  - Extmap
    
    Make
    
    Ord
    
    S
  - Extset
    
    Make
    
    M
    
    Ord
    
    MakeHashcons
    
    M
    
    MH
    
    MakeOfMap
    
    M
  - Hashcons
    
    HashedType
    
    Make
    
    H
    
    M
    
    S
    
    M
    
    MakeCat
    
    H
    
    M
    
    S
    
    M
    
    MakeTag
    
    H
    
    M
    
    S
    
    M
    
    S
    
    H
    
    M
    
    S
    
    M
  - IArray
  - Intmap
    
    Make
    
    K
    
    Make
    
    Data
    
    NT
  - Intmap_hetero
    
    Make1
    
    D
    
    K
    
    R1
    
    RMake1
    
    K
    
    S1
  - Leftistheap
    
    Make
    
    X
    
    Ordered
  - Lists
  - Map_intf
    
    Gen_Map_hashcons
    
    Make
    
    Data
    
    NT
    
    HashType
    
    Map
    
    MapUnit
    
    Map_hashcons
    
    OrderedType
    
    PMap
    
    Set
    
    M
    
    Set_hashcons
    
    M
    
    TaggedEqualType
  - Number
  - Opt
  - Popop_stdlib
    
    DBool
    
    H
    
    M
    
    S
    
    M
    
    DFloat
    
    H
    
    M
    
    S
    
    M
    
    DInt
    
    H
    
    M
    
    S
    
    M
    
    DIntOrd
    
    H
    
    M
    
    S
    
    M
    
    DStr
    
    H
    
    M
    
    S
    
    M
    
    DUnit
    
    H
    
    M
    
    S
    
    M
    
    Datatype
    
    H
    
    M
    
    S
    
    M
    
    MakeMSH
    
    H
    
    M
    
    S
    
    M
    
    X
    
    MakeMSHW
    
    H
    
    M
    
    S
    
    W
    
    X
    
    Map
    
    Make
    
    Ord
    
    S
    
    MkDatatype
    
    H
    
    M
    
    S
    
    M
    
    T
    
    NamedDatatype
    
    H
    
    M
    
    S
    
    M
    
    OrderedHashed
    
    X
    
    OrderedHashedType
    
    Printable
    
    TaggedType
    
    XHashtbl
    
    HashedType
    
    Make
    
    H
    
    Private
    
    S
  - Pp
    
    Ansi
  - Print_tree
    
    Make
    
    T
    
    PMake
    
    T
    
    PTree
    
    Tree
  - Refo
  - Simple_vector
  - Strings
    
    Fresh
    
    H
    
    M
    
    S
    
    M
    
    _
    
    Hashcons
    
    H
    
    M
    
    S
    
    M
    
    Make
    
    H
    
    M
    
    S
    
    M
    
    _
  - Sysutil
  - TimeWheel
    
    Make
    
    Context
    
    _
    
    S
  - Unit
    
    H
    
    M
    
    S
  - Util
  - Vector_hetero
    
    Make1
    
    D
    
    K
    
    Make2
    
    D
    
    K
    
    R1
    
    RMake1
    
    K
    
    S1
    
    S2
    
    T1
    
    TMake1
    
    K
  - Weakhtbl
    
    Make
    
    S
    
    S
    
    Weakey
colibri2.solver
- Colibri2_solver
  - Input
  - Scheduler
  - Solver
colibri2.stdlib
- Colibri2_stdlib
  - Context
    
    Array
    
    Basic
    
    S
    
    Clicket
    
    Expert
    
    Hashtbl
    
    S
    
    H
    
    M
    
    S
    
    M
    
    HashtblWithDefault
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Make
    
    S
    
    Memo
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Push
    
    Queue
    
    Ref
    
    Ref2
    
    TimeWheel
    
    Trie
    
    Fold
    
    List
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Set
  - Debug
    
    Args
  - Hashtbl_hetero
    
    Keys1
    
    Keys2
    
    MakeR1
    
    K
    
    MakeR2
    
    K
    
    MakeS1
    
    D
    
    K
    
    MakeS2
    
    D
    
    K
    
    MakeT1
    
    K
    
    R1
    
    R2
    
    S1
    
    S2
    
    T1
  - Hashtbl_hetero_sig
    
    Keys1
    
    Keys2
    
    R1
    
    R2
    
    S1
    
    S2
    
    T1
  - Keys
    
    Key
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    Key2
    
    Eq
    
    Make_Registry
    
    S
    
    MkVector
    
    D
    
    Vector
    
    Make_key
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    _
    
    Make_key2
    
    Eq
    
    Make_Registry
    
    S
    
    MkVector
    
    D
    
    Vector
    
    _
    
    NamedType
    
    NamedType2
    
    Registry
    
    Registry2
  - Keys_sig
    
    Key
    
    Eq
    
    M
    
    Make_Registry
    
    S
    
    MkMap
    
    D
    
    MkVector
    
    D
    
    Vector
    
    VectorH
    
    Key2
    
    Eq
    
    Make_Registry
    
    S
    
    MkVector
    
    D
    
    Vector
    
    NamedType
    
    NamedType2
    
    Registry
    
    Registry2
  - Map_hetero
    
    Keys
    
    MakeR
    
    K
    
    MakeS
    
    D
    
    K
    
    R
    
    S
  - Map_hetero_sig
    
    Keys
    
    R
    
    S
  - Shuffle
  - Std
    
    A
    
    H
    
    M
    
    S
    
    M
    
    Goption
    
    OrderedHashedType
    
    Poly
    
    Q
    
    H
    
    M
    
    S
    
    M
    
    TaggedType
  - Std_sig
    
    OrderedHashedType
    
    TaggedType
  - Wto
    
    Make
    
    Node
colibri2.theories.LRA
- Colibri2_theories_LRA
  - Delta
  - Dom_interval
    
    D
    
    H
    
    M
    
    S
    
    M
    
    Union
    
    Propagate
  - Dom_polynome
  - Dom_product
    
    SolveAbs
    
    SolveSign
  - Fourier
  - LRA
    
    RealValue
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - LRA_build
    
    LastEffort
  - Mul
  - Pivot
    
    Total
    
    P
    
    H
    
    M
    
    S
    
    M
    
    WithUnsolved
    
    P
    
    H
    
    M
    
    S
    
    M
  - Polynome
    
    H
    
    M
    
    S
    
    M
  - Product
    
    H
    
    M
    
    S
    
    M
  - RealValue
    
    Builtin
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - Sign_product
    
    H
    
    M
    
    S
    
    M
  - Simplex
colibri2.theories.LRA.stages.compare_stage
- Colibri2_theories_LRA_stages_compare_stage
  - Compare_stage
    
    Cmp
    
    H
    
    M
    
    S
    
    M
    
    S1
    
    H
    
    M
    
    S
    
    M
    
    Union
    
    S2
    
    H
    
    M
    
    S
    
    M
    
    Union
    
    Union
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.LRA.stages.def
- Colibri2_theories_LRA_stages_def
  - Bound
    
    H
    
    M
    
    S
    
    M
  - Interval_sig
    
    S
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.LRA.stages.stage0
- Colibri2_theories_LRA_stages
  - Interval_domain
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.LRA.stages.stage0.sign_domain
- Colibri2_theories_LRA_stages_stage0_sign_domain
  - Integer_sign_domain
    
    H
    
    M
    
    S
    
    M
    
    Union
  - Sign_domain
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.LRA.stages.stage2
- Colibri2_theories_LRA_stages
  - Interval_domain
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.LRA.stages.stage2.union_domain
- Colibri2_theories_LRA_stages_stage2_union_domain
  - Union
    
    H
    
    M
    
    S
    
    M
    
    Union
colibri2.theories.adt
- Colibri2_theories_adt
  - Adt
  - Adt_dom
  - Adt_value
    
    Case
    
    H
    
    M
    
    S
    
    M
    
    Field
    
    H
    
    M
    
    S
    
    M
    
    H
    
    M
    
    MonoAdt
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - Congruence
colibri2.theories.array
- Colibri2_theories_array
  - Array
  - Array_dom
  - Array_value
  - Common
    
    Builtin
    
    STV
  - DiffGraph
    
    DG
    
    Id_dom
    
    NHT
  - Foreign_dom
  - GE_Array_DP
  - Linearity_dom
  - SharingIsCaring
colibri2.theories.bool
- Colibri2_theories_bool
  - Boolean
    
    BoolValue
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - Equality
colibri2.theories.fp
- Colibri2_theories_fp
  - Dom_interval
  - Fp
  - Fp_value
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
  - Rounding_mode
    
    H
    
    M
    
    S
    
    M
    
    SD
    
    H
    
    M
    
    S
    
    M
colibri2.theories.nseq
- Colibri2_theories_nseq
  - Nseq
colibri2.theories.quantifiers
- Colibri2_theories_quantifiers
  - Callback
    
    H
    
    M
    
    S
    
    M
  - Common
  - Congruence_closure
  - Definitions
  - F
    
    EnvApps
  - FA
    
    H
    
    M
    
    S
    
    M
    
    T
  - F_Pos
    
    H
    
    M
    
    S
    
    M
  - Info
    
    Builtin_skipped_for_trigger
  - InvertedPath
    
    H
    
    HPC
    
    HPN
    
    HPP
    
    HPT
    
    M
    
    S
    
    M
  - PC
    
    H
    
    M
    
    S
    
    M
  - PN
    
    H
    
    M
    
    S
    
    M
  - PP
    
    H
    
    M
    
    S
    
    M
  - PT
    
    H
    
    M
    
    S
    
    M
  - Pattern
    
    EnvTy
    
    H
    
    M
    
    S
    
    M
  - Quantifier
    
    Quantifier_skipped
  - Subst
  - SubstTrie
  - Trigger
    
    H
    
    M
    
    S
    
    M
  - Uninterp
    
    On_uninterpreted_domain

Legend:
Library
Module
Module type
Parameter
Class
Class type

Key generators

Keys are the main programming tools used for implementing extensible types (sem, value, dom, pexp, ...)

Exceptions

Type comparison and coercion

module type Registry = sig ... end

module type NamedType = sig ... end

module type Key = sig ... end

Key with arity 1

module type NamedType2 = sig ... end

module type Registry2 = sig ... end

module type Key2 = sig ... end

Key with arity 2