Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

use_api.ml 6.51 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
(*******************

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

MARCHE Claude's avatar
MARCHE Claude committed
25
******************)
MARCHE Claude's avatar
MARCHE Claude committed
26

MARCHE Claude's avatar
MARCHE Claude committed
27
(* opening the Why3 library *)
MARCHE Claude's avatar
MARCHE Claude committed
28
open Why
MARCHE Claude's avatar
MARCHE Claude committed
29 30

(* a ground propositional goal: true or false *)
31 32 33
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
34 35

(* printing it *)
MARCHE Claude's avatar
MARCHE Claude committed
36
open Format
37
let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
MARCHE Claude's avatar
MARCHE Claude committed
38 39


MARCHE Claude's avatar
MARCHE Claude committed
40 41 42 43
(* 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") []
44 45 46
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
47
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_term fmla2
MARCHE Claude's avatar
MARCHE Claude committed
48 49


50 51
(* building the task for formula 1 alone *)
let task1 : Task.task = None (* empty task *)
Andrei Paskevich's avatar
Andrei Paskevich committed
52
let goal_id1 : Decl.prsymbol = Decl.create_prsymbol (Ident.id_fresh "goal1")
53 54 55 56 57 58 59
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
Andrei Paskevich's avatar
Andrei Paskevich committed
60 61 62
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")
63 64 65 66 67 68 69
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
70

MARCHE Claude's avatar
MARCHE Claude committed
71
(* reads the config file *)
72
let config : Whyconf.config = Whyconf.read_config None
MARCHE Claude's avatar
MARCHE Claude committed
73
(* the [main] section of the config file *)
74 75 76
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
77

MARCHE Claude's avatar
MARCHE Claude committed
78
(* the [prover alt-ergo] section of the config file *)
Andrei Paskevich's avatar
Andrei Paskevich committed
79
let alt_ergo : Whyconf.config_prover =
MARCHE Claude's avatar
MARCHE Claude committed
80
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
81
    Util.Mstr.find "alt-ergo" provers
MARCHE Claude's avatar
MARCHE Claude committed
82 83
  with Not_found ->
    eprintf "Prover alt-ergo not installed or not configured@.";
MARCHE Claude's avatar
MARCHE Claude committed
84
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
85

86
(* builds the environment from the [loadpath] *)
Andrei Paskevich's avatar
Andrei Paskevich committed
87 88 89
let env : Env.env =
  Env.create_env_of_loadpath (Whyconf.loadpath main)

MARCHE Claude's avatar
MARCHE Claude committed
90
(* loading the Alt-Ergo driver *)
Andrei Paskevich's avatar
Andrei Paskevich committed
91 92
let alt_ergo_driver : Driver.driver =
  Driver.load_driver env alt_ergo.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
93

MARCHE Claude's avatar
MARCHE Claude committed
94
(* call 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

*)

122 123
let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4")
Andrei Paskevich's avatar
Andrei Paskevich committed
124
let int_theory : Theory.theory =
125
  Env.find_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 151
(* quantifiers: let's build "forall x:int. x*x >= 0" *)
let zero : Term.term = Term.t_const (Term.ConstInt "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]
Andrei Paskevich's avatar
Andrei Paskevich committed
164
let fmla4_quant : Term.term_quant =
165 166 167
  Term.t_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.term =
  Term.t_forall fmla4_quant
168 169 170

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

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

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

(* build a theory with all these goals *)