Disabled age selection and ad hoc goal weight computation

[helm.git] / helm / software / components / ng_paramodulation / orderings.ml

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index ba6969aeb143ddaa1df97d72ea3ff61b4c2bcaab..182545b1edda93968fb00915f5a5c01f662da8da 100644 (file)
--- 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 :