genequlin.ml 5.18 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3 4 5 6 7
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

21 22 23 24
(*
*)


25
open Why3
26 27
open Format

28 29
(**************)
(*
30

31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
  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
53

54
*)
55 56 57 58 59 60 61

open Theory
open Term
open Util

open Ident

62 63 64 65 66 67 68 69
(** 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)))

70

71
(** the main function *)
72
let read_channel env path filename cin =
73
  (** Find the int theory and the needed operation *)
Andrei Paskevich's avatar
Andrei Paskevich committed
74
  let th_int = Env.find_theory (Env.env_of_library env) ["int"] "Int" in
75 76 77 78
  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

79
  let zero = t_int_const "0" in
80

81
  (** create a contraint : polynome <= constant *)
82 83 84
  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
85
      let monome = t_app mult_symbol [e;t_int_const const]
86 87
        (Some Ty.ty_int) in
      t_app plus_symbol [acc;monome] (Some Ty.ty_int)) zero lvar in
88
    let rconst = string_of_int ((Random.int k) - (k/2)) in
89
    t_and_simp lits (t_app leq [left;t_int_const rconst] None) in
90

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

Andrei Paskevich's avatar
Andrei Paskevich committed
133
let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel
134 135 136 137 138 139
  ~desc:"@[Generate rendomly linear arithmetic problems:@\n  \
  @[The first line give the seed to use. Each other lines corresond to one goal@\n  \
    @[- @[the first number give the number of variables@]@\n\
      - @[the second the number of equation@]@\n\
      - @[the third the absolute maximun of the constants used@]\
@]"