module Ac : sig ... endmodule Adt : sig ... endmodule Adt_rel : sig ... endmodule Arith : sig ... endmodule Arrays_rel : sig ... endmodule Bitlist : sig ... endBit-lists provide a domain on bit-vectors that represent the known bits sets to 1 and 0, respectively.
module Bitv : sig ... endmodule Bitv_rel : sig ... endmodule Ccx : sig ... endmodule Cnf : sig ... endmodule Commands : sig ... endmodule Compat : sig ... endmodule D_cnf : sig ... endmodule D_loop : sig ... endmodule D_state_option : sig ... endThe 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 ... endmodule Domains_intf : sig ... endmodule Emap : sig ... endmodule Errors : sig ... endmodule Explanation : sig ... endmodule Expr : sig ... endData structures
module Fpa_rounding : sig ... endmodule Frontend : sig ... endmodule Fun_sat : sig ... endmodule Fun_sat_frontend : sig ... endmodule Gc_debug : sig ... endmodule Hconsing : sig ... endGeneric Hashconsing.
module Heap : sig ... endHeaps.
module Hstring : sig ... endmodule Id : sig ... endmodule Inequalities : sig ... endmodule Input : sig ... endTyped input
module Instances : sig ... endmodule IntervalCalculus : sig ... endmodule Intervals : sig ... endmodule Intervals_core : sig ... endThis module implements union of intervals with explanations. See the Intervals_intf.Core signature.
module Intervals_intf : sig ... endInterface for union-of-interval modules.
module Ite_rel : sig ... endmodule Literal : sig ... endThis 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 ... endPosition in input files
module Matching : sig ... endmodule Matching_types : sig ... endmodule ModelMap : sig ... endmodule Models : sig ... endmodule My_list : sig ... endLists utilies This modules defines some helper functions on lists
module My_unix : sig ... endUnix wrapper
module My_zip : sig ... endA 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 ... endmodule Numbers : sig ... endmodule Objective : sig ... endmodule Options : sig ... endmodule Parsed : sig ... endmodule Parsed_interface : sig ... endDeclaration of types *
module Polynome : sig ... endmodule Printer : sig ... endmodule Profiling : sig ... endmodule Records : sig ... endmodule Records_rel : sig ... endmodule Rel_utils : sig ... endmodule Relation : sig ... endmodule Sat_solver : sig ... endmodule Sat_solver_sig : sig ... endmodule Satml : sig ... endmodule Satml_frontend : sig ... endmodule Satml_frontend_hybrid : sig ... endmodule Satml_types : sig ... endmodule Shostak : sig ... endmodule Sig : sig ... endmodule Sig_rel : sig ... endmodule Steps : sig ... endModule_Name
module Symbols : sig ... endmodule Th_util : sig ... endmodule Theories : sig ... endmodule Theory : sig ... endmodule Timers : sig ... endmodule Ty : sig ... endTypes
module Typechecker : sig ... endmodule Typed : sig ... endTyped AST
module Uf : sig ... endmodule Uid : sig ... endmodule Uqueue : sig ... endFirst-in first-out *unique* queues.
module Use : sig ... endmodule Util : sig ... endmodule Var : sig ... endmodule Vec : sig ... endmodule Version : sig ... endmodule Xliteral : sig ... end