review changes

src/bin/common/parse_command.ml

@@ -216,70 +216,71 @@ module Debug = struct
   let set_level src = Logs.Src.set_level src (Some Debug)
 
   let mk ~verbosity flags =
-    let module S = Sources in
+    let module S = Options.Sources in
     List.concat flags
     |> List.iter (function
         | Debug ->
           Options.set_debug true
         | Ac ->
           Options.set_debug_ac true;
-          set_level S.ac
+          set_level Ac.src
         | Adt ->
           Options.set_debug_adt true;
-          set_level S.adt;
-          set_level S.adt_rel
+          set_level Adt.src;
+          set_level Adt_rel.src
         | Arith ->
           Options.set_debug_arith true;
-          set_level S.arith;
-          set_level S.interval_calculus
+          set_level Arith.src;
+          set_level IntervalCalculus.src
         | Arrays ->
           Options.set_debug_arrays true;
-          set_level S.arrays_rel
+          set_level Arrays_rel.src
         | Bitv ->
           Options.set_debug_bitv true;
-          set_level S.bitv
+          set_level Bitv.src
         | Sum ->
           Printer.print_wrn
             "The debug flag 'sum' is deprecated and is replaced by 'adt'. \
              It has the same effect as 'adt' and will be removed in a future \
              version.";
           Options.set_debug_adt true;
-          set_level S.adt;
-          set_level S.adt_rel
+          set_level Adt.src;
+          set_level Adt_rel.src
         | Ite ->
           Options.set_debug_ite true;
-          set_level S.ite_rel
+          set_level Ite_rel.src
         | Cc ->
           Options.set_debug_cc true;
-          set_level S.cc
+          set_level Ccx.src
         | Combine ->
           Options.set_debug_combine true;
-          set_level S.combine
+          set_level Shostak.Combine.src
         | Constr ->
           Options.set_debug_constr true;
           set_level S.constr
         | Explanation ->
           Options.set_debug_explanation true;
-          set_level S.explanation
+          set_level Explanation.src
         | Fm ->
           Options.set_debug_fm true;
           set_level S.fm
         | Fpa ->
           Options.set_debug_fpa verbosity
         | Gc ->
           Options.set_debug_gc true;
-          set_level S.gc_debug
+          set_level Gc_debug.src
         | Interpretation ->
           Options.set_debug_interpretation true;
           set_level S.interpretation
         | Intervals ->
           Options.set_debug_intervals true;
-          set_level S.intervals
+          set_level Intervals.src
         | Matching ->
           Options.set_debug_matching verbosity
         | Sat ->
           Options.set_debug_sat true;
-          set_level S.sat
+          set_level Satml.src;
+          set_level Satml_frontend.src
         | Split ->
           Options.set_debug_split true;
           set_level S.split
@@ -295,13 +296,13 @@ module Debug = struct
              future version."
         | Uf ->
           Options.set_debug_uf true;
-          set_level S.uf
+          set_level Uf.src
         | Unsat_core ->
           Options.set_debug_unsat_core true;
           set_level S.unsat_core
         | Use ->
           Options.set_debug_use true;
-          set_level S.use
+          set_level Use.src
         | Warnings ->
           Printer.print_wrn
             "The debug flag 'warning' is deprecated and will be removed in a \
@@ -310,7 +311,7 @@ module Debug = struct
           set_level S.warnings
         | Commands ->
           Options.set_debug_commands true;
-          set_level S.commands
+          set_level Commands.src
         | Optimize ->
           Options.set_debug_optimize true;
           set_level S.optimize

src/lib/dune

@@ -62,7 +62,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_unix My_list Theories Nest Compat Sources
+    My_zip My_unix My_list Theories Nest Compat
   )
 
  (js_of_ocaml

src/lib/reasoners/ac.ml

@@ -28,6 +28,8 @@
 module HS = Hstring
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 module type S = sig
 
   (* embeded AC semantic values *)

src/lib/reasoners/ac.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   (* the type of amalgamated AC semantic values *)

src/lib/reasoners/adt.ml

@@ -28,6 +28,8 @@
 module Sy = Symbols
 module E  = Expr
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;
@@ -79,7 +81,6 @@ module Shostak (X : ALIEN) = struct
   module SX = Set.Make(struct type t = r let compare = X.hash_cmp end)
 
   let name = "Adt"
-
   let timer = Timers.M_Adt
 
   [@@ocaml.ppwarning "XXX: IsConstr not interpreted currently. Maybe \

src/lib/reasoners/adt.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;

src/lib/reasoners/adt_rel.ml

@@ -40,6 +40,8 @@ module DE = Dolmen.Std.Expr
 module DT = Dolmen.Std.Expr.Ty
 module B = Dolmen.Std.Builtin
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 module TSet =
   Set.Make
     (struct

src/lib/reasoners/arith.ml

@@ -32,6 +32,8 @@ module ZA = Z
 module Z = Numbers.Z
 module Q = Numbers.Q
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
 let mod_symb = Sy.name ~ns:Internal "@mod"
 
@@ -83,7 +85,6 @@ module Shostak
   type r = P.r
 
   let name = "arith"
-
   let timer = Timers.M_Arith
 
   (*BISECT-IGNORE-BEGIN*)

src/lib/reasoners/arith.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 (** [calc_power x y t] Compute x^y. Raise Exit if y is not an Int
     (castable in Int). *)
 val calc_power : Numbers.Q.t -> Numbers.Q.t -> Ty.t -> Numbers.Q.t

src/lib/reasoners/arrays_rel.ml

@@ -35,6 +35,8 @@ module Ex = Explanation
 
 module LR = Uf.LX
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 (* map get |-> { set } des associations (get,set) deja splites *)
 module Tmap = struct
   include E.Map

src/lib/reasoners/bitv.ml

@@ -28,6 +28,8 @@
 module Sy = Symbols
 module E = Expr
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 type sort_var = A | B | C
 (* The variables used by the bitvector solver can be split into three
    categories that have associated invariants.
@@ -364,7 +366,6 @@ module Shostak(X : ALIEN) = struct
   type r = X.r
 
   let name = "bitv"
-
   let timer = Timers.M_Bitv
 
   let is_mine_symb sy =

src/lib/reasoners/bitv.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a alpha_term = {
   bv : 'a;
   sz : int;

src/lib/reasoners/bitv_rel.ml

@@ -25,6 +25,8 @@ module MX = Shostak.MXH
 module HX = Shostak.HX
 module L = Xliteral
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 let timer = Timers.M_Bitv
 
 let is_bv_ty = function

src/lib/reasoners/ccx.ml

@@ -33,6 +33,8 @@ module SE = Expr.Set
 
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 module type S = sig
 
   type t

src/lib/reasoners/ccx.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   type t

src/lib/reasoners/fun_sat.ml

@@ -30,6 +30,8 @@ module SE = E.Set
 module ME = E.Map
 module Ex = Explanation
 
+let src = Logs.Src.create ~doc:"Sat" "AltErgoLib.Fun_sat"
+
 module Make (Th : Theory.S) = struct
   module Inst = Instances.Make(Th)
   module CDCL = Satml_frontend_hybrid.Make(Th)

src/lib/reasoners/fun_sat.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 (** A functional SAT solver implementation. *)
 module Make (_ : Theory.S) : sig
   type t

src/lib/reasoners/fun_sat_frontend.ml

@@ -16,6 +16,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let src = Logs.Src.create ~doc:"Sat" "AltErgoLib.Fun_sat_frontend"
+
 module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   exception Sat
   exception Unsat of Explanation.t

src/lib/reasoners/intervalCalculus.ml

@@ -50,6 +50,8 @@ module SX = Shostak.SXH
 module MX0 = Shostak.MXH
 module MPL = Expr.Map
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 let oracle =
   lazy (
     let module OracleContainer = (val Inequalities.get_current ()) in

src/lib/reasoners/intervals.ml

@@ -27,6 +27,8 @@
 
 open Intervals_intf
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 (* Let us pretend we are using [Logs]. *)
 module Log = struct
   type ('a, 'b) msgf =

src/lib/reasoners/intervals.mli

@@ -27,6 +27,8 @@
 
 open Intervals_intf
 
+val src : Logs.src
+
 val map_bound : ('a -> 'b) -> 'a bound -> 'b bound
 (** [map_bound f b] applies [f] to a finite (open or closed) bound [b] and
     does not change an unbounded bound. *)

src/lib/reasoners/ite_rel.ml

@@ -51,6 +51,8 @@ module TB =
         if c <> 0 then c else Bool.compare b1 b2
     end)
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 let timer = Timers.M_Ite
 
 (* The present theory simplifies the ite terms t of the form

src/lib/reasoners/matching.ml

@@ -29,6 +29,8 @@ module E = Expr
 module ME = E.Map
 module SubstE = Var.Map
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 module type S = sig
   type t
   type theory

src/lib/reasoners/matching.mli

@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
   type t
   type theory

src/lib/reasoners/records_rel.ml

@@ -27,6 +27,8 @@
 
 type t = unit
 
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 let timer = Timers.M_Records
 
 let empty uf = (), Uf.domains uf

src/lib/reasoners/relation.ml

@@ -41,6 +41,9 @@ module Rel5 : Sig_rel.RELATION = Adt_rel
 
 module Rel6 : Sig_rel.RELATION = Ite_rel
 
+(* This source is unused. *)
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 (* This value is unused. *)
 let timer = Timers.M_None
 

src/lib/reasoners/sat_solver_sig.ml

@@ -157,5 +157,7 @@ end
 
 
 module type SatContainer = sig
+  val src : Logs.src
+
   module Make (_ : Theory.S) : S
 end

src/lib/reasoners/sat_solver_sig.mli

@@ -137,5 +137,7 @@ end
 
 
 module type SatContainer = sig
+  val src : Logs.src
+
   module Make (_ : Theory.S) : S
 end

src/lib/reasoners/satml.ml

@@ -67,6 +67,8 @@ module FF = Satml_types.Flat_Formula
 
 module Ex = Explanation
 
+let src = Logs.Src.create ~doc:"Sat" "AltErgoLib.Satml"
+
 exception Sat
 exception Unsat of Atom.clause list option
 exception Last_UIP_reason of Atom.Set.t

src/lib/reasoners/satml.mli

@@ -36,6 +36,8 @@ type conflict_origin =
   | C_bool of Atom.clause
   | C_theory of Explanation.t
 
+val src : Logs.src
+
 module type SAT_ML = sig
 
   (*module Make (Dummy : sig end) : sig*)