driver.mli 2.23 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

MARCHE Claude's avatar
MARCHE Claude committed
20
(** Managing the drivers for external provers *)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
21

22
(** {2 create a driver} *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23

Andrei Paskevich's avatar
Andrei Paskevich committed
24
type driver
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
25

26
val load_driver : Env.env -> string -> driver
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
27 28
(** loads a driver from a file
    @param env TODO
29
    @param string driver file name
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
30
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31

32
(** {2 use a driver} *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33

34
val file_of_task : driver -> string -> string -> Task.task -> string
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38
(** [file_of_task d f th t] produces a filename
    for the prover of driver [d], for a task [t] generated from
    a goal in theory [th] of filename [f]
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
39

40
val call_on_buffer :
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
41
  command    : string ->
42 43
  ?timelimit : int ->
  ?memlimit  : int ->
44
  driver -> Buffer.t -> Call_provers.bare_prover_call
45

46
val print_task :
47
  ?old       : in_channel ->
48
  driver -> Format.formatter -> Task.task -> unit
49

50 51 52 53
val prove_task :
  command    : string ->
  ?timelimit : int ->
  ?memlimit  : int ->
54
  ?old       : in_channel ->
55
  driver -> Task.task -> Call_provers.bare_prover_call
56