benchrc.mli 936 Bytes
Newer Older
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


(**

[probs "myprobs"]
   file = "examples/monbut.why" #relatives to the rc file
   file = "examples/monprogram.mlw"
   theory = "monprogram.T"
   goal = "monbut.T.G"

   transform = "split_goal" #applied in the order
   transform = "..."
   transform = "..."

[tools "mytools"]
prover = cvc3
prover = altergo
#or only one
driver = "..."
command = "..."

loadpath = "..." #added to the one in why.conf
loadpath = "..."

timelimit = 30
memlimit = 300

use = "toto.T" #use the theory toto (allow to add metas)

transform = "simplify_array" #only 1 to 1

[bench "mybench"]
tools = "mytools"
tools = ...
probs = "myprobs"
probs = ...
François Bobot's avatar
François Bobot committed
37 38 39
timeline = "prgbench.time"
average = "prgbench.avg"
csv = "prgbench.csv"
40 41 42 43 44 45
*)

open Bench
open Why
open Util

46

47 48 49
type benchrc = { tools : tool list Mstr.t;
                 probs : prob list Mstr.t;
                 benchs : bench Mstr.t
50 51 52
               }

val read_file : Whyconf.config -> string -> benchrc