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
  22     let all_positions pos ctx t f =
  23       let rec aux pos ctx = function
  24       | Terms.Leaf _ as t -> f t pos ctx
  25       | Terms.Var _ -> []
  26       | Terms.Node l as t->
  27           let acc, _, _ =
  28             List.fold_left
  29             (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
  30                 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
  31                 let acc = aux (List.length pre :: pos) newctx t @ acc in
  32                 if post = [] then acc, l, []
  33                 else acc, pre @ [t], List.tl post)
  34              (f t pos ctx, [], List.tl l) l
  35           in
  36            acc
  37       in
  38         aux pos ctx t
  39     ;;
  40
  41     let superposition_right table varlist subterm pos context =
  42       let cands = IDX.DT.retrieve_unifiables table subterm in
  43       HExtlib.filter_map
  44         (fun (dir, (id,lit,vl,_)) ->
  45            match lit with
  46            | Terms.Predicate _ -> assert false
  47            | Terms.Equation (l,r,_,o) ->
  48                assert(o <> Terms.Eq);
  49                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
  50                try
  51                  let subst, varlist =
  52                    Unif.unification (varlist@vl) [] subterm side
  53                  in
  54                  if o = Terms.Incomparable then
  55                    let side = Subst.apply_subst subst side in
  56                    let newside = Subst.apply_subst subst newside in
  57                    let o = Order.compare_terms side newside in
  58                    (* XXX: check Riazanov p. 33 (iii) *)
  59                    if o <> Terms.Lt && o <> Terms.Eq then
  60                      Some (context newside, subst, varlist, id, pos, dir)
  61                    else
  62                      None
  63                  else
  64                    Some (context newside, subst, varlist, id, pos, dir)
  65                with FoUnif.UnificationFailure _ -> None)
  66         (IDX.ClauseSet.elements cands)
  67     ;;
  68
  69     let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
  70       let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
  71       let subst = Subst.concat relocsubst subst in
  72       let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
  73       let t = Subst.apply_subst subst t in
  74       if filter t then
  75         let literal =
  76           match t with
  77           | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
  78                let o = Order.compare_terms l r in
  79                Terms.Equation (l, r, ty, o)
  80           | t -> Terms.Predicate t
  81         in
  82         let bag, uc =
  83           Utils.add_to_bag bag (0, literal, vl, proof)
  84         in
  85         Some (bag, maxvar, uc)
  86       else
  87         None
  88     ;;
  89
  90     let fold_build_new_clause bag maxvar id filter res =
  91       let maxvar, bag, new_clauses =
  92         List.fold_left
  93           (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) ->
  94              match build_new_clause bag maxvar filter t subst vl id id2 pos dir
  95              with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
  96                 | None -> maxvar, bag, acc)
  97           (maxvar, bag, []) res
  98       in
  99       bag, maxvar, new_clauses
 100     ;;
 101
 102     let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
 103       match selected with
 104       | Terms.Predicate _ -> assert false
 105       | Terms.Equation (l,r,ty,Terms.Lt) ->
 106           fold_build_new_clause bag maxvar id (fun _ -> true)
 107             (all_positions [3]
 108               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
 109               r (superposition_right table vl))
 110       | Terms.Equation (l,r,ty,Terms.Gt) ->
 111           fold_build_new_clause bag maxvar id (fun _ -> true)
 112             (all_positions [2]
 113               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
 114               l (superposition_right table vl))
 115       | Terms.Equation (l,r,ty,Terms.Incomparable) ->
 116           fold_build_new_clause bag maxvar id
 117             (function (* Riazanov: p.33 condition (iv) *)
 118               | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
 119                   Order.compare_terms l r <> Terms.Eq
 120               | _ -> assert false)
 121             ((all_positions [3]
 122                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
 123                r (superposition_right table vl)) @
 124              (all_positions [2]
 125                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
 126                l (superposition_right table vl)))
 127       | _ -> assert false
 128     ;;
 129
 130   end
 131
 132
 133