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 *)