------------------------------------------------------------------------------
-- 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;