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