genequlin.ml 4.78 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 19
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

20 21 22 23
(*
*)


24
open Why3
25 26
open Format

27 28
(**************)
(*
29

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

53
*)
54 55 56 57 58 59 60

open Theory
open Term
open Util

open Ident

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

69

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

78
  let zero = t_int_const "0" in
79

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
132
let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel