genequlin.ml 4.61 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12 13 14 15
(*
*)


16
open Why3
17

18 19
(**************)
(*
20

21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
  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
43

44
*)
45 46 47

open Theory
open Term
48
open Stdlib
49 50 51

open Ident

52 53 54 55 56 57 58 59
(** 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)))

60

61
(** the main function *)
62
let read_channel env path filename cin =
63
  (** Find the int theory and the needed operation *)
64
  let th_int = Env.find_theory (Env.env_of_library env) ["int"] "Int" in
65 66
  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
67
  let neg_symbol = Theory.ns_find_ls th_int.Theory.th_export ["prefix -"] in
68 69
  let mult_symbol = Theory.ns_find_ls th_int.Theory.th_export ["infix *"] in

70 71 72 73 74
  let zero = t_nat_const 0 in
  let t_int_const n =
    if n >= 0 then t_nat_const n else
      t_app_infer neg_symbol [t_nat_const (-n)]
  in
75

76
  (** create a contraint : polynome <= constant *)
77 78
  let create_lit lvar k lits _ =
    let left = List.fold_left (fun acc e ->
79
      let const = (Random.int k) - (k/2) in
80
      let monome = t_app mult_symbol [e;t_int_const const]
81 82
        (Some Ty.ty_int) in
      t_app plus_symbol [acc;monome] (Some Ty.ty_int)) zero lvar in
83
    let rconst = (Random.int k) - (k/2) in
84
    t_and_simp lits (t_app leq [left;t_int_const rconst] None) in
85

86
  (** create a set of constraints *)
87
  let create_fmla nvar m k =
88
    let lvar = Util.mapi (fun _ -> create_vsymbol (id_fresh "x") Ty.ty_int)
89 90
      1 nvar in
    let lt = List.map t_var lvar in
91
    let lits = Util.foldi (create_lit lt k) t_true 1 m in
92 93 94
    t_forall_close lvar [] (t_implies_simp lits t_false) in

  (** read the first line *)
95 96
  let line = ref 0 in
  begin try
97
    let seed = input_line cin in
98 99 100 101 102
    Random.init (int_of_string seed)
  with _ ->
    Printf.eprintf "error file %s line 1\n" filename;
    exit 1
  end;
103 104
  (** Create the theory *)
  let th_uc_loc = Loc.user_position filename 1 0 0 in
105
  let th_uc = create_theory ~path (id_user "EqLin" th_uc_loc) in
106
  let th_uc = Theory.use_export th_uc th_int in
107
  (** Read one line and add it to the theory *)
108 109 110 111
  let fold th_uc s =
    let nvar,m,k =
      try
        incr line;
112 113 114 115
        (** 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
116
    with _ -> Printf.eprintf "Error file %s line %i" filename !line;exit 1 in
117
    let loc = Loc.user_position filename (!line+1) 0 (String.length s) in
118
    let goal_id = Decl.create_prsymbol
119
      (Ident.id_user (Printf.sprintf "goal%i" !line) loc) in
120 121 122
    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
123
  (** Read all the file *)
124
  let th_uc = Sysutil.fold_channel fold th_uc cin in
125
  (** Return the map with the theory *)
126
  (), Mstr.singleton "EquLin" (close_theory th_uc)
127

128
let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel
129 130 131 132 133 134
  ~desc:"@[<hov>Generate@ random@ linear@ arithmetic@ problems.@ \
    The@ first@ line@ gives@ the@ seed.@ Each@ other@ line@ \
    describes@ a@ goal@ and@ contains@ three@ numbers:@]@\n  \
    @[- @[the@ number@ of@ variables@]@\n\
      - @[the@ number@ of@ equations@]@\n\
      - @[the@ maximum@ absolute@ value@ of@ coefficients.@]@]"