some optimizations...

diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile
index be59fc135aad2d9fe0f972c677b2d90f79afd6b2..f16094a17c7e96af9907c21f146d227b46f40404 100644 (file)
--- a/helm/ocaml/paramodulation/Makefile
+++ b/helm/ocaml/paramodulation/Makefile
@@ -34,15 +34,18 @@ DEPOBJS = \
        path_indexing.ml \
        indexing.ml \
        saturation.ml \
-       test_path_indexing.ml
+       discrimination_tree.ml \
+       test_indexing.ml
 
 TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \
        path_indexing.cmo \
+       discrimination_tree.cmo \
        indexing.cmo \
        saturation.cmo
 TESTOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \
        path_indexing.cmo \
-       test_path_indexing.cmo
+       discrimination_tree.cmo \
+       test_indexing.cmo
 # REGTESTOBJS = $(TESTOBJS) regtest.cmo
 # TESTLIBOBJS = $(TESTOBJS) testlibrary.cmo
 
@@ -57,7 +60,7 @@ saturation: $(TOPLEVELOBJS) $(LIBRARIES)
 saturation.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT)
        $(OCAMLOPT) -thread -linkpkg -o $@ $(TOPLEVELOBJS:.cmo=.cmx)
 
-test_path_indexing: $(TESTOBJS) $(TEST_LIBRARIES)
+test_indexing: $(TESTOBJS) $(TEST_LIBRARIES)
        $(OCAMLC) -linkpkg -o $@ $(TESTOBJS)
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 84559b22247fdde62f74f2485562eb34fef34cbb..5607ca3db7b85e2ef3c80cf434445c2ff36f6584 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -1,61 +1,41 @@
 
-let head_of_term = function
-  | Cic.Appl (hd::tl) -> hd
-  | t -> t
-;;
+type retrieval_mode = Matching | Unification;;
 
 
-(*
 let empty_table () =
-  Hashtbl.create 10
+  Path_indexing.PSTrie.empty
 ;;
 
-
-let index table eq =
-  let _, (_, l, r, ordering), _, _ = eq in
-  let hl = head_of_term l in
-  let hr = head_of_term r in
-  let index x pos = 
-    let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    Hashtbl.replace table x ((pos, eq)::x_entry)
-  in
-  let _ = 
-    match ordering with
-    | Utils.Gt ->
-        index hl Utils.Left
-    | Utils.Lt ->
-        index hr Utils.Right
-    | _ -> index hl Utils.Left; index hr Utils.Right
+let index = Path_indexing.index
+and remove_index = Path_indexing.remove_index
+and in_index = Path_indexing.in_index;;
+  
+let get_candidates mode trie term =
+  let s = 
+    match mode with
+    | Matching -> Path_indexing.retrieve_generalizations trie term
+    | Unification -> Path_indexing.retrieve_unifiables trie term
   in
-(*   index hl Utils.Left; *)
-(*   index hr Utils.Right; *)
-  table
+  Path_indexing.PosEqSet.elements s
 ;;
 
 
-let remove_index table eq =
-  let _, (_, l, r, ordering), _, _ = eq in
-  let hl = head_of_term l
-  and hr = head_of_term r in
-  let remove_index x pos =
-    let x_entry = try Hashtbl.find table x with Not_found -> [] in
-    let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in
-    Hashtbl.replace table x newentry
-  in
-  remove_index hl Utils.Left;
-  remove_index hr Utils.Right;
-  table
+(*
+let empty_table () =
+  Discrimination_tree.DiscriminationTree.empty
 ;;
-*)
 
+let index = Discrimination_tree.index
+and remove_index = Discrimination_tree.remove_index
+and in_index = Discrimination_tree.in_index;;
 
-let empty_table () =
-  Path_indexing.PSTrie.empty
+let get_candidates mode tree term =
+  match mode with
+  | Matching -> Discrimination_tree.retrieve_generalizations tree term
+  | Unification -> Discrimination_tree.retrieve_unifiables tree term
 ;;
+*)
 
-let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index;;
-  
 
 let rec find_matches metasenv context ugraph lift_amount term =
   let module C = Cic in
@@ -157,27 +137,6 @@ let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
 ;;
 
 
-type retrieval_mode = Matching | Unification;;
-
-(*
-let get_candidates mode table term =
-  try Hashtbl.find table (head_of_term term) with Not_found -> []
-;;
-*)
-
-
-let get_candidates mode trie term =
-  let s = 
-    match mode with
-    | Matching ->
-        Path_indexing.retrieve_generalizations trie term
-    | Unification ->
-        Path_indexing.retrieve_unifiables trie term
-  in
-  Path_indexing.PosEqSet.elements s
-;;
-
-
 let subsumption env table target =
   let _, (ty, tl, tr, _), tmetas, _ = target in
   let metasenv, context, ugraph = env in

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 00e543c2e6d182e3f0cf05b4baa12b783aef99d6..e79d78e846cac9677d6280cba0f78cf3a6e45b07 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1214,3 +1214,25 @@ let subsumption env target source =
     );
     res
 ;;
+
+
+let extract_differing_subterms t1 t2 =
+  let module C = Cic in
+  let rec aux t1 t2 =
+    match t1, t2 with
+    | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
+        [(t1, t2)]
+    | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
+        let res = List.concat (List.map2 aux tl1 tl2) in
+        if h1 <> h2 then
+          if res = [] then [(h1, h2)] else [(t1, t2)]
+        else
+          if List.length res > 1 then [(t1, t2)] else res
+    | t1, t2 ->
+        if t1 <> t2 then [(t1, t2)] else []
+  in
+  let res = aux t1 t2 in
+  match res with
+  | hd::[] -> Some hd
+  | _ -> None
+;;

diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 0cc0fcb708d9f51be2a844a04fece6b5656e433a..5ced528bb81055550961d65e489068bded9c49cf 100644 (file)
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -79,3 +79,6 @@ val subsumption: environment -> equality -> equality -> bool
 val metas_of_term: Cic.term -> int list
 
 val fix_metas: int -> equality -> int * equality
+
+val extract_differing_subterms:
+  Cic.term -> Cic.term -> (Cic.term * Cic.term) option

diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml
index 87e917fff79b5c176401225a1cc757f20f64967c..bc9bc01f1608fa42d36c369a57808496364a6b08 100644 (file)
--- a/helm/ocaml/paramodulation/path_indexing.ml
+++ b/helm/ocaml/paramodulation/path_indexing.ml
@@ -160,6 +160,22 @@ let remove_index trie equality =
 ;;
 
 
+let in_index trie equality =
+  let _, (_, l, r, ordering), _, _ = equality in
+  let psl = path_strings_of_term 0 l
+  and psr = path_strings_of_term 0 r in
+  let meta_convertibility = Inference.meta_convertibility_eq equality in
+  let ok ps =
+    try
+      let set = PSTrie.find ps trie in
+      PosEqSet.exists (fun (p, e) -> meta_convertibility e) set
+    with Not_found ->
+      false
+  in
+  (List.exists ok psl) || (List.exists ok psr)
+;;
+
+
 let head_of_term = function
   | Cic.Appl (hd::tl) -> hd
   | term -> term

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index c45124338bde930c92517a31d8a65c713e0411d2..634df11ffb4a766f6ca18080f55197dcd815b3dd 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -1,6 +1,7 @@
 open Inference;;
 open Utils;;
 
+
 (* profiling statistics... *)
 let infer_time = ref 0.;;
 let forward_simpl_time = ref 0.;;
@@ -14,6 +15,7 @@ let elapsed_time = ref 0.;;
 let maximal_retained_equality = ref None;;
 
 (* equality-selection related globals *)
+let use_fullred = ref false;;
 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
 let weight_age_counter = ref !weight_age_ratio;;
 let symbols_ratio = ref 0;;
@@ -93,7 +95,11 @@ let select env passive (active, _) =
           (Negative, hd),
           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
       | [], hd::tl ->
-          let passive_table = Indexing.remove_index passive_table hd in
+          let passive_table =
+            Indexing.remove_index passive_table hd
+(*             if !use_fullred then Indexing.remove_index passive_table hd *)
+(*             else passive_table *)
+          in
           (Positive, hd),
           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
       | _, _ -> assert false
@@ -134,17 +140,26 @@ let select env passive (active, _) =
           let _, current = EqualitySet.fold f pos_set initial in
 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 (*             (string_of_equality ~env current); *)
-          let passive_table = Indexing.remove_index passive_table current in
+          let passive_table =
+            Indexing.remove_index passive_table current
+(*             if !use_fullred then Indexing.remove_index passive_table current *)
+(*             else passive_table *)
+          in
           (Positive, current),
           (([], neg_set),
            (remove current pos_list, EqualitySet.remove current pos_set),
            passive_table)
       | _ ->
           let current = EqualitySet.min_elt pos_set in
+          let passive_table =
+            Indexing.remove_index passive_table current
+(*             if !use_fullred then Indexing.remove_index passive_table current *)
+(*             else passive_table *)
+          in
           let passive =
             (neg_list, neg_set),
             (remove current pos_list, EqualitySet.remove current pos_set),
-            Indexing.remove_index passive_table current
+            passive_table
           in
           (Positive, current), passive
     )
@@ -157,6 +172,8 @@ let select env passive (active, _) =
           (neg_list, neg_set),
           (remove current pos_list, EqualitySet.remove current pos_set),
           Indexing.remove_index passive_table current
+(*           if !use_fullred then Indexing.remove_index passive_table current *)
+(*           else passive_table *)
         in
         (Positive, current), passive
       else
@@ -174,10 +191,18 @@ let make_passive neg pos =
   let set_of equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
   in
-  let table = Indexing.empty_table () in
+  let table =
+      List.fold_left (fun tbl e -> Indexing.index tbl e)
+        (Indexing.empty_table ()) pos
+(*     if !use_fullred then *)
+(*       List.fold_left (fun tbl e -> Indexing.index tbl e) *)
+(*         (Indexing.empty_table ()) pos *)
+(*     else *)
+(*       Indexing.empty_table () *)
+  in
   (neg, set_of neg),
   (pos, set_of pos),
-  List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+  table
 ;;
 
 
@@ -191,12 +216,19 @@ let add_to_passive passive (new_neg, new_pos) =
   let ok set equality = not (EqualitySet.mem equality set) in
   let neg = List.filter (ok neg_set) new_neg
   and pos = List.filter (ok pos_set) new_pos in
+  let table =
+      List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+(*     if !use_fullred then *)
+(*       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
+(*     else *)
+(*       table *)
+  in
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
   in
   (neg @ neg_list, add neg_set neg),
   (pos_list @ pos, add pos_set pos),
-  List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
+  table
 ;;
 
 
@@ -218,17 +250,6 @@ let prune_passive howmany (active, _) passive =
   let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
   and in_age = int_of_float (howmany /. (ratio +. 1.)) in 
   Printf.printf "in_weight: %d, in_age: %d\n" in_weight in_age;
-(*   let rec pickw w s = *)
-(*     if w > 0 then  *)
-(*       try *)
-(*         let e = EqualitySet.min_elt s in *)
-(*         let w, s' = pickw (w-1) (EqualitySet.remove e s) in *)
-(*         w, EqualitySet.add e s' *)
-(*       with Not_found -> *)
-(*         w, s *)
-(*     else *)
-(*       0, EqualitySet.empty *)
-(*   in *)
   let symbols, card =
     match active with
     | (Negative, e)::_ ->
@@ -311,7 +332,13 @@ let prune_passive howmany (active, _) passive =
     maximal_retained_equality := Some (EqualitySet.max_elt ps);
   let tbl =
     EqualitySet.fold
-      (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) in
+      (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
+(*     if !use_fullred then *)
+(*       EqualitySet.fold *)
+(*         (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
+(*     else *)
+(*       tbl *)
+  in
   (nl, ns), (pl, ps), tbl  
 ;;
 
@@ -375,14 +402,15 @@ 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 = active_list @ pl in
-  let rec find_duplicate sign current = function
-    | [] -> false
-    | (s, eq)::tl when s = sign ->
-        if meta_convertibility_eq current eq then true
-        else find_duplicate sign current tl
-    | _::tl -> find_duplicate sign current tl
-  in
+  let all = if pl = [] then active_list else active_list @ pl in
+
+(*   let rec find_duplicate sign current = function *)
+(*     | [] -> false *)
+(*     | (s, eq)::tl when s = sign -> *)
+(*         if meta_convertibility_eq current eq then true *)
+(*         else find_duplicate sign current tl *)
+(*     | _::tl -> find_duplicate sign current tl *)
+(*   in *)
   let demodulate table current = 
     let newmeta, newcurrent =
       Indexing.demodulation !maxmeta env table current in
@@ -403,11 +431,24 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   in
   match res with
   | None -> None
-  | Some (s, c) ->
-      if find_duplicate s c all then
+  | Some (Negative, c) ->
+      let ok = not (
+        List.exists
+          (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
+          all)
+      in
+      if ok then res else None
+  | Some (Positive, c) ->
+      if Indexing.in_index active_table c then
         None
       else
-        res
+        match passive_table with
+        | None -> res
+        | Some passive_table ->
+            if Indexing.in_index passive_table c then None else res
+
+(*   | Some (s, c) -> if find_duplicate s c all then None else res *)
+
 (*         if s = Utils.Negative then *)
 (*           res *)
 (*         else *)
@@ -490,14 +531,14 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   in
   let new_pos = EqualitySet.elements new_pos_set in
 
-  let subs =
-    match passive_table with
-    | None ->
-        (fun e -> not (Indexing.subsumption env active_table e))
-    | Some passive_table ->
-        (fun e -> not ((Indexing.subsumption env active_table e) ||
-                         (Indexing.subsumption env passive_table e)))
-  in
+(*   let subs = *)
+(*     match passive_table with *)
+(*     | None -> *)
+(*         (fun e -> not (Indexing.subsumption env active_table e)) *)
+(*     | Some passive_table -> *)
+(*         (fun e -> not ((Indexing.subsumption env active_table e) || *)
+(*                          (Indexing.subsumption env passive_table e))) *)
+(*   in *)
 
   let t1 = Unix.gettimeofday () in
 
@@ -514,7 +555,17 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let t2 = Unix.gettimeofday () in
   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
 
-  new_neg, new_pos
+  let is_duplicate =
+    match passive_table with
+    | None -> (fun e -> not (Indexing.in_index active_table e))
+    | Some passive_table ->
+        (fun e -> not ((Indexing.in_index active_table e) ||
+                         (Indexing.in_index passive_table e)))
+  in
+  new_neg, List.filter is_duplicate new_pos
+
+(*   new_neg, new_pos *)
+
 (*   let res = *)
 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
@@ -611,7 +662,9 @@ let backward_simplify env new' ?passive active =
 
 let get_selection_estimate () =
   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
-  !processed_clauses * (int_of_float (!time_limit /. !elapsed_time))
+  int_of_float (
+    ceil ((float_of_int !processed_clauses) *.
+            (!time_limit /. !elapsed_time -. 1.)))
 ;;
 
   
@@ -663,7 +716,7 @@ let rec given_clause env passive active =
               Success (proof, env)
             else 
               let t1 = Unix.gettimeofday () in
-              let new' = forward_simplify_new env new' active in
+              let new' = forward_simplify_new env new' (* ~passive *) active in
               let t2 = Unix.gettimeofday () in
               let _ =
                 forward_simpl_time := !forward_simpl_time +. (t2 -. t1)
@@ -900,7 +953,10 @@ let main () =
     let start = Unix.gettimeofday () in
     print_endline "GO!";
     start_time := Unix.gettimeofday ();
-    let res = !given_clause_ref env passive active in
+    let res =
+      (if !use_fullred then given_clause_fullred else given_clause)
+        env passive active
+    in
     let finish = Unix.gettimeofday () in
     match res with
     | Failure ->
@@ -932,7 +988,7 @@ let _ =
   and set_conf f = configuration_file := f
   and set_lpo () = Utils.compare_terms := lpo
   and set_kbo () = Utils.compare_terms := nonrec_kbo
-  and set_fullred () = given_clause_ref := given_clause_fullred
+  and set_fullred () = use_fullred := true
   and set_time_limit v = time_limit := float_of_int v
   in
   Arg.parse [