hypothesis_selection.ml 21.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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
(*s Transformation which removes most hypothesis, only keeping the one
21
22
23
24
25
26
27
28
29
30
a graph-based heuristic finds close enough to the goal *)

open Util
open Ident
open Ty
open Term
open Decl
open Task

(* requires ocamlgraph. TODO : recode this inside *)
31
32
33
34
35
36
37
38
open Graph.Persistent

module Int_Dft = struct
  type t = int
  let compare = Pervasives.compare
  let default = max_int
end

39
module GP = Digraph.ConcreteLabeled(
40
  struct
41
42
43
44
    type t = Term.lsymbol
    let compare x y = compare x.ls_name.id_tag y.ls_name.id_tag
    let hash x = x.ls_name.id_tag
    let equal x y = x.ls_name.id_tag = y.ls_name.id_tag
45
  end)(Int_Dft)
46
47
48
49
50
51
52
53
54
55
56
57
58
module ExprNode = struct
    type t = Term.expr
    let compare x y = match x,y with
      | Term t1, Term t2 -> compare t1.t_tag t2.t_tag
      | Fmla f1, Fmla f2 -> compare f1.f_tag f2.f_tag
      | Term _, Fmla _ -> -1
      | Fmla _, Term _ -> 1
    let hash x = match x with
      | Term t -> t.t_tag
      | Fmla f -> f.f_tag
    let equal x y = compare x y == 0
end
module GC = Graph.Concrete(ExprNode)
59
60
61
62
63
module SymbHashtbl =
  Hashtbl.Make(struct type t = Term.lsymbol
		      let equal x y = x.ls_name.id_tag = y.ls_name.id_tag
		      let hash x = x.ls_name.id_tag
	       end)
64
65
66
67
68
module FmlaHashtbl =
  Hashtbl.Make(struct type t = Term.fmla
		      let equal x y = x.f_tag = y.f_tag
		      let hash x = x.f_tag
	       end)
69
70
71
72
73
module TermHashtbl =
  Hashtbl.Make(struct type t = Term.term
		      let equal x y = x.t_tag = y.t_tag
		      let hash x = x.t_tag
	       end)
74
module Sls = Set.Make(GP.V)
75
module Sexpr = Set.Make(ExprNode)
76
77

let err = Format.err_formatter
78
79

module Util = struct
80
  let print_clause fmt = Format.fprintf fmt "@[[%a]@]"
81
    (Pp.print_list Pp.comma Pretty.print_fmla)
82
83
  let print_clauses fmt = Format.fprintf fmt "[%a]@."
    (Pp.print_list Pp.comma print_clause)
84

85
  (** all combinaisons of elements of left and right *)
86
87
88
89
  let map_complete combinator left right =
    let explorer left_elt =
      List.map (fun right_elt -> combinator left_elt right_elt) right in
    List.flatten (List.map explorer left)
90
91
92
93
94
95
96
97
98
99
100
101
102
103

(** all combinaisons of elements of left and right, folded *)
  let fold_complete combinator acc left right =
    let explorer acc left_elt =
      List.fold_left
	(fun acc right_elt -> combinator acc left_elt right_elt)
	acc right in
    List.fold_left explorer acc left

  (** given two lists of sets of expr, returns the list made from their union *)
  let rec merge_list l1 l2 = match l1,l2 with
    | x::xs,y::ys -> (Sexpr.union x y) :: merge_list xs ys
    | _,[] -> l1
    | [],_ -> l2
104
end
105

106
107

(** module used to reduce formulae to Normal Form *)
108
module NF = struct (* add memoization, one day ? *)
109
  (* TODO ! *)
110
111
  (** all quantifiers in prenex form *)
  let prenex_fmla fmla =
112
    Format.fprintf err "prenex_fmla : @[%a@]@." Pretty.print_fmla fmla;
113
114
    fmla

115
116
117
118
119
120
121
122
  (** creates a fresh formula representing a quantified formula *)
  let create_fmla (vars:Term.vsymbol list) : Term.fmla =
    let pred = create_psymbol (id_fresh "temoin")
      (List.map (fun var -> var.vs_ty) vars) in
    f_app pred (List.map t_var vars)


  (** transforms a formulae into its Normal Form as a list of clauses.
123
124
      The first argument is a hastable from formulae to formulae.
      A clause is a list of formulae *)
125
126
127
  let rec transform fmlaTable fmla =
    Format.fprintf err "transform : @[%a@]@." Pretty.print_fmla fmla;
    match fmla.f_node with
128
129
130
    | Fquant (_,f_bound) ->
	let var,_,f =  f_open_quant f_bound in
	traverse fmlaTable fmla var f
131
132
    | Fbinop (_,_,_) ->
	let clauses = split fmla in
133
	Format.fprintf err "split : @[%a@]@." Util.print_clause clauses;
134
135
136
137
138
139
140
141
142
143
	begin match clauses with
	  | [f] -> begin match f.f_node with
	      | Fbinop (For,f1,f2) ->
		  let left = transform fmlaTable f1 in
		  let right = transform fmlaTable f2 in
		  Util.map_complete List.append left right
	      | _ -> [[f]]
	    end
	  | _ -> List.concat (List.map (transform fmlaTable) clauses)
	end
144
    | Fnot f -> handle_not fmlaTable fmla f
145
146
    | Fapp (_,_) -> [[fmla]]
    | Ftrue | Ffalse -> [[fmla]]
147
148
149
150
151
    | Fif (_,_,_) -> failwith "if formulae not handled"
    | Flet (_,_) -> failwith "let formulae not handled"
    | Fcase (_,_) -> failwith "case formulae not handled"
  and traverse fmlaTable old_fmla vars fmla = match fmla.f_node with
    | Fquant (_,f_bound) ->
152
	let var,_,f = f_open_quant f_bound in
153
	traverse fmlaTable old_fmla (var@vars) f
154
    | _ ->
155
156
157
	if FmlaHashtbl.mem fmlaTable fmla then
	  [[FmlaHashtbl.find fmlaTable fmla]]
	else
158
	  let new_fmla = create_fmla vars in
159
	  FmlaHashtbl.add fmlaTable old_fmla new_fmla;
160
	  FmlaHashtbl.add fmlaTable new_fmla new_fmla;
161
162
163
	  [[new_fmla]]
  and skipPrenex fmlaTable fmla = match fmla.f_node with
    | Fquant (_,f_bound) ->
164
	let _,_,f = f_open_quant f_bound in
165
166
167
	skipPrenex fmlaTable f
    | _ -> transform fmlaTable fmla
  and split f = match f.f_node with
168
169
170
    | Fbinop (Fimplies,{f_node = Fbinop (For, h1, h2)},f2) ->
	(split (f_binary Fimplies h1 f2)) @ (split (f_binary Fimplies h2 f2))
    | Fbinop (Fimplies,f1,f2) ->
171
172
173
174
	let clauses = split f2 in
	if List.length clauses >= 2 then
	  List.concat
	    (List.map (fun f -> split (f_binary Fimplies f1 f)) clauses)
175
176
	else split (f_or (f_not f1) f2)
    | Fbinop (Fand,f1,f2) -> [f1; f2]
177
    | _ -> [f]
178
179
180
181
  and handle_not fmlaTable old_f f = match f.f_node with
    | Fquant (Fforall,f_bound) ->
	let vars,triggers,f1 = f_open_quant f_bound in
	transform fmlaTable (f_exists vars triggers (f_not f1))
182
183
184
185
186
187
188
189
190
    | Fnot f1 -> transform fmlaTable f1
    | Fbinop (Fand,f1,f2) ->
	transform fmlaTable (f_or (f_not f1) (f_not f2))
    | Fbinop (For,f1,f2) ->
	transform fmlaTable (f_and (f_not f1) (f_not f2))
    | Fbinop (Fimplies,f1,f2) ->
	transform fmlaTable (f_and f1 (f_not f2))
    | Fbinop (Fiff,f1,f2) ->
	transform fmlaTable (f_or (f_and f1 (f_not f2)) (f_and (f_not f1) f2))
191
    | _ -> [[old_f]] (* default case *)
192

193
194
195
196
197
  let make_clauses fmlaTable prop =
    let prenex_fmla = prenex_fmla prop in
    let clauses = skipPrenex fmlaTable prenex_fmla in
    Format.eprintf "==>@ @[%a@]@.@." Util.print_clauses clauses;
    clauses
198
199
200
201
202
end


(** module used to compute the graph of constants *)
module GraphConstant = struct
203
204
  (** memoizing for formulae and terms, and then expressions *)
  let rec findF fTbl fmla = try
205
206
    FmlaHashtbl.find fTbl fmla
  with Not_found ->
207
    let new_v = GC.V.create (Fmla fmla) in
208
209
210
211
    FmlaHashtbl.add fTbl fmla new_v;
    (* Format.eprintf "generating new vertex : %a@."
      Pretty.print_fmla fmla; *)
    new_v
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
  and findT tTbl term = try
    TermHashtbl.find tTbl term
  with Not_found ->
    let new_v = GC.V.create (Term term) in
    TermHashtbl.add tTbl term new_v;
    (* Format.eprintf "generating new vertex : %a@."
      Pretty.print_fmla fmla; *)
    new_v
  and find fTbl tTbl expr = match expr with
    | Term t -> findT tTbl t
    | Fmla f -> findF fTbl f

  let add_symbol fTbl tTbl gc expr =
    GC.add_vertex gc (find fTbl tTbl expr)

  (** analyse dynamic dependencies in one atomic formula, from the bottom *)
  let rec analyse_fmla_base fTbl tTbl gc fmla =
    let gc,_ = analyse_fmla fTbl tTbl (gc,[]) fmla in gc
  and analyse_fmla fTbl tTbl (gc,vertices) fmla = match fmla.f_node with
    | Fapp (_,terms) ->
	let gc,sub_vertices =
	  List.fold_left (analyse_term fTbl tTbl) (gc,[]) terms in
	(* make a clique with [sub_vertices] elements *)
	let gc = Util.fold_complete GC.add_edge gc sub_vertices sub_vertices in
	let pred_vertex = findF fTbl fmla in
	(* add edges between [pred_vertex] and [sub_vertices] *)
	let gc = List.fold_left
	  (fun gc term_vertex -> GC.add_edge gc pred_vertex term_vertex)
	  gc sub_vertices in
	(gc, pred_vertex :: vertices)
    | _ -> f_fold (analyse_term fTbl tTbl) (analyse_fmla fTbl tTbl)
	(gc,vertices) fmla
  and analyse_term fTbl tTbl (gc,vertices) term = match term.t_node with
    | Tvar _ | Tconst _ ->
	let vertex = findT tTbl term in
	(gc,vertex::vertices)
    | Tapp (_,terms) ->
	let gc,sub_vertices =
	  List.fold_left (analyse_term fTbl tTbl) (gc,[]) terms in
	(* make a clique with [sub_vertices] elements *)
	let gc = Util.fold_complete GC.add_edge gc sub_vertices sub_vertices in
	let func_vertex = findT tTbl term in
	(* add edges between [func_vertex] and [sub_vertices] *)
	let gc = List.fold_left
	  (fun gc term_vertex -> GC.add_edge gc func_vertex term_vertex)
	  gc sub_vertices in
	(gc, func_vertex :: vertices)
    | _ -> t_fold (analyse_term fTbl tTbl) (analyse_fmla fTbl tTbl)
	(gc,vertices) term

  let analyse_clause fTbl tTbl gc clause =
    List.fold_left (analyse_fmla_base fTbl tTbl) gc clause

  let analyse_prop fmlaTable fTbl tTbl gc prop =
266
    let clauses = NF.make_clauses fmlaTable prop in
267
    List.fold_left (analyse_clause fTbl tTbl) gc clauses
268
269

      (** processes a single task_head. *)
Andrei Paskevich's avatar
Andrei Paskevich committed
270
271
272
  let update fmlaTable fTbl tTbl gc task_head = 
    match task_head.task_decl.Theory.td_node with
    | Theory.Decl {d_node = Dprop(_,_,prop_decl)} ->
273
      analyse_prop fmlaTable fTbl tTbl gc prop_decl
274
    | _ -> gc
275
276
277
end

(** module used to compute the directed graph of predicates *)
278
module GraphPredicate = struct
279
280
281
282
283
284
  exception Exit of lsymbol

  let is_negative = function
    | { f_node = Fnot _ } -> true
    | _ -> false

285
  let extract_symbol fmla =
286
287
288
    let rec search = function
      | { f_node = Fapp(p,_) } -> raise (Exit p)
      | f -> f_map (fun t->t) search f in
289
    try ignore (search fmla);
290
291
292
      Format.eprintf "invalid formula : ";
      Pretty.print_fmla Format.err_formatter fmla; assert false
    with Exit p -> p
293

294
295
296
297
298
  let find symbTbl x = try
    SymbHashtbl.find symbTbl x
  with Not_found ->
    let new_v = GP.V.create x in
    SymbHashtbl.add symbTbl x new_v;
299
    (* Format.eprintf "generating new vertex : %a@." Pretty.print_ls x; *)
300
    new_v
301

302
303
  (** analyse a single clause, and creates an edge between every positive
      litteral and every negative litteral of [clause] in [gp] graph. *)
304
305
  let analyse_clause symbTbl gp clause =
    let get_symbol x = find symbTbl (extract_symbol x) in
306
    let negative,positive = List.partition is_negative clause in
307
308
309
310
    let negative = List.map get_symbol negative in
    let positive = List.map get_symbol positive in
    let n = List.length clause in
    let add left gp right =
311
312
313
314
315
316
317
318
319
320
      try
	let old = GP.find_edge gp left right in
	if GP.E.label old <= n
	then gp (* old edge is fine *)
	else
	  let new_gp = GP.remove_edge_e gp old in
	  assert (not (GP.mem_edge new_gp left right));
	  GP.add_edge_e gp (GP.E.create left n right)
      with Not_found ->
	let e = GP.E.create left n right in
321
322
323
	GP.add_edge_e gp e in
    List.fold_left (* add an edge from every negative to any positive *)
      (fun gp left ->
324
       List.fold_left (add left) gp positive) gp negative
325
326
327
328

  (** takes a prop, puts it in Normal Form and then builds a clause
      from it *)
  let analyse_prop fmlaTable symbTbl gp prop =
329
    let clauses = NF.make_clauses fmlaTable prop in
330
331
332
333
    List.fold_left (analyse_clause symbTbl) gp clauses

  let add_symbol symbTbl gp lsymbol =
    GP.add_vertex gp (find symbTbl lsymbol)
334
335

  (** takes a constant graph and a task_head, and add any interesting
336
337
      element to the graph it returns. *)
  let update fmlaTable symbTbl gp task_head =
Andrei Paskevich's avatar
Andrei Paskevich committed
338
339
    match task_head.task_decl.Theory.td_node with
      | Theory.Decl {d_node = Dprop (_,_,prop_decl) } ->
340
341
        (* a proposition to analyse *)
        analyse_prop fmlaTable symbTbl gp prop_decl
Andrei Paskevich's avatar
Andrei Paskevich committed
342
      | Theory.Decl {d_node = Dlogic logic_decls } ->
343
344
345
346
        (* a symbol to add *)
        List.fold_left
          (fun gp logic_decl -> add_symbol symbTbl gp (fst logic_decl))
          gp logic_decls
347
      | _ -> gp
348
349
350
351
end

(** module that makes the final selection *)
module Select = struct
352
353
354
355
356
357
358
359
  let get_predicates fmla =
    let id acc _ = acc in
    let rec explore acc fmla = match fmla.f_node with
      | Fapp (pred,_) -> pred::acc
      | _ -> f_fold id explore acc fmla
    in explore [] fmla

  let get_clause_predicates acc clause =
360
361
362
    let rec fmla_get_pred ?(pos=true) acc fmla = match fmla.f_node with
      | Fnot f -> fmla_get_pred ~pos:false acc f
      | Fapp (pred,_) -> (pred, (if pos then `Positive else `Negative))::acc
363
364
365
      | _ -> failwith "bad formula in get_predicates !"
    in List.fold_left fmla_get_pred acc clause

366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
  let rec get_sub_fmlas fTbl tTbl fmla =
    let rec gather_sub_fmla fTbl tTbl acc fmla = match fmla.f_node with
      | Fapp (_,terms) ->
	  let acc = List.fold_left (gather_sub_term fTbl tTbl) acc terms in
	  GraphConstant.findF fTbl fmla :: acc
      | _ -> f_fold (gather_sub_term fTbl tTbl)
	  (gather_sub_fmla fTbl tTbl) acc fmla
    and gather_sub_term fTbl tTbl acc term = match term.t_node with
      | Tapp (_,terms) ->
	  let acc = List.fold_left (gather_sub_term fTbl tTbl) acc terms in
	  GraphConstant.findT tTbl term :: acc
      | Tconst _ | Tvar _ -> GraphConstant.findT tTbl term :: acc
      | _ -> t_fold (gather_sub_term fTbl tTbl)
	  (gather_sub_fmla fTbl tTbl) acc term in
    gather_sub_fmla fTbl tTbl [] fmla

382
383
  (** get the predecessors of [positive] in the graph [gp], at distance <= [i]*)
  let rec get_predecessors i gp acc positive =
384
    if i < 0 then acc
385
    else
386
387
388
389
390
391
392
393
394
395
396
397
398
      let acc = Sls.add positive acc in
      List.fold_left (follow_edge gp i)
	acc (GP.pred_e gp positive)
  and follow_edge ?(forward=false) gp i acc edge =
    let f = if forward then get_successors else get_predecessors in
    f (i - GP.E.label edge) gp acc
      ((if forward then GP.E.dst else GP.E.src) edge)
  and get_successors j gp acc negative =
    if j < 0 then acc
    else
      let acc = Sls.add negative acc in
      List.fold_left (follow_edge ~forward:true gp j)
	acc (GP.succ_e gp negative)
399

400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
  exception FixPoint
  exception Exit of Sexpr.t list

  (** builds the list of reachable nodes *)
  let build_relevant_variables gc goal_clause =
    let acc = Sexpr.empty in
    let l0 = List.fold_right Sexpr.add goal_clause acc in

    (** explore one more step *)
    let rec one_step cur =
      let step = Sexpr.fold explore cur [cur;cur] in
      Format.eprintf "one step made !@.";
      step

    (** explores the neighbours of [vertex] *)
    and explore vertex l = match l with [next_cur;cur] ->

      (** [changed] indicates whether a vertex has been added;
	  [v] is a vertex *)
      let find_odd v ((acc,changed) as old) =
	if Sexpr.mem v acc then old else
	  let count = GC.fold_pred
	    (fun v2 count -> if Sexpr.mem v2 acc then count+1 else count)
	    gc v 0 in (* how many predecessors in acc ? *)
	  if count >= 2 then (Sexpr.add v acc,true) else old in
      let find_even prev_step v ((acc,changed) as old) =
	if Sexpr.mem v prev_step || Sexpr.mem v acc then old else
	  if GC.fold_pred (fun v2 bool -> bool || (Sexpr.mem v2 acc))
	    gc v false (* connected to a vertex in acc ? *)
	  then (Sexpr.add v acc, true) else old in
      let next_cur_odd,has_changed = (* compute 2^n+1 elts *)
	GC.fold_succ find_odd gc vertex (cur,false) in
      let next_cur_even,has_changed = (* compute 2^n+2 elts *)
	GC.fold_succ (find_even next_cur_odd)
	  gc vertex (cur,has_changed) in
      if has_changed then [next_cur_even;next_cur_odd]
      else raise FixPoint

      | _ -> assert false (*only not to have warnings on non-exhaustive match*)

    (** iterates [one_step] until an exception is raised *)
    and control cur acc =
      let next_acc = try
	let next_step = one_step cur in
	next_step @ acc (* next step contains *2* steps *)
      with FixPoint ->
	Format.eprintf "[control] : fixpoint reached !";
	raise (Exit acc) in
      control (List.hd next_acc) next_acc in
    try
      ignore (control l0 [l0]);
      [l0] (* never returns. this is an odd step (step 1) *)
    with Exit answer ->
      List.rev answer

  (* TODO : be more clear... *)
456
  (** determines if a proposition is pertinent w.r.t the given goal formula,
457
      from data stored in the graph [gp] given.
458
459
      [i] is the parameter of predicate graph ([gp]) based filtering.
      [j] is the parameter for dynamic constants ([gc]) dependency filtering *)
460
  let is_pertinent_predicate symTbl goal_clauses ?(i=4) gp fmla =
461
462
463
464
465
466
467
468
    let is_negative = function
      | (_,`Negative) -> true
      | (_,`Positive) -> false in
    let find_secure symbTbl x =
      try SymbHashtbl.find symbTbl x
      with Not_found ->
	Format.eprintf "failure finding %a !@." Pretty.print_ls x;
	raise Not_found in
469
470
471
472
473
    let goal_predicates =
      List.fold_left get_clause_predicates [] goal_clauses in
    let predicates = get_predicates fmla in
    let negative,positive = List.partition is_negative goal_predicates in
    let negative,positive = List.map fst negative, List.map fst positive in
474
    let negative = List.map (find_secure symTbl) negative in (* to be optimized ? *)
475
476
    let positive = List.map (find_secure symTbl) positive in
    let predicates = List.map (find_secure symTbl) predicates in
477
478
    (* list of negative predecessors of any positive predicate of the goal,
       at distance <= i *)
479
    let predecessors = List.fold_left (get_predecessors i gp) Sls.empty positive in
480
    let successors = List.fold_left (get_successors i gp) Sls.empty negative in
481
482
483
    (* a predicates is accepted iff all its predicates are close enough in
       successors or predecessors lists *)
    List.for_all
484
485
486
      (fun x -> if Sls.mem x predecessors || Sls.mem x successors
       then true else begin Format.eprintf "%a not close enough (dist %d)@."
	   Pretty.print_ls (GP.V.label x) i; false end)
487
488
      predicates

489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
  (** tests whether a formula is pertinent according to the dynamic dependency criterion. *)
  let is_pertinent_dynamic fTbl tTbl goal_clauses ?(j=4) gc =
    let relevant_variables = (* ideally, there should be only one goal clause *)
      List.fold_left Util.merge_list []
	(List.map (build_relevant_variables gc) goal_clauses) in
    function fmla ->
      let rec is_close_enough x l count = match (l,count) with 
	| _,n when n < 0 -> false
	| y::_,_ when Sexpr.mem x y -> true
	| _::ys,count -> is_close_enough x ys (count-1)
	| _,_ ->
	    false (* case where the fmla is not reachable from goal vars *) in
      let is_acceptable fmla = is_close_enough fmla relevant_variables j in
      let sub_fmlas = get_sub_fmlas fTbl tTbl fmla in
      let sub_fmlas = List.map GC.V.label sub_fmlas in
      List.for_all is_acceptable sub_fmlas

506
507
  (** preprocesses the goal formula and the graph, and returns a function
      that will accept or not axioms according to their relevance. *)
508
509
510
511
512
513
514
515
516
517
518
519
520
521
  let filter fTbl tTbl symTbl goal_clauses (gc,gp) decl =
    match decl.d_node with
      | Dtype _ | Dlogic _ | Dind _ -> [decl]
      | Dprop (Paxiom,_,fmla) -> (* filter only axioms *)
	  Format.eprintf "filter : @[%a@]@." Pretty.print_fmla fmla;
	  let goal_exprs = List.map (List.map (fun x -> Fmla x)) goal_clauses in
	  let return_value =
	    if is_pertinent_predicate symTbl goal_clauses gp fmla &&
	      is_pertinent_dynamic fTbl tTbl goal_exprs gc fmla
	    then [decl] else [] in
	  if return_value = [] then Format.eprintf "NO@.@."
	  else Format.eprintf "YES@.@.";
	  return_value
      | Dprop(_,_,_) -> [decl]
522
523
end

524
525
526
(** if this is the goal, return it as Some goal after checking there is no other
    goal. Else, return the option *)
let get_goal task_head option =
Andrei Paskevich's avatar
Andrei Paskevich committed
527
528
  match task_head.task_decl.Theory.td_node with
    | Theory.Decl {d_node = Dprop(Pgoal,_,goal_fmla)} ->
529
530
531
532
	assert (option = None); (* only one goal ! *)
	Some goal_fmla
    | _ -> option

533
(** collects data on predicates and constants in task *)
534
let collect_info fmlaTable fTbl tTbl symbTbl =
535
  Trans.fold
536
    (fun t (gc, gp, goal_option) ->
537
       GraphConstant.update fmlaTable fTbl tTbl gc t,
538
539
540
       GraphPredicate.update fmlaTable symbTbl gp t,
       get_goal t goal_option)
    (GC.empty, GP.empty, None)
541
542
543

(** the transformation, made from applying collect_info and
then mapping Select.filter *)
544
let transformation fmlaTable fTbl tTbl symbTbl task =
545
546
  (* first, collect data in 2 graphes *)
  let (gc,gp,goal_option) =
547
    Trans.apply (collect_info fmlaTable fTbl tTbl symbTbl) task in
548
549
550
551
  (* get the goal *)
  let goal_fmla = match goal_option with
    | None -> failwith "no goal !"
    | Some goal_fmla -> goal_fmla in
552
  let goal_clauses = NF.make_clauses fmlaTable goal_fmla in
553
554
555
  (* filter one declaration at once *)
  Trans.apply
    (Trans.decl
556
       (Select.filter fTbl tTbl symbTbl goal_clauses (gc,gp)) None) task
557

558
559
(** the transformation to be registered *)
let hypothesis_selection =
560
  Register.store
561
    (fun () -> (* create lots of hashtables... *)
562
563
       let fmlaTable = FmlaHashtbl.create 17 in
       let fTbl = FmlaHashtbl.create 17 in
564
       let tTbl = TermHashtbl.create 17 in
565
566
       let symbTbl = SymbHashtbl.create 17 in
       Trans.store
567
	 (transformation fmlaTable fTbl tTbl symbTbl))
568
569

let _ = Register.register_transform
570
571
  "hypothesis_selection" hypothesis_selection

572
(*
573
Local Variables:
574
  compile-command: "unset LANG; make"
575
576
End:
vim:foldmethod=indent:foldnestmax=1
577
578
*)