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 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
(* builds the environment from the [loadpath] *)
87
let env : Env.env = Lexer.create_env (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 93 94 95
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
96

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

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

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



(*

An arithmetic goal: 2+2 = 4

*)

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

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

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

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

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
(* 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 = 
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 181

(* build a theory with all these goals *)