[SAVer] Removed printer and simplified driver.

config/drivers/saver.drv

 (* Why3 drivers for SAVER *)
 
-printer "saver"
-filename "%f-%t-%g.why"
-
-valid "Result = [Tt]rue"
-invalid "Result = [Ff]alse"
-timeout "Result = [Tt]imeout"
-unknown "Result = [Uu]nknown" ""
-
-transformation "inline_trivial"
-transformation "introduce_premises"
-transformation "eliminate_builtin"
-transformation "simplify_formula"
-
 theory BuiltIn
   syntax type int   "int"
   syntax type real  "real"
@@ -163,23 +150,6 @@ theory real.RealInfix
 
 end
 
-theory Bool
-  syntax type     bool  "bool"
-  syntax function True  "true"
-  syntax function False "false"
-end
-
-theory Tuple0
-  syntax type     tuple0 "unit"
-  syntax function Tuple0 "void"
-end
-
-theory algebra.AC
-  meta AC function op
-  remove prop Comm
-  remove prop Assoc
-end
-
 theory ieee_float.Float64
   syntax predicate is_not_nan ""
   remove allprops

src/main.ml

@@ -15,8 +15,7 @@ let () =
 
 let () =
   Pyrat.init ();
-  Marabou.init ();
-  Saver.init ()
+  Marabou.init ()
 
 (* -- Logs. *)
 

src/printers/saver.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of CAISAR.                                          *)
-(*                                                                        *)
-(**************************************************************************)
-
-type info = {
-  info_syn : Why3.Printer.syntax_map;
-  variables : string Why3.Term.Hls.t;
-}
-
-let number_format =
-  {
-    Why3.Number.long_int_support = `Default;
-    Why3.Number.negative_int_support = `Default;
-    Why3.Number.dec_int_support = `Default;
-    Why3.Number.hex_int_support = `Unsupported;
-    Why3.Number.oct_int_support = `Unsupported;
-    Why3.Number.bin_int_support = `Unsupported;
-    Why3.Number.negative_real_support = `Default;
-    Why3.Number.dec_real_support = `Default;
-    Why3.Number.hex_real_support = `Unsupported;
-    Why3.Number.frac_real_support = `Unsupported (fun _ _ -> assert false);
-  }
-
-let rec print_term info fmt t =
-  let open Why3 in
-  match t.Term.t_node with
-  | Tbinop ((Timplies | Tiff), _, _)
-  | Tnot _ | Ttrue | Tfalse | Tvar _ | Tlet _ | Tif _ | Tcase _ | Tquant _
-  | Teps _
-  | Tbinop (Tor, _, _) ->
-    Printer.unsupportedTerm t "Not supported by SAVER"
-  | Tbinop (Tand, _, _) -> assert false (* Should appear only at top-level. *)
-  | Tconst c -> Constant.(print number_format unsupported_escape) fmt c
-  | Tapp (ls, l) -> (
-    match Printer.query_syntax info.info_syn ls.ls_name with
-    | Some s ->
-      (* Only print constants in a csv-like manner when
-       * encountering an equality. Constant is expected to
-       * be on the right side of the declaration *)
-      if String.contains s '=' then print_term info fmt (List.nth l 1) else ()
-    | None -> ())
-
-let rec print_top_level_term info fmt t =
-  let open Why3 in
-  (* Don't print things we don't know. *)
-  let t_is_known =
-    Term.t_s_all
-      (fun _ -> true)
-      (fun ls ->
-        Ident.Mid.mem ls.ls_name info.info_syn || Term.Hls.mem info.variables ls)
-  in
-  match t.Term.t_node with
-  | Tquant _ -> ()
-  | Tbinop (Tand, t1, t2) ->
-    if t_is_known t1 && t_is_known t2
-    then
-      Fmt.pf fmt "%a%a"
-        (print_top_level_term info)
-        t1
-        (print_top_level_term info)
-        t2
-  | _ -> if t_is_known t then Fmt.pf fmt ",%a" (print_term info) t
-
-let print_decl info fmt d =
-  let open Why3 in
-  match d.Decl.d_node with
-  | Dtype _ -> ()
-  | Ddata _ -> ()
-  | Dparam _ -> ()
-  | Dlogic _ -> ()
-  | Dind _ -> ()
-  | Dprop (Decl.Plemma, _, _) -> assert false
-  | Dprop (Decl.Paxiom, _, f) -> print_top_level_term info fmt f
-  | Dprop (Decl.Pgoal, _, f) -> print_top_level_term info fmt f
-
-let rec print_tdecl info fmt task =
-  let open Why3 in
-  match task with
-  | None -> ()
-  | Some { Task.task_prev; task_decl; _ } -> (
-    print_tdecl info fmt task_prev;
-    match task_decl.Theory.td_node with
-    | Use _ | Clone _ -> ()
-    | Meta (meta, l) when Theory.meta_equal meta Native_nn_prover.meta_input
-      -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "x%i" i)
-      | _ -> assert false)
-    | Meta (meta, l) when Theory.meta_equal meta Native_nn_prover.meta_output
-      -> (
-      match l with
-      | [ MAls ls; MAint i ] -> Term.Hls.add info.variables ls (Fmt.str "y%i" i)
-      | _ -> assert false)
-    | Meta (_, _) -> ()
-    | Decl d -> print_decl info fmt d)
-
-let print_task args ?old:_ fmt task =
-  let open Why3 in
-  let info =
-    {
-      info_syn = Discriminate.get_syntax_map task;
-      variables = Term.Hls.create 10;
-    }
-  in
-  Printer.print_prelude fmt args.Printer.prelude;
-  Format.fprintf fmt "# 1 3\n1";
-  print_tdecl info fmt task
-
-let init () =
-  Why3.Printer.register_printer ~desc:"Printer for the SAVer prover." "saver"
-    print_task