------------------------------------------------------------------------------
--  Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
--  This work is free. You can redistribute it and/or modify it under the
--  terms of the Do What The Fuck You Want To Public License, Version 2,
--  as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);

with Ada.Strings.Fixed;
with SI_Units.Metric;
with SI_Units.Names;

with SPAT.Command_Line;

package body SPAT is

   ---------------------------------------------------------------------------
   --  Nice_Image
   ---------------------------------------------------------------------------
   function Nice_Image is new
     SI_Units.Metric.Fixed_Image (Item        => Duration,
                                  Default_Aft => 0,
                                  Unit        => SI_Units.Names.Second);

   ---------------------------------------------------------------------------
   --  Image
   ---------------------------------------------------------------------------
   function Image (Value : in Duration) return String is
     (if SPAT.Command_Line.Raw_Mode.Get
      then Value'Image
      else Nice_Image (Value => Value));

   ---------------------------------------------------------------------------
   --  Image
   ---------------------------------------------------------------------------
   function Image (Value : in Duration;
                   Steps : in Prover_Steps) return String is
     (Image (Value => Value) & " (" &
      Ada.Strings.Fixed.Trim (Source => Steps'Image,
                              Side   => Ada.Strings.Both) & " step" &
      (if Steps /= 1 then "s)" else ")"));

   ---------------------------------------------------------------------------
   --  Scaled
   --
   --  See https://github.com/AdaCore/why3/blob/master/src/gnat/gnat_config.ml#L538
   ---------------------------------------------------------------------------
   function Scaled (Prover    : in Prover_Name;
                    Raw_Steps : in Prover_Steps) return Prover_Steps is
   begin
      --  Especially with Z3, negative steps indicate a proof failure (i.e. out
      --  of memory situation etc.), so if the input number is negative leave it
      --  as is.  At least I find it counterintuitive, that -1 would be
      --  converted to +1 instead.
      if Raw_Steps < 0 then
         return Raw_Steps;
      end if;

      if
        Ada.Strings.Unbounded.Index (Source  => Subject_Name (Prover),
                                     Pattern => "CVC4") = 1
      then
         --  add = 15_000, mult = 35
         return Prover_Steps'Max (Raw_Steps - 15_000, 0) / 35 + 1;
      end if;

      if
        Ada.Strings.Unbounded.Index (Source => Subject_Name (Prover),
                                     Pattern => "Z3") = 1
      then
         --  add = 450_000, mult = 800
         return Prover_Steps'Max (Raw_Steps - 450_000, 0) / 800 + 1;
      end if;

      --  alt-ergo, and others => no scaling
      return Raw_Steps + 1;
   end Scaled;

end SPAT;