Module AltErgoLib

module Ac : sig ... end
module Adt : sig ... end
module Adt_rel : sig ... end
module Arith : sig ... end
module Arrays_rel : sig ... end
module Bitlist : sig ... end

Bit-lists provide a domain on bit-vectors that represent the known bits sets to 1 and 0, respectively.

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
module D_cnf : sig ... end
module D_loop : sig ... end
module D_state_option : sig ... end

The Dolmen state option manager. Each module defined below is linked to an option that can be set, fetched et reset independently from the Options module, which is used as a static reference.

module Domains : sig ... end
module Domains_intf : sig ... end
module Emap : 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 Fun_sat_frontend : sig ... end
module Gc_debug : sig ... end
module Hconsing : sig ... end

Generic Hashconsing.

module Heap : sig ... end

Heaps.

module Hstring : sig ... end
module Id : sig ... end
module Inequalities : sig ... end
module Input : sig ... end

Typed input

module Instances : sig ... end
module IntervalCalculus : sig ... end
module Intervals : sig ... end
module Intervals_core : sig ... end

This module implements union of intervals with explanations. See the Intervals_intf.Core signature.

module Intervals_intf : sig ... end

Interface for union-of-interval modules.

module Ite_rel : sig ... end
module Literal : sig ... end

This module contains a definition of a "combined" literal type that can contain both syntaxic literals (expressions) and semantic literals (that contain semantic values, see also the Xliteral module).

module Loc : sig ... end

Position in input files

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

Lists utilies This modules defines some helper functions on lists

module My_unix : 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 Nest : sig ... end
module Numbers : sig ... end
module Objective : 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 Rel_utils : 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 Uid : sig ... end
module Uqueue : sig ... end

First-in first-out *unique* queues.

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