2 () (* prerr_endline s *)
5 let nparamod rdb metasenv subst context t table =
6 let nb_iter = ref 200 in
8 let metasenv = metasenv
13 let module B = NCicBlob.NCicBlob(C) in
14 let module Pp = Pp.Pp (B) in
15 let module FU = FoUnif.Founif(B) in
16 let module IDX = Index.Index(B) in
17 let module Sup = Superposition.Superposition(B) in
18 let module Utils = FoUtils.Utils(B) in
20 let module OrderedPassives =
22 type t = B.t Terms.passive_clause
24 let compare = Utils.compare_passive_clauses
27 let module PassiveSet = Set.Make(OrderedPassives)
29 let add_passive_clause passives cl =
30 PassiveSet.add (Utils.mk_passive_clause cl) passives
32 (* TODO : fairness condition *)
34 if PassiveSet.is_empty passives then None
35 else let cl = PassiveSet.min_elt passives in
36 Some (snd cl,PassiveSet.remove cl passives)
38 let rec given_clause bag maxvar actives
39 passives g_actives g_passives =
41 decr nb_iter; if !nb_iter = 0 then
42 (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
43 prerr_endline "Active table :";
44 (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
46 raise (Failure "Timeout !");
50 (* superposition left, simplifications on goals *)
51 debug "infer_left step...";
52 let bag, maxvar, g_actives, g_passives =
53 match select g_passives with
54 | None -> bag, maxvar, g_actives, g_passives
55 | Some (g_current, g_passives) ->
56 debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
58 Sup.simplify_goal maxvar (snd actives) bag g_current
60 let bag, maxvar, new_goals =
61 Sup.infer_left bag maxvar g_current actives
63 let new_goals = List.fold_left add_passive_clause
64 PassiveSet.empty new_goals
66 bag, maxvar, g_current::g_actives,
67 (PassiveSet.union new_goals g_passives)
70 (Printf.sprintf "Number of active goals : %d"
71 (List.length g_actives));
73 (Printf.sprintf "Number of passive goals : %d"
74 (PassiveSet.cardinal g_passives));
83 * new = supright e'' A'' *
84 * new'= demod A'' new *
86 debug "Forward infer step...";
87 let bag, maxvar, actives, passives, g_passives =
88 let rec aux_simplify passives =
89 match select passives with
90 | None -> assert false
91 | Some (current, passives) ->
92 debug ("Selected fact : " ^ Pp.pp_unit_clause current);
93 match Sup.keep_simplified current actives bag maxvar with
94 (* match Sup.one_pass_simplification current actives bag with *)
95 | None -> aux_simplify passives
96 | Some x -> x,passives
98 let (current, bag, actives),passives = aux_simplify passives
100 debug ("Fact after simplification :"
101 ^ Pp.pp_unit_clause current);
102 let bag, maxvar, actives, new_clauses =
103 Sup.infer_right bag maxvar current actives
105 debug "Demodulating goals with actives...";
106 (* keep goals demodulated w.r.t. actives and check if solved *)
110 let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
114 let ctable = IDX.index_unit_clause IDX.DT.empty current in
115 let bag, maxvar, new_goals =
117 (fun (bag,m,acc) g ->
118 let bag, m, ng = Sup.infer_left bag maxvar g
119 ([current],ctable) in
121 (bag,maxvar,[]) g_actives
123 let new_clauses = List.fold_left add_passive_clause
124 PassiveSet.empty new_clauses in
125 let new_goals = List.fold_left add_passive_clause
126 PassiveSet.empty new_goals in
127 bag, maxvar, actives,
128 PassiveSet.union new_clauses passives,
129 PassiveSet.union new_goals g_passives
132 (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
134 (Printf.sprintf "Number of passives : %d"
135 (PassiveSet.cardinal passives));
136 given_clause bag maxvar actives passives g_actives g_passives
139 let mk_clause bag maxvar (t,ty) =
140 let (proof,ty) = B.saturate t ty in
141 let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
142 let bag, c = Utils.add_to_bag bag c in
145 let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
146 let g_actives = [] in
147 let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
148 let passives, bag, maxvar =
150 (fun (cl, bag, maxvar) t ->
151 let bag, maxvar, c = mk_clause bag maxvar t in
152 (add_passive_clause cl c), bag, maxvar)
153 (PassiveSet.empty, bag, maxvar) table
155 let actives = [], IDX.DT.empty in
156 try given_clause bag maxvar actives passives g_actives g_passives
158 | Sup.Success (bag, _, (i,_,_,_)) ->
161 HTopoSort.Make(struct type t=int let compare=Pervasives.compare end)
163 let module C : Set.S with type elt = int =
164 Set.Make(struct type t=int let compare=Pervasives.compare end)
167 let rec traverse ongoal (accg,acce) i =
168 match Terms.M.find i bag with
169 | (_,_,_,Terms.Exact _) -> accg, acce
170 | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
172 if ongoal then C.add i1 accg, acce
173 else accg, C.add i1 acce
175 let acce = C.add i2 acce in
176 traverse false (traverse ongoal (accg,acce) i1) i2
178 traverse true (C.empty,C.empty) id
181 S.topological_sort (C.elements (snd (all i)))
182 (fun i -> C.elements (C.union (snd (all i)) (fst (all i)) ))
185 S.topological_sort (C.elements (fst (all i)))
186 (fun i -> C.elements (fst (all i)))
188 let gsteps = List.rev gsteps in
192 debug ("Meeting point : " ^ (string_of_int i));
194 (*List.iter (fun x -> prerr_endline (string_of_int x);
195 prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l; *)
196 let proofterm = B.mk_proof bag i l in
197 prerr_endline (NCicPp.ppterm ~metasenv:C.metasenv
198 ~subst:C.subst ~context:C.context proofterm);
199 let metasenv, subst, proofterm, _prooftype =
201 (rdb#set_coerc_db NCicCoercion.empty_db)
202 C.metasenv C.subst C.context proofterm None
204 proofterm, metasenv, subst
205 | Failure _ -> prerr_endline "FAILURE"; assert false