driver.mli 3.22 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    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
21
(** Managing the drivers for external provers *)
MARCHE Claude's avatar
API doc  
MARCHE Claude committed
22

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

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

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

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

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

42 43 44 45
val file_of_theory : driver -> string -> Theory.theory -> string
(** [file_of_theory d f th] produces a filename
    for the prover of driver [d], for a theory [th] from filename [f] *)

46
val call_on_buffer :
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
47
  command    : string ->
48 49
  ?timelimit : int ->
  ?memlimit  : int ->
50
  ?inplace   : bool ->
51
  filename   : string ->
Andrei Paskevich's avatar
Andrei Paskevich committed
52
  driver -> Buffer.t -> Call_provers.pre_prover_call
53

54

55
val print_task :
56
  ?old       : in_channel ->
57
  driver -> Format.formatter -> Task.task -> unit
58

59 60 61 62 63
val print_theory :
  ?old       : in_channel ->
  driver -> Format.formatter -> Theory.theory -> unit
  (** produce a realization of the given theory using the given driver *)

64 65 66 67
val prove_task :
  command    : string ->
  ?timelimit : int ->
  ?memlimit  : int ->
68 69
  ?old       : string ->
  ?inplace   : bool ->
Andrei Paskevich's avatar
Andrei Paskevich committed
70
  driver -> Task.task -> Call_provers.pre_prover_call
71

72
(** Split the previous function in two simpler functions *)
73
val prepare_task : driver -> Task.task -> Task.task
74

75 76 77 78 79 80 81 82
val print_task_prepared :
  ?old       : in_channel ->
  driver -> Format.formatter -> Task.task -> unit

val prove_task_prepared :
  command    : string ->
  ?timelimit : int ->
  ?memlimit  : int ->
83 84
  ?old       : string ->
  ?inplace   : bool ->
85
  driver -> Task.task -> Call_provers.pre_prover_call
MARCHE Claude's avatar
MARCHE Claude committed
86