]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/superposition.ml
Proved old axiom.
[helm.git] / matita / components / ng_paramodulation / superposition.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: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
13
14 module Superposition (B : Orderings.Blob) = 
15   struct
16     module IDX = Index.Index(B)
17     module Unif = FoUnif.Founif(B)
18     module Subst = FoSubst 
19     module Order = B
20     module Utils = FoUtils.Utils(B)
21     module Pp = Pp.Pp(B)
22     
23     exception Success of 
24       B.t Terms.bag 
25       * int 
26       * B.t Terms.unit_clause
27       * B.t Terms.substitution
28
29     let print s = prerr_endline (Lazy.force s);; 
30     let debug _ = ();; 
31     let enable = true;;
32
33     let rec list_first f = function
34       | [] -> None
35       | x::tl -> match f x with Some _ as x -> x | _ -> list_first f tl
36     ;;
37
38     let first_position pos ctx t f =
39       let inject_pos pos ctx = function
40         | None -> None
41         | Some (a,b,c,d) -> Some(ctx a,b,c,d,pos)
42       in
43       let rec aux pos ctx = function
44       | Terms.Leaf _ as t -> inject_pos pos ctx (f t)
45       | Terms.Var _ -> None
46       | Terms.Node l as t->
47           match f t with
48           | Some _ as x -> inject_pos pos ctx x
49           | None ->
50               let rec first pre post = function
51                 | [] -> None
52                 | t :: tl -> 
53                      let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
54                      match aux (List.length pre :: pos) newctx t with
55                      | Some _ as x -> x
56                      | None -> 
57                          if post = [] then None (* tl is also empty *)
58                          else first (pre @ [t]) (List.tl post) tl
59               in
60                 first [] (List.tl l) l 
61       in
62         aux pos ctx t
63     ;;
64                                      
65     let all_positions pos ctx t f =
66       let rec aux pos ctx = function
67       | Terms.Leaf _ as t -> f t pos ctx 
68       | Terms.Var _ -> []
69       | Terms.Node l as t-> 
70           let acc, _, _ = 
71             List.fold_left
72             (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
73                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
74                 let acc = aux (List.length pre :: pos) newctx t @ acc in
75                 if post = [] then acc, l, []
76                 else acc, pre @ [t], List.tl post)
77              (f t pos ctx, [], List.tl l) l
78           in
79            acc
80       in
81         aux pos ctx t
82     ;;
83
84     let parallel_positions bag pos ctx id t f =
85       let rec aux bag pos ctx id = function
86       | Terms.Leaf _ as t -> f bag t pos ctx id
87       | Terms.Var _ as t -> bag,t,id
88       | Terms.Node (hd::l) as t->
89           let bag,t,id1 = f bag t pos ctx id in
90             if id = id1 then
91               let bag, l, _, id = 
92                 List.fold_left
93                   (fun (bag,pre,post,id) t ->
94                      let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
95                      let newpos = (List.length pre)::pos in
96                      let bag,newt,id = aux bag newpos newctx id t in
97                        if post = [] then bag, pre@[newt], [], id
98                        else bag, pre @ [newt], List.tl post, id)
99                   (bag, [hd], List.tl l, id) l
100               in
101                 bag, Terms.Node l, id
102             else bag,t,id1 
103             (* else aux bag pos ctx id1 t *) 
104       | _ -> assert false
105       in
106         aux bag pos ctx id t
107     ;;
108
109     let visit bag pos ctx id t f =
110       let rec aux bag pos ctx id subst = function
111       | Terms.Leaf _ as t -> 
112           let  bag,subst,t,id = f bag t pos ctx id in
113            assert (subst=[]); bag,t,id
114       | Terms.Var i as t ->  
115           let t= Subst.apply_subst subst t in
116             bag,t,id
117       | Terms.Node (hd::l) ->
118           let bag, l, _, id = 
119             List.fold_left
120               (fun (bag,pre,post,id) t ->
121                  let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
122                  let newpos = (List.length pre)::pos in
123                  let bag,newt,id = aux bag newpos newctx id subst t in
124                    if post = [] then bag, pre@[newt], [], id
125                    else bag, pre @ [newt], List.tl post, id)
126               (bag, [hd], List.map (Subst.apply_subst subst) (List.tl l), id) l
127           in
128           let bag,subst,t,id1 = f bag (Terms.Node l) pos ctx id
129           in
130             if id1 = id then (assert (subst=[]); bag,t,id)
131             else aux bag pos ctx id1 subst t
132       | _ -> assert false
133       in
134         aux bag pos ctx id [] t
135     ;;
136     
137     let build_clause bag filter rule t subst id id2 pos dir =
138       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
139       let t = Subst.apply_subst subst t in
140       if filter subst then
141         let literal = 
142           match t with
143           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
144                let o = Order.compare_terms l r in
145                (* CSC: to avoid equations of the form ? -> T that
146                   can always be applied and that lead to type-checking errors *)
147                (match l,r,o with 
148 (*
149                    (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,Terms.Gt
150                  | _,(Terms.Var _ | Terms.Node (Terms.Var _ ::_)),Terms.Lt -> assert false
151 *)
152                  | (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),_,(Terms.Incomparable | Terms.Invertible) ->
153                     Terms.Equation (l, r, ty, Terms.Lt)
154                  | _, (Terms.Var _ | Terms.Node (Terms.Var _ ::_)),(Terms.Incomparable | Terms.Invertible) ->
155                     Terms.Equation (l, r, ty, Terms.Gt)
156                  | _ -> Terms.Equation (l, r, ty, o))
157           | t -> Terms.Predicate t
158         in
159         let bag, uc = 
160           Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
161         in
162         Some (bag, uc)
163       else
164         ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
165     ;;
166     let prof_build_clause = HExtlib.profile ~enable "build_clause";;
167     let build_clause bag filter rule t subst id id2 pos x =
168       prof_build_clause.HExtlib.profile (build_clause bag filter rule t subst id id2 pos) x
169     ;;
170       
171     
172     (* ============ simplification ================= *)
173     let prof_demod_u = HExtlib.profile ~enable "demod.unify";;
174     let prof_demod_r = HExtlib.profile ~enable "demod.retrieve_generalizations";;
175     let prof_demod_o = HExtlib.profile ~enable "demod.compare_terms";;
176     let prof_demod_s = HExtlib.profile ~enable "demod.apply_subst";;
177
178     let demod table varlist subterm =
179       let cands = 
180         prof_demod_r.HExtlib.profile 
181          (IDX.DT.retrieve_generalizations table) subterm 
182       in
183       list_first
184         (fun (dir, (id,lit,vl,_)) ->
185            match lit with
186            | Terms.Predicate _ -> assert false
187            | Terms.Equation (l,r,_,o) ->
188                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
189                try 
190                  let subst =
191                    prof_demod_u.HExtlib.profile 
192                      (Unif.unification (* (varlist@vl) *) varlist subterm) side 
193                  in 
194                  let side = 
195                    prof_demod_s.HExtlib.profile 
196                      (Subst.apply_subst subst) side 
197                  in
198                  let newside = 
199                    prof_demod_s.HExtlib.profile 
200                      (Subst.apply_subst subst) newside 
201                  in
202                  if o = Terms.Incomparable || o = Terms.Invertible then
203                    let o = 
204                      prof_demod_o.HExtlib.profile 
205                       (Order.compare_terms newside) side in
206                    (* Riazanov, pp. 45 (ii) *)
207                    if o = Terms.Lt then
208                      Some (newside, subst, id, dir)
209                    else 
210                      ((*prerr_endline ("Filtering: " ^ 
211                         Pp.pp_foterm side ^ " =(< || =)" ^ 
212                         Pp.pp_foterm newside ^ " coming from " ^ 
213                         Pp.pp_unit_clause uc );*)None)
214                  else
215                    Some (newside, subst, id, dir)
216                with FoUnif.UnificationFailure _ -> None)
217         (IDX.ClauseSet.elements cands)
218     ;;
219     let prof_demod = HExtlib.profile ~enable "demod";;
220     let demod table varlist x =
221       prof_demod.HExtlib.profile (demod table varlist) x
222     ;;
223
224     let mydemod table varlist subterm = 
225       let cands = 
226         prof_demod_r.HExtlib.profile 
227          (IDX.DT.retrieve_generalizations table) subterm 
228       in
229       list_first
230         (fun (dir, ((id,lit,vl,_) as c)) ->
231            debug (lazy("candidate: " 
232                        ^ Pp.pp_unit_clause c)); 
233            match lit with
234            | Terms.Predicate _ -> assert false
235            | Terms.Equation (l,r,_,o) ->
236                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
237                try 
238                  let subst =
239                    prof_demod_u.HExtlib.profile 
240                      (Unif.unification (* (varlist@vl) *) varlist subterm) side 
241                  in 
242                  let iside = 
243                    prof_demod_s.HExtlib.profile 
244                      (Subst.apply_subst subst) side 
245                  in
246                  let inewside = 
247                    prof_demod_s.HExtlib.profile 
248                      (Subst.apply_subst subst) newside 
249                  in
250                  if o = Terms.Incomparable || o = Terms.Invertible then
251                    let o = 
252                      prof_demod_o.HExtlib.profile 
253                       (Order.compare_terms inewside) iside in
254                    (* Riazanov, pp. 45 (ii) *)
255                    if o = Terms.Lt then
256                      Some (newside, subst, id, dir)
257                    else 
258                      ((*prerr_endline ("Filtering: " ^ 
259                         Pp.pp_foterm side ^ " =(< || =)" ^ 
260                         Pp.pp_foterm newside ^ " coming from " ^ 
261                         Pp.pp_unit_clause uc );*)
262                        debug (lazy "not applied");None)
263                  else
264                    Some (newside, subst, id, dir)
265                with FoUnif.UnificationFailure _ -> 
266                  debug (lazy "not applied"); None)
267         (IDX.ClauseSet.elements cands)
268     ;;
269
270     let ctx_demod table vl bag t pos ctx id =
271       match mydemod table vl t with
272         | None -> (bag,[],t,id)
273         | Some (newside, subst, id2, dir) ->
274             let inewside = Subst.apply_subst subst newside in
275             match build_clause bag (fun _ -> true)
276               Terms.Demodulation (ctx inewside) subst id id2 pos dir
277             with
278               | None -> assert false
279               | Some (bag,(id,_,_,_)) ->
280                     (bag,subst,newside,id)
281     ;;
282       
283     let rec demodulate bag (id, literal, vl, pr) table =
284       debug (lazy ("demodulate " ^ (string_of_int id)));
285        match literal with
286       | Terms.Predicate t -> (* assert false *)
287           let bag,_,id1 =
288             visit bag [] (fun x -> x) id t (ctx_demod table vl)
289           in          
290           let cl,_,_ = Terms.get_from_bag id1 bag in
291             bag,cl
292       | Terms.Equation (l,r,ty,_) ->
293           let bag,l,id1 = 
294             visit bag [2]
295             (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) id l
296             (ctx_demod table vl)
297           in 
298           let bag,_,id2 = 
299             visit bag [3]
300               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) id1 r
301               (ctx_demod table vl)
302           in 
303           let cl,_,_ = Terms.get_from_bag id2 bag in
304             bag,cl
305     ;;
306       
307     let parallel_demod table vl bag t pos ctx id =
308       match demod table vl t with
309         | None -> (bag,t,id)
310         | Some (newside, subst, id2, dir) ->
311             match build_clause bag (fun _ -> true)
312               Terms.Demodulation (ctx newside) subst id id2 pos dir
313             with
314               | None -> assert false
315               | Some (bag,(id,_,_,_)) ->
316                     (bag,newside,id)
317     ;;
318
319     let are_alpha_eq cl1 cl2 =
320       let get_term (_,lit,_,_) =
321         match lit with
322           | Terms.Predicate _ -> assert false
323           | Terms.Equation (l,r,ty,_) ->
324               Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
325       in
326         try ignore(Unif.alpha_eq (get_term cl1) (get_term cl2)) ; true
327         with FoUnif.UnificationFailure _ -> false
328     ;;
329
330     let prof_demodulate = HExtlib.profile ~enable "demodulate";;
331     let demodulate bag clause x =
332       prof_demodulate.HExtlib.profile (demodulate bag clause) x
333     ;;
334
335     (* move away *)
336     let is_identity_clause = function
337       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
338       | _, Terms.Equation (_,_,_,_), _, _ -> false
339       | _, Terms.Predicate _, _, _ -> assert false          
340     ;;
341
342     let is_identity_goal = function
343       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
344       | _, Terms.Equation (l,r,_,_), vl, proof ->
345           (try Some (Unif.unification (* vl *) [] l r)
346            with FoUnif.UnificationFailure _ -> None)
347       | _, Terms.Predicate _, _, _ -> assert false          
348     ;;
349
350     let build_new_clause_reloc bag maxvar filter rule t subst id id2 pos dir =
351       let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
352       (Subst.apply_subst subst t)) subst in
353       match build_clause bag filter rule t subst id id2 pos dir with
354       | Some (bag, c) -> Some ((bag, maxvar), c), subst
355       | None -> None,subst
356     ;;
357
358     let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
359       fst (build_new_clause_reloc bag maxvar filter rule t 
360              subst id id2 pos dir)
361     ;;
362
363     let prof_build_new_clause = HExtlib.profile ~enable "build_new_clause";;
364     let build_new_clause bag maxvar filter rule t subst id id2 pos x =
365       prof_build_new_clause.HExtlib.profile (build_new_clause bag maxvar filter
366       rule t subst id id2 pos) x
367     ;;
368
369     let fold_build_new_clause bag maxvar id rule filter res =
370       let (bag, maxvar), res =
371        HExtlib.filter_map_acc 
372          (fun (bag, maxvar) (t,subst,id2,pos,dir) ->
373             build_new_clause bag maxvar filter rule t subst id id2 pos dir)
374          (bag, maxvar) res
375       in
376        bag, maxvar, res
377     ;;
378     
379     (* rewrite_eq check if in table there an equation matching l=r; 
380        used in subsumption and deep_eq. In deep_eq, we need to match 
381        several times times w.r.t. the same table, hence we should refresh 
382        the retrieved clauses, to avoid clashes of variables *)
383
384     let rewrite_eq ~refresh ~unify maxvar l r ty vl table =
385       let retrieve = if unify then IDX.DT.retrieve_unifiables
386       else IDX.DT.retrieve_generalizations in
387       let lcands = retrieve table l in
388       let rcands = retrieve table r in
389       let f b c =
390         let id, dir, l, r, vl = 
391           match c with
392             | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
393             |_ -> assert false 
394         in 
395         let reverse = (dir = Terms.Left2Right) = b in
396         let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
397         else r,l, Terms.Right2Left in
398           (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
399       in
400       let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
401       let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
402       let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
403       let locked_vars = if unify then [] else vl in
404       let rec aux = function
405         | [] -> None
406         | (id2,dir,c,vl1)::tl ->
407             try
408               let c,maxvar = if refresh then
409                 let maxvar,_,r = Utils.relocate maxvar vl1 [] in
410                 Subst.apply_subst r c,maxvar
411                 else c,maxvar in 
412               let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
413               Some (id2, dir, subst, maxvar)
414             with FoUnif.UnificationFailure _ -> aux tl
415       in
416         aux (cands1 @ cands2)
417     ;;
418
419     let is_subsumed ~unify bag maxvar (id, lit, vl, _) table =
420       match lit with
421       | Terms.Predicate _ -> assert false
422       | Terms.Equation (l,r,ty,_) -> 
423           match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with
424             | None -> None
425             | Some (id2, dir, subst, maxvar) ->
426                 let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
427                   build_new_clause bag maxvar (fun _ -> true)
428                   Terms.Superposition id_t subst id id2 [2] dir 
429     ;;
430     let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";;
431     let is_subsumed ~unify bag maxvar c x =
432       prof_is_subsumed.HExtlib.profile (is_subsumed ~unify bag maxvar c) x
433     ;;
434     (* id refers to a clause proving contextl l = contextr r *)
435
436     let rec deep_eq ~unify l r ty pos contextl contextr table acc =
437       (* let _ = prerr_endline ("pos = " ^ String.concat "," 
438             (List.map string_of_int pos)) in *)
439       match acc with 
440       | None -> None
441       | Some(bag,maxvar,(id,lit,vl,p),subst) -> 
442           (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
443           (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *)
444           (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *)
445           let l = Subst.apply_subst subst l in 
446           let r = Subst.apply_subst subst r in 
447           (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *)
448           (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *)
449             try 
450               let subst1 = Unif.unification (* vl *) [] l r in
451               let lit = 
452                 match lit with Terms.Predicate _ -> assert false
453                   | Terms.Equation (l,r,ty,o) -> 
454                     let l = Subst.apply_subst subst1 l in 
455                     let r = Subst.apply_subst subst1 r in 
456                      Terms.Equation (l, r, ty, o)
457               in
458                 Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst)
459             with FoUnif.UnificationFailure _ -> 
460               match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with
461               | Some (id2, dir, subst1, maxvar) ->
462                   (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
463                     prerr_endline ("old subst = "^Pp.pp_substitution subst); *)
464                   let newsubst = Subst.concat subst1 subst in
465                   let id_t = 
466                     FoSubst.apply_subst newsubst
467                       (Terms.Node[Terms.Leaf B.eqP;ty;contextl r;contextr r]) 
468                   in
469                   (match 
470                       build_new_clause_reloc bag maxvar (fun _ -> true)
471                         Terms.Superposition id_t 
472                         subst1 id id2 (pos@[2]) dir  
473                    with
474                     | Some ((bag, maxvar), c), r ->
475                      (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *)
476                      (* prerr_endline ("r = "^Pp.pp_substitution r); *)
477                         let newsubst = Subst.flat 
478                           (Subst.concat r subst) in
479                         Some(bag,maxvar,c,newsubst)
480                     | None, _ -> assert false)
481               | None ->
482                   match l,r with 
483                   | Terms.Node (a::la), Terms.Node (b::lb) when 
484                       a = b && List.length la = List.length lb ->
485                       let acc,_,_,_ =
486                         List.fold_left2 
487                           (fun (acc,pre,postl,postr) a b -> 
488                              let newcl = 
489                               fun x -> contextl(Terms.Node (pre@(x::postl))) in
490                              let newcr = 
491                               fun x -> contextr(Terms.Node (pre@(x::postr))) in
492                              let newpos = List.length pre::pos in
493                              let footail l =
494                                if l = [] then [] else List.tl l in
495                                (deep_eq ~unify a b ty 
496                                  newpos newcl newcr table acc,pre@[b],
497                                  footail postl, footail postr))
498                           (acc,[a],List.tl la,List.tl lb) la lb
499                       in acc
500                   | _,_ -> None
501     ;;
502
503     let prof_deep_eq = HExtlib.profile ~enable "deep_eq";;
504     let deep_eq ~unify l r ty pos contextl contextr table x =
505       prof_deep_eq.HExtlib.profile (deep_eq ~unify l r ty pos contextl contextr table) x
506     ;;
507
508     let rec orphan_murder bag acc i =
509       match Terms.get_from_bag i bag with
510         | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc)
511         | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc)
512         | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ ->
513             if (List.mem i acc) then (false,acc)
514             else match orphan_murder bag acc i1 with
515               | (true,acc) -> (true,acc)
516               | (false,acc) ->
517                   let (res,acc) = orphan_murder bag acc i2 in
518                   if res then res,acc else res,i::acc
519     ;;
520
521     let orphan_murder bag actives cl =
522       let (id,_,_,_) = cl in
523       let actives = List.map (fun (i,_,_,_) -> i) actives in
524       let (res,_) = orphan_murder bag actives id in
525         if res then debug (lazy "Orphan murdered"); res
526     ;;
527     let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";;
528     let orphan_murder bag actives x =
529       prof_orphan_murder.HExtlib.profile (orphan_murder bag actives) x
530     ;;
531
532     (* demodulate and check for subsumption *)
533     let simplify table maxvar bag clause =
534       debug (lazy "simplify...");
535       if is_identity_clause clause then bag,None
536       (* else if orphan_murder bag actives clause then bag,None *)
537       else let bag, clause = demodulate bag clause table in
538       if is_identity_clause clause then bag,None
539       else
540         match is_subsumed ~unify:false bag maxvar clause table with
541           | None -> bag, Some clause
542           | Some _ -> bag, None
543     ;;
544
545     let simplify table maxvar bag clause =
546       match simplify table maxvar bag clause with
547         | bag, None ->
548             let (id,_,_,_) = clause in
549             let (_,_,iter) = Terms.get_from_bag id bag in
550             Terms.replace_in_bag (clause,true,iter) bag, None
551         | bag, Some clause -> bag, Some clause
552     (*let (id,_,_,_) = clause in
553             if orphan_murder bag clause then
554               Terms.M.add id (clause,true) bag, Some clause
555             else bag, Some clause*)
556     ;;
557     let prof_simplify = HExtlib.profile ~enable "simplify";;
558     let simplify table maxvar bag x =
559       prof_simplify.HExtlib.profile (simplify table maxvar bag ) x
560     ;;
561
562     let one_pass_simplification new_clause (alist,atable) bag maxvar =
563       match simplify atable maxvar bag new_clause with
564         | bag,None -> bag,None (* new_clause has been discarded *)
565         | bag,(Some clause) ->
566             let ctable = IDX.index_unit_clause IDX.DT.empty clause in
567             let bag, alist, atable = 
568               List.fold_left 
569                 (fun (bag, alist, atable) c ->
570                    match simplify ctable maxvar bag c with
571                      |bag,None -> (bag,alist,atable)
572                         (* an active clause as been discarded *)
573                      |bag,Some c1 ->
574                         bag, c :: alist, IDX.index_unit_clause atable c)
575                 (bag,[],IDX.DT.empty) alist
576             in
577               bag, Some (clause, (alist,atable))
578     ;;
579     let prof_one_pass_simplification = HExtlib.profile ~enable "one_pass_simplification";;
580     let one_pass_simplification new_clause t bag x =
581       prof_one_pass_simplification.HExtlib.profile (one_pass_simplification new_clause t bag ) x
582     ;;
583
584     let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
585       let atable1 =
586         if new_cl then atable else
587         IDX.index_unit_clause atable cl
588       in
589         (* Simplification of new_clause with :      *
590          * - actives and cl if new_clause is not cl *
591          * - only actives otherwise                 *)
592         match
593           simplify atable1 maxvar bag new_clause with
594           | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
595           | bag,Some clause ->
596               (* Simplification of each active clause with clause *
597                * which is the simplified form of new_clause       *)
598               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
599               let bag, newa, alist, atable = 
600                 List.fold_left 
601                   (fun (bag, newa, alist, atable) c ->
602                      match simplify ctable maxvar bag c with
603                        |bag,None -> (bag, newa, alist, atable)
604                           (* an active clause as been discarded *)
605                        |bag,Some c1 ->
606                             if (c1 == c) then 
607                               bag, newa, c :: alist,
608                             IDX.index_unit_clause atable c
609                             else
610                               bag, c1 :: newa, alist, atable)                  
611                   (bag,[],[],IDX.DT.empty) alist
612               in
613                 if new_cl then
614                   bag, (Some cl, Some (clause, (alist,atable), newa))
615                 else
616                   (* if new_clause is not cl, we simplify cl with clause *)
617                   match simplify ctable maxvar bag cl with
618                     | bag,None ->
619                         (* cl has been discarded *)
620                         bag,(None, Some (clause, (alist,atable), newa))
621                     | bag,Some cl1 ->
622                         bag,(Some cl1, Some (clause, (alist,atable), newa))
623     ;;
624     let prof_simplification_step = HExtlib.profile ~enable "simplification_step";;
625     let simplification_step ~new_cl cl (alist,atable) bag maxvar x =
626       prof_simplification_step.HExtlib.profile (simplification_step ~new_cl cl (alist,atable) bag maxvar) x
627     ;;
628
629     let keep_simplified cl (alist,atable) bag maxvar =
630       let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
631         if new_cl then
632           match simplification_step ~new_cl cl (alist,atable) bag maxvar cl with
633             | _,(None, _) -> assert false
634             | bag,(Some _, None) -> bag,None
635             | bag,(Some _, Some (clause, (alist,atable), newa)) ->
636                 keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
637                   bag (newa@newc)
638         else
639           match newc with
640             | [] -> bag, Some (cl, (alist,atable))
641             | hd::tl ->
642                 match simplification_step ~new_cl cl
643                   (alist,atable) bag maxvar hd with
644                   | _,(None,None) -> assert false
645                   | bag,(Some _,None) ->
646                       keep_simplified_aux ~new_cl cl (alist,atable) bag tl
647                   | bag,(None, Some _) -> bag,None
648                   | bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
649                       let alist,atable =
650                      (clause::alist, IDX.index_unit_clause atable clause)
651                       in
652                         keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
653                           bag (newa@tl)
654       in
655         keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
656     ;;
657     let prof_keep_simplified = HExtlib.profile ~enable "keep_simplified";;
658     let keep_simplified cl t bag x =
659       prof_keep_simplified.HExtlib.profile (keep_simplified cl t bag) x
660     ;;
661
662     (* this is like simplify but raises Success *)
663     let simplify_goal ~no_demod maxvar table bag g_actives clause = 
664       let bag, clause = 
665         if no_demod then bag, clause else demodulate bag clause table 
666       in
667       let _ = debug(lazy ("demodulated goal  : " 
668                              ^ Pp.pp_unit_clause clause))
669       in
670       if List.exists (are_alpha_eq clause) g_actives then None
671       else match (is_identity_goal clause) with
672         | Some subst -> raise (Success (bag,maxvar,clause,subst))
673         | None ->
674         let (id,lit,vl,_) = clause in 
675         (* this optimization makes sense only if we demodulated, since in 
676            that case the clause should have been turned into an identity *)
677         if (vl = [] && not(no_demod)) 
678         then Some (bag,clause)
679         else
680          let l,r,ty = 
681            match lit with
682              | Terms.Equation(l,r,ty,_) -> l,r,ty
683              | _ -> assert false 
684          in
685          match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) 
686            table (Some(bag,maxvar,clause,Subst.id_subst)) with
687          | None -> Some (bag,clause)
688          | Some (bag,maxvar,cl,subst) -> 
689              debug (lazy "Goal subsumed");
690              debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst));
691              raise (Success (bag,maxvar,cl,subst))
692 (*
693         match is_subsumed ~unify:true bag maxvar clause table with
694         | None -> Some (bag, clause)
695         | Some ((bag,maxvar),c) -> 
696             debug (lazy "Goal subsumed");
697             raise (Success (bag,maxvar,c))
698 *)
699     ;;
700
701     let prof_simplify_goal = HExtlib.profile ~enable "simplify_goal";;
702     let  simplify_goal ~no_demod maxvar table bag g_actives x =
703       prof_simplify_goal.HExtlib.profile ( simplify_goal ~no_demod maxvar table bag g_actives) x
704     ;;
705
706     (* =================== inference ===================== *)
707
708     (* this is OK for both the sup_left and sup_right inference steps *)
709     let superposition table varlist subterm pos context =
710       let cands = IDX.DT.retrieve_unifiables table subterm in
711       HExtlib.filter_map
712         (fun (dir, (id,lit,vl,_ (*as uc*))) ->
713            match lit with
714            | Terms.Predicate _ -> assert false
715            | Terms.Equation (l,r,_,o) ->
716                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
717                try 
718                  let subst = 
719                    Unif.unification (* (varlist@vl)*)  [] subterm side 
720                  in 
721                  if o = Terms.Incomparable || o = Terms.Invertible then
722                    let side = Subst.apply_subst subst side in
723                    let newside = Subst.apply_subst subst newside in
724                    let o = Order.compare_terms side newside in
725                    (* XXX: check Riazanov p. 33 (iii) *)
726                    if o <> Terms.Lt && o <> Terms.Eq then  
727                      Some (context newside, subst, id, pos, dir)
728                    else 
729                      ((*prerr_endline ("Filtering: " ^ 
730                         Pp.pp_foterm side ^ " =(< || =)" ^ 
731                         Pp.pp_foterm newside);*)None)
732                  else
733                    Some (context newside, subst, id, pos, dir)
734                with FoUnif.UnificationFailure _ -> None)
735         (IDX.ClauseSet.elements cands)
736     ;;
737
738     (* Superposes selected equation with equalities in table *)
739     let superposition_with_table bag maxvar (id,selected,vl,_) table =
740       match selected with 
741       | Terms.Predicate _ -> assert false
742       | Terms.Equation (l,r,ty,Terms.Lt) ->
743           fold_build_new_clause bag maxvar id Terms.Superposition
744             (fun _ -> true)
745             (all_positions [3] 
746               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
747               r (superposition table vl))
748       | Terms.Equation (l,r,ty,Terms.Invertible)
749       | Terms.Equation (l,r,ty,Terms.Gt) ->
750           fold_build_new_clause bag maxvar id Terms.Superposition
751             (fun _ -> true)
752             (all_positions [2] 
753               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
754               l (superposition table vl))
755       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
756           let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
757             let l = Subst.apply_subst subst l in
758             let r = Subst.apply_subst subst r in
759             let o = Order.compare_terms l r in
760             o <> avoid && o <> Terms.Eq
761           in
762           let bag, maxvar,r_terms =
763             fold_build_new_clause bag maxvar id Terms.Superposition
764               (filtering Terms.Gt)
765               (all_positions [3] 
766                  (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
767                  r (superposition table vl))
768           in
769           let bag, maxvar, l_terms =
770             fold_build_new_clause bag maxvar id Terms.Superposition
771               (filtering Terms.Lt)
772               (all_positions [2] 
773                  (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
774                  l (superposition table vl))
775           in
776             bag, maxvar, r_terms @ l_terms
777       | _ -> assert false
778     ;;
779
780     (* the current equation is normal w.r.t. demodulation with atable
781      * (and is not the identity) *)
782     let infer_right bag maxvar current (alist,atable) = 
783       (* We demodulate actives clause with current until all *
784        * active clauses are reduced w.r.t each other         *)
785       (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
786       let ctable = IDX.index_unit_clause IDX.DT.empty current in
787       (* let bag, (alist, atable) = 
788         let bag, alist = 
789           HExtlib.filter_map_acc (simplify ctable) bag alist
790         in
791         bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
792       in*)
793         debug (lazy "Simplified active clauses with fact");
794       (* We superpose active clauses with current *)
795       let bag, maxvar, new_clauses =
796         List.fold_left 
797           (fun (bag, maxvar, acc) active ->
798              let bag, maxvar, newc = 
799                superposition_with_table bag maxvar active ctable 
800              in
801              bag, maxvar, newc @ acc)
802           (bag, maxvar, []) alist
803       in
804         debug
805         (lazy 
806          ("New clauses :" ^ (String.concat ";\n" 
807             (List.map Pp.pp_unit_clause new_clauses)))); 
808         debug (lazy "First superpositions");
809         (* We add current to active clauses so that it can be *
810          * superposed with itself                             *)
811       let alist, atable = 
812         current :: alist, IDX.index_unit_clause atable current
813       in
814         debug (lazy "Indexed");
815       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
816         (* We need to put fresh_current into the bag so that all *
817          * variables clauses refer to are known.                 *)
818       let bag, fresh_current = Terms.add_to_bag fresh_current bag in
819         (* We superpose current with active clauses *)
820       let bag, maxvar, additional_new_clauses =
821         superposition_with_table bag maxvar fresh_current atable 
822       in
823         debug (lazy "Another superposition");
824       let new_clauses = new_clauses @ additional_new_clauses in
825         (* debug (lazy (Printf.sprintf "Demodulating %d clauses"
826                  (List.length new_clauses))); *)
827       let bag, new_clauses = 
828         HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
829       in
830         debug (lazy "Demodulated new clauses");
831       bag, maxvar, (alist, atable), new_clauses
832     ;;
833
834     let prof_ir = HExtlib.profile ~enable "infer_right";;
835     let infer_right bag maxvar current t = 
836       prof_ir.HExtlib.profile (infer_right bag maxvar current) t
837     ;;
838
839     let infer_left bag maxvar goal (_alist, atable) =
840         (* We superpose the goal with active clauses *)
841      if (match goal with (_,_,[],_) -> true | _ -> false) then bag, maxvar, []
842      else
843       let bag, maxvar, new_goals =        
844         superposition_with_table bag maxvar goal atable 
845       in
846         debug(lazy  "Superposed goal with active clauses");
847         (* We simplify the new goals with active clauses *)
848       let bag, new_goals = 
849         List.fold_left
850          (fun (bag, acc) g -> 
851             match simplify_goal ~no_demod:false maxvar atable bag [] g with
852               | None -> assert false
853               | Some (bag,g) -> bag,g::acc)
854          (bag, []) new_goals
855       in
856         debug (lazy "Simplified new goals with active clauses");
857       bag, maxvar, List.rev new_goals
858     ;;
859
860     let prof_il = HExtlib.profile ~enable "infer_left";;
861     let infer_left bag maxvar goal t = 
862       prof_il.HExtlib.profile (infer_left bag maxvar goal) t
863     ;;
864
865   end