added a flag for age selection

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index c0099a604ccd6015ed31a32eac839563db5d99ba..6dc4150c1c6b9ec51ca09ea100c0d3baa852114e 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -5,7 +5,7 @@ foUtils.cmi: terms.cmi orderings.cmi
 index.cmi: terms.cmi orderings.cmi 
 foUnif.cmi: terms.cmi orderings.cmi 
 superposition.cmi: terms.cmi orderings.cmi index.cmi 
-stats.cmi: orderings.cmi 
+stats.cmi: terms.cmi orderings.cmi 
 paramod.cmi: terms.cmi orderings.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
@@ -20,8 +20,10 @@ orderings.cmo: terms.cmi pp.cmi orderings.cmi
 orderings.cmx: terms.cmx pp.cmx orderings.cmi 
 foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
 foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
-index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi 
-index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi 
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    index.cmi 
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    index.cmi 
 foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
 foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 5c085c5188db5a4473337995e167d17b290f5bfe..3179f000068897755b450fcc8c315cc051c597ce 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -93,11 +93,11 @@ module Index(B : Orderings.Blob) = struct
     | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
           DT.index t r (Terms.Right2Left, c)
     | (_,Terms.Equation (l,r,_,Terms.Incomparable),vl,_) as c ->
-       if are_invertible maxvar vl l r then
+(*     if are_invertible maxvar vl l r then
          (prerr_endline ("Invertible " ^ (Pp.pp_foterm l) ^ "=" ^
             (Pp.pp_foterm r));
            DT.index t l (Terms.Left2Right, c))
-          else
+          else *)
           DT.index  
            (DT.index t l (Terms.Left2Right, c))
            r (Terms.Right2Left, c)

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index be7e140f3521749ba5e5bd86090e31617fb6203c..8c740a0e4605c5d282ff89270b6f1134587553f2 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -33,7 +33,7 @@ let nparamod rdb metasenv subst context t table =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
   match 
-    P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
+    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
       ~g_passives:goals ~passives (bag,maxvar) 
   with 
   | P.Error _ | P.GaveUp | P.Timeout _ -> []

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 06d3251f77125e87c52a19e6cad9ac7e927ff174..ac73df2d0b90fb1fd0fc9110536c13bee8885922 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -28,7 +28,8 @@ module type Paramod =
     type bag = t Terms.bag * int
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
-    val paramod : 
+    val paramod :
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
@@ -213,7 +214,7 @@ module Paramod (B : Orderings.Blob) = struct
     add_passive_goals g_passives new_goals
   ;;
  
-  let rec given_clause ~noinfer 
+  let rec given_clause ~useage ~noinfer 
     bag maxvar iterno weight_picks max_steps timeout 
     actives passives g_actives g_passives 
   =
@@ -244,14 +245,14 @@ module Paramod (B : Orderings.Blob) = struct
         else if false then (* activates last chance strategy *)
           begin
            debug("Last chance: "^string_of_float (Unix.gettimeofday()));
-           given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps 
+           given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps 
              (Some (Unix.gettimeofday () +. 20.))
              actives passives g_actives g_passives;
            raise (Stop (Timeout (maxvar,bag)));
           end
         else raise (Stop (Timeout (maxvar,bag)));
 
-    let use_age = false && (weight_picks = (iterno / 6 + 1)) in
+    let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in
 
@@ -341,12 +342,12 @@ module Paramod (B : Orderings.Blob) = struct
       debug
         (Printf.sprintf "Number of passives : %d"
            (passive_set_cardinal passives));
-      given_clause ~noinfer
+      given_clause ~useage ~noinfer
         bag maxvar iterno weight_picks max_steps timeout 
         actives passives g_actives g_passives
   ;;
 
-  let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+  let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
@@ -357,7 +358,7 @@ module Paramod (B : Orderings.Blob) = struct
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
-     given_clause ~noinfer:false
+     given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index e133036af34d66487ed7181f9621621d90ae3c66..9cffd9d2889af4958d8dc8254ce1af33e31dc18d 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -24,6 +24,7 @@ module type Paramod =
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
     val paramod : 
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 

diff --git a/helm/software/components/ng_paramodulation/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 0f9f45d960e6c30aac980d5bde0f62950d7678a1..fd68f0fe765cd7cd75be5805dac8c516a0f623fb 100644 (file)
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -83,6 +83,12 @@ module Stats (B : Terms.Blob) =
                        (t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
     ;;
 
+    let rec leaf_count = function
+      | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
+      | Terms.Leaf _ -> 1
+      | _ -> 0
+    ;;
+
     let rec dependencies op clauses acc =
       match clauses with
        | [] -> acc
@@ -109,10 +115,21 @@ module Stats (B : Terms.Blob) =
                            else
                              dependencies op tl acc
                        else dependencies op tl acc
+                    | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+                    | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+                         let rec term_leaves = function
+                           | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+                           | Terms.Leaf x -> [x]
+                           | _ -> []
+                         in
+                         if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then 
+                           dependencies op tl (op1::acc)
+                         else
+                           dependencies op tl acc
                    | _ -> dependencies op tl acc
     ;;
 
-    let dependencies op clauses = dependencies op clauses [];;
+    let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
 
     (* let max_weight_hyp = *)