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.4 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 31 32 33 34 35

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


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


50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
(* 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
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 *)
79
let alt_ergo : Whyconf.config_prover = 
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82 83
  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
84
    exit 0
MARCHE Claude's avatar
MARCHE Claude committed
85

86 87
(* 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
88
(* loading the Alt-Ergo driver *)
89
let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
MARCHE Claude's avatar
MARCHE Claude committed
90

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

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

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

105 106 107
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
108 109 110 111 112 113 114 115 116



(*

An arithmetic goal: 2+2 = 4

*)

117 118 119 120 121 122 123 124 125
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
126 127 128 129 130 131

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

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

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

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 172 173
(* 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
174 175 176 177

(* build a theory with all these goals *)