From 016f069da6221053873b4d505716ef1bd80f08b6 Mon Sep 17 00:00:00 2001 From: denes Date: Fri, 3 Jul 2009 13:22:28 +0000 Subject: [PATCH] Implemented LPO --- .../components/ng_paramodulation/orderings.ml | 36 +++++++++++++++++-- .../components/ng_paramodulation/paramod.ml | 2 +- .../ng_paramodulation/superposition.ml | 10 +----- .../components/ng_paramodulation/terms.ml | 8 +++++ .../components/ng_paramodulation/terms.mli | 2 ++ 5 files changed, 46 insertions(+), 12 deletions(-) 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 *) -- 2.39.2