review changes

rsc/extra/worker_json_example.json

@@ -10,7 +10,7 @@
     "debug": false, "debug_ac": false, "debug_adt": false,
     "debug_arith": false, "debug_arrays": false, "debug_bitv": false,
     "debug_cc": false, "debug_combine": false, "debug_constr": false,
-    "debug_explanation": false, "debug_fm": false, "debug_fpa": 0,
+    "debug_explanations": false, "debug_fm": false, "debug_fpa": 0,
     "debug_gc": false, "debug_interpretation": false, "debug_ite": false,
     "debug_matching": 0, "debug_sat": false, "debug_split": false,
     "debug_triggers": false, "debug_types": false,

src/bin/common/parse_command.ml

@@ -154,7 +154,8 @@ module Debug = struct
     | Cc
     | Combine
     | Constr
-    | Explanation
+    | Explanation (* deprecated *)
+    | Explanations
     | Fm
     | Fpa
     | Gc
@@ -176,7 +177,7 @@ module Debug = struct
 
   let all = [
     Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
-    Cc; Combine; Constr; Explanation; Fm; Fpa; Gc;
+    Cc; Combine; Constr; Explanation; Explanations; Fm; Fpa; Gc;
     Interpretation; Intervals; Matching; Sat; Split; Triggers;
     Types; Typing; Uf; Unsat_core; Use; Warnings;
     Commands; Optimize
@@ -195,6 +196,7 @@ module Debug = struct
     | Combine -> "combine"
     | Constr -> "constr"
     | Explanation -> "explanation"
+    | Explanations -> "explanations"
     | Fm -> "fm"
     | Fpa -> "fpa"
     | Gc -> "gc"
@@ -216,70 +218,77 @@ 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
+          Printer.print_wrn
+            "The debug flag 'explanation' is deprecated and is replaced \
+             by 'explanations'. It has the same effect as 'explanations' \
+             and will be removed in a future version.";
+          Options.set_debug_explanations true
+        | Explanations ->
+          Options.set_debug_explanations true
         | 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
+          Options.set_debug_matching verbosity;
+          set_level Matching.src
         | 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,22 +304,21 @@ 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 \
              future version.";
-          Options.set_debug_warnings true;
-          set_level S.warnings
+          Options.set_debug_warnings true
         | 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/bin/js/options_interface.ml

@@ -106,7 +106,7 @@ let set_options r =
   set_options_opt Options.set_debug_cc r.debug_cc;
   set_options_opt Options.set_debug_combine r.debug_combine;
   set_options_opt Options.set_debug_constr r.debug_constr;
-  set_options_opt Options.set_debug_explanation r.debug_explanation;
+  set_options_opt Options.set_debug_explanations r.debug_explanations;
   set_options_opt Options.set_debug_fm r.debug_fm;
   set_options_opt Options.set_debug_fpa r.debug_fpa;
   set_options_opt Options.set_debug_gc r.debug_gc;

src/bin/js/worker_interface.ml

@@ -185,7 +185,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanation : bool option;
+  debug_explanations : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;
@@ -286,7 +286,7 @@ let init_options () = {
   debug_cc = None;
   debug_combine = None;
   debug_constr = None;
-  debug_explanation = None;
+  debug_explanations = None;
   debug_fm = None;
   debug_fpa = None;
   debug_gc = None;
@@ -392,7 +392,7 @@ let opt_dbg1_encoding =
        (opt "debug_cc" bool)
        (opt "debug_combine" bool)
        (opt "debug_constr" bool)
-       (opt "debug_explanation" bool)
+       (opt "debug_explanations" bool)
     )
 
 let opt_dbg2_encoding =
@@ -555,7 +555,7 @@ let options_to_json opt =
      opt.debug_cc,
      opt.debug_combine,
      opt.debug_constr,
-     opt.debug_explanation)
+     opt.debug_explanations)
   in
   let dbg_opt2 =
     (opt.debug_fm,
@@ -685,7 +685,7 @@ let options_from_json options =
          debug_cc,
          debug_combine,
          debug_constr,
-         debug_explanation) =
+         debug_explanations) =
       dbg_opt1 in
     let (debug_fm,
          debug_fpa,
@@ -771,7 +771,7 @@ let options_from_json options =
       debug_cc;
       debug_combine;
       debug_constr;
-      debug_explanation;
+      debug_explanations;
       debug_fm;
       debug_fpa;
       debug_gc;

src/bin/js/worker_interface.mli

@@ -68,7 +68,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanation : bool option;
+  debug_explanations : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;

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,9 @@
 module HS = Hstring
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:"Ac" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 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,9 @@
 module Sy = Symbols
 module E  = Expr
 
+let src = Logs.Src.create ~doc:"Adt" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;
@@ -79,7 +82,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,9 @@ module DE = Dolmen.Std.Expr
 module DT = Dolmen.Std.Expr.Ty
 module B = Dolmen.Std.Builtin
 
+let src = Logs.Src.create ~doc:"Adt_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module TSet =
   Set.Make
     (struct

src/lib/reasoners/arith.ml

@@ -32,6 +32,9 @@ module ZA = Z
 module Z = Numbers.Z
 module Q = Numbers.Q
 
+let src = Logs.Src.create ~doc:"Arith" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
 let mod_symb = Sy.name ~ns:Internal "@mod"
 
@@ -83,7 +86,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,9 @@ module Ex = Explanation
 
 module LR = Uf.LX
 
+let src = Logs.Src.create ~doc:"Arrays_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 (* map get |-> { set } des associations (get,set) deja splites *)
 module Tmap = struct
   include E.Map

src/lib/reasoners/bitv.ml

@@ -28,6 +28,9 @@
 module Sy = Symbols
 module E = Expr
 
+let src = Logs.Src.create ~doc:"Bitv" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 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 +367,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,9 @@ module MX = Shostak.MXH
 module HX = Shostak.HX
 module L = Xliteral
 
+let src = Logs.Src.create ~doc:"Bitv_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let timer = Timers.M_Bitv
 
 let is_bv_ty = function

src/lib/reasoners/ccx.ml

@@ -33,6 +33,9 @@ module SE = Expr.Set
 
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:"Ccx" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 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,9 @@ module SE = E.Set
 module ME = E.Map
 module Ex = Explanation
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module Make (Th : Theory.S) = struct
   module Inst = Instances.Make(Th)
   module CDCL = Satml_frontend_hybrid.Make(Th)