use_api.ml 6.38 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
(*    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
19

MARCHE Claude's avatar
MARCHE Claude committed
20
21
This file builds some goals using the API and calls
the alt-ergo prover to check them
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
MARCHE Claude committed
23
******************)
MARCHE Claude's avatar
MARCHE Claude committed
24

MARCHE Claude's avatar
MARCHE Claude committed
25
(* opening the Why3 library *)
MARCHE Claude's avatar
MARCHE Claude committed
26
open Why
MARCHE Claude's avatar
MARCHE Claude committed
27
28
29
30
31
32
33

(* 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
34
open Format
MARCHE Claude's avatar
MARCHE Claude committed
35
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_fmla fmla1
MARCHE Claude's avatar
MARCHE Claude committed
36
37


MARCHE Claude's avatar
MARCHE Claude committed
38
39
40
41
42
43
44
45
(* 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
46
47


48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1") 
let task1 : Task.task = Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1

(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1

(* task for formula 2 *)
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



(* To call a prover, we need to access the Why configuration *)
MARCHE Claude's avatar
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69
(* reads the config file *)
70
let config : Whyconf.config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
71
(* the [main] section of the config file *)
72
73
74
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Util.Mstr.t = Whyconf.get_provers config
MARCHE Claude's avatar
MARCHE Claude committed
75

MARCHE Claude's avatar
MARCHE Claude committed
76
(* the [prover alt-ergo] section of the config file *)
77
let alt_ergo : Whyconf.config_prover = 
MARCHE Claude's avatar
MARCHE Claude committed
78
79
80
81
  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
82
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
83

84
85
(* builds the environment from the [loadpath] *)
let env : Env.env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) 
MARCHE Claude's avatar
MARCHE Claude committed
86
(* loading the Alt-Ergo driver *)
87
let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
88

MARCHE Claude's avatar
MARCHE Claude committed
89
(* call Alt-Ergo *)
90
let result1 : Call_provers.prover_result = 
MARCHE Claude's avatar
MARCHE Claude committed
91
  Driver.prove_task ~command:alt_ergo.Whyconf.command
92
    alt_ergo_driver task1 () ()
MARCHE Claude's avatar
MARCHE Claude committed
93

MARCHE Claude's avatar
MARCHE Claude committed
94
(* prints Alt-Ergo answer *)
MARCHE Claude's avatar
MARCHE Claude committed
95
96
97
let () = printf "@[On task 1, alt-ergo answers %a@."
  Call_provers.print_prover_result result1

98
let result2 : Call_provers.prover_result = 
MARCHE Claude's avatar
MARCHE Claude committed
99
  Driver.prove_task ~command:alt_ergo.Whyconf.command
100
    ~timelimit:10
101
    alt_ergo_driver task2 () ()
MARCHE Claude's avatar
MARCHE Claude committed
102

103
104
105
let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
  Call_provers.print_prover_answer result1.Call_provers.pr_answer
  result1.Call_provers.pr_time
MARCHE Claude's avatar
MARCHE Claude committed
106
107
108
109
110
111
112
113
114



(*

An arithmetic goal: 2+2 = 4

*)

115
116
117
118
119
120
121
122
123
let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4")
let int_theory : Theory.theory = 
  Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term = Term.t_app plus_symbol [two;two] Ty.ty_int
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two] 
let fmla3 : Term.fmla = Term.f_equ two_plus_two four
MARCHE Claude's avatar
MARCHE Claude committed
124
125
126
127
128
129

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
130
(*
MARCHE Claude's avatar
MARCHE Claude committed
131
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
132
133
*)
let () = printf "@[task 3 created@]@." 
MARCHE Claude's avatar
MARCHE Claude committed
134
135
136

let result3 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
137
    alt_ergo_driver task3 () ()
MARCHE Claude's avatar
MARCHE Claude committed
138
139
140
141

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

142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
(* quantifiers: let's build "forall x:int. x*x >= 0" *)
let zero : Term.term = Term.t_const (Term.ConstInt "0")
let mult_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol = 
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]

let var_x : Term.vsymbol = 
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
let x : Term.term = Term.t_var var_x
let x_times_x : Term.term = 
  Term.t_app_infer mult_symbol [x;x] 
let fmla4_aux : Term.fmla = 
  Term.f_app ge_symbol [x_times_x;zero]
let fmla4_quant : Term.fmla_quant = 
  Term.f_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.fmla =
  Term.f_forall fmla4_quant

let task4 = None
let task4 = Task.use_export task4 int_theory
let goal_id4 = Decl.create_prsymbol (Ident.id_fresh "goal4") 
let task4 = Task.add_prop_decl task4 Decl.Pgoal goal_id4 fmla4

let result4 = 
  Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task4 () ()

let () = printf "@[On task 4, alt-ergo answers %a@."
  Call_provers.print_prover_result result4
MARCHE Claude's avatar
MARCHE Claude committed
172
173
174
175

(* build a theory with all these goals *)