logic.ml 8.19 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1
2
3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5
6
7
8
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

MARCHE Claude's avatar
MARCHE Claude committed
12
13
(*******************

MARCHE Claude's avatar
MARCHE Claude committed
14
15
This file builds some goals using the API and calls
the alt-ergo prover to check them
MARCHE Claude's avatar
MARCHE Claude committed
16

MARCHE Claude's avatar
MARCHE Claude committed
17
******************)
MARCHE Claude's avatar
MARCHE Claude committed
18

MARCHE Claude's avatar
MARCHE Claude committed
19
(* opening the Why3 library *)
20
open Why3
MARCHE Claude's avatar
MARCHE Claude committed
21
22

(* a ground propositional goal: true or false *)
23
24
25
let fmla_true : Term.term = Term.t_true
let fmla_false : Term.term = Term.t_false
let fmla1 : Term.term = Term.t_or fmla_true fmla_false
MARCHE Claude's avatar
MARCHE Claude committed
26
27

(* printing it *)
MARCHE Claude's avatar
MARCHE Claude committed
28
open Format
29
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
MARCHE Claude's avatar
MARCHE Claude committed
30
31


MARCHE Claude's avatar
MARCHE Claude committed
32
33
34
35
(* 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") []
36
37
38
let atom_A : Term.term = Term.ps_app prop_var_A []
let atom_B : Term.term = Term.ps_app prop_var_B []
let fmla2 : Term.term = Term.t_implies (Term.t_and atom_A atom_B) atom_A
39
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
MARCHE Claude's avatar
MARCHE Claude committed
40
41


42
43
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
Andrei Paskevich's avatar
Andrei Paskevich committed
44
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
45
46
47
48
49
50
51
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
52
53
let task2 = Task.add_param_decl task2 prop_var_A
let task2 = Task.add_param_decl task2 prop_var_B
Andrei Paskevich's avatar
Andrei Paskevich committed
54
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
55
56
57
58
59
60
61
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
62

MARCHE Claude's avatar
MARCHE Claude committed
63
(* reads the config file *)
64
let config : Whyconf.config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
65
(* the [main] section of the config file *)
66
67
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
68
69
let provers : Whyconf.config_prover Whyconf.Mprover.t =
  Whyconf.get_provers config
MARCHE Claude's avatar
MARCHE Claude committed
70

71
(* One prover named Alt-Ergo in the config file *)
Andrei Paskevich's avatar
Andrei Paskevich committed
72
let alt_ergo : Whyconf.config_prover =
73
74
75
76
  let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
  (** all provers that have the name "Alt-Ergo" *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
77
    eprintf "Prover Alt-Ergo not installed or not configured@.";
78
    exit 0
79
  end else
Andrei Paskevich's avatar
Andrei Paskevich committed
80
    snd (Whyconf.Mprover.max_binding provers)
MARCHE Claude's avatar
MARCHE Claude committed
81

82
(* builds the environment from the [loadpath] *)
83
let env : Env.env = Env.create_env (Whyconf.loadpath main)
Andrei Paskevich's avatar
Andrei Paskevich committed
84

MARCHE Claude's avatar
MARCHE Claude committed
85
(* loading the Alt-Ergo driver *)
Andrei Paskevich's avatar
Andrei Paskevich committed
86
let alt_ergo_driver : Driver.driver =
MARCHE Claude's avatar
MARCHE Claude committed
87
  try
Guillaume Melquiond's avatar
Guillaume Melquiond committed
88
    Driver.load_driver env alt_ergo.Whyconf.driver []
MARCHE Claude's avatar
MARCHE Claude committed
89
90
91
92
  with e ->
    eprintf "Failed to load driver for alt-ergo: %a@."
      Exn_printer.exn_printer e;
    exit 1
MARCHE Claude's avatar
MARCHE Claude committed
93

94
(* calls Alt-Ergo *)
95
96
97
98
let result1 : Call_provers.prover_result =
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task1 ()) ()
MARCHE Claude's avatar
MARCHE Claude committed
99

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

Andrei Paskevich's avatar
Andrei Paskevich committed
104
let result2 : Call_provers.prover_result =
105
106
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
107
    ~timelimit:10
108
    alt_ergo_driver task2 ()) ()
MARCHE Claude's avatar
MARCHE Claude committed
109

110
111
112
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
113
114
115
116
117
118
119
120
121



(*

An arithmetic goal: 2+2 = 4

*)

Andrei Paskevich's avatar
Andrei Paskevich committed
122
123
let two : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "2"))
let four : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "4"))
Andrei Paskevich's avatar
Andrei Paskevich committed
124
let int_theory : Theory.theory =
125
  Env.read_theory env ["int"] "Int"
Andrei Paskevich's avatar
Andrei Paskevich committed
126
let plus_symbol : Term.lsymbol =
127
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
128
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
Andrei Paskevich's avatar
Andrei Paskevich committed
129
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
130
let fmla3 : Term.term = Term.t_equ two_plus_two four
MARCHE Claude's avatar
MARCHE Claude committed
131
132
133

let task3 = None
let task3 = Task.use_export task3 int_theory
Andrei Paskevich's avatar
Andrei Paskevich committed
134
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
MARCHE Claude's avatar
MARCHE Claude committed
135
136
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3

MARCHE Claude's avatar
MARCHE Claude committed
137
(*
MARCHE Claude's avatar
MARCHE Claude committed
138
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
139
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
140
let () = printf "@[task 3 created@]@."
MARCHE Claude's avatar
MARCHE Claude committed
141

Andrei Paskevich's avatar
Andrei Paskevich committed
142
let result3 =
143
144
145
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task3 ()) ()
MARCHE Claude's avatar
MARCHE Claude committed
146
147
148
149

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

150
(* quantifiers: let's build "forall x:int. x*x >= 0" *)
Andrei Paskevich's avatar
Andrei Paskevich committed
151
let zero : Term.term = Term.t_const (Number.ConstInt (Number.int_const_dec "0"))
Andrei Paskevich's avatar
Andrei Paskevich committed
152
let mult_symbol : Term.lsymbol =
153
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
Andrei Paskevich's avatar
Andrei Paskevich committed
154
let ge_symbol : Term.lsymbol =
155
156
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]

Andrei Paskevich's avatar
Andrei Paskevich committed
157
let var_x : Term.vsymbol =
158
159
  Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
let x : Term.term = Term.t_var var_x
Andrei Paskevich's avatar
Andrei Paskevich committed
160
161
162
let x_times_x : Term.term =
  Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term =
163
  Term.ps_app ge_symbol [x_times_x;zero]
164
let fmla4 : Term.term = Term.t_forall_close [var_x] [] fmla4_aux
165
166
167

let task4 = None
let task4 = Task.use_export task4 int_theory
Andrei Paskevich's avatar
Andrei Paskevich committed
168
let goal_id4 = Decl.create_prsymbol (Ident.id_fresh "goal4")
169
170
let task4 = Task.add_prop_decl task4 Decl.Pgoal goal_id4 fmla4

Andrei Paskevich's avatar
Andrei Paskevich committed
171
let result4 =
172
173
174
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task4 ()) ()
175
176
177

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

(* build a theory with all these goals *)

181
182
183
(* create a theory *)
let () = printf "@[creating theory 'My_theory'@]@."

184
let my_theory : Theory.theory_uc =
185
186
187
188
189
190
191
192
193
194
195
  Theory.create_theory (Ident.id_fresh "My_theory")

(* add declarations of goals *)

let () = printf "@[adding goal 1@]@."
let decl_goal1 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id1 fmla1
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal1

let () = printf "@[adding goal 2@]@."
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_A
let my_theory : Theory.theory_uc = Theory.add_param_decl my_theory prop_var_B
196
let decl_goal2 : Decl.decl =
197
198
199
200
201
202
203
  Decl.create_prop_decl Decl.Pgoal goal_id2 fmla2
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal2

(* helper function: [use th1 th2] insert the equivalent of a "use import th2"
   in theory th1 under construction *)
let use th1 th2 =
  let name = th2.Theory.th_name in
204
205
206
  Theory.close_scope
    (Theory.use_export (Theory.open_scope th1 name.Ident.id_string) th2)
    ~import:true
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226

let () = printf "@[adding goal 3@]@."
(* use import int.Int *)
let my_theory : Theory.theory_uc = use my_theory int_theory
let decl_goal3 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id3 fmla3
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal3

let () = printf "@[adding goal 4@]@."
let decl_goal4 : Decl.decl = Decl.create_prop_decl Decl.Pgoal goal_id4 fmla4
let my_theory : Theory.theory_uc = Theory.add_decl my_theory decl_goal4

(* closing the theory *)
let my_theory : Theory.theory = Theory.close_theory my_theory

(* printing the result *)

let () = printf "@[theory is:@\n%a@]@." Pretty.print_theory my_theory

(* getting set of task from a theory *)

227
let my_tasks : Task.task list =
228
229
230
  List.rev (Task.split_theory my_theory None None)


231
let () =
232
233
234
235
236
237
  printf "Tasks are:@.";
  let _ =
    List.fold_left
      (fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
      1 my_tasks
  in ()
238
239
240
241
242





243
244
245


(*
246
247
248
Local Variables:
compile-command: "ocaml -I ../../lib/why3 unix.cma nums.cma str.cma dynlink.cma ../../lib/why3/why3.cma use_api.ml"
End:
249
*)