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 exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
26 ()(* prerr_endline s *)
29 let rec list_first f = function
31 | x::tl -> match f x with Some _ as x -> x | _ -> list_first f tl
34 let first_position pos ctx t f =
35 let rec aux pos ctx = function
36 | Terms.Leaf _ as t -> f t pos ctx
39 match f t pos ctx with
42 let rec first pre post = function
45 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
46 match aux (List.length pre :: pos) newctx t with
49 if post = [] then None (* tl is also empty *)
50 else first (pre @ [t]) (List.tl post) tl
52 first [] (List.tl l) l
57 let all_positions pos ctx t f =
58 let rec aux pos ctx = function
59 | Terms.Leaf _ as t -> f t pos ctx
64 (fun (acc,pre,post) t -> (* Invariant: pre @ [t] @ post = l *)
65 let newctx = fun x -> ctx (Terms.Node (pre@[x]@post)) in
66 let acc = aux (List.length pre :: pos) newctx t @ acc in
67 if post = [] then acc, l, []
68 else acc, pre @ [t], List.tl post)
69 (f t pos ctx, [], List.tl l) l
76 let build_clause bag filter rule t subst vl id id2 pos dir =
77 let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
78 let t = Subst.apply_subst subst t in
82 | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
83 let o = Order.compare_terms l r in
84 Terms.Equation (l, r, ty, o)
85 | t -> Terms.Predicate t
88 Utils.add_to_bag bag (0, literal, vl, proof)
92 ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None)
96 (* ============ simplification ================= *)
98 let demod table varlist subterm pos context =
99 let cands = IDX.DT.retrieve_generalizations table subterm in
101 (fun (dir, (id,lit,vl,_)) ->
103 | Terms.Predicate _ -> assert false
104 | Terms.Equation (l,r,_,o) ->
105 let side, newside = if dir=Terms.Left2Right then l,r else r,l in
108 Unif.unification (varlist@vl) varlist subterm side
110 if o = Terms.Incomparable then
111 let side = Subst.apply_subst subst side in
112 let newside = Subst.apply_subst subst newside in
113 let o = Order.compare_terms newside side in
114 (* Riazanov, pp. 45 (ii) *)
116 Some (context newside, subst, varlist, id, pos, dir)
118 ((*prerr_endline ("Filtering: " ^
119 Pp.pp_foterm side ^ " =(< || =)" ^
120 Pp.pp_foterm newside ^ " coming from " ^
121 Pp.pp_unit_clause uc );*)None)
123 Some (context newside, subst, varlist, id, pos, dir)
124 with FoUnif.UnificationFailure _ -> None)
125 (IDX.ClauseSet.elements cands)
128 (* XXX: possible optimization, if the literal has a "side" already
129 * in normal form we should not traverse it again *)
130 let demodulate_once bag (id, literal, vl, pr) table =
131 debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));
134 | Terms.Predicate t -> t
135 | Terms.Equation (l,r,ty,_) -> Terms.Node [ Terms.Leaf B.eqP; ty; l; r ]
137 match first_position [] (fun x -> x) t (demod table vl) with
139 | Some (newt, subst, varlist, id2, pos, dir) ->
140 build_clause bag (fun _ -> true) Terms.Demodulation
141 newt subst varlist id id2 pos dir
144 let rec demodulate bag clause table =
145 match demodulate_once bag clause table with
146 | None -> bag, clause
147 | Some (bag, clause) -> demodulate bag clause table
151 let is_identity_clause = function
152 | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
153 | _, Terms.Predicate _, _, _ -> assert false
157 let is_subsumed ~unify (id, lit, vl, _) table =
159 | Terms.Predicate _ -> assert false
160 | Terms.Equation (l,r,ty,_) ->
161 let retrieve = if unify then IDX.DT.retrieve_unifiables
162 else IDX.DT.retrieve_generalizations in
163 let lcands = retrieve table l in
164 let rcands = retrieve table r in
168 | (d, (_,Terms.Equation (l,r,ty,_),vl,_))-> d, l, r, vl
171 let l, r = if (dir = Terms.Left2Right) = b then l,r else r,l in
172 Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl
174 let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
175 let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
176 let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
177 let locked_vars = if unify then [] else vl in
180 try ignore(Unif.unification (vl@vl1) locked_vars c t); true
181 with FoUnif.UnificationFailure _ -> false)
185 (* demodulate and check for subsumption *)
186 let simplify table bag clause =
187 let bag, clause = demodulate bag clause table in
188 if is_identity_clause clause then None
190 if is_subsumed ~unify:false clause table then None
191 else Some (bag, clause)
194 let simplification_step ~new_cl cl (alist,atable) bag new_clause =
196 if new_cl then atable else
197 IDX.index_unit_clause atable cl
199 match simplify atable1 bag new_clause with
200 | None -> (Some cl, None)
201 | Some (bag, clause) ->
202 let ctable = IDX.index_unit_clause IDX.DT.empty clause in
203 let bag, newa, alist, atable =
205 (fun (bag, newa, alist, atable as acc) c ->
206 match simplify ctable bag c with
210 bag, newa, c :: alist,
211 IDX.index_unit_clause atable c
213 bag, c1 :: newa, alist, atable)
214 (bag,[],[],IDX.DT.empty) alist
217 (Some cl, Some (clause, (alist,atable), newa, bag))
219 match simplify ctable bag cl with
221 (None, Some (clause, (alist,atable), newa, bag))
223 (Some cl1, Some (clause, (alist,atable), newa, bag))
226 let keep_simplified cl (alist,atable) bag =
227 let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
229 match simplification_step ~new_cl cl (alist,atable) bag cl with
230 | (None, _) -> assert false
231 | (Some _, None) -> None
232 | (Some _, Some (clause, (alist,atable), newa, bag)) ->
233 keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
237 | [] -> Some (cl, bag, (alist,atable))
239 match simplification_step ~new_cl cl
240 (alist,atable) bag hd with
241 | (None,None) -> assert false
243 keep_simplified_aux ~new_cl cl (alist,atable) bag tl
244 | (None, Some _) -> None
245 | (Some cl1, Some (clause, (alist,atable), newa, bag)) ->
247 (clause::alist, IDX.index_unit_clause atable clause)
249 keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
252 keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
255 (* this is like simplify but raises Success *)
256 let simplify_goal maxvar table bag clause =
257 let bag, clause = demodulate bag clause table in
258 if (is_identity_clause clause) || (is_subsumed ~unify:true clause table)
259 then raise (Success (bag, maxvar, clause))
263 (* =================== inference ===================== *)
265 (* this is OK for both the sup_left and sup_right inference steps *)
266 let superposition table varlist subterm pos context =
267 let cands = IDX.DT.retrieve_unifiables table subterm in
269 (fun (dir, (id,lit,vl,_ (*as uc*))) ->
271 | Terms.Predicate _ -> assert false
272 | Terms.Equation (l,r,_,o) ->
273 let side, newside = if dir=Terms.Left2Right then l,r else r,l in
276 Unif.unification (varlist@vl) [] subterm side
278 if o = Terms.Incomparable then
279 let side = Subst.apply_subst subst side in
280 let newside = Subst.apply_subst subst newside in
281 let o = Order.compare_terms side newside in
282 (* XXX: check Riazanov p. 33 (iii) *)
283 if o <> Terms.Lt && o <> Terms.Eq then
284 Some (context newside, subst, varlist, id, pos, dir)
286 ((*prerr_endline ("Filtering: " ^
287 Pp.pp_foterm side ^ " =(< || =)" ^
288 Pp.pp_foterm newside ^ " coming from " ^
289 Pp.pp_unit_clause uc );*)None)
291 Some (context newside, subst, varlist, id, pos, dir)
292 with FoUnif.UnificationFailure _ -> None)
293 (IDX.ClauseSet.elements cands)
296 let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
297 let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
298 let subst = Subst.concat relocsubst subst in
299 match build_clause bag filter rule t subst vl id id2 pos dir with
300 | Some (bag, c) -> Some ((bag, maxvar), c)
305 let fold_build_new_clause bag maxvar id rule filter res =
306 let (bag, maxvar), res =
307 HExtlib.filter_map_acc
308 (fun (bag, maxvar) (t,subst,vl,id2,pos,dir) ->
309 build_new_clause bag maxvar filter rule t subst vl id id2 pos dir)
315 (* Superposes selected equation with equalities in table *)
316 let superposition_with_table bag maxvar (id,selected,vl,_) table =
318 | Terms.Predicate _ -> assert false
319 | Terms.Equation (l,r,ty,Terms.Lt) ->
320 fold_build_new_clause bag maxvar id Terms.Superposition
323 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
324 r (superposition table vl))
325 | Terms.Equation (l,r,ty,Terms.Gt) ->
326 fold_build_new_clause bag maxvar id Terms.Superposition
329 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
330 l (superposition table vl))
331 | Terms.Equation (l,r,ty,Terms.Incomparable) ->
332 fold_build_new_clause bag maxvar id Terms.Superposition
333 (function (* Riazanov: p.33 condition (iv) *)
334 | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq ->
335 Order.compare_terms l r <> Terms.Eq
338 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
339 r (superposition table vl)) @
341 (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
342 l (superposition table vl)))
346 (* the current equation is normal w.r.t. demodulation with atable
347 * (and is not the identity) *)
348 let infer_right bag maxvar current (alist,atable) =
349 (* We demodulate actives clause with current until all *
350 * active clauses are reduced w.r.t each other *)
351 (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
352 let ctable = IDX.index_unit_clause IDX.DT.empty current in
353 (* let bag, (alist, atable) =
355 HExtlib.filter_map_acc (simplify ctable) bag alist
357 bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
359 debug "Simplified active clauses with fact";
360 (* We superpose active clauses with current *)
361 let bag, maxvar, new_clauses =
363 (fun (bag, maxvar, acc) active ->
364 let bag, maxvar, newc =
365 superposition_with_table bag maxvar active ctable
367 bag, maxvar, newc @ acc)
368 (bag, maxvar, []) alist
370 debug "First superpositions";
371 (* We add current to active clauses so that it can be *
372 * superposed with itself *)
374 current :: alist, IDX.index_unit_clause atable current
377 let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
378 (* We need to put fresh_current into the bag so that all *
379 * variables clauses refer to are known. *)
380 let bag, fresh_current = Utils.add_to_bag bag fresh_current in
381 (* We superpose current with active clauses *)
382 let bag, maxvar, additional_new_clauses =
383 superposition_with_table bag maxvar fresh_current atable
385 debug "Another superposition";
386 let new_clauses = new_clauses @ additional_new_clauses in
387 let bag, new_clauses =
388 HExtlib.filter_map_acc (simplify atable) bag new_clauses
390 debug "Demodulated new clauses";
391 bag, maxvar, (alist, atable), new_clauses
394 let infer_left bag maxvar goal (_alist, atable) =
395 (* We superpose the goal with active clauses *)
396 let bag, maxvar, new_goals =
397 superposition_with_table bag maxvar goal atable
399 (* We demodulate the goal with active clauses *)
403 let bag, g = demodulate bag g atable in
407 bag, maxvar, List.rev new_goals