From 156e5aad803c661dc2967b8f33642e89e8e878a1 Mon Sep 17 00:00:00 2001 From: denes Date: Wed, 29 Jul 2009 16:28:29 +0000 Subject: [PATCH] Added Clauses module --- .../components/ng_paramodulation/clauses.ml | 84 +++++++++++++++++++ .../components/ng_paramodulation/clauses.mli | 40 +++++++++ 2 files changed, 124 insertions(+) create mode 100644 helm/software/components/ng_paramodulation/clauses.ml create mode 100644 helm/software/components/ng_paramodulation/clauses.mli diff --git a/helm/software/components/ng_paramodulation/clauses.ml b/helm/software/components/ng_paramodulation/clauses.ml new file mode 100644 index 000000000..895d3865e --- /dev/null +++ b/helm/software/components/ng_paramodulation/clauses.ml @@ -0,0 +1,84 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) + +module type Blob = + sig + include Orderings.Blob + + end + +module Clauses (B : Orderings.Blob) = struct + module Order = B;; + module Utils = FoUtils.Utils(B) + + let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2 + let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2 + + let fresh_clause maxvar (id, nlit, plit, varlist, proof) = + let maxvar, varlist, subst = Utils.relocate maxvar varlist FoSubst.id_subst in + let apply_subst_on_lit = function + | Terms.Equation (l,r,ty,o) -> + let l = FoSubst.apply_subst subst l in + let r = FoSubst.apply_subst subst r in + let ty = FoSubst.apply_subst subst ty in + Terms.Equation (l,r,ty,o) + | Terms.Predicate p -> + let p = FoSubst.apply_subst subst p in + Terms.Predicate p + in + let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in + let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in + let proof = + match proof with + | Terms.Exact t -> Terms.Exact (FoSubst.apply_subst subst t) + | Terms.Step (rule,c1,c2,dir,pos,s) -> + Terms.Step(rule,c1,c2,dir,pos,FoSubst.concat subst s) + in + (id, nlit, plit, varlist, proof), maxvar + ;; + + (* may be moved inside the bag *) + let mk_clause maxvar nlit plit proofterm = + let foterm_to_lit (acc,literals) ty = + let vars = Terms.vars_of_term ~start_acc:acc ty in + match ty with + | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> + let o = Order.compare_terms l r in + (vars,(Terms.Equation (l, r, ty, o),true)::literals) + | _ -> (vars,(Terms.Predicate ty,true)::literals) + in + let varlist = Terms.vars_of_term proofterm in + let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in + let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in + let proof = Terms.Exact proofterm in + fresh_clause maxvar (0, nlit, plit, varlist, proof) + ;; + + let mk_passive_clause cl = + (Order.compute_clause_weight cl, cl) + ;; + + let mk_passive_goal g = + (Order.compute_clause_weight g, g) + ;; + + let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) = + if w1 = w2 then id1 - id2 + else w1 - w2 + ;; + + let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) = + id1 - id2 + ;; + +end diff --git a/helm/software/components/ng_paramodulation/clauses.mli b/helm/software/components/ng_paramodulation/clauses.mli new file mode 100644 index 000000000..885e97607 --- /dev/null +++ b/helm/software/components/ng_paramodulation/clauses.mli @@ -0,0 +1,40 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) + +module type Blob = + sig + include Orderings.Blob + + end + +module Clauses (B : Orderings.Blob) : + sig + + val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool + val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int + val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int + + val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list + -> B.t Terms.foterm -> B.t Terms.clause * int + + val mk_passive_clause : B.t Terms.clause -> int * B.t Terms.clause + + val mk_passive_goal : B.t Terms.clause -> int * B.t Terms.clause + + val compare_passive_clauses_weight : + int * B.t Terms.clause -> int * B.t Terms.clause -> int + + val compare_passive_clauses_age : + int * B.t Terms.clause -> int * B.t Terms.clause -> int + +end -- 2.39.2