]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_paramodulation/paramod.ml
update in delayed_updating
[helm.git] / matitaB / components / ng_paramodulation / paramod.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.      
9      \ /   This software is distributed as is, NO WARRANTY.     
10       V_______________________________________________________________ *)
11
12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
13
14 let print s = prerr_endline (Lazy.force s) ;; 
15 let noprint s = ();;  
16 let debug = noprint;;
17
18 let monster = 100;;
19     
20 module type Paramod =
21   sig
22     type t
23     type input
24     type szsontology = 
25       | Unsatisfiable of 
26           (t Terms.bag * int * t Terms.substitution * int list) list
27       | GaveUp 
28       | Error of string 
29       | Timeout of int * t Terms.bag
30     type bag = t Terms.bag * int
31     type state
32     val empty_state : state
33     val size_of_state : state -> int*int
34     val bag_of_state : state -> bag
35     val replace_bag: state -> bag -> state
36     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
37     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
38     val forward_infer_step : 
39       state ->
40       t Terms.unit_clause ->
41       int ->
42       state
43     val goal_narrowing : 
44       int 
45       -> int
46       -> float option
47       -> state
48       -> state
49     val paramod :
50       useage:bool ->
51       max_steps:int ->
52       ?timeout:float ->
53       bag -> 
54       g_passives:t Terms.unit_clause list -> 
55       passives:t Terms.unit_clause list -> szsontology
56     val demod :
57       state -> input* input -> szsontology
58     val fast_eq_check :
59       state -> input* input -> szsontology
60     val nparamod :
61       useage:bool ->
62       max_steps:int ->
63       ?timeout:float ->
64       state -> input* input -> szsontology
65   end
66
67 module Paramod (B : Orderings.Blob) = struct
68   module Pp = Pp.Pp (B) 
69   module FU = FoUnif.Founif(B) 
70   module IDX = Index.Index(B) 
71   module Sup = Superposition.Superposition(B) 
72   module Utils = FoUtils.Utils(B) 
73   module Order = B
74   module WeightOrderedPassives =
75       struct
76         type t = B.t Terms.passive_clause
77         let compare = Utils.compare_passive_clauses_weight
78       end
79
80   module AgeOrderedPassives =
81       struct
82         type t = B.t Terms.passive_clause
83         let compare = Utils.compare_passive_clauses_age
84       end
85   
86   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
87   module AgePassiveSet = Set.Make(AgeOrderedPassives)
88
89   type t = B.t
90   type input = B.input
91   type bag = B.t Terms.bag * int 
92   type szsontology = 
93     | Unsatisfiable of 
94         (B.t Terms.bag * int * B.t Terms.substitution * int list) list
95     | GaveUp 
96     | Error of string 
97     | Timeout of int * B.t Terms.bag
98   exception Stop of szsontology
99   type state = 
100       t Terms.bag 
101       * int
102       * Index.Index(B).active_set 
103       * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t) 
104       * B.t Terms.unit_clause list 
105       * (WeightPassiveSet.t * AgePassiveSet.t)
106
107   let empty_state = 
108     Terms.empty_bag,
109     0,
110     ([],IDX.DT.empty),
111     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty),
112     [],
113     (WeightPassiveSet.empty,AgePassiveSet.empty)
114   ;;
115
116   let bag_of_state (bag,n,_,_,_,_) = bag,n
117   ;;
118   
119   let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d
120   ;;
121
122   let add_passive_clause ?(no_weight=false)
123       (passive_t,passives_w,passives_a) cl =
124     let pcl = if no_weight then (0,cl)
125     else Utils.mk_passive_clause cl in
126     IDX.index_unit_clause passive_t cl,
127     WeightPassiveSet.add pcl passives_w, 
128     AgePassiveSet.add pcl passives_a
129   ;;
130
131   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
132     let g = if no_weight then (0,g)
133     else Utils.mk_passive_goal g in
134     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
135   ;;
136
137   let remove_passive_clause (passive_t,passives_w,passives_a) cl =
138     let passive_t = IDX.remove_unit_clause passive_t (snd cl) in
139     let passives_w = WeightPassiveSet.remove cl passives_w in
140     let passives_a = AgePassiveSet.remove cl passives_a in
141       passive_t,passives_w,passives_a
142   ;;
143
144   let add_passive_clauses ?(no_weight=false) =
145     List.fold_left (add_passive_clause ~no_weight)
146   ;;
147
148   let add_passive_goals ?(no_weight=false)
149       (passives_w,passives_a) new_clauses =
150     let new_clauses_w,new_clauses_a =
151       List.fold_left (add_passive_goal ~no_weight)
152       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
153     in
154       (WeightPassiveSet.union new_clauses_w passives_w,
155        AgePassiveSet.union new_clauses_a passives_a)
156   ;;
157
158   let remove_passive_goal (passives_w,passives_a) cl =
159     let passives_w = WeightPassiveSet.remove cl passives_w in
160     let passives_a = AgePassiveSet.remove cl passives_a in
161       passives_w,passives_a
162   ;;
163
164   let is_passive_set_empty (_,passives_w,passives_a) =
165     if (WeightPassiveSet.is_empty passives_w) then begin
166       assert (AgePassiveSet.is_empty passives_a); true
167     end else begin
168       assert (not (AgePassiveSet.is_empty passives_a)); false
169     end
170   ;;
171
172   let is_passive_g_set_empty (passives_w,passives_a) =
173     if (WeightPassiveSet.is_empty passives_w) then begin
174       assert (AgePassiveSet.is_empty passives_a); true
175     end else begin
176       assert (not (AgePassiveSet.is_empty passives_a)); false
177     end
178   ;;
179
180   let passive_set_cardinal (_,passives_w,_) 
181       = WeightPassiveSet.cardinal passives_w
182   ;;
183
184   let g_passive_set_cardinal (passives_w,_) 
185       = WeightPassiveSet.cardinal passives_w
186   ;;
187
188   let passive_empty_set =
189     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty)
190   ;;
191
192   let g_passive_empty_set =
193     (WeightPassiveSet.empty,AgePassiveSet.empty)
194   ;;
195
196   let pick_min_passive ~use_age (_,passives_w,passives_a) =
197     if use_age then AgePassiveSet.min_elt passives_a
198     else WeightPassiveSet.min_elt passives_w
199   ;;
200
201   let pick_min_g_passive ~use_age (passives_w,passives_a) =
202     if use_age then AgePassiveSet.min_elt passives_a
203     else WeightPassiveSet.min_elt passives_w
204   ;;
205
206   let mk_unit_clause bag maxvar (t,ty) =
207     let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
208     let bag, c = Terms.add_to_bag c bag in
209     (bag, maxvar), c
210   ;;
211
212 (*
213   let mk_clause bag maxvar (proof,ty) =
214     let (proof,ty) = B.saturate t ty in 
215     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
216     let bag, c = Terms.add_to_bag c bag in
217     (bag, maxvar), c
218   ;; *)
219   
220   let mk_passive (bag,maxvar) = mk_unit_clause bag maxvar;;
221
222   let mk_goal (bag,maxvar) = mk_unit_clause bag maxvar;;
223
224   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
225     let (bag,maxvar), g = mk_unit_clause bag maxvar t in
226     let g_passives = g_passive_empty_set in
227     (* if the goal is not an equation we return an empty
228        passive set *)
229     let g_passives =
230       if Terms.is_eq_clause g then add_passive_goal g_passives g
231       else g_passives 
232     in
233       (bag,maxvar,actives,passives,[],g_passives)
234
235
236   (* TODO : global age over facts and goals (without comparing weights) *)
237   let select ~use_age passives g_passives =
238     if is_passive_set_empty passives then begin
239       if (is_passive_g_set_empty g_passives) then
240         raise (Stop GaveUp) (* we say we are incomplete *)
241       else
242        let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
243         (true,g_cl,passives,remove_passive_goal g_passives g_cl)
244     end
245     else let cl = pick_min_passive ~use_age:use_age passives in
246       if is_passive_g_set_empty g_passives then
247         (false,cl,remove_passive_clause passives cl,g_passives)
248       else
249         let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
250         let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
251         let cmp = if use_age then id1 <= id2
252         else fst cl <= fst g_cl
253         in
254           if cmp then
255             (false,cl,remove_passive_clause passives cl,g_passives)
256           else
257             (true,g_cl,passives,remove_passive_goal g_passives g_cl)
258   ;;
259
260   let backward_infer_step bag maxvar actives passives
261                           g_actives g_passives g_current iterno =
262     (* superposition left, simplifications on goals *)
263       debug (lazy "infer_left step...");
264       let bag, maxvar, new_goals = 
265         Sup.infer_left bag maxvar g_current actives 
266       in
267         debug (lazy "Performed infer_left step");
268         let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
269           bag, maxvar, actives, passives, g_current::g_actives,
270     (add_passive_goals g_passives new_goals)
271   ;;
272
273   let pp_clauses actives passives =
274     let actives_l, _ = actives in
275     let passive_t,_,_ = passives in
276     let wset = IDX.elems passive_t in
277       ("Actives :" ^ (String.concat ";\n" 
278         (List.map Pp.pp_unit_clause actives_l)))
279       ^ 
280       ("Passives:" ^(String.concat ";\n" 
281         (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
282                (IDX.ClauseSet.elements wset))))
283   ;;
284
285   let forward_infer_step 
286       ((bag,maxvar,actives,passives,g_actives,g_passives) as s)  
287       current iterno =
288     (* forward step *)
289     
290     (* e = select P           *
291      * e' = demod A e         *
292      * A' = demod [e'] A      *
293      * A'' = A' + e'          *
294      * e'' = fresh e'         *
295      * new = supright e'' A'' *
296      * new'= demod A'' new    *
297      * P' = P + new'          *)
298     debug (lazy "Forward infer step...");
299     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
300     noprint (lazy (pp_clauses actives passives));
301     match Sup.keep_simplified current actives bag maxvar
302     with
303       | _,None -> s
304       | bag,Some (current,actives) ->
305     debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
306     let bag, maxvar, actives, new_clauses = 
307       Sup.infer_right bag maxvar current actives 
308     in
309       debug
310         (lazy 
311          ("New clauses :" ^ (String.concat ";\n" 
312             (List.map Pp.pp_unit_clause new_clauses)))); 
313       debug (lazy "Demodulating goals with actives...");
314       (* keep goals demodulated w.r.t. actives and check if solved *)
315       let bag, g_actives = 
316         List.fold_left 
317           (fun (bag,acc) c -> 
318              match 
319                Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
320              with
321                | None -> bag, acc
322                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
323           (bag,[]) g_actives 
324       in
325       let ctable = IDX.index_unit_clause IDX.DT.empty current in
326       let bag, maxvar, new_goals = 
327         List.fold_left 
328           (fun (bag,m,acc) g -> 
329              let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
330                bag,m,ng@acc) 
331           (bag,maxvar,[]) g_actives 
332       in
333       let bag = Terms.replace_in_bag (current,false,iterno) bag in
334         (* prerr_endline (Pp.pp_bag bag); *)
335     bag, maxvar, actives,
336     add_passive_clauses passives new_clauses, g_actives,
337     add_passive_goals g_passives new_goals
338   ;;
339
340   let size_of_state (_,_,(a,_),p,_,_) = List.length a, passive_set_cardinal p;;
341
342   let debug_status (_,_,actives,passives,g_actives,g_passives) =
343     lazy
344       ((Printf.sprintf "Number of active goals : %d\n"
345           (List.length g_actives)) ^
346        (Printf.sprintf "Number of passive goals : %d\n"
347           (g_passive_set_cardinal g_passives)) ^
348        (Printf.sprintf "Number of actives : %d\n" 
349           (List.length (fst actives))) ^
350        (Printf.sprintf "Number of passives : %d\n"
351          (passive_set_cardinal passives)))
352   ;;
353
354
355   (* we just check if any of the active goals is subsumed by a
356      passive clause, or if any of the passive goal is subsumed
357      by an active or passive clause *) 
358   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
359     debug (lazy("Last chance " ^ string_of_float
360                   (Unix.gettimeofday())));
361     let actives_l, active_t = actives in
362     let passive_t,wset,_ = passives in
363     let _ = noprint
364       (lazy 
365          ("Actives :" ^ (String.concat ";\n" 
366             (List.map Pp.pp_unit_clause actives_l)))) in 
367     let wset = IDX.elems passive_t in
368     let _ = noprint
369       (lazy 
370          ("Passives:" ^(String.concat ";\n" 
371             (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
372                (IDX.ClauseSet.elements wset))))) in 
373     let g_passives = 
374       WeightPassiveSet.fold 
375         (fun (_,x) acc ->
376           if List.exists (Sup.are_alpha_eq x) g_actives then acc
377           else x::acc)
378           (fst g_passives) []
379     in 
380       ignore
381       (List.iter
382         (fun x -> 
383             ignore 
384              (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
385                Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
386        g_passives); 
387       ignore
388       (List.iter
389          (fun x -> 
390             ignore 
391               (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
392         Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
393         (g_actives@g_passives)); 
394     raise (Stop (Timeout (maxvar,bag)))
395
396   let check_timeout = function
397     | None -> false
398     | Some timeout -> Unix.gettimeofday () > timeout
399  
400   let rec given_clause ~useage
401     bag maxvar iterno weight_picks max_steps timeout 
402     actives passives g_actives g_passives 
403   =
404     let iterno = iterno + 1 in
405     if iterno = max_steps || check_timeout timeout then
406       last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
407     else 
408     let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
409     let weight_picks = if use_age then 0 else weight_picks+1
410     in
411
412     let rec aux_select bag 
413         (passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
414         g_passives =
415       let backward,(weight,current),passives,g_passives =
416         select ~use_age passives g_passives
417       in
418         if use_age && weight > monster then
419           let bag,cl = Terms.add_to_bag current bag in
420             if backward then
421               aux_select bag passives (add_passive_goal g_passives cl)
422             else
423               aux_select bag (add_passive_clause passives cl) g_passives
424         else
425           let bag = Terms.replace_in_bag (current,false,iterno) bag in
426         if backward then
427           let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
428          match 
429            Sup.simplify_goal 
430              ~no_demod:false maxvar (snd actives) bag g_actives current 
431          with
432            | None -> aux_select bag passives g_passives
433            | Some (bag,g_current) ->
434                backward_infer_step bag maxvar actives passives
435                  g_actives g_passives g_current iterno
436         else
437           let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current)) 
438           in
439             if Sup.orphan_murder bag (fst actives) current then
440               let _ = debug (lazy "Orphan murdered") in
441               let bag = Terms.replace_in_bag (current,true,iterno) bag in
442                 aux_select bag passives g_passives
443             else
444               let s = bag,maxvar,actives,passives,g_actives,g_passives in
445               let s1 = forward_infer_step s current iterno
446               in 
447                 if s == s1 then aux_select bag passives g_passives  
448                 else s1
449     in
450       (*prerr_endline "Active table :"; 
451        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
452           (fst actives)); *)
453
454     let (bag,maxvar,actives,passives,g_actives,g_passives) as status  =      
455       aux_select bag passives g_passives
456     in
457       debug (debug_status status);       
458       given_clause ~useage
459         bag maxvar iterno weight_picks max_steps timeout 
460         actives passives g_actives g_passives
461   ;;
462
463   let check_and_infer ~no_demod iterno status current =
464     let bag,maxvar,actives,passives,g_actives,g_passives = status in
465     match 
466       Sup.simplify_goal 
467         ~no_demod maxvar (snd actives) bag g_actives current 
468     with
469       | None -> debug (lazy "None"); status
470       | Some (bag,g_current) -> 
471           let _ = 
472             debug (lazy("Infer on goal : " 
473                         ^ Pp.pp_unit_clause g_current)) 
474           in
475             backward_infer_step bag maxvar actives passives
476               g_actives g_passives g_current iterno
477
478   (* similar to given_clause, but it merely works on goals, 
479      in parallel, at each iteration *)
480   let rec goal_narrowing iterno max_steps timeout status
481   = 
482     debug (debug_status status);
483     let iterno = iterno + 1 in
484     if iterno = max_steps || check_timeout timeout then
485       last_chance status
486     else 
487     let _,_,_,_,_,g_passives = status in 
488     let passive_goals = WeightPassiveSet.elements (fst g_passives) in
489     let newstatus = 
490       List.fold_left
491         (fun acc g ->
492            let bag,maxvar,actives,passives,g_actives,g_passives = acc in
493            let g_passives =
494              remove_passive_goal g_passives g in
495            let current = snd g in
496            let _ = 
497              debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) 
498            in
499              (* we work both on the original goal and the demodulated one*)
500            let acc = check_and_infer ~no_demod:false iterno acc current
501            in check_and_infer ~no_demod:true iterno acc current)
502         status passive_goals
503     in
504       goal_narrowing iterno max_steps timeout newstatus
505
506     let compute_result bag i subst =
507       let l =
508         let rec traverse ongoal (accg,acce) i =
509           match Terms.get_from_bag i bag with
510             | (id,_,_,Terms.Exact _),_,_ ->
511                 if ongoal then [i],acce else
512                   if (List.mem i acce) then accg,acce else accg,acce@[i]
513             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
514                 if (not ongoal) && (List.mem i acce) then accg,acce
515                 else
516                   let accg,acce = 
517                     traverse false (traverse ongoal (accg,acce) i1) i2
518                   in
519                     if ongoal then i::accg,acce else accg,i::acce
520         in
521         let gsteps,esteps = traverse true ([],[]) i in
522           (List.rev esteps)@gsteps
523       in
524       debug (lazy ("steps: " ^ (string_of_int (List.length l))));
525       let max_w = 
526         List.fold_left 
527           (fun acc i ->
528              let (cl,_,_) = Terms.get_from_bag i bag in
529                max acc (Order.compute_unit_clause_weight cl)) 0 l in
530         debug (lazy ("Max weight : " ^ (string_of_int max_w)));
531 (*        List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
532             Terms.get_from_bag id bag in
533               if d then
534                 prerr_endline
535                 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
536                    id it (Order.compute_unit_clause_weight cl) 
537                    (Pp.pp_proof_step proof))
538               else
539                prerr_endline
540                 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
541                    id it (Order.compute_unit_clause_weight cl) 
542                    (Pp.pp_proof_step proof))) l;*)
543         debug (lazy ("Proof:" ^
544           (String.concat "\n" 
545              (List.map 
546                 (fun x ->
547                    let cl,_,_ = Terms.get_from_bag x bag in
548                      Pp.pp_unit_clause cl) l))));
549         Unsatisfiable [ bag, i, subst, l ]
550
551   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
552     let _initial_timestamp = Unix.gettimeofday () in
553     let passives =
554       add_passive_clauses ~no_weight:true passive_empty_set passives
555     in
556     let g_passives =
557       add_passive_goals ~no_weight:true g_passive_empty_set g_passives
558     in
559     let g_actives = [] in
560     let actives = [], IDX.DT.empty in
561     try 
562      given_clause ~useage ~noinfer:false
563       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
564     with 
565     | Sup.Success (bag, _, (i,_,_,_),subst) ->
566         compute_result bag i subst
567     | Stop (Unsatisfiable _) -> Error "solution found!"
568     | Stop o -> o
569   ;;
570
571 let demod s goal =
572   let bag,maxvar,actives,passives,g_actives,g_passives = s in
573   let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
574   let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
575     if g1 = g then GaveUp else compute_result bag i []
576 (*
577   if Terms.is_eq_clause g then 
578
579   else GaveUp *)
580
581 let fast_eq_check s goal =
582   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
583   if is_passive_g_set_empty g_passives then Error "not an equation"
584   else
585   try 
586     goal_narrowing 0 2 None s
587   with
588     | Sup.Success (bag, _, (i,_,_,_),subst) ->
589         compute_result bag i subst
590     | Stop (Unsatisfiable _) -> Error "solution found!"
591     | Stop o -> o
592   ;;
593
594 let nparamod ~useage ~max_steps ?timeout s goal =
595   let bag,maxvar,actives,passives,g_actives,g_passives
596       = initialize_goal s goal in
597   if is_passive_g_set_empty g_passives then Error "not an equation" 
598   else
599     try given_clause ~useage ~noinfer:false
600       bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
601   with
602     | Sup.Success (bag, _, (i,_,_,_),subst) ->
603         compute_result bag i subst
604     | Stop (Unsatisfiable _) -> Error "solution found!"
605     | Stop o -> o
606   ;;
607
608 end