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
  - Compat
    
    Seq
    
    String
  - D_cnf
  - D_loop
    
    Header
    
    Parser
    
    Pipeline
    
    Typer
    
    Typer_Pipe
  - Emap
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Enum
    
    ALIEN
    
    Shostak
    
    X
  - Enum_rel
  - Errors
  - Explanation
  - Expr
    
    BV
    
    Core
    
    Ints
  - Fpa_rounding
  - Frontend
    
    Make
    
    SAT
    
    S
  - Fun_sat
    
    Make
    
    Th
  - Gc_debug
  - Hconsing
    
    HASHED
    
    Make
    
    H
    
    S
  - Hstring
  - Iheap
  - Inequalities
    
    Container_SIG
    
    Make
    
    MINEQS
    
    P
    
    FM
    
    MINEQS
    
    P
    
    S
    
    MINEQS
    
    P
  - Input
    
    S
  - Instances
    
    Make
    
    X
    
    S
  - IntervalCalculus
  - Intervals
  - Ite
    
    ALIEN
    
    Shostak
    
    X
  - Ite_rel
  - Lists
  - Loc
  - Matching
    
    Arg
    
    Make
    
    X
    
    S
  - Matching_types
  - ModelMap
  - Models
  - MyUnix
  - My_zip
  - Numbers
    
    Q
    
    Z
  - Options
    
    Output
    
    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
    
    Atom
    
    FLAT_FORMULA
    
    Flat_Formula
    
    Proxy_formula
  - Shostak
    
    Ac
    
    Adt
    
    Arith
    
    Arrays
    
    Bitv
    
    Combine
    
    Enum
    
    Ite
    
    Polynome
    
    Records
  - Sig
    
    SHOSTAK
    
    X
  - Sig_rel
    
    RELATION
  - Steps
  - Symbols
    
    Map
  - Th_util
  - Theories
  - Theory
    
    Main_Default
    
    Main_Empty
    
    S
  - Timers
  - Ty
  - Typechecker
  - Typed
  - Uf
    
    LX
  - Use
  - Util
  - Var
  - Vec
  - Version
  - Xliteral
    
    Make
    
    X
    
    OrderedType
    
    S

Legend:
Library
Module
Module type
Parameter
Class
Class type

Hashed values.

This signature defines the interface required for values to be hashconsed.

type elt

The type of hashed elements

val eq : elt -> elt -> bool

Equality predicate on values.

val hash : elt -> int

Hash function on values. Must be compatible with the equality function, i.e: equality of values imply that hashes are equal.

val set_id : int -> elt -> elt

Set an id to the given value. This id should not be considered by the equality function when comparing values. Should not mutate the given value for the hashconsing to be correct.

val initial_size : int

Initial size for the hashconsing table.

val disable_weaks : unit -> bool

Values hashconsed when this returns true are treated as always reachable by the gc and thus will not be collected.