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)
23 let all_positions pos ctx t f =
24 let rec aux pos ctx = function
25 | Terms.Leaf _ as t -> f t pos ctx
30 (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
31 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
32 let acc = aux (List.length pre :: pos) newctx t @ acc in
33 if post = [] then acc, l, []
34 else acc, pre @ [t], List.tl post)
35 (f t pos ctx, [], List.tl l) l
42 let superposition_right table varlist subterm pos context =
43 let cands = IDX.DT.retrieve_unifiables table subterm in
45 (fun (dir, (id,lit,vl,_ (*as uc*))) ->
47 | Terms.Predicate _ -> assert false
48 | Terms.Equation (l,r,_,o) ->
49 assert(o <> Terms.Eq);
50 let side, newside = if dir=Terms.Left2Right then l,r else r,l in
53 Unif.unification (varlist@vl) [] subterm side
55 if o = Terms.Incomparable then
56 let side = Subst.apply_subst subst side in
57 let newside = Subst.apply_subst subst newside in
58 let o = Order.compare_terms side newside in
59 (* XXX: check Riazanov p. 33 (iii) *)
60 if o <> Terms.Lt && o <> Terms.Eq then
61 Some (context newside, subst, varlist, id, pos, dir)
63 ((*prerr_endline ("Filtering: " ^
64 Pp.pp_foterm side ^ " =(< || =)" ^
65 Pp.pp_foterm newside ^ " coming from " ^
66 Pp.pp_unit_clause uc );*)None)
68 Some (context newside, subst, varlist, id, pos, dir)
69 with FoUnif.UnificationFailure _ -> None)
70 (IDX.ClauseSet.elements cands)
73 let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
74 let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
75 let subst = Subst.concat relocsubst subst in
76 let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
77 let t = Subst.apply_subst subst t in
81 | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
82 let o = Order.compare_terms l r in
83 Terms.Equation (l, r, ty, o)
84 | t -> Terms.Predicate t
87 Utils.add_to_bag bag (0, literal, vl, proof)
89 Some (bag, maxvar, uc)
91 ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
94 let fold_build_new_clause bag maxvar id filter res =
95 let maxvar, bag, new_clauses =
97 (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) ->
98 match build_new_clause bag maxvar filter t subst vl id id2 pos dir
99 with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
100 | None -> maxvar, bag, acc)
101 (maxvar, bag, []) res
103 bag, maxvar, new_clauses
106 let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
108 | Terms.Predicate _ -> assert false
109 | Terms.Equation (l,r,ty,Terms.Lt) ->
110 fold_build_new_clause bag maxvar id (fun _ -> true)
112 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
113 r (superposition_right table vl))
114 | Terms.Equation (l,r,ty,Terms.Gt) ->
115 fold_build_new_clause bag maxvar id (fun _ -> true)
117 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
118 l (superposition_right table vl))
119 | Terms.Equation (l,r,ty,Terms.Incomparable) ->
120 fold_build_new_clause bag maxvar id
121 (function (* Riazanov: p.33 condition (iv) *)
122 | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
123 Order.compare_terms l r <> Terms.Eq
126 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
127 r (superposition_right table vl)) @
129 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
130 l (superposition_right table vl)))
134 (* the current equation is normal w.r.t. demodulation with atable
135 * (and is not the identity) *)
136 let superposition_right bag maxvar current (alist,atable) =
137 let ctable = IDX.index_unit_clause IDX.DT.empty current in
138 let bag, maxvar, new_clauses =
140 (fun (bag, maxvar, acc) active ->
141 let bag, maxvar, newc =
142 superposition_right_with_table bag maxvar active ctable
144 bag, maxvar, newc @ acc)
145 (bag, maxvar, []) alist
148 current :: alist, IDX.index_unit_clause atable current
150 let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
151 let bag, maxvar, additional_new_clauses =
152 superposition_right_with_table bag maxvar fresh_current atable
154 bag, maxvar, (alist, atable), new_clauses @ additional_new_clauses