Remove debug_warnings

Author: Halbaroth

src/bin/js/options_interface.ml

@@ -113,7 +113,6 @@ let set_options r =
   set_options_opt Options.set_debug_uf r.debug_uf;
   set_options_opt Options.set_debug_unsat_core r.debug_unsat_core;
   set_options_opt Options.set_debug_use r.debug_use;
-  set_options_opt Options.set_debug_warnings r.debug_warnings;
   set_options_opt Options.set_rule r.rule;
 
   set_options_opt Options.set_case_split_policy

src/bin/js/worker_interface.ml

@@ -181,7 +181,6 @@ type options = {
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;
-  debug_warnings : bool option;
   rule : int option;
 
   case_split_policy : case_split_policy option;
@@ -281,7 +280,6 @@ let init_options () = {
   debug_uf = None;
   debug_unsat_core = None;
   debug_use = None;
-  debug_warnings = None;
   rule = None;
 
   case_split_policy = None;
@@ -395,12 +393,11 @@ let opt_dbg3_encoding =
   conv
     (fun dbg3 -> dbg3)
     (fun dbg3 -> dbg3)
-    (obj5
+    (obj4
        (opt "debug_types" bool)
        (opt "debug_uf" bool)
        (opt "debug_unsat_core" bool)
        (opt "debug_use" bool)
-       (opt "debug_warnings" bool)
     )
 
 let opt1_encoding =
@@ -551,8 +548,7 @@ let options_to_json opt =
     (opt.debug_types,
      opt.debug_uf,
      opt.debug_unsat_core,
-     opt.debug_use,
-     opt.debug_warnings)
+     opt.debug_use)
   in
   let all_opt1 =
     (opt.rule,
@@ -677,8 +673,7 @@ let options_from_json options =
     let (debug_types,
          debug_uf,
          debug_unsat_core,
-         debug_use,
-         debug_warnings) = dbg_opt3 in
+         debug_use) = dbg_opt3 in
     let (rule,
          case_split_policy,
          enable_adts_cs,
@@ -762,7 +757,6 @@ let options_from_json options =
       debug_uf;
       debug_unsat_core;
       debug_use;
-      debug_warnings;
       rule;
       case_split_policy;
       enable_adts_cs;

src/bin/js/worker_interface.mli

@@ -78,7 +78,6 @@ type options = {
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;
-  debug_warnings : bool option;
   rule : int option;
 
   case_split_policy : case_split_policy option;

src/lib/structures/expr.ml

@@ -1146,8 +1146,7 @@ let mk_forall_ter =
         let q = match form_view lem with Lemma q -> q | _ -> assert false in
         assert (equal q.main f (* should be true *));
         if compare_quant q new_q <> 0 then raise Exit;
-        Printer.print_wrn ~warning:(Options.get_debug_warnings ())
-          "(sub) axiom %s replaced with %s" name q.name;
+        Printer.print_wrn "(sub) axiom %s replaced with %s" name q.name;
         lem
       with Not_found | Exit ->
         let d = new_q.main.depth in (* + 1 ?? *)

src/lib/util/options.ml

@@ -175,7 +175,6 @@ let debug_types = ref false
 let debug_uf = ref false
 let debug_unsat_core = ref false
 let debug_use = ref false
-let debug_warnings = ref false
 let debug_commands = ref false
 let debug_optimize = ref false
 let rule = ref (-1)
@@ -204,7 +203,6 @@ let set_debug_types b = debug_types := b
 let set_debug_uf b = debug_uf := b
 let set_debug_unsat_core b = debug_unsat_core := b
 let set_debug_use b = debug_use := b
-let set_debug_warnings b = debug_warnings := b
 let set_debug_commands b = debug_commands := b
 let set_debug_optimize b = debug_optimize := b
 let set_rule b = rule := b
@@ -233,7 +231,6 @@ let get_debug_types () = !debug_types
 let get_debug_uf () = !debug_uf
 let get_debug_unsat_core () = !debug_unsat_core
 let get_debug_use () = !debug_use
-let get_debug_warnings () = !debug_warnings
 let get_debug_commands () = !debug_commands
 let get_debug_optimize () = !debug_optimize
 let get_rule () = !rule

src/lib/util/options.mli

@@ -173,9 +173,6 @@ val set_debug_unsat_core : bool -> unit
 (** Set [debug_use] accessible with {!val:get_debug_use} *)
 val set_debug_use : bool -> unit
 
-(** Set [debug_warnings] accessible with {!val:get_debug_warnings} *)
-val set_debug_warnings : bool -> unit
-
 (** Set [debug_commands] accessible with {!val:get_debug_commands} *)
 val set_debug_commands : bool -> unit
 
@@ -465,9 +462,6 @@ val set_used_context_file : string -> unit
 (** Get the debugging flag. *)
 val get_debug : unit -> bool
 
-(** Get the debugging flag of warnings. *)
-val get_debug_warnings : unit -> bool
-
 (** Get the debugging flag of commands. If enabled, Alt-Ergo will display all
     the commands that are sent to the solver. *)
 val get_debug_commands : unit -> bool

src/lib/util/printer.ml

@@ -227,12 +227,10 @@ let print_err ?(flushed=true) ?(header=(Options.get_output_with_headers ()))
   end
   else Format.ifprintf Format.err_formatter s
 
-let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ()))
-    ?(warning=true) s =
+let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ())) s =
   if Options.get_warning_as_error () then
-    print_err ~flushed ~header ~error:warning s
+    print_err ~flushed ~header ~error:true s
   else
-  if warning then begin
     let fmt = Options.Output.get_fmt_diagnostic () in
     Format.fprintf fmt "@[<v 0>%s" (pp_smt clean_wrn_print);
     if header then
@@ -242,8 +240,6 @@ let print_wrn ?(flushed=true) ?(header=(Options.get_output_with_headers ()))
         Format.fprintf fmt "@[<v 10>[Warning] " ;
     if flushed || Options.get_output_with_forced_flush ()
     then Format.kfprintf flush fmt s else Format.fprintf fmt s
-  end
-  else Format.ifprintf Format.err_formatter s
 
 let print_dbg ?(flushed=true) ?(header=(Options.get_output_with_headers ()))
     ?(module_name="") ?(function_name="") s =

src/lib/util/printer.mli

@@ -47,13 +47,11 @@ val print_err :
 
 (** Print warning message on the warning formatter accessible with
     {!val:Options.get_fmt_wrn} and set by default to stderr.
-    Prints only if warning (true by default) is true.
     If header is set, prints a header "[Warning]".
     The wrn formatter is flushed after the print if flushed is set *)
 val print_wrn :
   ?flushed:bool ->
   ?header:bool ->
-  ?warning:bool ->
   ('a, Format.formatter, unit) format -> 'a
 
 (** Print debug message on the debug formatter accessible with