X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=654195c06360bd16ee0d274a3d5425bc1723774b;hb=8b4a227cafd6707cf466c02606b2f1f3f6b60219;hp=6a700d868a30fd792279e13affc4e7a0b10ae2d6;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 6a700d868..654195c06 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -28,6 +28,7 @@ open Inference;; open Utils;; + (* for debugging let check_equation env equation msg = @@ -69,9 +70,9 @@ let maximal_retained_equality = ref None;; (* equality-selection related globals *) let use_fullred = ref true;; -let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *) -let weight_age_counter = ref !weight_age_ratio;; -let symbols_ratio = ref (* 0 *) 3;; +let weight_age_ratio = ref 5 (* 5 *);; (* settable by the user *) +let weight_age_counter = ref !weight_age_ratio ;; +let symbols_ratio = ref 0 (* 3 *);; let symbols_counter = ref 0;; (* non-recursive Knuth-Bendix term ordering by default *) @@ -134,16 +135,60 @@ module OrderedEquality = struct with Failure "hd" -> Pervasives.compare eq1 eq2 ) | res -> res -end +end module EqualitySet = Set.Make(OrderedEquality);; +exception Empty_list;; + +let passive_is_empty = function + | ([], _), ([], _), _ -> true + | _ -> false +;; + + +let size_of_passive ((_, ns), (_, ps), _) = + (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) +;; + + +let size_of_active (active_list, _) = + List.length active_list +;; + +let age_factor = 0.01;; + +let min_elt weight l = + fst + (match l with + [] -> raise Empty_list + | a::tl -> + let wa = float_of_int (weight a) in + let x = ref 0. in + List.fold_left + (fun (current,w) arg -> + x:=!x +. 1.; + let w1 = weight arg in + let wa = (float_of_int w1) +. !x *. age_factor in + if wa < w then (arg,wa) else (current,w)) + (a,wa) tl) +;; + +(* +let compare eq1 eq2 = + let w1, _, (ty, left, right, _), m1, _ = eq1 in + let w2, _, (ty', left', right', _), m2, _ = eq2 in + match Pervasives.compare w1 w2 with + | 0 -> (List.length m1) - (List.length m2) + | res -> res +;; +*) (** selects one equality from passive. The selection strategy is a combination of weight, age and goal-similarity *) -let select env goals passive (active, _) = +let rec select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; let goal = match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false @@ -163,15 +208,15 @@ let select env goals passive (active, _) = (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], (hd:EqualitySet.elt)::tl -> + let w,_,_,_,_ = hd in let passive_table = - Indexing.remove_index passive_table hd - in - (Positive, hd), + Indexing.remove_index passive_table hd + in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) | _, _ -> assert false ) - | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> ( - symbols_counter := !symbols_counter - 1; + | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> + (symbols_counter := !symbols_counter - 1; let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 in @@ -215,7 +260,8 @@ let select env goals passive (active, _) = ) | _ -> symbols_counter := !symbols_ratio; - let set_selection set = EqualitySet.min_elt set in + let set_selection set = EqualitySet.min_elt set in + (* let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in *) if EqualitySet.is_empty neg_set then let current = set_selection pos_set in let passive = @@ -273,22 +319,6 @@ let add_to_passive passive (new_neg, new_pos) = ;; -let passive_is_empty = function - | ([], _), ([], _), _ -> true - | _ -> false -;; - - -let size_of_passive ((_, ns), (_, ps), _) = - (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps) -;; - - -let size_of_active (active_list, _) = - List.length active_list -;; - - (* removes from passive equalities that are estimated impossible to activate within the current time limit *) let prune_passive howmany (active, _) passive = @@ -391,41 +421,75 @@ let prune_passive howmany (active, _) passive = (** inference of new equalities between current and some in active *) let infer env sign current (active_list, active_table) = + let (_,c,_) = env in + if Utils.debug_metas then + (ignore(Indexing.check_target c current "infer1"); + ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list)); let new_neg, new_pos = match sign with | Negative -> let maxm, res = Indexing.superposition_left !maxmeta env active_table current in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup-1") res); maxmeta := maxm; res, [] | Positive -> let maxm, res = Indexing.superposition_right !maxmeta env active_table current in - maxmeta := maxm; + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup0") res); + maxmeta := maxm; let rec infer_positive table = function | [] -> [], [] | (Negative, equality)::tl -> let maxm, res = Indexing.superposition_left !maxmeta env table equality in maxmeta := maxm; + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "supl") res); let neg, pos = infer_positive table tl in res @ neg, pos | (Positive, equality)::tl -> let maxm, res = Indexing.superposition_right !maxmeta env table equality in maxmeta := maxm; + if Utils.debug_metas then + ignore + (List.map + (function current -> + Indexing.check_target c current "sup2") res); let neg, pos = infer_positive table tl in neg, res @ pos in let curr_table = Indexing.index Indexing.empty current in let neg, pos = infer_positive curr_table active_list in + if Utils.debug_metas then + ignore(List.map + (function current -> + Indexing.check_target c current "sup3") pos); neg, res @ pos in derived_clauses := !derived_clauses + (List.length new_neg) + (List.length new_pos); match !maximal_retained_equality with - | None -> new_neg, new_pos + | None -> + if Utils.debug_metas then + (ignore(List.map + (function current -> + Indexing.check_target c current "sup4") new_pos); + ignore(List.map + (function current -> + Indexing.check_target c current "sup5") new_neg)); + new_neg, new_pos | Some eq -> + ignore(assert false); (* if we have a maximal_retained_equality, we can discard all equalities "greater" than it, as they will never be reached... An equality is greater than maximal_retained_equality if it is bigger @@ -469,7 +533,7 @@ let infer env sign current (active_list, active_table) = in List.filter filterfun new_pos in - new_neg, new_pos + new_neg, new_pos ;; @@ -490,6 +554,7 @@ let contains_empty env (negative, positive) = (** simplifies current using active and passive *) let forward_simplify env (sign, current) ?passive (active_list, active_table) = + let _, context, _ = env in let pl, passive_table = match passive with | None -> [], None @@ -498,7 +563,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = and pp = List.map (fun e -> (Positive, e)) pp in pn @ pp, Some pt in - let all = if pl = [] then active_list else active_list @ pl in + let all = if pl = [] then active_list else active_list @ pl in let demodulate table current = let newmeta, newcurrent = @@ -523,7 +588,12 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = Some (sign, newcurrent) in let res = + if Utils.debug_metas then + ignore (Indexing.check_target context current "demod0"); let res = demodulate active_table current in + if Utils.debug_metas then + ignore ((function None -> () | Some (_,x) -> + Indexing.check_target context x "demod1";()) res); match res with | None -> None | Some (sign, newcurrent) -> @@ -570,6 +640,16 @@ let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; (** simplifies new using active and passive *) let forward_simplify_new env (new_neg, new_pos) ?passive active = + if Utils.debug_metas then + begin + let m,c,u = env in + ignore(List.map + (fun current -> + Indexing.check_target c current "forward new neg") new_neg); + ignore(List.map + (fun current -> Indexing.check_target c current "forward new pos") + new_pos;) + end; let t1 = Unix.gettimeofday () in let active_list, active_table = active in @@ -596,9 +676,8 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = let new_neg, new_pos = let new_neg = List.map (demodulate Negative active_table) new_neg and new_pos = List.map (demodulate Positive active_table) new_pos in - new_neg,new_pos - -(* PROVA + new_neg,new_pos +(* PROVA match passive_table with | None -> new_neg, new_pos | Some passive_table -> @@ -735,12 +814,52 @@ let backward_simplify env new' ?passive active = | None -> active, (make_passive [] []), newa, None | Some passive -> + active, passive, newa, None +(* prova let passive, newp = backward_simplify_passive env new_pos new_table min_weight passive in - active, passive, newa, newp + active, passive, newa, newp *) ;; +let close env new' given = + let new_pos, new_table, min_weight = + List.fold_left + (fun (l, t, w) e -> + let ew, _, _, _, _ = e in + (Positive, e)::l, Indexing.index t e, min ew w) + ([], Indexing.empty, 1000000) (snd new') + in + List.fold_left + (fun (n,p) (s,c) -> + let neg,pos = infer env s c (new_pos,new_table) in + neg@n,pos@p) + ([],[]) given +;; + +let is_commutative_law eq = + let w, proof, (eq_ty, left, right, order), metas, args = snd eq in + match left,right with + Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], + Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> + f1 = f2 && a1 = b2 && a2 = b1 + | _ -> false +;; + +let prova env new' active = + let given = List.filter is_commutative_law (fst active) in + let _ = + debug_print + (lazy + (Printf.sprintf "symmetric:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + (given)))))) in + close env new' given +;; + (* returns an estimation of how many equalities in passive can be activated within the current time limit *) let get_selection_estimate () = @@ -929,7 +1048,7 @@ let apply_equality_to_goal env equality goal = try let subst, metasenv', _ = let menv = metasenv @ metas @ gmetas in - Inference.unification menv context eqterm gterm ugraph + Inference.unification metas gmetas context eqterm gterm ugraph in let newproof = match proof with @@ -1427,6 +1546,7 @@ let apply_theorem_to_goals env theorems active goals = (* given-clause algorithm with lazy reduction strategy *) let rec given_clause dbd env goals theorems passive active = + let _,context,_ = env in let goals = simplify_goals env goals active in let ok, goals = activate_goal goals in (* let theorems = simplify_theorems env theorems active in *) @@ -1460,8 +1580,9 @@ let rec given_clause dbd env goals theorems passive active = else given_clause_aux dbd env goals theorems passive active and given_clause_aux dbd env goals theorems passive active = + let _,context,_ = env in let time1 = Unix.gettimeofday () in - + let selection_estimate = get_selection_estimate () in let kept = size_of_passive passive in let passive = @@ -1490,6 +1611,9 @@ and given_clause_aux dbd env goals theorems passive active = given_clause dbd env goals theorems passive active | false -> let (sign, current), passive = select env (fst goals) passive active in + let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in + prerr_endline ("Selected = " ^ + (CicPp.pp (Inference.term_of_equality current) names)); let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1504,7 +1628,7 @@ and given_clause_aux dbd env goals theorems passive active = (string_of_equality ~env current))); let _, proof, _, _, _ = current in ParamodulationSuccess (Some proof, env) - ) else ( + ) else ( debug_print (lazy "\n================================================"); debug_print (lazy (Printf.sprintf "selected: %s %s" @@ -1582,10 +1706,14 @@ and given_clause_aux dbd env goals theorems passive active = (** given-clause algorithm with full reduction strategy *) let rec given_clause_fullred dbd env goals theorems passive active = - let goals = simplify_goals env goals ~passive active in + let goals = simplify_goals env goals ~passive active in + let _,context,_ = env in let ok, goals = activate_goal goals in (* let theorems = simplify_theorems env theorems ~passive active in *) if ok then + let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in + let _, _, t = List.hd (snd (List.hd (fst goals))) in + let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in (* let _ = *) (* debug_print *) (* (lazy *) @@ -1607,7 +1735,21 @@ let rec given_clause_fullred dbd env goals theorems passive active = | (_, [proof, _, _])::_ -> Some proof | _ -> assert false in - ParamodulationSuccess (proof, env) + ( prerr_endline "esco qui"; + let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + (fst active)))) in + let sp = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + (let x,y,_ = passive in (fst x)@(fst y)))) in + prerr_endline s; + prerr_endline sp; + ParamodulationSuccess (proof, env)) else given_clause_fullred_aux dbd env goals theorems passive active else @@ -1628,8 +1770,26 @@ let rec given_clause_fullred dbd env goals theorems passive active = else given_clause_fullred_aux dbd env goals theorems passive active and given_clause_fullred_aux dbd env goals theorems passive active = + prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^ + " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ + " #ACTIVES: " ^ string_of_int (size_of_active active) ^ + " #PASSIVES: " ^ string_of_int (size_of_passive passive)); + if (size_of_active active) mod 54 = 0 then + (let s = Printf.sprintf "actives:\n%s\n" + (String.concat "\n" + ((List.map + (fun (s, e) -> (string_of_sign s) ^ " " ^ + (string_of_equality ~env e)) + (fst active)))) in + let sp = Printf.sprintf "passives:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + (let x,y,_ = passive in (fst x)@(fst y)))) in + prerr_endline s; + prerr_endline sp); let time1 = Unix.gettimeofday () in - + let (_,context,_) = env in let selection_estimate = get_selection_estimate () in let kept = size_of_passive passive in let passive = @@ -1658,6 +1818,10 @@ and given_clause_fullred_aux dbd env goals theorems passive active = given_clause_fullred dbd env goals theorems passive active | false -> let (sign, current), passive = select env (fst goals) passive active in + let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in + prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^ + string_of_equality ~env current); + (* (CicPp.pp (Inference.term_of_equality current) names));*) let time1 = Unix.gettimeofday () in let res = forward_simplify env (sign, current) ~passive active in let time2 = Unix.gettimeofday () in @@ -1681,9 +1845,22 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let t1 = Unix.gettimeofday () in let new' = infer env sign current active in + let _ = + match new' with + | neg, pos -> + debug_print + (lazy + (Printf.sprintf "new' (senza semplificare):\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))))) + in let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); - let active = if is_identity env current then active else @@ -1703,19 +1880,40 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let active, passive, newa, retained = backward_simplify env new' ~passive active in let t2 = Unix.gettimeofday () in - backward_simpl_time := !backward_simpl_time +. (t2 -. t1); + backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa, retained with | None, None -> active, passive, new' | Some (n, p), None | None, Some (n, p) -> let nn, np = new' in + if Utils.debug_metas then + ignore ( + List.map (fun x -> Indexing.check_target context x "simplify1")n; + List.map (fun x -> Indexing.check_target context x "simplify2")p); simplify (nn @ n, np @ p) active passive | Some (n, p), Some (rn, rp) -> let nn, np = new' in simplify (nn @ n @ rn, np @ p @ rp) active passive in let active, passive, new' = simplify new' active passive in - +(* pessima prova + let new1 = prova env new' active in + let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in + let _ = + match new1 with + | neg, pos -> + debug_print + (lazy + (Printf.sprintf "new1:\n%s\n" + (String.concat "\n" + ((List.map + (fun e -> "Negative " ^ + (string_of_equality ~env e)) neg) @ + (List.map + (fun e -> "Positive " ^ + (string_of_equality ~env e)) pos))))) + in +end prova *) let k = size_of_passive passive in if k < (kept - 1) then processed_clauses := !processed_clauses + (kept - 1 - k); @@ -1892,7 +2090,8 @@ let main dbd full term metasenv ugraph = in (*try*) let goal = Inference.BasicProof new_meta_goal, [], goal in - let equalities = simplify_equalities env (equalities@library_equalities) in + let equalities = simplify_equalities env + (equalities@library_equalities) in let active = make_active () in let passive = make_passive [] equalities in Printf.printf "\ncurrent goal: %s\n" @@ -1952,23 +2151,29 @@ let main dbd full term metasenv ugraph = | ParamodulationSuccess (None, env) -> Printf.printf "Success, but no proof?!?\n\n" in - Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ + if Utils.time then + begin + prerr_endline + ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^ "forward_simpl_new_time: %.9f\n" ^^ "backward_simpl_time: %.9f\n") - !infer_time !forward_simpl_time !forward_simpl_new_time - !backward_simpl_time; - Printf.printf "passive_maintainance_time: %.9f\n" - !passive_maintainance_time; - Printf.printf " successful unification/matching time: %.9f\n" - !Indexing.match_unif_time_ok; - Printf.printf " failed unification/matching time: %.9f\n" - !Indexing.match_unif_time_no; - Printf.printf " indexing retrieval time: %.9f\n" - !Indexing.indexing_retrieval_time; - Printf.printf " demodulate_term.build_newtarget_time: %.9f\n" - !Indexing.build_newtarget_time; - Printf.printf "derived %d clauses, kept %d clauses.\n" - !derived_clauses !kept_clauses; + !infer_time !forward_simpl_time !forward_simpl_new_time + !backward_simpl_time) ^ + (Printf.sprintf "beta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "passive_maintainance_time: %.9f\n" + !passive_maintainance_time) ^ + (Printf.sprintf " successful unification/matching time: %.9f\n" + !Indexing.match_unif_time_ok) ^ + (Printf.sprintf " failed unification/matching time: %.9f\n" + !Indexing.match_unif_time_no) ^ + (Printf.sprintf " indexing retrieval time: %.9f\n" + !Indexing.indexing_retrieval_time) ^ + (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n" + !Indexing.build_newtarget_time) ^ + (Printf.sprintf "derived %d clauses, kept %d clauses.\n" + !derived_clauses !kept_clauses)) + end (* with exc -> print_endline ("EXCEPTION: " ^ (Printexc.to_string exc)); @@ -1982,6 +2187,7 @@ and default_width = !maxwidth;; let reset_refs () = maxmeta := 0; + Indexing.local_max := 100; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -1995,6 +2201,8 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; + Indexing.beta_expand_time := 0.; + Inference.metas_of_proof_time := 0.; ;; let saturate @@ -2030,7 +2238,7 @@ let saturate let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; - let equalities = simplify_equalities env (equalities@library_equalities) in + let equalities = simplify_equalities env (equalities@library_equalities) in debug_print (lazy (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); @@ -2131,15 +2339,25 @@ let saturate let tall = fs_time_info.build_all in let tdemodulate = fs_time_info.demodulate in let tsubsumption = fs_time_info.subsumption in - debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); - debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall)); - debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate)); - debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption)); - debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time)); - debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time)); - debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time)); - debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time)); - debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time)); + if Utils.time then + begin + prerr_endline ( + (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^ + (Printf.sprintf "\ntall: %.9f" tall) ^ + (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ + (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ + (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ + (Printf.sprintf "\nbeta_expand_time: %.9f\n" + !Indexing.beta_expand_time) ^ + (Printf.sprintf "\nmetas_of_proof: %.9f\n" + !Inference.metas_of_proof_time) ^ + (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ + (Printf.sprintf "\nforward_simpl_new_times: %.9f" + !forward_simpl_new_time) ^ + (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^ + (Printf.sprintf "\npassive_maintainance_time: %.9f" + !passive_maintainance_time)) + end; newstatus | _ -> raise (ProofEngineTypes.Fail (lazy "NO proof found")) @@ -2190,7 +2408,7 @@ let retrieve_and_print dbd term metasenv ugraph = (* (string_of_equality e) *) ) equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); + debug_print (lazy "RETR: SIMPLYFYING EQUALITIES..."); let rec simpl e others others_simpl = let (u, e) = e in let active = List.map (fun (u, e) -> (Positive, e)) @@ -2331,7 +2549,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = let goalterm = Cic.Meta (metano,irl) in let initgoal = Inference.BasicProof goalterm, [], ty in let env = (metasenv, context, CicUniv.empty_ugraph) in - let equalities = simplify_equalities env (equalities@library_equalities) in + let equalities = simplify_equalities env (equalities@library_equalities) in let table = List.fold_left (fun tbl eq -> Indexing.index tbl eq)