helm/software/components/ng_paramodulation/clauses.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
  13
  14 module type Blob =
  15   sig
  16     include Orderings.Blob
  17
  18   end
  19
  20 module Clauses (B : Orderings.Blob) = struct
  21   module Order = B;;
  22   module Utils = FoUtils.Utils(B)
  23
  24   let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
  25   let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
  26
  27   let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
  28     let maxvar, varlist, subst = Utils.relocate maxvar varlist FoSubst.id_subst in
  29     let apply_subst_on_lit = function
  30       | Terms.Equation (l,r,ty,o) ->
  31           let l = FoSubst.apply_subst subst l in
  32           let r = FoSubst.apply_subst subst r in
  33           let ty = FoSubst.apply_subst subst ty in
  34           Terms.Equation (l,r,ty,o)
  35       | Terms.Predicate p ->
  36           let p = FoSubst.apply_subst subst p in
  37           Terms.Predicate p
  38     in
  39     let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
  40     let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
  41     let proof =
  42       match proof with
  43       | Terms.Exact t -> Terms.Exact (FoSubst.apply_subst subst t)
  44       | Terms.Step (rule,c1,c2,dir,pos,s) ->
  45           Terms.Step(rule,c1,c2,dir,pos,FoSubst.concat subst s)
  46     in
  47      (id, nlit, plit, varlist, proof), maxvar
  48   ;;
  49
  50   (* may be moved inside the bag *)
  51   let mk_clause maxvar nlit plit proofterm =
  52     let foterm_to_lit (acc,literals) ty =
  53       let vars = Terms.vars_of_term ~start_acc:acc ty in
  54       match ty with
  55       | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
  56            let o = Order.compare_terms l r in
  57            (vars,(Terms.Equation (l, r, ty, o),true)::literals)
  58       | _ -> (vars,(Terms.Predicate ty,true)::literals)
  59     in
  60     let varlist = Terms.vars_of_term proofterm in
  61     let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
  62     let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in
  63     let proof = Terms.Exact proofterm in
  64     fresh_clause maxvar (0, nlit, plit, varlist, proof)
  65   ;;
  66
  67   let mk_passive_clause cl =
  68     (Order.compute_clause_weight cl, cl)
  69   ;;
  70
  71   let mk_passive_goal g =
  72     (Order.compute_clause_weight g, g)
  73   ;;
  74
  75   let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) =
  76     if w1 = w2 then id1 - id2
  77     else w1 - w2
  78   ;;
  79
  80   let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) =
  81     id1 - id2
  82   ;;
  83
  84 end