package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

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

Parameters

module Th : Theory.S

Signature

type th = Th.t

type t

val solve : t -> unit

val set_new_proxies : 
  t ->
  (Satml_types.Atom.atom * Satml_types.Atom.atom list * bool)
    AltErgoLib.Util.MI.t ->
  unit

val new_vars : 
  t ->
  nbv:int ->
  Satml_types.Atom.var list ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list * Satml_types.Atom.atom list list

val assume : 
  t ->
  Satml_types.Atom.atom list list ->
  Satml_types.Atom.atom list list ->
  Expr.t ->
  cnumber:int ->
  Satml_types.Atom.atom option AltErgoLib.Satml_types.Flat_Formula.Map.t ->
  dec_lvl:int ->
  unit

val boolean_model : t -> Satml_types.Atom.atom list

val instantiation_context : 
  t ->
  Satml_types.Flat_Formula.hcons_env ->
  AltErgoLib.Satml_types.Atom.Set.t

val current_tbox : t -> th

val set_current_tbox : t -> th -> unit

val empty : unit -> t

val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit

val decision_level : t -> int

val cancel_until : t -> int -> unit

val update_lazy_cnf : 
  t ->
  do_bcp:bool ->
  Satml_types.Atom.atom option AltErgoLib.Satml_types.Flat_Formula.Map.t ->
  dec_lvl:int ->
  unit

val exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> bool

val known_lazy_formulas : t -> int AltErgoLib.Satml_types.Flat_Formula.Map.t

val reason_of_deduction : 
  Satml_types.Atom.atom ->
  AltErgoLib.Satml_types.Atom.Set.t

val assume_simple : t -> Satml_types.Atom.atom list list -> unit

val decide : t -> Satml_types.Atom.atom -> unit

val conflict_analyze_and_fix : t -> conflict_origin -> unit

val push : t -> Satml_types.Atom.atom -> unit

val pop : t -> unit