Module AltErgoLibSource

module Ac : sig ... end
module Adt : sig ... end
module Adt_rel : sig ... end
module Arith : sig ... end
module Arrays : sig ... end
module Arrays_rel : sig ... end
module Bitv : sig ... end
module Bitv_rel : sig ... end
module Ccx : sig ... end
module Cnf : sig ... end
module Commands : sig ... end
module Compat : sig ... end

This module enables some of the newer functions from OCaml's stdlib while still supporting old versions of the compiler.

module D_cnf : sig ... end
module D_loop : sig ... end
module Emap : sig ... end
module Enum : sig ... end
module Enum_rel : sig ... end
module Errors : sig ... end
module Explanation : sig ... end
module Expr : sig ... end

Data structures

module Fpa_rounding : sig ... end
module Frontend : sig ... end
module Fun_sat : sig ... end
module Gc_debug : sig ... end
module Hconsing : sig ... end

Generic Hashconsing.

module Hstring : sig ... end
module Iheap : sig ... end

Integer heaps

module Inequalities : sig ... end
module Input : sig ... end

Typed input

module Instances : sig ... end
module IntervalCalculus : sig ... end
module Intervals : sig ... end
module Ite : sig ... end
module Ite_rel : sig ... end
module Lists : sig ... end

Lists utilies

module Loc : sig ... end

Position in input files

module Matching : sig ... end
module Matching_types : sig ... end
module ModelMap : sig ... end

Maps of values for alt-ergo's models. Elements are sorted by symbols/types (P) and accumulated as sets of expressions matching the P.key type (V).

module Models : sig ... end
module MyUnix : sig ... end

Unix wrapper

module My_zip : sig ... end

A wrapper of the Zip module of CamlZip: we use Zip except when we want to generate the.js file for try-Alt-Ergo *

module Numbers : sig ... end
module Options : sig ... end
module Parsed : sig ... end
module Parsed_interface : sig ... end

Declaration of types *

module Polynome : sig ... end
module Printer : sig ... end
module Profiling : sig ... end
module Records : sig ... end
module Records_rel : sig ... end
module Relation : sig ... end
module Sat_solver : sig ... end
module Sat_solver_sig : sig ... end
module Satml : sig ... end
module Satml_frontend : sig ... end
module Satml_frontend_hybrid : sig ... end
module Satml_types : sig ... end
module Shostak : sig ... end
module Sig : sig ... end
module Sig_rel : sig ... end
module Steps : sig ... end

Module_Name

module Symbols : sig ... end
module Th_util : sig ... end
module Theories : sig ... end
module Theory : sig ... end
module Timers : sig ... end
module Ty : sig ... end

Types

module Typechecker : sig ... end
module Typed : sig ... end

Typed AST

module Uf : sig ... end
module Use : sig ... end
module Util : sig ... end
module Var : sig ... end
module Vec : sig ... end
module Version : sig ... end
module Xliteral : sig ... end