Implemented LPO

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 5c42090c4508d03308809a78d125d65590d73b6c..f2e0273c84a5b4976d7baf3187e97dafb35d5250 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -219,9 +219,41 @@ let compute_goal_weight (_,l, _, _) =
         ) else r 
     | res -> res
   ;;
-            
+
+  let rec lpo s t =
+    match s,t with
+      | Terms.Var i, Terms.Var j when i = j ->
+         XEQ
+      | Terms.Var _, Terms.Var _ ->
+         XINCOMPARABLE
+      | Terms.Var _, _ ->
+         (match lpo t s with
+           | XGT -> XLT
+           | XLT -> XGT
+           | o -> o)
+      | _, Terms.Var i ->
+         if (List.mem i (Terms.vars_of_term s)) then XGT
+         else XINCOMPARABLE
+      | Terms.Leaf a1, Terms.Leaf a2 -> 
+          let cmp = B.compare a1 a2 in
+            if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+      | Terms.Node (hd1::tl1), Terms.Node (hd2::tl2) ->
+         (match lpo hd1 hd2 with
+           | XGT -> if List.for_all (fun x -> lpo s x = XGT) tl2 then XGT
+             else XINCOMPARABLE
+           | XLT -> if List.for_all (fun x -> lpo s x = XLT) tl2 then XLT
+             else XINCOMPARABLE
+           | XEQ -> List.fold_left2
+               (fun acc si ti -> if acc = XEQ then lpo si ti else acc)
+                 XEQ tl1 tl2
+           | XINCOMPARABLE -> XINCOMPARABLE
+           | _ -> assert false)
+      | _ -> assert false
+           
+  ;;
+
   let compare_terms x y = 
-    match nonrec_kbo x y with
+    match kbo x y with
     | XINCOMPARABLE -> Terms.Incomparable
     | XGT -> Terms.Gt
     | XLT -> Terms.Lt

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 983dd53e84bd28e567904e2c51c74fe8209db52a..f156ff0ffae30fe93d6318363f74387072da736b 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -229,7 +229,7 @@ module Paramod (B : Terms.Blob) = struct
           end
         else raise (Stop (Timeout (maxvar,bag)));
 
-    let use_age = weight_picks = (iterno / 10 + 1) in
+    let use_age = weight_picks = (iterno / 6 + 1) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in
 

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c1d5f8bdcffcd9ab3d7a2f226a278e0afe4c6440..eca23e720dd9909f23ce10e2004ce6023d649470 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -98,14 +98,6 @@ module Superposition (B : Terms.Blob) =
       in
         aux bag pos ctx id t
     ;;
-
-    let vars_of_term t =
-      let rec aux acc = function
-       | Terms.Leaf _ -> acc
-       | Terms.Var i -> if (List.mem i acc) then acc else i::acc
-       | Terms.Node l -> List.fold_left aux acc l
-      in aux [] t
-    ;;
     
     let build_clause bag filter rule t subst vl id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
@@ -119,7 +111,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Terms.add_to_bag (0, literal, vars_of_term t, proof) bag
+          Terms.add_to_bag (0, literal, Terms.vars_of_term t, proof) bag
         in
         Some (bag, uc)
       else

diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 169d19b80b68a52d0eb062162464e451a96a5757..9a225fd27b2807f3a3ea37d57276eb93332e384a 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -47,6 +47,14 @@ type 'a unit_clause =
 type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
 
 
+let vars_of_term t =
+  let rec aux acc = function
+    | Leaf _ -> acc
+    | Var i -> if (List.mem i acc) then acc else i::acc
+    | Node l -> List.fold_left aux acc l
+  in aux [] t
+;;
+
 module OT =
  struct
    type t = int 

diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index fe03cc454fc88120faf22837305477c1d342d7f5..47295035ca47e7196beb616887c4d98cccbb7a5c 100644 (file)
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -52,6 +52,8 @@ type 'a unit_clause =
 
 type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
 
+val vars_of_term : 'a foterm -> int list
+
 module M : Map.S with type key = int 
 
 type 'a bag = int (* max ID  *)