From dfcc9008eaa46f517a3174fbb1402c015333e0bb Mon Sep 17 00:00:00 2001 From: Pierrot Date: Thu, 22 Aug 2024 14:05:32 +0200 Subject: [PATCH] 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. --- CHANGES.md | 1 + src/bin/common/parse_command.ml | 117 ++++++++++++++++++------- src/bin/text/main_text.ml | 1 + src/lib/dune | 2 + src/lib/reasoners/ac.ml | 3 + src/lib/reasoners/ac.mli | 2 + src/lib/reasoners/adt.ml | 2 + src/lib/reasoners/adt.mli | 2 + src/lib/reasoners/adt_rel.ml | 3 + src/lib/reasoners/adt_rel.mli | 1 + src/lib/reasoners/arith.ml | 3 + src/lib/reasoners/arith.mli | 2 + src/lib/reasoners/arrays_rel.ml | 3 + src/lib/reasoners/arrays_rel.mli | 1 + src/lib/reasoners/bitv.ml | 3 + src/lib/reasoners/bitv.mli | 2 + src/lib/reasoners/bitv_rel.ml | 3 + src/lib/reasoners/bitv_rel.mli | 1 + src/lib/reasoners/ccx.ml | 3 + src/lib/reasoners/ccx.mli | 2 + src/lib/reasoners/fun_sat.ml | 3 + src/lib/reasoners/fun_sat.mli | 2 + src/lib/reasoners/fun_sat_frontend.ml | 3 + src/lib/reasoners/intervalCalculus.ml | 3 + src/lib/reasoners/intervalCalculus.mli | 1 + src/lib/reasoners/intervals.ml | 21 +---- src/lib/reasoners/intervals.mli | 2 + src/lib/reasoners/ite_rel.ml | 3 + src/lib/reasoners/ite_rel.mli | 1 + src/lib/reasoners/matching.ml | 3 + src/lib/reasoners/matching.mli | 2 + src/lib/reasoners/records_rel.ml | 3 + src/lib/reasoners/records_rel.mli | 1 + src/lib/reasoners/sat_solver_sig.ml | 2 + src/lib/reasoners/sat_solver_sig.mli | 2 + src/lib/reasoners/satml.ml | 3 + src/lib/reasoners/satml.mli | 2 + src/lib/reasoners/satml_frontend.ml | 3 + src/lib/reasoners/shostak.ml | 3 + src/lib/reasoners/shostak.mli | 2 + src/lib/reasoners/uf.ml | 3 + src/lib/reasoners/uf.mli | 2 + src/lib/reasoners/use.ml | 3 + src/lib/reasoners/use.mli | 1 + src/lib/structures/commands.ml | 3 + src/lib/structures/commands.mli | 2 + src/lib/util/gc_debug.ml | 3 + src/lib/util/gc_debug.mli | 2 + src/lib/util/options.ml | 15 ++++ src/lib/util/options.mli | 14 +++ src/lib/util/printer.ml | 32 +++++++ src/lib/util/printer.mli | 9 ++ 52 files changed, 262 insertions(+), 49 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index dc26af6c7..33e612d17 100644 --- 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 index 9702d7162..5d83f65b1 100644 --- 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 index ee4860fad..c00e609d2 100644 --- 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 index 12b197a39..2d7f7575e 100644 --- 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 index 95645ba25..bedf31684 100644 --- 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 index 992118898..b2cb57c94 100644 --- 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 index 3c1dafd98..9c443c0f7 100644 --- 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 index fea79eb1e..2cd25de23 100644 --- 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 index 9e52bb78f..87b8655d1 100644 --- 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 index f68d130ca..cac59a5a1 100644 --- 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 index c95bdb1a5..afc1b7ae9 100644 --- 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 index ce95a86b2..63489d53e 100644 --- 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 index 2551f2947..4d3f9f5fb 100644 --- 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 index f68d130ca..cac59a5a1 100644 --- 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 index a61f10623..66431a44b 100644 --- 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 index 3b5064cb1..77b68f080 100644 --- 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 index 9537eb49c..f7f72d70a 100644 --- 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 index ffd2a6ce0..3671a034f 100644 --- 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 index 5642c89d4..5d9f56787 100644 --- 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 index c121d46c3..83c09ed50 100644 --- 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 index d382b2f3b..347ef6cc4 100644 --- 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 index 73376ebab..6e018f04e 100644 --- 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 index abeb97259..af11bfcc8 100644 --- 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 index aeb8ca415..a11045bf6 100644 --- 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 index e1c92cf9f..a649208a2 100644 --- 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 diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index 6e1296b38..61e2a96a1 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -27,25 +27,8 @@ open Intervals_intf -(* Let us pretend we are using [Logs]. *) -module Log = struct - type ('a, 'b) msgf = - (?header:string -> - ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a) - -> 'b - - type 'a log = ('a, unit) msgf -> unit - - let module_name = "AltErgoLib.Intervals" - - let debug : 'a log = - fun k -> - if Options.get_debug_intervals () then - k (fun ?header:function_name fmt -> - let header = Option.is_some function_name in - Printer.print_dbg ~header ~module_name ?function_name fmt - ) -end +let src = Logs.Src.create ~doc:"Intervals" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) let map_bound f = function | Unbounded -> Unbounded diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli index 04b7b569e..ebdd8cc8e 100644 --- a/src/lib/reasoners/intervals.mli +++ b/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. *) diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml index 2d7c90759..ccbf93145 100644 --- a/src/lib/reasoners/ite_rel.ml +++ b/src/lib/reasoners/ite_rel.ml @@ -51,6 +51,9 @@ module TB = if c <> 0 then c else Bool.compare b1 b2 end) +let src = Logs.Src.create ~doc:"Ite_rel" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + let timer = Timers.M_Ite (* The present theory simplifies the ite terms t of the form diff --git a/src/lib/reasoners/ite_rel.mli b/src/lib/reasoners/ite_rel.mli index f68d130ca..cac59a5a1 100644 --- a/src/lib/reasoners/ite_rel.mli +++ b/src/lib/reasoners/ite_rel.mli @@ -26,3 +26,4 @@ (**************************************************************************) include Sig_rel.RELATION +val src : Logs.src diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index e7faf625e..8e9dedd3d 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -29,6 +29,9 @@ module E = Expr module ME = E.Map module SubstE = Var.Map +let src = Logs.Src.create ~doc:"Matching" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + module type S = sig type t type theory diff --git a/src/lib/reasoners/matching.mli b/src/lib/reasoners/matching.mli index ac57eac60..249c92307 100644 --- a/src/lib/reasoners/matching.mli +++ b/src/lib/reasoners/matching.mli @@ -25,6 +25,8 @@ (* *) (**************************************************************************) +val src : Logs.src + module type S = sig type t type theory diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml index 0463fac01..84f2a54ea 100644 --- a/src/lib/reasoners/records_rel.ml +++ b/src/lib/reasoners/records_rel.ml @@ -27,6 +27,9 @@ type t = unit +let src = Logs.Src.create ~doc:"Records" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + let timer = Timers.M_Records let empty uf = (), Uf.domains uf diff --git a/src/lib/reasoners/records_rel.mli b/src/lib/reasoners/records_rel.mli index f68d130ca..cac59a5a1 100644 --- a/src/lib/reasoners/records_rel.mli +++ b/src/lib/reasoners/records_rel.mli @@ -26,3 +26,4 @@ (**************************************************************************) include Sig_rel.RELATION +val src : Logs.src diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 6d4a547f5..c8450e6d3 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/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 diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index bb79c01d4..9380bbbbc 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/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 diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 6345abe07..59248fffa 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -67,6 +67,9 @@ module FF = Satml_types.Flat_Formula module Ex = Explanation +let src = Logs.Src.create ~doc:"Sat" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + exception Sat exception Unsat of Atom.clause list option exception Last_UIP_reason of Atom.Set.t diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 8772104d0..166b2ff5a 100644 --- a/src/lib/reasoners/satml.mli +++ b/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*) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 2952a1ea1..2200a8e0a 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -27,6 +27,9 @@ module X = Shostak.Combine +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 module SAT = Satml.Make(Th) module Inst = Instances.Make(Th) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 8b308859b..919783407 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -680,6 +680,9 @@ and AC : Ac.S module Combine = struct include CX + let src = Logs.Src.create ~doc:"Combine" "AltErgoLib__Combine" + module Log = (val Logs.src_log src : Logs.LOG) + module H = Ephemeron.K1.Make(Expr) let make, save_cache, reinit_cache = diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 42d9d7bfa..0fdc94591 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -28,6 +28,8 @@ module Combine : sig include Sig.X + val src : Logs.src + val top : r val bot : r end diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 46f330070..eefe70e82 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -37,6 +37,9 @@ module SE = Expr.Set module LX = Shostak.L module MapL = Emap.Make(LX) +let src = Logs.Src.create ~doc:"Uf" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + module MapX = struct include Shostak.MXH let find m x = Steps.incr (Steps.Uf); find m x diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index f231441e6..f73f3f794 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -34,6 +34,8 @@ type r = Shostak.Combine.r type _ id = .. (** Extensible type for global domains identifiers, see {!GlobalDomains}. *) +val src : Logs.src + module type GlobalDomain = sig (** Module signature for global domains used by the union-find module. diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml index b02fef1fe..1d6670acd 100644 --- a/src/lib/reasoners/use.ml +++ b/src/lib/reasoners/use.ml @@ -39,6 +39,9 @@ module X = Shostak.Combine module MX = Shostak.MXH +let src = Logs.Src.create ~doc:"Use" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + type t = (SE.t * SA.t) MX.t type r = X.r diff --git a/src/lib/reasoners/use.mli b/src/lib/reasoners/use.mli index 76a9329c6..98e059dee 100644 --- a/src/lib/reasoners/use.mli +++ b/src/lib/reasoners/use.mli @@ -30,6 +30,7 @@ module SA : Set.S with type elt = Expr.t * Explanation.t type t type r = Shostak.Combine.r +val src : Logs.src val empty : t val find : r -> t -> Expr.Set.t * SA.t val add : r -> Expr.Set.t * SA.t -> t -> t diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index f06b4a5dd..47856b2a4 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -27,6 +27,9 @@ (* Sat entry *) +let src = Logs.Src.create ~doc:"Commands" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + type sat_decl_aux = | Decl of Id.typed | Assume of string * Expr.t * bool diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index bc1cafb49..152f1ca0b 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -43,4 +43,6 @@ type sat_tdecl = { st_decl : sat_decl_aux } +val src : Logs.src + val print : Format.formatter -> sat_tdecl -> unit diff --git a/src/lib/util/gc_debug.ml b/src/lib/util/gc_debug.ml index b63e79108..7f36b0201 100644 --- a/src/lib/util/gc_debug.ml +++ b/src/lib/util/gc_debug.ml @@ -37,6 +37,9 @@ major_words; (* num of alloc words in major heap, since beginning *) *) +let src = Logs.Src.create ~doc:"Gc_debug" __MODULE__ +module Log = (val Logs.src_log src : Logs.LOG) + let init () = if Options.get_debug_gc() then begin diff --git a/src/lib/util/gc_debug.mli b/src/lib/util/gc_debug.mli index 5fa64511e..c127ae5b3 100644 --- a/src/lib/util/gc_debug.mli +++ b/src/lib/util/gc_debug.mli @@ -25,6 +25,8 @@ (* *) (**************************************************************************) +val src : Logs.src + (** Prints some debug info about the GC's activity. *) val init : unit -> unit diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 00b32305c..05a24f270 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -91,6 +91,21 @@ module Output = struct let get_fmt_models () = to_formatter !dump_models_output end +module Sources = struct + let constr = Logs.Src.create ~doc:"Constr" "AltErgoLib.constr" + let fm = Logs.Src.create ~doc:"fm" "AltErgoLib.fm" + let fpa = Logs.Src.create ~doc:"fpa" "AltErgoLib.fpa" + let interpretation = + Logs.Src.create ~doc:"Interpretation" "AltErgoLib.Interpretation" + let model = Logs.Src.create ~doc:"Model" "AltErgoLib.Model" + let optimize = Logs.Src.create ~doc:"Optimize" "AltErgoLib.Optimize" + let split = Logs.Src.create ~doc:"Split" "AltErgoLib.Split" + let triggers = Logs.Src.create ~doc:"Triggers" "AltErgoLib.Triggers" + let types = Logs.Src.create ~doc:"Types" "AltErgoLib.Types" + let typing = Logs.Src.create ~doc:"Typing" "AltErgoLib.Typing" + let unsat_core = Logs.Src.create ~doc:"Unsat_core" "AltErgoLib.Unsat_core" +end + (* Declaration of all the options as refs with default values *) type instantiation_heuristic = INormal | IAuto | IGreedy diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 323febc69..37006c235 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -1163,6 +1163,20 @@ module Output : sig Default to [Format.err_formatter]. *) end +module Sources : sig + val constr : Logs.src + val fm : Logs.src + val fpa : Logs.src + val interpretation : Logs.src + val model : Logs.src + val optimize : Logs.src + val split : Logs.src + val triggers : Logs.src + val types : Logs.src + val typing : Logs.src + val unsat_core : Logs.src +end + (** Print message as comment in the corresponding output format *) val pp_comment: Format.formatter -> string -> unit diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index fba40ff4d..5a76274e0 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -396,3 +396,35 @@ let print_smtlib_err ?(flushed=true) s = in Format.fprintf fmt "(error \""; Format.kfprintf k fmt s + +let pp_source ppf src = + let name = Logs.Src.doc src in + Fmt.pf ppf "%s" name + +let pp_smtlib_header ppf level = + match (level : Logs.level) with + | App | Info -> () + | Debug | Warning | Error -> Fmt.pf ppf "; " + +let reporter = + let report src level ~over k msgf = + let k _ = over (); k () in + let with_header h _tags k fmt = + if Logs.Src.equal src Logs.default then + Fmt.kpf k (Options.Output.get_fmt_regular ()) + ("%a@[" ^^ fmt ^^ "@]@.") + pp_smtlib_header level + else if Logs.Src.equal src Options.Sources.model then + Fmt.kpf k (Options.Output.get_fmt_models ()) + ("@[" ^^ fmt ^^ "@]@.") + else + let ppf = Options.Output.get_fmt_diagnostic () in + if Options.get_output_with_colors () then + Fmt.set_style_renderer ppf `Ansi_tty; + Fmt.kpf k ppf ("%a[%a] @[" ^^ fmt ^^ "@]@.") + Logs_fmt.pp_header (level, h) + pp_source src + in + msgf @@ fun ?header ?tags fmt -> with_header header tags k fmt + in + { Logs.report } diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index 91855f137..55245c69c 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -178,3 +178,12 @@ val print_status_preprocess : val print_smtlib_err : ?flushed:bool -> ('a, Format.formatter, unit) format -> 'a + +val reporter : Logs.reporter +(** Recommended reporter used by both the library and the binary. + + All the sources are printed on [Options.Output.get_fmt_diagnostic ()] but: + - [Sources.model] is printed on [Options.Output.get_fmt_models ()] + - [Sources.default] is printed on [Options.Output.get_fmt_regular ()] + + The library never prints on [Sources.default] or [Sources.model]. *)