helm/software/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 : Terms.Blob) =
  15   struct
  16     module IDX = Index.Index(B)
  17     module Unif = FoUnif.Founif(B)
  18     module Subst = FoSubst.Subst(B)
  19     module Order = Orderings.Orderings(B)
  20     module Utils = FoUtils.Utils(B)
  21     module Pp = Pp.Pp(B)
  22
  23     let rec list_first f = function
  24       | [] -> None
  25       | x::tl -> match f x with Some _ as x -> x | _ -> list_first f tl
  26     ;;
  27
  28     let first_position pos ctx t f =
  29       let rec aux pos ctx = function
  30       | Terms.Leaf _ as t -> f t pos ctx
  31       | Terms.Var _ -> None
  32       | Terms.Node l as t->
  33           match f t pos ctx with
  34           | Some _ as x -> x
  35           | None ->
  36               let rec first pre post = function
  37                 | [] -> None
  38                 | t :: tl ->
  39                      let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
  40                      match aux (List.length pre :: pos) newctx t with
  41                      | Some _ as x -> x
  42                      | None ->
  43                          if post = [] then None (* tl is also empty *)
  44                          else first (pre @ [t]) (List.tl post) tl
  45               in
  46                 first [] (List.tl l) l
  47       in
  48         aux pos ctx t
  49     ;;
  50
  51     let all_positions pos ctx t f =
  52       let rec aux pos ctx = function
  53       | Terms.Leaf _ as t -> f t pos ctx
  54       | Terms.Var _ -> []
  55       | Terms.Node l as t->
  56           let acc, _, _ =
  57             List.fold_left
  58             (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
  59                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
  60                 let acc = aux (List.length pre :: pos) newctx t @ acc in
  61                 if post = [] then acc, l, []
  62                 else acc, pre @ [t], List.tl post)
  63              (f t pos ctx, [], List.tl l) l
  64           in
  65            acc
  66       in
  67         aux pos ctx t
  68     ;;
  69
  70     let build_clause bag filter rule t subst vl id id2 pos dir =
  71       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
  72       let t = Subst.apply_subst subst t in
  73       if filter t then
  74         let literal =
  75           match t with
  76           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
  77                let o = Order.compare_terms l r in
  78                Terms.Equation (l, r, ty, o)
  79           | t -> Terms.Predicate t
  80         in
  81         let bag, uc =
  82           Utils.add_to_bag bag (0, literal, vl, proof)
  83         in
  84         Some (bag, uc)
  85       else
  86         ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
  87     ;;
  88
  89
  90     (* ============ simplification ================= *)
  91
  92     let demod table varlist subterm pos context =
  93       let cands = IDX.DT.retrieve_generalizations table subterm in
  94       list_first
  95         (fun (dir, (id,lit,vl,_)) ->
  96            match lit with
  97            | Terms.Predicate _ -> assert false
  98            | Terms.Equation (l,r,_,o) ->
  99                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
 100                try
 101                  let subst, varlist =
 102                    Unif.unification (varlist@vl) varlist subterm side
 103                  in
 104                  if o = Terms.Incomparable then
 105                    let side = Subst.apply_subst subst side in
 106                    let newside = Subst.apply_subst subst newside in
 107                    let o = Order.compare_terms side newside in
 108                    (* Riazanov, pp. 45 (ii) *)
 109                    if o = Terms.Lt then
 110                      Some (context newside, subst, varlist, id, pos, dir)
 111                    else
 112                      ((*prerr_endline ("Filtering: " ^
 113                         Pp.pp_foterm side ^ " =(< || =)" ^
 114                         Pp.pp_foterm newside ^ " coming from " ^
 115                         Pp.pp_unit_clause uc );*)None)
 116                  else
 117                    Some (context newside, subst, varlist, id, pos, dir)
 118                with FoUnif.UnificationFailure _ -> None)
 119         (IDX.ClauseSet.elements cands)
 120     ;;
 121
 122     (* XXX: possible optimization, if the literal has a "side" already
 123      * in normal form we should not traverse it again *)
 124     let demodulate_once bag (id, literal, vl, _) table =
 125       let t =
 126         match literal with
 127         | Terms.Predicate t -> t
 128         | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
 129       in
 130       match first_position [] (fun x -> x) t (demod table vl) with
 131       | None -> None
 132       | Some (newt, subst, varlist, id2, pos, dir) ->
 133           build_clause bag (fun _ -> true) Terms.Demodulation
 134             newt subst varlist id id2 pos dir
 135     ;;
 136
 137     let rec demodulate bag clause table =
 138       match demodulate_once bag clause table with
 139       | None -> bag, clause
 140       | Some (bag, clause) -> demodulate bag clause table
 141     ;;
 142
 143     (* move away *)
 144     let is_identity_clause = function
 145       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
 146       | _, Terms.Predicate _, _, _ -> assert false
 147       | _ -> false
 148     ;;
 149
 150     let is_subsumed (id, lit, vl, _) table =
 151       match lit with
 152       | Terms.Predicate _ -> assert false
 153       | Terms.Equation (l,r,ty,_) ->
 154           let lcands = IDX.DT.retrieve_generalizations table l in
 155           let rcands = IDX.DT.retrieve_generalizations table l in
 156           let f b c =
 157             let dir, l, r, vl =
 158               match c with
 159               | (d, (_,Terms.Equation (l,r,ty,_),vl,_))-> d, l, r, vl
 160               |_ -> assert false
 161             in
 162             let l, r = if (dir = Terms.Left2Right) = b then l,r else r,l in
 163             Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl
 164           in
 165           let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
 166           let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
 167           let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
 168           List.exists
 169             (fun (c, vl1) ->
 170                try ignore(Unif.unification (vl@vl1) vl c t); true
 171                with FoUnif.UnificationFailure _ -> false)
 172             (cands1 @ cands2)
 173     ;;
 174
 175     (* demodulate and check for subsumption *)
 176     let forward_simplify table bag clause =
 177       let bag, clause = demodulate bag clause table in
 178       if is_identity_clause clause then None
 179       else
 180         if is_subsumed clause table then None
 181         else Some (bag, clause)
 182     ;;
 183
 184     (* =================== inference ===================== *)
 185
 186     let superposition_right table varlist subterm pos context =
 187       let cands = IDX.DT.retrieve_unifiables table subterm in
 188       HExtlib.filter_map
 189         (fun (dir, (id,lit,vl,_ (*as uc*))) ->
 190            match lit with
 191            | Terms.Predicate _ -> assert false
 192            | Terms.Equation (l,r,_,o) ->
 193                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
 194                try
 195                  let subst, varlist =
 196                    Unif.unification (varlist@vl) [] subterm side
 197                  in
 198                  if o = Terms.Incomparable then
 199                    let side = Subst.apply_subst subst side in
 200                    let newside = Subst.apply_subst subst newside in
 201                    let o = Order.compare_terms side newside in
 202                    (* XXX: check Riazanov p. 33 (iii) *)
 203                    if o <> Terms.Lt && o <> Terms.Eq then
 204                      Some (context newside, subst, varlist, id, pos, 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 (context newside, subst, varlist, id, pos, dir)
 212                with FoUnif.UnificationFailure _ -> None)
 213         (IDX.ClauseSet.elements cands)
 214     ;;
 215
 216     let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
 217       let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
 218       let subst = Subst.concat relocsubst subst in
 219       match build_clause bag filter rule t subst vl id id2 pos dir with
 220       | Some (bag, c) -> Some ((bag, maxvar), c)
 221       | None -> None
 222     ;;
 223
 224
 225     let fold_build_new_clause bag maxvar id rule filter res =
 226       let (bag, maxvar), res =
 227        HExtlib.filter_map_acc
 228          (fun (bag, maxvar) (t,subst,vl,id2,pos,dir) ->
 229             build_new_clause bag maxvar filter rule t subst vl id id2 pos dir)
 230          (bag, maxvar) res
 231       in
 232        bag, maxvar, res
 233     ;;
 234
 235     let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
 236       match selected with
 237       | Terms.Predicate _ -> assert false
 238       | Terms.Equation (l,r,ty,Terms.Lt) ->
 239           fold_build_new_clause bag maxvar id Terms.SuperpositionRight
 240             (fun _ -> true)
 241             (all_positions [3]
 242               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
 243               r (superposition_right table vl))
 244       | Terms.Equation (l,r,ty,Terms.Gt) ->
 245           fold_build_new_clause bag maxvar id Terms.SuperpositionRight
 246             (fun _ -> true)
 247             (all_positions [2]
 248               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
 249               l (superposition_right table vl))
 250       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
 251           fold_build_new_clause bag maxvar id Terms.SuperpositionRight
 252             (function (* Riazanov: p.33 condition (iv) *)
 253               | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
 254                   Order.compare_terms l r <> Terms.Eq
 255               | _ -> assert false)
 256             ((all_positions [3]
 257                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
 258                r (superposition_right table vl)) @
 259              (all_positions [2]
 260                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
 261                l (superposition_right table vl)))
 262       | _ -> assert false
 263     ;;
 264
 265     (* the current equation is normal w.r.t. demodulation with atable
 266      * (and is not the identity) *)
 267     let infer_right bag maxvar current (alist,atable) =
 268       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 269       let bag, maxvar, new_clauses =
 270         List.fold_left
 271           (fun (bag, maxvar, acc) active ->
 272              let bag, maxvar, newc =
 273                superposition_right_with_table bag maxvar active ctable
 274              in
 275              bag, maxvar, newc @ acc)
 276           (bag, maxvar, []) alist
 277       in
 278       let alist, atable =
 279         current :: alist, IDX.index_unit_clause atable current
 280       in
 281       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
 282       let bag, maxvar, additional_new_clauses =
 283         superposition_right_with_table bag maxvar fresh_current atable
 284       in
 285       let new_clauses = new_clauses @ additional_new_clauses in
 286       let bag, new_clauses =
 287         HExtlib.filter_map_acc (forward_simplify atable) bag new_clauses
 288       in
 289       bag, maxvar, (alist, atable), new_clauses
 290     ;;
 291
 292   end
 293
 294
 295