use_api.ml 5.04 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


31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
(* 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
51

MARCHE Claude's avatar
MARCHE Claude committed
52
(* reads the config file *)
53
let config : Whyconf.config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
54
(* the [main] section of the config file *)
55
56
57
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
58

MARCHE Claude's avatar
MARCHE Claude committed
59
(* the [prover alt-ergo] section of the config file *)
60
let alt_ergo : Whyconf.config_prover = 
MARCHE Claude's avatar
MARCHE Claude committed
61
62
63
64
  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
65
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
66

67
68
(* 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
69
(* loading the Alt-Ergo driver *)
70
let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
71

MARCHE Claude's avatar
MARCHE Claude committed
72
(* call Alt-Ergo *)
73
let result1 : Call_provers.prover_result = 
MARCHE Claude's avatar
MARCHE Claude committed
74
  Driver.prove_task ~command:alt_ergo.Whyconf.command
75
    alt_ergo_driver task1 () ()
MARCHE Claude's avatar
MARCHE Claude committed
76

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

81
let result2 : Call_provers.prover_result = 
MARCHE Claude's avatar
MARCHE Claude committed
82
  Driver.prove_task ~command:alt_ergo.Whyconf.command
83
    ~timelimit:10
84
    alt_ergo_driver task2 () ()
MARCHE Claude's avatar
MARCHE Claude committed
85

86
87
88
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
89
90
91
92
93
94
95
96
97



(*

An arithmetic goal: 2+2 = 4

*)

98
99
100
101
102
103
104
105
106
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
107
108
109
110
111
112

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
113
(*
MARCHE Claude's avatar
MARCHE Claude committed
114
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
115
116
*)
let () = printf "@[task 3 created@]@." 
MARCHE Claude's avatar
MARCHE Claude committed
117
118
119

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

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

125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
(* 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
155
156
157
158

(* build a theory with all these goals *)