Added the computation of max_weight for equations in proofs.

diff --git a/components/tactics/.depend b/components/tactics/.depend
index 43ed94aa9dd287dcc9f31eed229e25d8ff636aed..2ed8b5147261eaf8a07373e496682e87789d5791 100644 (file)
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -190,5 +190,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \
     introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
     equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
     autoTactic.cmx tactics.cmi 
-declarative.cmo: tactics.cmi tacticals.cmi declarative.cmi 
-declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi 
+declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+    declarative.cmi 
+declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+    declarative.cmi 

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index 4414d2f435f3af14a1d8cc1d32c131bd0b241db7..ac5cb1a0ccae66e3495e267aedb339e096321a98 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -67,6 +67,7 @@ let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
+
   eq
 ;;
 
@@ -108,6 +109,31 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
+let rec max_weight_in_proof current =
+  function
+   | Exact _ -> current
+   | Step (_, (_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+       let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+       let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+       let current = max current w1 in
+       let current = max_weight_in_proof current p1 in
+       let current = max current w2 in
+       max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+  List.fold_left 
+    (fun current (_,_,id,_,_) ->
+       let eq = Hashtbl.find id_to_eq id in
+       let (w,p,(_,_,_,_),_,_) = open_equality eq in
+       let current = max current w in
+       max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+  let current = max_weight_in_proof 0 proof in
+  max_weight_in_goal_proof current goal_proof
+
 let proof_of_id id =
   try
     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 1a62ee2ff0e2a7e159e059ca2db41cafe7a95e7b..019578ccc363d53d43c7c36f5af90bc9f707af4c 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -58,6 +58,8 @@ val open_equality :
     Cic.metasenv * int
 val depend : equality -> int -> bool
 val compare : equality -> equality -> int
+val max_weight_in_proof : int-> proof -> int
+val max_weight : goal_proof -> proof -> int
 val string_of_equality : ?env:Utils.environment -> equality -> string
 val string_of_proof : 
   ?names:(Cic.name option)list -> proof -> goal_proof -> string

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 8f031a4a7728d2fb44acf33c919fec90fc6b4f78..408a7cdb8904771bc82a0e9f18dc2642ec66c0a1 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -243,8 +243,8 @@ let find_equalities context proof =
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
-(*                     let w = compute_equality_weight stat in *)
-                    let w = 0 in
+                    (* let w = compute_equality_weight stat in *)
+                    let w = 0 in 
                     let proof = Equality.Exact p in
                     let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index d4ccf8f42bbcc71f172f6b69085c273437541f36..c40b4a9ac238de328366c0c49fa9ec6e067dc23b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -153,11 +153,13 @@ let age_factor = 0.01;;
    of weight, age and goal-similarity
 *)
 
-let rec select env (goals,_) passive =
+let rec select env g passive =
   processed_clauses := !processed_clauses + 1;
+(*
   let goal =
     match (List.rev goals) with goal::_ -> goal | _ -> assert false
   in
+*)
   let pos_list, pos_set = passive in
   let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
   if !weight_age_ratio > 0 then
@@ -165,20 +167,38 @@ let rec select env (goals,_) passive =
   match !weight_age_counter with
   | 0 -> (
       weight_age_counter := !weight_age_ratio;
+      let skip_giant pos_list pos_set =
+        match pos_list with
+          | (hd:EqualitySet.elt)::tl ->
+              let w,_,_,_,_ = Equality.open_equality hd in
+                if w < 30 then
+                  hd, (tl, EqualitySet.remove hd pos_set)
+                else
+                  (prerr_endline 
+                    ("+++ skipping giant of size "^string_of_int w^" +++");
+                  select env g (tl@[hd],pos_set))
+          | _ -> assert false
+                  in
+                   skip_giant pos_list pos_set)
+
+(*
       let rec skip_giant pos_list pos_set =
         match pos_list with
           | (hd:EqualitySet.elt)::tl ->
               let w,_,_,_,_ = Equality.open_equality hd in
               let pos_set = EqualitySet.remove hd pos_set in
-                if w < 500 then
+                if w < 30 then
                   hd, (tl, pos_set)
                 else
                   (prerr_endline 
                     ("+++ skipping giant of size "^string_of_int w^" +++");
                   skip_giant tl pos_set)
           | _ -> assert false
-      in
-        skip_giant pos_list pos_set)
+      in        
+  skip_giant pos_list pos_set)
+
+*)
+(*
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
@@ -216,6 +236,7 @@ let rec select env (goals,_) passive =
       let _, current = EqualitySet.fold f pos_set initial in
         current,
       (remove current pos_list, EqualitySet.remove current pos_set))
+*)
   | _ ->
       symbols_counter := !symbols_ratio;
       let my_min e1 e2 =
@@ -843,6 +864,10 @@ let simplify_goal_set env goals active =
   let find (_,_,g) where =
     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
   in
+    (* prova:tengo le passive semplificate 
+  let passive_goals = 
+    List.map (fun g -> snd (simplify_goal env g active)) passive_goals 
+  in *)
     List.fold_left
       (fun (acc_a,acc_p) goal -> 
         match simplify_goal env goal active with 
@@ -864,6 +889,7 @@ let check_if_goals_set_is_solved env active goals =
           check goal [
             check_if_goal_is_identity env;
             check_if_goal_is_subsumed env (snd active)])
+(* provare active and passive?*)
     None active_goals
 ;;
 
@@ -958,7 +984,6 @@ let given_clause
     int_of_float iterations_left 
   in
   let rec step goals theorems passive active iterno =
-    pp_goals "xxx" goals context;
     if iterno > max_iterations then
       (ParamodulationFailure "No more iterations to spend")
     else if Unix.gettimeofday () > max_time then
@@ -989,7 +1014,8 @@ let given_clause
           passive
       in
       kept_clauses := (size_of_passive passive) + (size_of_active active);
-      let goals = infer_goal_set env active goals in
+      let goals = infer_goal_set env active goals 
+      in
       match check_if_goals_set_is_solved env active goals with
       | Some p -> 
           prerr_endline 
@@ -1267,7 +1293,9 @@ let saturate
       prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline "ENDOFPROOFS";
+      prerr_endline "ENDOFPROOFS___";
+      prerr_endline ("max weight: " ^ 
+       (string_of_int (Equality.max_weight goalproof newproof)));
       (* generation of the CIC proof *)
       let side_effects = 
         List.filter (fun i -> i <> goalno)