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 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     (* rewrite_eq check if in table there an equation matching l=r;
 378        used in subsumption and deep_eq. In deep_eq, we need to match
 379        several times times w.r.t. the same table, hence we should refresh
 380        the retrieved clauses, to avoid clashes of variables *)
 381
 382     let rewrite_eq ~refresh ~unify maxvar l r ty vl table =
 383       let retrieve = if unify then IDX.DT.retrieve_unifiables
 384       else IDX.DT.retrieve_generalizations in
 385       let lcands = retrieve table l in
 386       let rcands = retrieve table r in
 387       let f b c =
 388         let id, dir, l, r, vl =
 389           match c with
 390             | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
 391             |_ -> assert false
 392         in
 393         let reverse = (dir = Terms.Left2Right) = b in
 394         let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
 395         else r,l, Terms.Right2Left in
 396           (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ], vl)
 397       in
 398       let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
 399       let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
 400       let t = Terms.Node [ Terms.Leaf (B.eqP()); ty; l; r ] in
 401       let locked_vars = if unify then [] else vl in
 402       let rec aux = function
 403         | [] -> None
 404         | (id2,dir,c,vl1)::tl ->
 405             try
 406               let c,maxvar = if refresh then
 407                 let maxvar,_,r = Utils.relocate maxvar vl1 [] in
 408                 Subst.apply_subst r c,maxvar
 409                 else c,maxvar in
 410               let subst = Unif.unification (* (vl@vl1) *) locked_vars c t in
 411               Some (id2, dir, subst, maxvar)
 412             with FoUnif.UnificationFailure _ -> aux tl
 413       in
 414         aux (cands1 @ cands2)
 415     ;;
 416
 417     let is_subsumed ~unify bag maxvar (id, lit, vl, _) table =
 418       match lit with
 419       | Terms.Predicate _ -> assert false
 420       | Terms.Equation (l,r,ty,_) ->
 421           match rewrite_eq ~refresh:false ~unify maxvar l r ty vl table with
 422             | None -> None
 423             | Some (id2, dir, subst, maxvar) ->
 424                 let id_t = Terms.Node [ Terms.Leaf (B.eqP()); ty; r; r ] in
 425                   build_new_clause bag maxvar (fun _ -> true)
 426                   Terms.Superposition id_t subst id id2 [2] dir
 427     ;;
 428     let prof_is_subsumed = HExtlib.profile ~enable "is_subsumed";;
 429     let is_subsumed ~unify bag maxvar c x =
 430       prof_is_subsumed.HExtlib.profile (is_subsumed ~unify bag maxvar c) x
 431     ;;
 432     (* id refers to a clause proving contextl l = contextr r *)
 433
 434     let rec deep_eq ~unify l r ty pos contextl contextr table acc =
 435       (* let _ = prerr_endline ("pos = " ^ String.concat ","
 436             (List.map string_of_int pos)) in *)
 437       match acc with
 438       | None -> None
 439       | Some(bag,maxvar,(id,lit,vl,p),subst) ->
 440           (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
 441           (* prerr_endline ("l prima =" ^ Pp.pp_foterm l); *)
 442           (* prerr_endline ("r prima =" ^ Pp.pp_foterm r); *)
 443           let l = Subst.apply_subst subst l in
 444           let r = Subst.apply_subst subst r in
 445           (* prerr_endline ("l dopo =" ^ Pp.pp_foterm l); *)
 446           (* prerr_endline ("r dopo =" ^ Pp.pp_foterm r); *)
 447             try
 448               let subst1 = Unif.unification (* vl *) [] l r in
 449               let lit =
 450                 match lit with Terms.Predicate _ -> assert false
 451                   | Terms.Equation (l,r,ty,o) ->
 452                     let l = Subst.apply_subst subst1 l in
 453                     let r = Subst.apply_subst subst1 r in
 454                      Terms.Equation (l, r, ty, o)
 455               in
 456                 Some(bag,maxvar,(id,lit,vl,p),Subst.concat subst1 subst)
 457             with FoUnif.UnificationFailure _ ->
 458               match rewrite_eq ~refresh:true ~unify maxvar l r ty vl table with
 459               | Some (id2, dir, subst1, maxvar) ->
 460                   (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
 461                     prerr_endline ("old subst = "^Pp.pp_substitution subst); *)
 462                   let newsubst = Subst.concat subst1 subst in
 463                   let id_t =
 464                     FoSubst.apply_subst newsubst
 465                       (Terms.Node[Terms.Leaf (B.eqP());ty;contextl r;contextr r])
 466                   in
 467                   (match
 468                       build_new_clause_reloc bag maxvar (fun _ -> true)
 469                         Terms.Superposition id_t
 470                         subst1 id id2 (pos@[2]) dir
 471                    with
 472                     | Some ((bag, maxvar), c), r ->
 473                      (* prerr_endline ("creo "^ Pp.pp_unit_clause c); *)
 474                      (* prerr_endline ("r = "^Pp.pp_substitution r); *)
 475                         let newsubst = Subst.flat
 476                           (Subst.concat r subst) in
 477                         Some(bag,maxvar,c,newsubst)
 478                     | None, _ -> assert false)
 479               | None ->
 480                   match l,r with
 481                   | Terms.Node (a::la), Terms.Node (b::lb) when
 482                       a = b && List.length la = List.length lb ->
 483                       let acc,_,_,_ =
 484                         List.fold_left2
 485                           (fun (acc,pre,postl,postr) a b ->
 486                              let newcl =
 487                               fun x -> contextl(Terms.Node (pre@(x::postl))) in
 488                              let newcr =
 489                               fun x -> contextr(Terms.Node (pre@(x::postr))) in
 490                              let newpos = List.length pre::pos in
 491                              let footail l =
 492                                if l = [] then [] else List.tl l in
 493                                (deep_eq ~unify a b ty
 494                                  newpos newcl newcr table acc,pre@[b],
 495                                  footail postl, footail postr))
 496                           (acc,[a],List.tl la,List.tl lb) la lb
 497                       in acc
 498                   | _,_ -> None
 499     ;;
 500
 501     let prof_deep_eq = HExtlib.profile ~enable "deep_eq";;
 502     let deep_eq ~unify l r ty pos contextl contextr table x =
 503       prof_deep_eq.HExtlib.profile (deep_eq ~unify l r ty pos contextl contextr table) x
 504     ;;
 505
 506     let rec orphan_murder bag acc i =
 507       match Terms.get_from_bag i bag with
 508         | (_,_,_,Terms.Exact _),discarded,_ -> (discarded,acc)
 509         | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true,_ -> (true,acc)
 510         | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false,_ ->
 511             if (List.mem i acc) then (false,acc)
 512             else match orphan_murder bag acc i1 with
 513               | (true,acc) -> (true,acc)
 514               | (false,acc) ->
 515                   let (res,acc) = orphan_murder bag acc i2 in
 516                   if res then res,acc else res,i::acc
 517     ;;
 518
 519     let orphan_murder bag actives cl =
 520       let (id,_,_,_) = cl in
 521       let actives = List.map (fun (i,_,_,_) -> i) actives in
 522       let (res,_) = orphan_murder bag actives id in
 523         if res then debug (lazy "Orphan murdered"); res
 524     ;;
 525     let prof_orphan_murder = HExtlib.profile ~enable "orphan_murder";;
 526     let orphan_murder bag actives x =
 527       prof_orphan_murder.HExtlib.profile (orphan_murder bag actives) x
 528     ;;
 529
 530     (* demodulate and check for subsumption *)
 531     let simplify table maxvar bag clause =
 532       debug (lazy "simplify...");
 533       if is_identity_clause clause then bag,None
 534       (* else if orphan_murder bag actives clause then bag,None *)
 535       else let bag, clause = demodulate bag clause table in
 536       if is_identity_clause clause then bag,None
 537       else
 538         match is_subsumed ~unify:false bag maxvar clause table with
 539           | None -> bag, Some clause
 540           | Some _ -> bag, None
 541     ;;
 542
 543     let simplify table maxvar bag clause =
 544       match simplify table maxvar bag clause with
 545         | bag, None ->
 546             let (id,_,_,_) = clause in
 547             let (_,_,iter) = Terms.get_from_bag id bag in
 548             Terms.replace_in_bag (clause,true,iter) bag, None
 549         | bag, Some clause -> bag, Some clause
 550     (*let (id,_,_,_) = clause in
 551             if orphan_murder bag clause then
 552               Terms.M.add id (clause,true) bag, Some clause
 553             else bag, Some clause*)
 554     ;;
 555     let prof_simplify = HExtlib.profile ~enable "simplify";;
 556     let simplify table maxvar bag x =
 557       prof_simplify.HExtlib.profile (simplify table maxvar bag ) x
 558     ;;
 559
 560     let one_pass_simplification new_clause (alist,atable) bag maxvar =
 561       match simplify atable maxvar bag new_clause with
 562         | bag,None -> bag,None (* new_clause has been discarded *)
 563         | bag,(Some clause) ->
 564             let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 565             let bag, alist, atable =
 566               List.fold_left
 567                 (fun (bag, alist, atable) c ->
 568                    match simplify ctable maxvar bag c with
 569                      |bag,None -> (bag,alist,atable)
 570                         (* an active clause as been discarded *)
 571                      |bag,Some c1 ->
 572                         bag, c :: alist, IDX.index_unit_clause atable c)
 573                 (bag,[],IDX.DT.empty) alist
 574             in
 575               bag, Some (clause, (alist,atable))
 576     ;;
 577     let prof_one_pass_simplification = HExtlib.profile ~enable "one_pass_simplification";;
 578     let one_pass_simplification new_clause t bag x =
 579       prof_one_pass_simplification.HExtlib.profile (one_pass_simplification new_clause t bag ) x
 580     ;;
 581
 582     let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
 583       let atable1 =
 584         if new_cl then atable else
 585         IDX.index_unit_clause atable cl
 586       in
 587         (* Simplification of new_clause with :      *
 588          * - actives and cl if new_clause is not cl *
 589          * - only actives otherwise                 *)
 590         match
 591           simplify atable1 maxvar bag new_clause with
 592           | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
 593           | bag,Some clause ->
 594               (* Simplification of each active clause with clause *
 595                * which is the simplified form of new_clause       *)
 596               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 597               let bag, newa, alist, atable =
 598                 List.fold_left
 599                   (fun (bag, newa, alist, atable) c ->
 600                      match simplify ctable maxvar bag c with
 601                        |bag,None -> (bag, newa, alist, atable)
 602                           (* an active clause as been discarded *)
 603                        |bag,Some c1 ->
 604                             if (c1 == c) then
 605                               bag, newa, c :: alist,
 606                             IDX.index_unit_clause atable c
 607                             else
 608                               bag, c1 :: newa, alist, atable)
 609                   (bag,[],[],IDX.DT.empty) alist
 610               in
 611                 if new_cl then
 612                   bag, (Some cl, Some (clause, (alist,atable), newa))
 613                 else
 614                   (* if new_clause is not cl, we simplify cl with clause *)
 615                   match simplify ctable maxvar bag cl with
 616                     | bag,None ->
 617                         (* cl has been discarded *)
 618                         bag,(None, Some (clause, (alist,atable), newa))
 619                     | bag,Some cl1 ->
 620                         bag,(Some cl1, Some (clause, (alist,atable), newa))
 621     ;;
 622     let prof_simplification_step = HExtlib.profile ~enable "simplification_step";;
 623     let simplification_step ~new_cl cl (alist,atable) bag maxvar x =
 624       prof_simplification_step.HExtlib.profile (simplification_step ~new_cl cl (alist,atable) bag maxvar) x
 625     ;;
 626
 627     let keep_simplified cl (alist,atable) bag maxvar =
 628       let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
 629         if new_cl then
 630           match simplification_step ~new_cl cl (alist,atable) bag maxvar cl with
 631             | _,(None, _) -> assert false
 632             | bag,(Some _, None) -> bag,None
 633             | bag,(Some _, Some (clause, (alist,atable), newa)) ->
 634                 keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
 635                   bag (newa@newc)
 636         else
 637           match newc with
 638             | [] -> bag, Some (cl, (alist,atable))
 639             | hd::tl ->
 640                 match simplification_step ~new_cl cl
 641                   (alist,atable) bag maxvar hd with
 642                   | _,(None,None) -> assert false
 643                   | bag,(Some _,None) ->
 644                       keep_simplified_aux ~new_cl cl (alist,atable) bag tl
 645                   | bag,(None, Some _) -> bag,None
 646                   | bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
 647                       let alist,atable =
 648                      (clause::alist, IDX.index_unit_clause atable clause)
 649                       in
 650                         keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
 651                           bag (newa@tl)
 652       in
 653         keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
 654     ;;
 655     let prof_keep_simplified = HExtlib.profile ~enable "keep_simplified";;
 656     let keep_simplified cl t bag x =
 657       prof_keep_simplified.HExtlib.profile (keep_simplified cl t bag) x
 658     ;;
 659
 660     (* this is like simplify but raises Success *)
 661     let simplify_goal ~no_demod maxvar table bag g_actives clause =
 662       let bag, clause =
 663         if no_demod then bag, clause else demodulate bag clause table
 664       in
 665       let _ = debug(lazy ("demodulated goal  : "
 666                              ^ Pp.pp_unit_clause clause))
 667       in
 668       if List.exists (are_alpha_eq clause) g_actives then None
 669       else match (is_identity_goal clause) with
 670         | Some subst -> raise (Success (bag,maxvar,clause,subst))
 671         | None ->
 672         let (id,lit,vl,_) = clause in
 673         (* this optimization makes sense only if we demodulated, since in
 674            that case the clause should have been turned into an identity *)
 675         if (vl = [] && not(no_demod))
 676         then Some (bag,clause)
 677         else
 678          let l,r,ty =
 679            match lit with
 680              | Terms.Equation(l,r,ty,_) -> l,r,ty
 681              | _ -> assert false
 682          in
 683          match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x)
 684            table (Some(bag,maxvar,clause,Subst.id_subst)) with
 685          | None -> Some (bag,clause)
 686          | Some (bag,maxvar,cl,subst) ->
 687              debug (lazy "Goal subsumed");
 688              debug (lazy ("subst in superpos: " ^ Pp.pp_substitution subst));
 689              raise (Success (bag,maxvar,cl,subst))
 690 (*
 691         match is_subsumed ~unify:true bag maxvar clause table with
 692         | None -> Some (bag, clause)
 693         | Some ((bag,maxvar),c) ->
 694             debug (lazy "Goal subsumed");
 695             raise (Success (bag,maxvar,c))
 696 *)
 697     ;;
 698
 699     let prof_simplify_goal = HExtlib.profile ~enable "simplify_goal";;
 700     let  simplify_goal ~no_demod maxvar table bag g_actives x =
 701       prof_simplify_goal.HExtlib.profile ( simplify_goal ~no_demod maxvar table bag g_actives) x
 702     ;;
 703
 704     (* =================== inference ===================== *)
 705
 706     (* this is OK for both the sup_left and sup_right inference steps *)
 707     let superposition table varlist subterm pos context =
 708       let cands = IDX.DT.retrieve_unifiables table subterm in
 709       HExtlib.filter_map
 710         (fun (dir, (id,lit,vl,_ (*as uc*))) ->
 711            match lit with
 712            | Terms.Predicate _ -> assert false
 713            | Terms.Equation (l,r,_,o) ->
 714                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
 715                try
 716                  let subst =
 717                    Unif.unification (* (varlist@vl)*)  [] subterm side
 718                  in
 719                  if o = Terms.Incomparable || o = Terms.Invertible then
 720                    let side = Subst.apply_subst subst side in
 721                    let newside = Subst.apply_subst subst newside in
 722                    let o = Order.compare_terms side newside in
 723                    (* XXX: check Riazanov p. 33 (iii) *)
 724                    if o <> Terms.Lt && o <> Terms.Eq then
 725                      Some (context newside, subst, id, pos, dir)
 726                    else
 727                      ((*prerr_endline ("Filtering: " ^
 728                         Pp.pp_foterm side ^ " =(< || =)" ^
 729                         Pp.pp_foterm newside);*)None)
 730                  else
 731                    Some (context newside, subst, id, pos, dir)
 732                with FoUnif.UnificationFailure _ -> None)
 733         (IDX.ClauseSet.elements cands)
 734     ;;
 735
 736     (* Superposes selected equation with equalities in table *)
 737     let superposition_with_table bag maxvar (id,selected,vl,_) table =
 738       match selected with
 739       | Terms.Predicate _ -> assert false
 740       | Terms.Equation (l,r,ty,Terms.Lt) ->
 741           fold_build_new_clause bag maxvar id Terms.Superposition
 742             (fun _ -> true)
 743             (all_positions [3]
 744               (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
 745               r (superposition table vl))
 746       | Terms.Equation (l,r,ty,Terms.Invertible)
 747       | Terms.Equation (l,r,ty,Terms.Gt) ->
 748           fold_build_new_clause bag maxvar id Terms.Superposition
 749             (fun _ -> true)
 750             (all_positions [2]
 751               (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
 752               l (superposition table vl))
 753       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
 754           let filtering avoid subst = (* Riazanov: p.33 condition (iv) *)
 755             let l = Subst.apply_subst subst l in
 756             let r = Subst.apply_subst subst r in
 757             let o = Order.compare_terms l r in
 758             o <> avoid && o <> Terms.Eq
 759           in
 760           let bag, maxvar,r_terms =
 761             fold_build_new_clause bag maxvar id Terms.Superposition
 762               (filtering Terms.Gt)
 763               (all_positions [3]
 764                  (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; l; x ])
 765                  r (superposition table vl))
 766           in
 767           let bag, maxvar, l_terms =
 768             fold_build_new_clause bag maxvar id Terms.Superposition
 769               (filtering Terms.Lt)
 770               (all_positions [2]
 771                  (fun x -> Terms.Node [ Terms.Leaf (B.eqP()); ty; x; r ])
 772                  l (superposition table vl))
 773           in
 774             bag, maxvar, r_terms @ l_terms
 775       | _ -> assert false
 776     ;;
 777
 778     (* the current equation is normal w.r.t. demodulation with atable
 779      * (and is not the identity) *)
 780     let infer_right bag maxvar current (alist,atable) =
 781       (* We demodulate actives clause with current until all *
 782        * active clauses are reduced w.r.t each other         *)
 783       (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
 784       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 785       (* let bag, (alist, atable) =
 786         let bag, alist =
 787           HExtlib.filter_map_acc (simplify ctable) bag alist
 788         in
 789         bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
 790       in*)
 791         debug (lazy "Simplified active clauses with fact");
 792       (* We superpose active clauses with current *)
 793       let bag, maxvar, new_clauses =
 794         List.fold_left
 795           (fun (bag, maxvar, acc) active ->
 796              let bag, maxvar, newc =
 797                superposition_with_table bag maxvar active ctable
 798              in
 799              bag, maxvar, newc @ acc)
 800           (bag, maxvar, []) alist
 801       in
 802         debug
 803         (lazy
 804          ("New clauses :" ^ (String.concat ";\n"
 805             (List.map Pp.pp_unit_clause new_clauses))));
 806         debug (lazy "First superpositions");
 807         (* We add current to active clauses so that it can be *
 808          * superposed with itself                             *)
 809       let alist, atable =
 810         current :: alist, IDX.index_unit_clause atable current
 811       in
 812         debug (lazy "Indexed");
 813       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
 814         (* We need to put fresh_current into the bag so that all *
 815          * variables clauses refer to are known.                 *)
 816       let bag, fresh_current = Terms.add_to_bag fresh_current bag in
 817         (* We superpose current with active clauses *)
 818       let bag, maxvar, additional_new_clauses =
 819         superposition_with_table bag maxvar fresh_current atable
 820       in
 821         debug (lazy "Another superposition");
 822       let new_clauses = new_clauses @ additional_new_clauses in
 823         (* debug (lazy (Printf.sprintf "Demodulating %d clauses"
 824                  (List.length new_clauses))); *)
 825       let bag, new_clauses =
 826         HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
 827       in
 828         debug (lazy "Demodulated new clauses");
 829       bag, maxvar, (alist, atable), new_clauses
 830     ;;
 831
 832     let prof_ir = HExtlib.profile ~enable "infer_right";;
 833     let infer_right bag maxvar current t =
 834       prof_ir.HExtlib.profile (infer_right bag maxvar current) t
 835     ;;
 836
 837     let infer_left bag maxvar goal (_alist, atable) =
 838         (* We superpose the goal with active clauses *)
 839      if (match goal with (_,_,[],_) -> true | _ -> false) then bag, maxvar, []
 840      else
 841       let bag, maxvar, new_goals =
 842         superposition_with_table bag maxvar goal atable
 843       in
 844         debug(lazy  "Superposed goal with active clauses");
 845         (* We simplify the new goals with active clauses *)
 846       let bag, new_goals =
 847         List.fold_left
 848          (fun (bag, acc) g ->
 849             match simplify_goal ~no_demod:false maxvar atable bag [] g with
 850               | None -> assert false
 851               | Some (bag,g) -> bag,g::acc)
 852          (bag, []) new_goals
 853       in
 854         debug (lazy "Simplified new goals with active clauses");
 855       bag, maxvar, List.rev new_goals
 856     ;;
 857
 858     let prof_il = HExtlib.profile ~enable "infer_left";;
 859     let infer_left bag maxvar goal t =
 860       prof_il.HExtlib.profile (infer_left bag maxvar goal) t
 861     ;;
 862
 863   end