package colibri2

You can search for identifiers within the package.

in-package search v0.2.0

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

Context and backtrack point management

type context

A context, with an history of backtrack point

type creator

Same than context, but only used for creating datastructure

val creator : context -> creator

type bp

A backtrack point associated to a context

val create : unit -> context

Create a new context, with a base backtrack point. It is not possible to go below this backtrack point.

val bp : context -> bp

Get the current backtrack point

val push : context -> unit

Push a new backtrack point

exception AlreadyPoped

val pop : bp -> unit

Pop the context associated to this backtrack point to this backtrack point. All the backtrack point created since the given backtrack point are also poped.

raise AlreadyPoped if it already has been poped.

module Ref : sig ... end

module Ref2 : sig ... end

type 'a history

history of the values

module Make (S : sig ... end) : sig ... end

module Basic (S : sig ... end) : sig ... end

module Expert : sig ... end

module Push : sig ... end

module Queue : sig ... end

The saving is equal to the current size of the datastructure. Should be used when usually it is empty at backtrack point

module Array : sig ... end

module TimeWheel : Colibri2_popop_lib.TimeWheel.S with type context := creator

module type Hashtbl = sig ... end

module Hashtbl
  (S : Colibri2_popop_lib.Popop_stdlib.Datatype) : 
  Hashtbl with type key := S.t

module type HashtblWithDefault = sig ... end

module HashtblWithDefault
  (S : Colibri2_popop_lib.Popop_stdlib.Datatype) : 
  HashtblWithDefault with type key := S.t

module type Memo = sig ... end

module Memo
  (S : Colibri2_popop_lib.Popop_stdlib.Datatype) : 
  Memo with type key := S.t

Clicket

The added element are given back after each pop

module type Clicket = sig ... end

module Clicket : Clicket

type 'k fold = {

fold : 'a. ('a -> 'k -> 'a) -> 'a -> 'a;

}

module type Trie = sig ... end

module Trie
  (S : Colibri2_popop_lib.Popop_stdlib.Datatype) : 
  Trie with type key := S.t and type Set.set := S.S.t