use_api.ml 3.53 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(***************
MARCHE Claude's avatar
MARCHE Claude committed
2

MARCHE Claude's avatar
MARCHE Claude committed
3 4
This file builds some goals using the API and calls
the alt-ergo prover to check them
MARCHE Claude's avatar
MARCHE Claude committed
5

MARCHE Claude's avatar
MARCHE Claude committed
6
******************)
MARCHE Claude's avatar
MARCHE Claude committed
7

MARCHE Claude's avatar
MARCHE Claude committed
8
(* opening the Why3 library *)
MARCHE Claude's avatar
MARCHE Claude committed
9
open Why
MARCHE Claude's avatar
MARCHE Claude committed
10 11 12 13 14 15 16

(* a ground propositional goal: true or false *)
let fmla_true : Term.fmla = Term.f_true
let fmla_false : Term.fmla = Term.f_false
let fmla1 : Term.fmla = Term.f_or fmla_true fmla_false

(* printing it *)
MARCHE Claude's avatar
MARCHE Claude committed
17
open Format
MARCHE Claude's avatar
MARCHE Claude committed
18
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
MARCHE Claude's avatar
MARCHE Claude committed
19 20


MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24 25 26 27 28
(* a propositional goal: A and B implies A *)

let prop_var_A : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol = Term.create_psymbol (Ident.id_fresh "B") []
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla = Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
MARCHE Claude's avatar
MARCHE Claude committed
29 30


MARCHE Claude's avatar
MARCHE Claude committed
31
(* To build tasks and call prover, we need to access the Why configuration *)
MARCHE Claude's avatar
MARCHE Claude committed
32

MARCHE Claude's avatar
MARCHE Claude committed
33
(* reads the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
34
let config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
35 36

(* the [main] section of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
37
let main = Whyconf.get_main config
MARCHE Claude's avatar
MARCHE Claude committed
38 39

(* builds the environment from the [loadpath] *)
40
let env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) 
MARCHE Claude's avatar
MARCHE Claude committed
41

MARCHE Claude's avatar
MARCHE Claude committed
42
(* the [provers] of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
43 44
let provers = Whyconf.get_provers config

MARCHE Claude's avatar
MARCHE Claude committed
45
(* the [prover alt-ergo] section of the config file *)
MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50
let alt_ergo = 
  try
    Util.Mstr.find "alt-ergo" provers 
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
MARCHE Claude's avatar
MARCHE Claude committed
51
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
52

MARCHE Claude's avatar
MARCHE Claude committed
53
(* loading the Alt-Ergo driver *)
MARCHE Claude's avatar
MARCHE Claude committed
54 55
let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver

MARCHE Claude's avatar
MARCHE Claude committed
56 57
(* building the task for formula 1 alone *)
let task1 = None (* empty task *)
MARCHE Claude's avatar
MARCHE Claude committed
58 59 60
let goal_id1 = Decl.create_prsymbol (Ident.id_fresh "goal1") 
let task1 = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1

MARCHE Claude's avatar
MARCHE Claude committed
61 62
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
MARCHE Claude's avatar
MARCHE Claude committed
63

MARCHE Claude's avatar
MARCHE Claude committed
64
(* call Alt-Ergo *)
MARCHE Claude's avatar
MARCHE Claude committed
65 66
let result1 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
67
    alt_ergo_driver task1 () ()
MARCHE Claude's avatar
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69
(* prints Alt-Ergo answer *)
MARCHE Claude's avatar
MARCHE Claude committed
70 71 72 73 74 75 76 77 78 79 80 81 82
let () = printf "@[On task 1, alt-ergo answers %a@."
  Call_provers.print_prover_result result1

let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None] 
let task2 = Task.add_logic_decl task2 [prop_var_B, None] 
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2") 
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2

let () = printf "@[task 2 created:@\n%a@]@." Pretty.print_task task2

let result2 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
83
    alt_ergo_driver task2 () ()
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111

let () = printf "@[On task 2, alt-ergo answers %a@."
  Call_provers.print_prover_result result2



(*

An arithmetic goal: 2+2 = 4

*)

let two = Term.t_const (Term.ConstInt "2")
let four = Term.t_const (Term.ConstInt "4")

let int_theory = Env.find_theory env ["int"] "Int"

let plus_symbol = Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]

let two_plus_two = Term.t_app plus_symbol [two;two] Ty.ty_int

let fmla3 = Term.f_equ two_plus_two four

let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3") 
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3

MARCHE Claude's avatar
MARCHE Claude committed
112
(*
MARCHE Claude's avatar
MARCHE Claude committed
113
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
114 115
*)
let () = printf "@[task 3 created@]@." 
MARCHE Claude's avatar
MARCHE Claude committed
116 117 118

let result3 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
119
    alt_ergo_driver task3 () ()
MARCHE Claude's avatar
MARCHE Claude committed
120 121 122 123 124 125 126 127

let () = printf "@[On task 3, alt-ergo answers %a@."
  Call_provers.print_prover_result result3


(* build a theory with all these goals *)