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
    
    Ints
    
    Map
    
    Set
    
    X
    
    Type
    
    Ints
    
    Map
    
    Set
    
    X
  - Arrays_rel
  - Bitlist
  - Bitv
    
    ALIEN
    
    Shostak
    
    X
  - Bitv_rel
  - Ccx
    
    Main
    
    S
  - Cnf
  - Commands
  - Compat
    
    List
    
    Seq
    
    String
    
    Type
    
    Id
  - D_cnf
  - D_loop
    
    Header
    
    Parser
    
    Pipeline
    
    State
    
    Typer
    
    Ext
    
    Typer_Pipe
  - D_state_option
    
    Accessor
    
    Mode
    
    ProduceAssignment
    
    S
    
    SatSolver
    
    SatSolverModule
    
    Steps
    
    StrictMode
  - Domains
    
    Make
    
    D
    
    Ephemeral
    
    Canon
    
    Entry
    
    Entry
    
    NF
    
    Atom
    
    Map
    
    Set
    
    Table
    
    Composite
    
    Map
    
    Set
    
    Table
    
    W
    
    Map
    
    Set
  - Domains_intf
    
    ComparableType
    
    Map
    
    Set
    
    Table
    
    Domain
    
    EntryNotation
    
    EphemeralDomainMap
    
    Entry
    
    NormalForm
    
    Atom
    
    Map
    
    Set
    
    Table
    
    Composite
    
    Map
    
    Set
    
    Table
    
    OrderedType
    
    Map
    
    Set
    
    S
    
    Ephemeral
    
    Canon
    
    Entry
    
    Entry
    
    NF
    
    Atom
    
    Map
    
    Set
    
    Table
    
    Composite
    
    Map
    
    Set
    
    Table
  - Emap
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Errors
  - Explanation
    
    MI
  - Expr
    
    ArraysEx
    
    BV
    
    Core
    
    Ints
    
    Map
    
    Reals
    
    Set
    
    Table
  - Fpa_rounding
  - Frontend
    
    Make
    
    SAT
    
    S
  - Fun_sat
    
    Make
    
    _
  - Fun_sat_frontend
    
    Make
    
    _
  - Gc_debug
  - Hconsing
    
    HASHED
    
    Make
    
    H
    
    S
  - Heap
    
    MakeOrdered
    
    V
    
    MakeRanked
    
    Rank
    
    OrderedTypeDefault
    
    RankedType
  - Hstring
    
    Map
    
    Set
  - Id
    
    Namespace
    
    Abstract
    
    Internal
    
    S
    
    Skolem
  - Inequalities
    
    Container_SIG
    
    Make
    
    MINEQS
    
    MP
    
    P
    
    Ints
    
    Map
    
    Set
    
    FM
    
    MINEQS
    
    MP
    
    P
    
    Ints
    
    Map
    
    Set
    
    S
    
    MINEQS
    
    MP
    
    P
    
    Ints
    
    Map
    
    Set
  - Input
    
    S
  - Instances
    
    Make
    
    X
    
    S
  - IntervalCalculus
  - Intervals
    
    Int
    
    Interval
    
    Legacy
    
    Real
    
    Interval
  - Intervals_core
    
    Make
    
    Ex
    
    Union
    
    Interval
    
    OT
  - Intervals_intf
    
    AlgebraicField
    
    Interval
    
    AlgebraicType
    
    Core
    
    Union
    
    Interval
    
    OT
    
    EuclideanRing
    
    Interval
    
    EuclideanType
    
    Explanations
    
    Field
    
    Interval
    
    FieldType
    
    Interval
    
    OrderedType
    
    Ring
    
    Interval
    
    RingType
    
    Union
    
    Interval
  - Ite_rel
  - Literal
    
    Make
    
    Map
    
    Sem
    
    Map
    
    Set
    
    Set
    
    Table
    
    S
    
    Map
    
    Set
    
    Table
  - Loc
  - Matching
    
    Arg
    
    Make
    
    X
    
    S
  - Matching_types
  - ModelMap
  - Models
  - My_list
  - My_unix
  - My_zip
  - Nest
  - Numbers
    
    Q
    
    Z
  - Objective
    
    Function
    
    Model
    
    Value
  - Options
    
    Output
    
    Sources
    
    Time
  - Parsed
  - Parsed_interface
  - Polynome
    
    EXTENDED_Polynome
    
    Ints
    
    Map
    
    Set
    
    Make
    
    Ints
    
    Map
    
    Set
    
    X
    
    S
    
    T
    
    Ints
    
    Map
    
    Set
  - Printer
  - Profiling
  - Records
    
    ALIEN
    
    Shostak
    
    X
  - Records_rel
  - Rel_utils
    
    Delayed
    
    HLR
    
    XComparable
  - Relation
  - Sat_solver
  - Sat_solver_sig
    
    S
    
    SatContainer
    
    Make
    
    _
  - Satml
    
    Make
    
    Th
    
    SAT_ML
  - Satml_frontend
    
    Make
    
    _
  - Satml_frontend_hybrid
    
    Make
    
    _
  - Satml_types
    
    ATOM
    
    Map
    
    Set
    
    Atom
    
    Map
    
    Set
    
    FLAT_FORMULA
    
    Map
    
    Set
    
    Flat_Formula
    
    Map
    
    Set
    
    Proxy_formula
  - Shostak
    
    Ac
    
    Adt
    
    Arith
    
    Bitv
    
    Combine
    
    HX
    
    L
    
    Map
    
    Set
    
    Literal
    
    Map
    
    Set
    
    Table
    
    MXH
    
    Polynome
    
    Ints
    
    Map
    
    Set
    
    Records
    
    SXH
  - Sig
    
    SHOSTAK
    
    X
  - Sig_rel
    
    RELATION
  - Steps
  - Symbols
    
    Map
    
    Set
  - Th_util
  - Theories
    
    Set
  - Theory
    
    Main_Default
    
    Main_Empty
    
    S
  - Timers
  - Ty
    
    M
    
    Set
    
    Svty
  - Typechecker
  - Typed
  - Uf
    
    GlobalDomain
    
    GlobalDomains
  - Uid
    
    Term_set
    
    Ty_map
  - Uqueue
    
    Make
    
    H
    
    S
  - Use
    
    SA
  - Util
    
    MI
    
    MS
    
    SI
    
    SS
  - Var
    
    Map
    
    Set
  - Vec
  - Version
  - Xliteral
    
    Make
    
    Map
    
    Set
    
    X
    
    OrderedType
    
    S
    
    Map
    
    Set

Legend:
Library
Module
Module type
Parameter
Class
Class type

Module signature for normal form computations.

type constant

The type of constant values.

module Atom : Domains_intf.ComparableType

Atomic variables cannot be decomposed further.

val type_info : Atom.t -> Ty.t

type_info a returns the type of atomic variable x.

module Composite : Domains_intf.ComparableType

Composite variables are obtained through a combination of atomic variables (e.g. a multi-variate polynomial).

val fold_composite : (Atom.t -> 'a -> 'a) -> Composite.t -> 'a -> 'a

fold_composite f c acc folds f over all the atoms that make up c.

type t =

| Constant of constant
(*
A constant value.
*)
| Atom of Atom.t * constant
(*
An atomic variable with a constant offset.
*)
| Composite of Composite.t * constant
(*
A composite variable with a constant offset.
*)

The type of normal forms.

val normal_form : AltErgoLib.Domains_intf.X.r -> t

normal_form e computes the normal form of expression e.