Minimal Logs integration (#1206)

* Add minimal Logs integration This PR adds: - `Logs` as a new dependency; - Logs' sources for each debug flag; - A reporter that prints on the appropriate output (regular or diagnostic) according to the source.
OCamlPro · Aug 22, 2024 · dfcc900 · dfcc900
1 parent 1445b14
commit dfcc900
Show file tree

Hide file tree

Showing 52 changed files with 262 additions and 49 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -99,6 +99,7 @@
  - Uniformization of internal identifiers generation (#905, #918)
  - Use an efficient `String.starts_with` implementation (#912)
  - Fix the Makefile (#914)
+ - Add `Logs` dependency (#1206)
 
 ### Testing
 

diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
@@ -154,7 +154,7 @@ module Debug = struct
     | Cc
     | Combine
     | Constr
-    | Explanation
+    | Explanations
     | Fm
     | Fpa
     | Gc
@@ -176,7 +176,7 @@ module Debug = struct
 
   let all = [
     Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
-    Cc; Combine; Constr; Explanation; Fm; Fpa; Gc;
+    Cc; Combine; Constr; Explanations; Fm; Fpa; Gc;
     Interpretation; Intervals; Matching; Sat; Split; Triggers;
     Types; Typing; Uf; Unsat_core; Use; Warnings;
     Commands; Optimize
@@ -194,7 +194,7 @@ module Debug = struct
     | Cc -> "cc"
     | Combine -> "combine"
     | Constr -> "constr"
-    | Explanation -> "explanation"
+    | Explanations -> "explanations"
     | Fm -> "fm"
     | Fpa -> "fpa"
     | Gc -> "gc"
@@ -213,50 +213,107 @@ module Debug = struct
     | Commands -> "commands"
     | Optimize -> "optimize"
 
+  let set_level src = Logs.Src.set_level src (Some Debug)
+
   let mk ~verbosity flags =
+    let module S = Options.Sources in
     List.concat flags
     |> List.iter (function
-        | Debug -> Options.set_debug true
-        | Ac -> Options.set_debug_ac true
-        | Adt -> Options.set_debug_adt true
-        | Arith -> Options.set_debug_arith true
-        | Arrays -> Options.set_debug_arrays true
-        | Bitv -> Options.set_debug_bitv true
+        | Debug ->
+          Options.set_debug true
+        | Ac ->
+          Options.set_debug_ac true;
+          set_level Ac.src
+        | Adt ->
+          Options.set_debug_adt true;
+          set_level Adt.src;
+          set_level Adt_rel.src
+        | Arith ->
+          Options.set_debug_arith true;
+          set_level Arith.src;
+          set_level IntervalCalculus.src
+        | Arrays ->
+          Options.set_debug_arrays true;
+          set_level Arrays_rel.src
+        | Bitv ->
+          Options.set_debug_bitv true;
+          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
-        | Ite -> Options.set_debug_ite true
-        | Cc -> Options.set_debug_cc true
-        | Combine -> Options.set_debug_combine true
-        | Constr -> Options.set_debug_constr true
-        | Explanation -> Options.set_debug_explanations true
-        | Fm -> Options.set_debug_fm true
-        | Fpa -> Options.set_debug_fpa verbosity
-        | Gc -> Options.set_debug_gc true
-        | Interpretation -> Options.set_debug_interpretation true
-        | Intervals -> Options.set_debug_intervals true
-        | Matching -> Options.set_debug_matching verbosity
-        | Sat -> Options.set_debug_sat true
-        | Split -> Options.set_debug_split true
-        | Triggers -> Options.set_debug_triggers true
-        | Types -> Options.set_debug_types true
+          Options.set_debug_adt true;
+          set_level Adt.src;
+          set_level Adt_rel.src
+        | Ite ->
+          Options.set_debug_ite true;
+          set_level Ite_rel.src
+        | Cc ->
+          Options.set_debug_cc true;
+          set_level Ccx.src
+        | Combine ->
+          Options.set_debug_combine true;
+          set_level Shostak.Combine.src
+        | Constr ->
+          Options.set_debug_constr true;
+          set_level S.constr
+        | 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 Gc_debug.src
+        | Interpretation ->
+          Options.set_debug_interpretation true;
+          set_level S.interpretation
+        | Intervals ->
+          Options.set_debug_intervals true;
+          set_level Intervals.src
+        | Matching ->
+          Options.set_debug_matching verbosity;
+          set_level Matching.src
+        | Sat ->
+          Options.set_debug_sat true;
+          set_level Satml.src;
+          set_level Satml_frontend.src
+        | Split ->
+          Options.set_debug_split true;
+          set_level S.split
+        | Triggers ->
+          Options.set_debug_triggers true;
+          set_level S.triggers
+        | Types ->
+          Options.set_debug_types true;
+          set_level S.types
         | Typing ->
           Printer.print_wrn
             "The debug flag 'typing' has no effect. It will be removed in a \
              future version."
-        | Uf -> Options.set_debug_uf true
-        | Unsat_core -> Options.set_debug_unsat_core true
-        | Use -> Options.set_debug_use true
+        | Uf ->
+          Options.set_debug_uf true;
+          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 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
-        | Commands -> Options.set_debug_commands true
-        | Optimize -> Options.set_debug_optimize true
+        | Commands ->
+          Options.set_debug_commands true;
+          set_level Commands.src
+        | Optimize ->
+          Options.set_debug_optimize true;
+          set_level S.optimize
       )
 
   let light_flag_term, medium_flag_term, full_flag_term =

diff --git a/src/bin/text/main_text.ml b/src/bin/text/main_text.ml
@@ -43,4 +43,5 @@ let () =
   AltErgoLib.Printer.init_colors ();
   AltErgoLib.Printer.init_output_format ();
   Signals_profiling.init_signals ();
+  Logs.set_reporter (AltErgoLib.Printer.reporter);
   Solving_loop.main ()
diff --git a/src/lib/dune b/src/lib/dune
@@ -24,6 +24,8 @@
     dune-build-info
     alt_ergo_prelude
     fmt
+    logs
+    logs.fmt
   )
   (preprocess
     (pps

diff --git a/src/lib/reasoners/ac.ml b/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 *)

diff --git a/src/lib/reasoners/ac.mli b/src/lib/reasoners/ac.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   (* the type of amalgamated AC semantic values *)

diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
@@ -28,6 +28,8 @@
 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 {

diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;

diff --git a/src/lib/reasoners/adt_rel.ml b/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

diff --git a/src/lib/reasoners/adt_rel.mli b/src/lib/reasoners/adt_rel.mli
@@ -26,3 +26,4 @@
 (**************************************************************************)
 
 include Sig_rel.RELATION
+val src : Logs.src
diff --git a/src/lib/reasoners/arith.ml b/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"
 

diff --git a/src/lib/reasoners/arith.mli b/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

diff --git a/src/lib/reasoners/arrays_rel.ml b/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

diff --git a/src/lib/reasoners/arrays_rel.mli b/src/lib/reasoners/arrays_rel.mli
@@ -26,3 +26,4 @@
 (**************************************************************************)
 
 include Sig_rel.RELATION
+val src : Logs.src
diff --git a/src/lib/reasoners/bitv.ml b/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.

diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a alpha_term = {
   bv : 'a;
   sz : int;

diff --git a/src/lib/reasoners/bitv_rel.ml b/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

diff --git a/src/lib/reasoners/bitv_rel.mli b/src/lib/reasoners/bitv_rel.mli
@@ -17,6 +17,7 @@
 (**************************************************************************)
 
 include Sig_rel.RELATION
+val src : Logs.src
 
 (**/**)
 

diff --git a/src/lib/reasoners/ccx.ml b/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

diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   type t

diff --git a/src/lib/reasoners/fun_sat.ml b/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)

diff --git a/src/lib/reasoners/fun_sat.mli b/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

diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
@@ -16,6 +16,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   exception Sat
   exception Unsat of Explanation.t

diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
@@ -50,6 +50,9 @@ module SX = Shostak.SXH
 module MX0 = Shostak.MXH
 module MPL = Expr.Map
 
+let src = Logs.Src.create ~doc:"IntervalCalculus" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let oracle =
   lazy (
     let module OracleContainer = (val Inequalities.get_current ()) in

diff --git a/src/lib/reasoners/intervalCalculus.mli b/src/lib/reasoners/intervalCalculus.mli
@@ -26,6 +26,7 @@
 (**************************************************************************)
 
 include Sig_rel.RELATION
+val src : Logs.src
 
 val reinit_cache : unit -> unit
 (** Reinitializes the E-matching functor instance's inner cache