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.
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_______________________________________________________________ *)
12 (* $Id: index.mli 9822 2009-06-03 15:37:06Z tassi $ *)
14 module Superposition (B : Terms.Blob) =
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)
22 let all_positions pos ctx t f =
23 let rec aux pos ctx = function
24 | Terms.Leaf _ as t -> f t pos ctx
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
41 let superposition_right table varlist subterm pos context =
42 let cands = IDX.DT.retrieve_unifiables table subterm in
44 (fun (dir, (id,lit,vl,_)) ->
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
52 Unif.unification (varlist@vl) [] subterm side
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)
64 Some (context newside, subst, varlist, id, pos, dir)
65 with FoUnif.UnificationFailure _ -> None)
66 (IDX.ClauseSet.elements cands)
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
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
83 Utils.add_to_bag bag (0, literal, vl, proof)
85 Some (bag, maxvar, uc)
90 let fold_build_new_clause bag maxvar id filter res =
91 let maxvar, bag, new_clauses =
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)
99 bag, maxvar, new_clauses
102 let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
104 | Terms.Predicate _ -> assert false
105 | Terms.Equation (l,r,ty,Terms.Lt) ->
106 fold_build_new_clause bag maxvar id (fun _ -> true)
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)
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
122 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
123 r (superposition_right table vl)) @
125 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
126 l (superposition_right table vl)))