5 let nparamod rdb metasenv subst context t table =
6 let nb_iter = ref 100 in
7 prerr_endline "========================================";
9 let metasenv = metasenv
14 let module B = NCicBlob.NCicBlob(C) in
15 let module Pp = Pp.Pp (B) in
16 let module FU = FoUnif.Founif(B) in
17 let module IDX = Index.Index(B) in
18 let module Sup = Superposition.Superposition(B) in
19 let module Utils = FoUtils.Utils(B) in
21 let module OrderedPassives =
23 type t = B.t Terms.passive_clause
25 let compare = Utils.compare_passive_clauses
28 let module PassiveSet = Set.Make(OrderedPassives)
30 let add_passive_clause passives cl =
31 PassiveSet.add (Utils.mk_passive_clause cl) passives
33 (* TODO : fairness condition *)
35 if PassiveSet.is_empty passives then None
36 else let cl = PassiveSet.min_elt passives in
37 Some (snd cl,PassiveSet.remove cl passives)
39 let rec given_clause bag maxvar actives
40 passives g_actives g_passives =
42 decr nb_iter; if !nb_iter = 0 then raise (Failure "Timeout !");
44 (* keep goals demodulated w.r.t. actives and check if solved *)
45 (* we may move this at the end of infer_right *)
49 let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
54 (* superposition left, simplifications on goals *)
55 debug "infer_left step...";
56 let bag, maxvar, g_actives, g_passives =
57 match select g_passives with
58 | None -> bag, maxvar, g_actives, g_passives
59 | Some (g_current, g_passives) ->
60 debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
62 Sup.simplify_goal maxvar (snd actives) bag g_current
64 let bag, maxvar, new_goals =
65 Sup.infer_left bag maxvar g_current actives
67 let new_goals = List.fold_left add_passive_clause
68 PassiveSet.empty new_goals
70 bag, maxvar, g_current::g_actives,
71 (PassiveSet.union new_goals g_passives)
74 (Printf.sprintf "Number of active goals : %d"
75 (List.length g_actives));
77 (Printf.sprintf "Number of passive goals : %d"
78 (PassiveSet.cardinal g_passives));
87 * new = supright e'' A'' *
88 * new'= demod A'' new *
90 debug "Forward infer step...";
91 let bag, maxvar, actives, passives, g_passives =
92 let rec aux_simplify passives =
93 match select passives with
94 | None -> assert false
95 | Some (current, passives) ->
96 debug ("Selected fact : " ^ Pp.pp_unit_clause current);
97 match Sup.keep_simplified current actives bag with
98 | None -> aux_simplify passives
101 let (current, bag, actives) = aux_simplify passives
103 debug ("Fact after simplification :"
104 ^ Pp.pp_unit_clause current);
105 let bag, maxvar, actives, new_clauses =
106 Sup.infer_right bag maxvar current actives
108 let ctable = IDX.index_unit_clause IDX.DT.empty current in
109 let bag, maxvar, new_goals =
111 (fun (bag,m,acc) g ->
112 let bag, m, ng = Sup.infer_left bag maxvar g
113 ([current],ctable) in
115 (bag,maxvar,[]) g_actives
117 let new_clauses = List.fold_left add_passive_clause
118 PassiveSet.empty new_clauses in
119 let new_goals = List.fold_left add_passive_clause
120 PassiveSet.empty new_goals in
121 bag, maxvar, actives,
122 PassiveSet.union new_clauses passives,
123 PassiveSet.union new_goals g_passives
126 (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
128 (Printf.sprintf "Number of passives : %d"
129 (PassiveSet.cardinal passives));
130 given_clause bag maxvar actives passives g_actives g_passives
133 let mk_clause bag maxvar (t,ty) =
134 let (proof,ty) = B.saturate t ty in
135 let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
136 let bag, c = Utils.add_to_bag bag c in
139 let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
140 let g_actives = [] in
141 let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
142 let passives, bag, maxvar =
144 (fun (cl, bag, maxvar) t ->
145 let bag, maxvar, c = mk_clause bag maxvar t in
146 (add_passive_clause cl c), bag, maxvar)
147 (PassiveSet.empty, bag, maxvar) table
149 let actives = [], IDX.DT.empty in
150 try given_clause bag maxvar actives passives g_actives g_passives
152 | Sup.Success (bag, _, (i,_,_,_)) ->
155 HTopoSort.Make(struct type t=int let compare=Pervasives.compare end)
157 let module C : Set.S with type elt = int =
158 Set.Make(struct type t=int let compare=Pervasives.compare end)
161 let rec traverse acc i =
162 match Terms.M.find i bag with
163 | (_,_,_,Terms.Exact _) -> acc
164 | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
165 traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2
167 C.elements (traverse C.empty id)
169 S.topological_sort (all i) all
171 prerr_endline "YES!";
172 prerr_endline "Proof:";
174 prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
175 let proofterm = B.mk_proof bag l in
177 (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
179 let _metasenv, _subst, _proofterm, _prooftype =
180 NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
183 | Failure _ -> prerr_endline "FAILURE";