Branched paramodulation for CNF (Horn clauses)

[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..f2151528f698df8472f17c2d608bb2e03a5729ed 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -25,9 +25,7 @@ module type Blob =
     val compare_terms : 
           t Terms.foterm -> t Terms.foterm -> Terms.comparison
 
-    val compute_unit_clause_weight : 't Terms.unit_clause -> int
-
-    val compute_goal_weight : 't Terms.unit_clause -> int
+    val compute_clause_weight : 't Terms.clause -> int
 
     val name : string
 
@@ -76,7 +74,7 @@ let weight_of_term term =
     (w, List.sort compare l) (* from the smallest meta to the bigest *)
 ;;
   
-let compute_unit_clause_weight (_,l, _, _) = 
+let compute_literal_weight l =
     let weight_of_polynomial w m =
       let factor = 2 in      
       w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
@@ -96,22 +94,10 @@ let compute_unit_clause_weight (_,l, _, _) =
         weight_of_polynomial (wl+wr) (ml@mr)
 ;;
 
-let compute_goal_weight (_,l, _, _) = 
-    let weight_of_polynomial w m =
-      let factor = 2 in      
-      w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
-    in
-    match l with
-    | Terms.Predicate t -> 
-        let w, m = weight_of_term t in 
-        weight_of_polynomial w m
-    | Terms.Equation (l,r,_,_) ->
-        let wl, ml = weight_of_term l in 
-        let wr, mr = weight_of_term r in 
-        let wl = weight_of_polynomial wl ml in
-        let wr = weight_of_polynomial wr mr in
-          - (abs (wl-wr))
-  ;;
+let compute_clause_weight (_,nl,pl,_,_) =
+  List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+
+let compute_goal_weight = compute_clause_weight;;
   
 (* Riazanov: 3.1.5 pag 38 *)
 (* Compare weights normalized in a new way :
@@ -206,7 +192,7 @@ module NRKBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
+  let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
   
   (* Riazanov: p. 40, relation >_n *)
@@ -239,7 +225,7 @@ module KBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
+  let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
   (* Riazanov: p. 38, relation > *)
@@ -304,7 +290,7 @@ module LPO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
-  let compute_unit_clause_weight = compute_unit_clause_weight;;
+  let compute_clause_weight = compute_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
 
   let rec lpo s t =