spat_1.3.0_4ad4ab14/src/core/spat-spark_info-heuristics.ads

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
------------------------------------------------------------------------------
--  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);

------------------------------------------------------------------------------
--
--  SPARK Proof Analysis Tool
--
--  S.P.A.T. - Heuristic stuff. Tries to find optimal prover configuration.
--
------------------------------------------------------------------------------

with SPAT.GPR_Support;
with Ada.Containers.Vectors;

package SPAT.Spark_Info.Heuristics is

   type Workloads is
      record
         --  The name of the prover.
         Success_Time : Duration;
         --  accumulated time of successful attempts
         Failed_Time  : Duration;
         --  accumulated time of failed attempts
         Max_Success  : Time_And_Steps;
         --  maximum time/steps for a successful attempt
      end record;

   type Prover_Data is
      record
         Name     : Prover_Name;
         Workload : Workloads;
      end record;

   package Prover_Vectors is new
     Ada.Containers.Vectors (Index_Type   => Positive,
                             Element_Type => Prover_Data);

   type File_Data is
      record
         Name    : Source_File_Name;
         Provers : Prover_Vectors.Vector;
      end record;

   package File_Vectors is new
     Ada.Containers.Vectors (Index_Type   => Positive,
                             Element_Type => File_Data);

   ---------------------------------------------------------------------------
   --  Find_Optimum
   --
   --  This is a highly experimental feature.
   --
   --  Tries to find an "optimal" prover configuration.
   ---------------------------------------------------------------------------
   function Find_Optimum
     (Info     : in T;
      File_Map : in GPR_Support.SPARK_Source_Maps.Map)
      return File_Vectors.Vector;

end SPAT.Spark_Info.Heuristics;