5 let nparamod 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
151 with Sup.Success (bag, _, mp) ->
152 prerr_endline "YES!";
153 prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp)
154 (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
155 | Failure _ -> prerr_endline "FAILURE"