fixed infer_goal, added simplification before inferring with current

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index bb1b3a853515d22c49fecc0e9b43e944e0b55d17..81c2a15f1920d2cd7e496643cf912d6042432bc3 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -901,6 +901,17 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
               
+let pp_goal_set msg goals names = 
+  let active_goals, passive_goals = goals in
+  prerr_endline ("////" ^ msg);
+  prerr_endline ("ACTIVE G: " ^
+    (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+    active_goals)));
+  prerr_endline ("PASSIVE G: " ^
+    (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
+    passive_goals)))
+;;
+
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
 (*
   let names = names_of_context ctx in
@@ -959,7 +970,7 @@ let rec check goal = function
       | (Some p) as ok  -> ok
 ;;
   
-let simplify_goal_set env goals passive active = 
+let simplify_goal_set env goals ?passive active = 
   let active_goals, passive_goals = goals in 
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
@@ -967,7 +978,7 @@ let simplify_goal_set env goals passive active =
   let simplified =
     List.fold_left
       (fun acc goal -> 
-        match simplify_goal env goal ~passive active with 
+        match simplify_goal env goal ?passive active with 
         | changed, g -> 
             if changed then prerr_endline "???????????????cambiato ancora";
             if find g acc then acc else g::acc)
@@ -1000,26 +1011,28 @@ let check_if_goals_set_is_solved env active goals =
 let infer_goal_set env active goals = 
   let active_goals, passive_goals = goals in
   let rec aux = function
-    | [] -> goals
+    | [] -> active_goals, []
     | hd::tl ->
         let changed,selected = simplify_goal env hd active in
         if changed then
           prerr_endline ("--------------- goal semplificato");
         let (_,_,t1) = selected in
-        if (List.exists 
-             (fun (_,_,t) -> 
-                Equality.meta_convertibility t t1) 
-              active_goals) then aux tl
-        else
-        let passive_goals = tl in
-        let new_passive_goals =
-          if Utils.metas_of_term t1 = [] then passive_goals
-          else 
-            let new' = 
-               Indexing.superposition_left env (snd active) selected in
-            passive_goals @ new'
+        let already_in = 
+          List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) 
+              active_goals
         in
-        selected::active_goals, new_passive_goals
+        if already_in then 
+             aux tl
+          else
+            let passive_goals = tl in
+            let new_passive_goals =
+              if Utils.metas_of_term t1 = [] then passive_goals
+              else 
+                let new' = 
+                   Indexing.superposition_left env (snd active) selected in
+                passive_goals @ new'
+            in
+            selected::active_goals, new_passive_goals
   in 
   aux passive_goals
 ;;
@@ -1053,8 +1066,11 @@ let infer_goal_set env active goals =
 
 let infer_goal_set_with_current env current goals = 
   let active_goals, passive_goals = goals in
-  let _,table,_ = build_table [current] in
-  active_goals,
+  let l,table,_  = build_table [current] in
+  let active_goals, _ = 
+    simplify_goal_set env goals (l,table)
+  in
+  active_goals, 
   List.fold_left 
     (fun acc g ->
       let new' = Indexing.superposition_left env table g in
@@ -1152,6 +1168,11 @@ let given_clause
                    prerr_endline (Printf.sprintf  "Current goal = %s\n"
                     (CicPp.pp g names))) 
                  (fst goals);
+                List.iter                 
+                 (fun _,_,g -> 
+                   prerr_endline (Printf.sprintf  "Passive goal = %s\n"
+                    (CicPp.pp g names))) 
+                 (snd goals);
                 prerr_endline (Printf.sprintf  "Selected = %s\n"
                   (Equality.string_of_equality ~env current))
               in
@@ -1194,7 +1215,7 @@ let given_clause
                   let goals = 
                     let a,b,_ = build_table new' in
                     let _ = <:start<simplify_goal_set new>> in
-                    let rc = simplify_goal_set env goals passive (a,b) in
+                    let rc = simplify_goal_set env goals ~passive (a,b) in
                     let _ = <:stop<simplify_goal_set new>> in
                     rc
                   in
@@ -1225,6 +1246,8 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
             let al, tbl = active in
             al @ [current], Indexing.index tbl current
         in
+        (* alla fine new' contiene anche le attive semplificate!
+         * quindi le aggiungo alle passive insieme alle new *)
         let rec simplify new' active passive =
           let new' = forward_simplify_new eq_uri env new' ~passive active in
           let active, passive, newa, retained, pruned =
@@ -1461,6 +1484,7 @@ let eq_and_ty_of_goal = function
 ;;
 
 let saturate 
+    caso_strano 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
   reset_refs ();
@@ -1481,7 +1505,7 @@ let saturate
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
-      find_library_equalities dbd context (proof, goalno) (maxm+2)
+      find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
     in
     let library_equalities = List.map snd library_equalities in
     let t2 = Unix.gettimeofday () in
@@ -1675,7 +1699,7 @@ let retrieve_and_print dbd term metasenv ugraph =
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
   let lib_eq_uris, library_equalities, maxm =
-    find_library_equalities dbd context (proof, goal') (maxm+2) in
+    find_library_equalities false dbd context (proof, goal') (maxm+2) in
   let t2 = Unix.gettimeofday () in
   maxmeta := maxm+2;
   let equalities = (* equalities @ *) library_equalities in
@@ -1753,7 +1777,7 @@ let main_demod_equalities dbd term metasenv ugraph =
   let eq_uri = eq_of_goal goal 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)
+    find_library_equalities false dbd context (proof, goal') (maxm+2)
   in
   let library_equalities = List.map snd library_equalities in
   maxmeta := maxm+2; (* TODO ugly!! *)
@@ -1832,7 +1856,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
     Inference.find_equalities context proof 
   in
   let lib_eq_uris, library_equalities, maxm =
-    Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in
+    Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 9f1ad293d97cfa1563df07112ed52a4bf6b3b642..8a03cd547a0be220daae305c3f44c379ca9b9524 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -27,6 +27,7 @@
 
 
 val saturate :
+  bool ->
   HMysql.dbd ->
   ?full:bool ->
   ?depth:int ->