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