package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

doc
- Library alt-ergo-lib
  - AltErgoLib
    
    Ac
    
    S
    
    Make
    
    Adt
    
    ALIEN
    
    Shostak
    
    Adt_rel
    
    Arith
    
    Type
    
    Shostak
    
    Arrays
    
    ALIEN
    
    Shostak
    
    Arrays_rel
    
    Bitv
    
    ALIEN
    
    Shostak
    
    Bitv_rel
    
    Ccx
    
    S
    
    Main
    
    Cnf
    
    Commands
    
    Config
    
    Emap
    
    OrderedType
    
    S
    
    Make
    
    Enum
    
    ALIEN
    
    Shostak
    
    Enum_rel
    
    Errors
    
    Explanation
    
    MI
    
    Expr
    
    Set
    
    Map
    
    Fpa_rounding
    
    Frontend
    
    S
    
    Make
    
    Fun_sat
    
    Make
    
    Gc_debug
    
    Hconsing
    
    HASHED
    
    S
    
    Make
    
    Hstring
    
    Set
    
    Map
    
    Iheap
    
    Inequalities
    
    S
    
    P
    
    MP
    
    MINEQS
    
    FM
    
    P
    
    MP
    
    MINEQS
    
    Container_SIG
    
    Make
    
    P
    
    MP
    
    MINEQS
    
    Input
    
    S
    
    Instances
    
    S
    
    Make
    
    IntervalCalculus
    
    Intervals
    
    Ite
    
    ALIEN
    
    Shostak
    
    Ite_rel
    
    Lists
    
    Loc
    
    Matching
    
    S
    
    Arg
    
    Make
    
    Matching_types
    
    MyDynlink
    
    MyUnix
    
    Numbers
    
    Z
    
    Q
    
    Z
    
    NumbersInterface
    
    ZSig
    
    QSig
    
    Z
    
    NumsNumbers
    
    Z
    
    Q
    
    Z
    
    Options
    
    Time
    
    Parsed
    
    Parsed_interface
    
    Polynome
    
    S
    
    T
    
    EXTENDED_Polynome
    
    Make
    
    Profiling
    
    Records
    
    ALIEN
    
    Shostak
    
    Records_rel
    
    Relation
    
    Sat_solver
    
    Sat_solver_sig
    
    S
    
    SatContainer
    
    Make
    
    Satml
    
    SAT_ML
    
    Make
    
    Satml_frontend
    
    Make
    
    Satml_frontend_hybrid
    
    Make
    
    Satml_types
    
    ATOM
    
    Set
    
    Map
    
    Atom
    
    Set
    
    Map
    
    FLAT_FORMULA
    
    Set
    
    Map
    
    Flat_Formula
    
    Set
    
    Map
    
    Proxy_formula
    
    Shostak
    
    Combine
    
    Polynome
    
    Arith
    
    Records
    
    Bitv
    
    Arrays
    
    Enum
    
    Adt
    
    Ite
    
    Ac
    
    Sig
    
    SHOSTAK
    
    X
    
    Sig_rel
    
    RELATION
    
    Symbols
    
    Set
    
    Map
    
    Th_util
    
    Theory
    
    S
    
    Main_Default
    
    Main_Empty
    
    Timers
    
    Ty
    
    Svty
    
    Set
    
    M
    
    Typechecker
    
    Typed
    
    Uf
    
    LX
    
    Map
    
    Set
    
    Use
    
    SA
    
    Util
    
    MI
    
    SS
    
    Var
    
    Map
    
    Set
    
    Vec
    
    Version
    
    Xliteral
    
    OrderedType
    
    S
    
    Map
    
    Set
    
    Make
    
    Map
    
    Set
    
    ZarithNumbers
    
    Z
    
    Q
    
    Z
- Sources
  - alt-ergo-lib
    
    ac.ml
    
    adt.ml
    
    adt_rel.ml
    
    altErgoLib.ml
    
    arith.ml
    
    arrays.ml
    
    arrays_rel.ml
    
    bitv.ml
    
    bitv_rel.ml
    
    ccx.ml
    
    cnf.ml
    
    commands.ml
    
    config.ml
    
    emap.ml
    
    enum.ml
    
    enum_rel.ml
    
    errors.ml
    
    explanation.ml
    
    expr.ml
    
    fpa_rounding.ml
    
    frontend.ml
    
    fun_sat.ml
    
    gc_debug.ml
    
    hconsing.ml
    
    hstring.ml
    
    iheap.ml
    
    inequalities.ml
    
    input.ml
    
    instances.ml
    
    intervalCalculus.ml
    
    intervals.ml
    
    ite.ml
    
    ite_rel.ml
    
    lists.ml
    
    loc.ml
    
    matching.ml
    
    myDynlink.ml
    
    myUnix.ml
    
    numbers.ml
    
    numsNumbers.ml
    
    options.ml
    
    parsed.ml
    
    parsed_interface.ml
    
    polynome.ml
    
    profiling.ml
    
    records.ml
    
    records_rel.ml
    
    relation.ml
    
    sat_solver.ml
    
    sat_solver_sig.ml
    
    satml.ml
    
    satml_frontend.ml
    
    satml_frontend_hybrid.ml
    
    satml_types.ml
    
    shostak.ml
    
    symbols.ml
    
    th_util.ml
    
    theory.ml
    
    timers.ml
    
    ty.ml
    
    typechecker.ml
    
    typed.ml
    
    uf.ml
    
    use.ml
    
    util.ml
    
    var.ml
    
    vec.ml
    
    version.ml
    
    xliteral.ml
    
    zarithNumbers.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `AltErgoLib.Sat_solver`Source

Sourceval get_current : unit -> (module Sat_solver_sig.SatContainer)

returns the current activated SAT-solver depending on the value of `Options.sat_solver ()`. See command-line option `-sat-solver` for more details *

package alt-ergo-lib

Module AltErgoLib.Sat_solverSource

Module `AltErgoLib.Sat_solver`Source