From: denes <??>
Date: Fri, 3 Jul 2009 13:22:28 +0000 (+0000)
Subject: Implemented LPO
X-Git-Tag: make_still_working~3754
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=016f069da6221053873b4d505716ef1bd80f08b6

Implemented LPO
---

diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 5c42090c4..f2e0273c8 100644
--- 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 983dd53e8..f156ff0ff 100644
--- 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 c1d5f8bdc..eca23e720 100644
--- 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 169d19b80..9a225fd27 100644
--- 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 fe03cc454..47295035c 100644
--- 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  *)