Commit 46bc918d authored by François Bobot's avatar François Bobot

plugin genequlin : update it to the new API for the release, add locations

parent d49abbed
......@@ -24,30 +24,33 @@
open Why3
open Format
(***************
This file builds some goals using the API and calls
the alt-ergo prover to check them
******************)
(* First, we need to access the Why configuration *)
(* let config = Whyconf.read_config None *)
(* let main = Whyconf.get_main config *)
(* let env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) *)
(* let provers = Whyconf.get_provers config *)
(* let alt_ergo = *)
(* try *)
(* Util.Mstr.find "alt-ergo" provers *)
(* with Not_found -> *)
(* eprintf "Prover alt-ergo not installed or not configured@."; *)
(* exit 0 *)
(**************)
(*
(* let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver *)
This plugin generate randomly linear arithmetic problems from a
source file.Here an exemple :
========
2
5 5 5
15 5 5
5 15 5
5 5 15
========
The first line give the seed to use. Each other lines corresond to one goal :
- the first number give the number of variables
- the second the number of equation
- the third the absolute maximun of the constants used
For compiling it :
make example_plugins.opt
cp examples/plugins/genequlin.cmxs plugins
bin/why3config --detect-plugins
For testing it :
bin/why3ide examples/plugins/test.equlin
*)
open Theory
open Term
......@@ -55,67 +58,77 @@ open Util
open Ident
(** read one line *)
let scanf s =
let invar = String.index_from s 0 ' ' in
let im = String.index_from s (invar+1) ' ' in
int_of_string (String.sub s 0 invar),
int_of_string (String.sub s (invar+1) (im-(invar+1))),
int_of_string (String.sub s (im+1) ((String.length s) - (im+1)))
(** the main function *)
let read_channel env filename cin =
(** Find the int theory and the needed operation *)
let th_int = Env.find_theory env ["int"] "Int" in
let leq = ns_find_ls th_int.th_export ["infix <"] in
let plus_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix +"] in
let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in
(*
An arithmetic goal: 2+2 = 4
*)
let zero = t_const (ConstInt "0") in
(** create a contraint : polynome <= constant *)
let create_lit lvar k lits _ =
let left = List.fold_left (fun acc e ->
let const = string_of_int ((Random.int k) - (k/2)) in
let monome = t_app mult_symbol [e;t_const(ConstInt const)] Ty.ty_int in
t_app plus_symbol [acc;monome] Ty.ty_int) zero lvar in
let monome = t_app mult_symbol [e;t_const(ConstInt const)]
(Some Ty.ty_int) in
t_app plus_symbol [acc;monome] (Some Ty.ty_int)) zero lvar in
let rconst = string_of_int ((Random.int k) - (k/2)) in
f_and_simp lits (f_app leq [left;t_const(ConstInt rconst)]) in
t_and_simp lits (t_app leq [left;t_const(ConstInt rconst)] None) in
(** create a set of constraints *)
let create_fmla nvar m k =
let lvar = mapi (fun _ -> create_vsymbol (id_fresh "x") Ty.ty_int)
1 nvar in
let lt = List.map t_var lvar in
let lits = foldi (create_lit lt k) f_true 1 m in
f_forall_close lvar [] (f_implies_simp lits f_false) in
(* let create_task nvar m k = *)
(* let task = None in *)
(* let task = Task.use_export task th_int in *)
(* let goal_id = Decl.create_prsymbol (Ident.id_fresh "goal") in *)
(* let fmla = create_fmla nvar m k in *)
(* let task = Task.add_prop_decl task Decl.Pgoal goal_id fmla in *)
(* task in *)
let seed = input_line cin in
let lits = foldi (create_lit lt k) t_true 1 m in
t_forall_close lvar [] (t_implies_simp lits t_false) in
(** read the first line *)
let line = ref 0 in
begin try
let seed = input_line cin in
Random.init (int_of_string seed)
with _ ->
Printf.eprintf "error file %s line 1\n" filename;
exit 1
end;
let th_uc = create_theory (id_fresh "EqLin") in
(** Create the theory *)
let th_uc_loc = Loc.user_position filename 1 0 0 in
let th_uc = create_theory (id_user "EqLin" th_uc_loc) in
let th_uc = Theory.use_export th_uc th_int in
(** Read one line and add it to the theory *)
let fold th_uc s =
let nvar,m,k =
try
incr line;
Scanf.sscanf s "%i %i %i" (fun nvar m k -> nvar,m,k)
(** Dont use scanf because I don't know how to link it in plugin
(without segfault) *)
(* Scanf.sscanf s "%i %i %i" (fun nvar m k -> nvar,m,k) *)
scanf s
with _ -> Printf.eprintf "Error file %s line %i" filename !line;exit 1 in
let loc = Loc.user_position filename (!line+1) 0 (String.length s) in
let goal_id = Decl.create_prsymbol
(Ident.id_fresh (Printf.sprintf "goal%i" !line)) in
(Ident.id_user (Printf.sprintf "goal%i" !line) loc) in
let fmla = create_fmla nvar m k in
let th_uc = Theory.add_prop_decl th_uc Decl.Pgoal goal_id fmla in
th_uc in
(** Read all the file *)
let th_uc = Sysutil.fold_channel fold th_uc cin in
Mnm.add "EqLin" (close_theory th_uc) Mnm.empty
(** Return the map with the theory *)
Mstr.singleton "EqLin" (close_theory th_uc)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment