From: denes <??>
Date: Thu, 16 Jul 2009 11:23:59 +0000 (+0000)
Subject: Disabled age selection and ad hoc goal weight computation
X-Git-Tag: make_still_working~3677
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a7850ef56dc04532777e53eb7f0a4fddb62d7f6f;p=helm.git

Disabled age selection and ad hoc goal weight computation
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index ba6969aeb..182545b1e 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -96,6 +96,7 @@ let compute_unit_clause_weight (_,l, _, _) =
         weight_of_polynomial (wl+wr) (ml@mr)
 ;;
 
+(* UNUSED for now *)
 let compute_goal_weight (_,l, _, _) = 
     let weight_of_polynomial w m =
       let factor = 2 in      
@@ -112,6 +113,8 @@ let compute_goal_weight (_,l, _, _) =
         let wr = weight_of_polynomial wr mr in
           - (abs (wl-wr))
   ;;
+
+let compute_goal_weight = compute_unit_clause_weight;;
   
 (* Riazanov: 3.1.5 pag 38 *)
 (* Compare weights normalized in a new way :
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f3afc16f4..3491f4019 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -251,7 +251,7 @@ module Paramod (B : Orderings.Blob) = struct
           end
         else raise (Stop (Timeout (maxvar,bag)));
 
-    let use_age = weight_picks = (iterno / 6 + 1) in
+    let use_age = false && (weight_picks = (iterno / 6 + 1)) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in