X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Fsaturation.ml;h=eb4a35d6c443f823e2b94438b4c4f13f6cc17549;hb=727d6939c3f3ff1769ac1d11cad11d2e06433295;hp=8e67bc7a05cee8147a2f0a774f56f0fe7073d12e;hpb=db57b08d789de234c152c3f2a665000311b7335d;p=helm.git

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 8e67bc7a0..eb4a35d6c 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open Inference;;
 open Utils;;
 
@@ -55,6 +57,7 @@ let symbols_counter = ref 0;;
 
 (* non-recursive Knuth-Bendix term ordering by default *)
 Utils.compare_terms := Utils.nonrec_kbo;; 
+(* Utils.compare_terms := Utils.ao;; *)
 
 (* statistics... *)
 let derived_clauses = ref 0;;
@@ -141,7 +144,7 @@ let select env goals passive (active, _) =
           (* Negatives aren't indexed, no need to remove them... *)
           (Negative, hd),
           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
-      | [], hd::tl ->
+      | [], (hd:EqualitySet.elt)::tl ->
           let passive_table =
             Indexing.remove_index passive_table hd
           in
@@ -220,8 +223,7 @@ let make_passive neg pos =
     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
   in
   let table =
-      List.fold_left (fun tbl e -> Indexing.index tbl e)
-        (Indexing.empty_table ()) pos
+      List.fold_left (fun tbl e -> Indexing.index tbl e) Indexing.empty pos
   in
   (neg, set_of neg),
   (pos, set_of pos),
@@ -230,7 +232,7 @@ let make_passive neg pos =
 
 
 let make_active () =
-  [], Indexing.empty_table () 
+  [], Indexing.empty
 ;;
 
 
@@ -363,7 +365,7 @@ 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 ())
+      (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
   in
   (nl, ns), (pl, ps), tbl  
 ;;
@@ -397,7 +399,7 @@ let infer env sign current (active_list, active_table) =
               let neg, pos = infer_positive table tl in
               neg, res @ pos
         in
-        let curr_table = Indexing.index (Indexing.empty_table ()) current in
+        let curr_table = Indexing.index Indexing.empty current in
         let neg, pos = infer_positive curr_table active_list in
         neg, res @ pos
   in
@@ -654,7 +656,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
          ) 
          else
            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
-      active_list ([], Indexing.empty_table ()),
+      active_list ([], Indexing.empty),
     List.fold_right
       (fun (s, eq) (n, p) ->
          if (s <> Negative) && (is_identity env eq) then (
@@ -691,7 +693,7 @@ let backward_simplify_passive env new_pos new_table min_weight passive =
   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
   let passive_table =
     List.fold_left
-      (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
+      (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
   in
   match newn, newp with
   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
@@ -705,7 +707,7 @@ let backward_simplify env new' ?passive active =
       (fun (l, t, w) e ->
          let ew, _, _, _, _ = e in
          (Positive, e)::l, Indexing.index t e, min ew w)
-      ([], Indexing.empty_table (), 1000000) (snd new')
+      ([], Indexing.empty, 1000000) (snd new')
   in
   let active, newa =
     backward_simplify_active env new_pos new_table min_weight active in
@@ -1697,6 +1699,76 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
 ;;
 
 
+let rec saturate_equations env goal accept_fun passive active =
+  elapsed_time := Unix.gettimeofday () -. !start_time;
+  if !elapsed_time > !time_limit then
+    (active, passive)
+  else
+    let (sign, current), passive = select env [1, [goal]] passive active in
+    let res = forward_simplify env (sign, current) ~passive active in
+    match res with
+    | None ->
+        saturate_equations env goal accept_fun passive active
+    | Some (sign, current) ->
+        assert (sign = Positive);
+        debug_print
+          (lazy "\n================================================");
+        debug_print (lazy (Printf.sprintf "selected: %s %s"
+                             (string_of_sign sign)
+                             (string_of_equality ~env current)));
+        let new' = infer env sign current active in
+        let active =
+          if is_identity env current then active
+          else
+            let al, tbl = active in
+            al @ [(sign, current)], Indexing.index tbl current
+        in
+        let rec simplify new' active passive =
+          let new' = forward_simplify_new env new' ~passive active in
+          let active, passive, newa, retained =
+            backward_simplify env new' ~passive active in
+          match newa, retained with
+          | None, None -> active, passive, new'
+          | Some (n, p), None
+          | None, Some (n, p) ->
+              let nn, np = new' in
+              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
+        let _ =
+          debug_print
+            (lazy
+               (Printf.sprintf "active:\n%s\n"
+                  (String.concat "\n"
+                     ((List.map
+                         (fun (s, e) -> (string_of_sign s) ^ " " ^
+                            (string_of_equality ~env e))
+                         (fst active))))))
+        in
+        let _ =
+          match new' with
+          | neg, pos ->
+              debug_print
+                (lazy
+                   (Printf.sprintf "new':\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 new' = match new' with _, pos -> [], List.filter accept_fun pos in
+        let passive = add_to_passive passive new' in
+        saturate_equations env goal accept_fun passive active
+;;
+  
+
+
 
 let main dbd full term metasenv ugraph =
   let module C = Cic in
@@ -1772,7 +1844,7 @@ let main dbd full term metasenv ugraph =
         let tbl =
           List.fold_left
             (fun t (_, e) -> Indexing.index t e)
-            (Indexing.empty_table ()) active
+             Indexing.empty active
         in
         let res = forward_simplify env e (active, tbl) in
         match others with
@@ -1949,7 +2021,7 @@ let saturate
         let tbl =
           List.fold_left
             (fun t (_, e) -> Indexing.index t e)
-            (Indexing.empty_table ()) active
+             Indexing.empty active
         in
         let res = forward_simplify env e (active, tbl) in
         match others with
@@ -2144,7 +2216,7 @@ let retrieve_and_print dbd term metasenv ugraph =
           let tbl =
             List.fold_left
               (fun t (_, e) -> Indexing.index t e)
-              (Indexing.empty_table ()) active
+              Indexing.empty active
           in
           let res = forward_simplify env (Positive, e) (active, tbl) in
             match others with
@@ -2183,3 +2255,125 @@ let retrieve_and_print dbd term metasenv ugraph =
 	(lazy
            (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
 ;;
+
+
+let main_demod_equalities dbd term metasenv ugraph =
+  let module C = Cic in
+  let module T = CicTypeChecker in
+  let module PET = ProofEngineTypes in
+  let module PP = CicPp in
+  let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+  let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+  let proof, goals = status in
+  let goal' = List.nth goals 0 in
+  let _, metasenv, meta_proof, _ = proof in
+  let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+  let eq_indexes, equalities, maxm = find_equalities context proof in
+  let lib_eq_uris, library_equalities, maxm =
+    find_library_equalities dbd context (proof, goal') (maxm+2)
+  in
+  let library_equalities = List.map snd library_equalities in
+  maxmeta := maxm+2; (* TODO ugly!! *)
+  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+  let new_meta_goal, metasenv, type_of_goal =
+    let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+    debug_print
+      (lazy
+         (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+            (CicPp.ppterm ty)));
+    Cic.Meta (maxm+1, irl),
+    (maxm+1, context, ty)::metasenv,
+    ty
+  in
+  let env = (metasenv, context, ugraph) in
+  let t1 = Unix.gettimeofday () in
+  try
+    let goal = Inference.BasicProof new_meta_goal, [], goal in
+    let equalities =
+      let equalities = equalities @ library_equalities in
+      debug_print
+        (lazy 
+           (Printf.sprintf "equalities:\n%s\n"
+              (String.concat "\n"
+                 (List.map string_of_equality equalities))));
+      debug_print (lazy "SIMPLYFYING EQUALITIES...");
+      let rec simpl e others others_simpl =
+        let active = others @ others_simpl in
+        let tbl =
+          List.fold_left
+            (fun t (_, e) -> Indexing.index t e)
+            Indexing.empty active
+        in
+        let res = forward_simplify env e (active, tbl) in
+        match others with
+        | hd::tl -> (
+            match res with
+            | None -> simpl hd tl others_simpl
+            | Some e -> simpl hd tl (e::others_simpl)
+          )
+        | [] -> (
+            match res with
+            | None -> others_simpl
+            | Some e -> e::others_simpl
+          )
+      in
+      match equalities with
+      | [] -> []
+      | hd::tl ->
+          let others = List.map (fun e -> (Positive, e)) tl in
+          let res =
+            List.rev (List.map snd (simpl (Positive, hd) others []))
+          in
+          debug_print
+            (lazy
+               (Printf.sprintf "equalities AFTER:\n%s\n"
+                  (String.concat "\n"
+                     (List.map string_of_equality res))));
+          res
+    in
+    let active = make_active () in
+    let passive = make_passive [] equalities in
+    Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
+    Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+    Printf.printf "\nequalities:\n%s\n"
+      (String.concat "\n"
+         (List.map
+            (string_of_equality ~env) equalities));
+    print_endline "--------------------------------------------------";
+    let start = Unix.gettimeofday () in
+    print_endline "GO!";
+    start_time := Unix.gettimeofday ();
+    if !time_limit < 1. then time_limit := 60.;    
+    let ra, rp =
+      saturate_equations env goal (fun e -> true) passive active
+    in
+    let finish = Unix.gettimeofday () in
+
+    let initial =
+      List.fold_left (fun s e -> EqualitySet.add e s)
+        EqualitySet.empty equalities
+    in
+    let addfun s e =
+      if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+    in
+
+    let passive =
+      match rp with
+      | (n, _), (p, _), _ ->
+          EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+    in
+    let active =
+      let l = List.map snd (fst ra) in
+      EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+    in
+    Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+(*       (String.concat "\n" (List.map (string_of_equality ~env) active)) *)
+      (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active))
+(*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+      (String.concat "\n"
+         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
+    print_newline ();
+  with e ->
+    debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+;;