]> matita.cs.unibo.it Git - helm.git/commitdiff
- patch to consider the symbols of the goal when computing the weight of an
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 3 Jul 2006 11:48:44 +0000 (11:48 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 3 Jul 2006 11:48:44 +0000 (11:48 +0000)
  equality.
- actives simplified during fwd/back are not appended (but put in front) of the
  passive list

components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/utils.ml
components/tactics/paramodulation/utils.mli

index 306f02dcf1c911ba05d5298308433b6a9ba0d066..4fe509981954ec67c774242fcc20a07e4dfd4ec7 100644 (file)
@@ -224,8 +224,8 @@ let rec select env (goals,_) passive =
         | [] -> min
        | hd::tl -> my_min_elt (my_min hd min) tl
       in
-      (* let current = EqualitySet.min_elt pos_set in *)
-      let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in
+(*        let current = EqualitySet.min_elt pos_set in  *)
+       let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in 
       let passive_table =
         Indexing.remove_index passive_table current
       in
@@ -276,7 +276,7 @@ let make_active () =
 
 
 (* adds to passive a list of equalities new_pos *)
-let add_to_passive passive new_pos =
+let add_to_passive passive new_pos preferred =
   let (pos_list, pos_set), table = passive in
   let ok set equality = not (EqualitySet.mem equality set) in
   let pos = List.filter (ok pos_set) new_pos in
@@ -286,7 +286,12 @@ let add_to_passive passive new_pos =
   let add set equalities =
     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
   in
-  (pos_list @ pos, add pos_set pos),
+  let pos_head, pos_tail =
+    List.partition 
+      (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)  
+      pos 
+  in
+  (pos_head @ pos_list @ pos_tail, add pos_set pos),
   table
 ;;
 
@@ -976,24 +981,15 @@ let simplify_goal_set env goals ?passive active =
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
   in
-  let simplified =
     List.fold_left
-      (fun acc goal -> 
+      (fun (acc_a,acc_p) goal -> 
         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)
-      (* active_goals active_goals *)
-      [] active_goals
-  in
-  if List.length active_goals <>  List.length simplified then
-    prerr_endline "SEMPLIFICANDO HO SCARTATO...";
-  (simplified,passive_goals)
-        (*
-  HExtlib.list_uniq ~eq:(fun (_,_,t1) (_,_,t2) -> t1 = t2)
-    (List.sort (fun (_,_,t1) (_,_,t2) -> compare t1 t1)
-      ((*goals @*) simplified))
-      *)
+            if changed then 
+              if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
+            else
+              if find g acc_a then acc_a,acc_p else g::acc_a,acc_p)
+      ([],passive_goals) active_goals
 ;;
 
 let check_if_goals_set_is_solved env active goals =
@@ -1069,8 +1065,7 @@ let infer_goal_set env active goals =
 *)
 
 let infer_goal_set_with_current env current goals active = 
-  let active_goals, passive_goals = goals in
-  let active_goals, _ = 
+  let active_goals, passive_goals = 
     simplify_goal_set env goals active
   in
   let l,table,_  = build_table [current] in
@@ -1096,13 +1091,26 @@ let ids_of_goal_set (ga,gp) =
 
 let size_of_goal_set_a (l,_) = List.length l;;
 let size_of_goal_set_p (_,l) = List.length l;;
+      
+let pp_goals label goals context = 
+  let names = Utils.names_of_context context in
+  List.iter                 
+    (fun _,_,g -> 
+      prerr_endline 
+        (Printf.sprintf  "Current goal: %s = %s\n" label (CicPp.pp g names))) 
+    (fst goals);
+  List.iter                 
+    (fun _,_,g -> 
+      prerr_endline 
+        (Printf.sprintf  "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))) 
+      (snd goals);
+;;
 
 (** given-clause algorithm with full reduction strategy: NEW implementation *)
 (* here goals is a set of goals in OR *)
 let given_clause 
   eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
-  let names = Utils.names_of_context context in
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
     let now = Unix.gettimeofday () in
@@ -1171,27 +1179,21 @@ let given_clause
                   Equality.collect active passive goal
                 end;
               let current, passive = select env goals passive in
-              let _ = 
-                List.iter                 
-                 (fun _,_,g -> 
-                   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
               (* SIMPLIFICATION OF CURRENT *)
+              prerr_endline
+                    ("Selected : " ^ 
+                      Equality.string_of_equality ~env  current);
               let res = 
                 forward_simplify eq_uri env (Utils.Positive, current) active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
               | Some current ->
+(*
+                  prerr_endline 
+                    ("Selected simpl: " ^ 
+                      Equality.string_of_equality ~env  current);
+*)
                   (* GENERATION OF NEW EQUATIONS *)
                   prerr_endline "infer";
                   let new' = infer eq_uri env current active in
@@ -1214,7 +1216,7 @@ let given_clause
                   in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
                   prerr_endline "fwd/back simpl";
-                  let rec simplify new' active passive =
+                  let rec simplify new' active passive head =
                     let new' = 
                       forward_simplify_new eq_uri env new' ~passive active 
                     in
@@ -1225,12 +1227,15 @@ let given_clause
                       List.fold_left filter_dependent passive pruned 
                     in
                     match newa, retained with
-                    | None, None -> active, passive, new'
+                    | None, None -> active, passive, new', head
                     | Some p, None 
-                    | None, Some p -> simplify (new' @ p) active passive
-                    | Some p, Some rp -> simplify (new' @ p @ rp) active passive
+                    | None, Some p -> simplify (new' @ p) active passive head
+                    | Some p, Some rp -> 
+                        simplify (new' @ p @ rp) active passive (head @ p)
+                  in
+                  let active, passive, new', head = 
+                    simplify new' active passive []
                   in
-                  let active, passive, new' = simplify new' active passive in
                   prerr_endline "simpl goal with new";
                   let goals = 
                     let a,b,_ = build_table new' in
@@ -1239,7 +1244,7 @@ let given_clause
                     let _ = <:stop<simplify_goal_set new>> in
                     rc
                   in
-                  let passive = add_to_passive passive new' in
+                  let passive = add_to_passive passive new' head in
                   step goals theorems passive active (iterno+1)
             end
   in
@@ -1300,7 +1305,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
                             (Equality.string_of_equality ~env e)) new'))))
         in
         let new' = List.filter accept_fun new' in
-        let passive = add_to_passive passive new' in
+        let passive = add_to_passive passive new' [] in
         saturate_equations eq_uri env goal accept_fun passive active
 ;;
   
@@ -1516,11 +1521,12 @@ let saturate
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
+  let cleaned_goal = Utils.remove_local_context type_of_goal in
+  Utils.set_goal_symbols cleaned_goal;
   let names = Utils.names_of_context context in
   let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let cleaned_goal = Utils.remove_local_context type_of_goal in
   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
@@ -1575,7 +1581,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in
@@ -1993,6 +1999,9 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
     CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
+      let eql = 
+        if eql = [] then [eq_what] else eql
+      in
       let demod = 
         let demod = Str.split (Str.regexp "_") demod_table in 
         List.map (fun other -> find_in_ctx 1 other context) demod 
index 542c2dd77d26e6c6bae42937abd63d9fc2257a72..8d0ba901b055d9dba4b20b5b02d8f2b3829f0c69 100644 (file)
@@ -299,6 +299,29 @@ end
 
 module IntSet = Set.Make(OrderedInt)
 
+let goal_symbols = ref TermSet.empty
+
+let set_of_map m = 
+  TermMap.fold (fun k _ s -> TermSet.add k s) m TermSet.empty
+;;
+
+let set_goal_symbols term = 
+  let m = symbols_of_term term in
+  goal_symbols := (set_of_map m)
+;;
+
+let symbols_of_eq (ty,left,right,_) = 
+  let sty = set_of_map (symbols_of_term ty) in
+  let sl = set_of_map (symbols_of_term left) in
+  let sr = set_of_map (symbols_of_term right) in
+  TermSet.union sty (TermSet.union sl sr)
+;;
+
+let distance sgoal seq =
+  let s = TermSet.diff seq sgoal in
+  TermSet.cardinal s
+;;
+
 let compute_equality_weight (ty,left,right,o) =
   let factor = 2 in
   match o with
@@ -321,6 +344,21 @@ let compute_equality_weight (ty,left,right,o) =
       w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2))
 ;;
 
+let compute_equality_weight e =
+  let w = compute_equality_weight e in
+  let d = distance !goal_symbols (symbols_of_eq e) in
+(*
+  prerr_endline (Printf.sprintf "dist %s --- %s === %d" 
+   (String.concat ", " (List.map (CicPp.ppterm) (TermSet.elements
+     !goal_symbols)))
+   (String.concat ", " (List.map (CicPp.ppterm) (TermSet.elements
+     (symbols_of_eq e))))
+   d
+  );
+*)
+  w + d
+;;
+
 (* old
 let compute_equality_weight (ty,left,right,o) =
   let metasw = ref 0 in
index c64eacfd61f3c3364df483305e51624d04e96aab..d761045b85a75c18eb27d36e66cff82c558f518e 100644 (file)
@@ -63,6 +63,7 @@ val names_of_context: Cic.context -> (Cic.name option) list
 module TermMap: Map.S with type key = Cic.term
 
 val symbols_of_term: Cic.term -> int TermMap.t
+val set_goal_symbols: Cic.term -> unit
 
 val lpo: Cic.term -> Cic.term -> comparison