package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

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

The model is search using iterative deepening depth-first search for ensuring optimality even in presence of infinite choice

val next_dec : Egraph.wt -> (Egraph.wt -> unit) Base.Sequence.t

Add a level of decision for fixing the model, another level could be needed. Could raise unsatisfiable if all the model have been tried