use_api.ml 6.62 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
let alt_ergo_driver : Driver.driver =
MARCHE Claude's avatar
MARCHE Claude committed
92 93 94 95 96 97
  try
    Driver.load_driver env alt_ergo.Whyconf.driver
  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
98

MARCHE Claude's avatar
MARCHE Claude committed
99
(* call Alt-Ergo *)
100 101 102 103
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
104

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

Andrei Paskevich's avatar
Andrei Paskevich committed
109
let result2 : Call_provers.prover_result =
110 111
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
112
    ~timelimit:10
113
    alt_ergo_driver task2 ()) ()
MARCHE Claude's avatar
MARCHE Claude committed
114

115 116 117
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
118 119 120 121 122 123 124 125 126



(*

An arithmetic goal: 2+2 = 4

*)

127 128
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
129
let int_theory : Theory.theory =
130
  Env.find_theory env ["int"] "Int"
Andrei Paskevich's avatar
Andrei Paskevich committed
131
let plus_symbol : Term.lsymbol =
132
  Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
133
let two_plus_two : Term.term = Term.fs_app plus_symbol [two;two] Ty.ty_int
Andrei Paskevich's avatar
Andrei Paskevich committed
134
let two_plus_two : Term.term = Term.t_app_infer plus_symbol [two;two]
135
let fmla3 : Term.term = Term.t_equ two_plus_two four
MARCHE Claude's avatar
MARCHE Claude committed
136 137 138

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

MARCHE Claude's avatar
MARCHE Claude committed
142
(*
MARCHE Claude's avatar
MARCHE Claude committed
143
let () = printf "@[task 3 created:@\n%a@]@." Pretty.print_task task3
MARCHE Claude's avatar
MARCHE Claude committed
144
*)
Andrei Paskevich's avatar
Andrei Paskevich committed
145
let () = printf "@[task 3 created@]@."
MARCHE Claude's avatar
MARCHE Claude committed
146

Andrei Paskevich's avatar
Andrei Paskevich committed
147
let result3 =
148 149 150
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task3 ()) ()
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153 154

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

155 156
(* 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
157
let mult_symbol : Term.lsymbol =
158
  Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
Andrei Paskevich's avatar
Andrei Paskevich committed
159
let ge_symbol : Term.lsymbol =
160 161
  Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]

Andrei Paskevich's avatar
Andrei Paskevich committed
162
let var_x : Term.vsymbol =
163 164
  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
165 166 167
let x_times_x : Term.term =
  Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.term =
168
  Term.ps_app ge_symbol [x_times_x;zero]
Andrei Paskevich's avatar
Andrei Paskevich committed
169
let fmla4_quant : Term.term_quant =
170 171 172
  Term.t_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.term =
  Term.t_forall fmla4_quant
173 174 175

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

Andrei Paskevich's avatar
Andrei Paskevich committed
179
let result4 =
180 181 182
  Call_provers.wait_on_call
    (Driver.prove_task ~command:alt_ergo.Whyconf.command
    alt_ergo_driver task4 ()) ()
183 184 185

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

(* build a theory with all these goals *)