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   module Unif = FoUnif.FoUnif(B)
  24
  25   let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
  26   let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
  27
  28   let fresh_clause maxvar ?(subst=FoSubst.id_subst) (id, nlit, plit, varlist, proof) =
  29     let maxvar, varlist, subst = Utils.relocate maxvar varlist subst in
  30     let apply_subst_on_lit = function
  31       | Terms.Equation (l,r,ty,o) ->
  32           let l = FoSubst.apply_subst subst l in
  33           let r = FoSubst.apply_subst subst r in
  34           let ty = FoSubst.apply_subst subst ty in
  35           Terms.Equation (l,r,ty,o)
  36       | Terms.Predicate p ->
  37           let p = FoSubst.apply_subst subst p in
  38           Terms.Predicate p
  39     in
  40     let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
  41     let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
  42     let proof =
  43       match proof with
  44       | Terms.Exact t -> Terms.Exact (FoSubst.apply_subst subst t)
  45       | Terms.Step (rule,c1,c2,dir,pos,s) ->
  46           Terms.Step(rule,c1,c2,dir,pos,FoSubst.concat subst s)
  47     in
  48      (id, nlit, plit, varlist, proof), maxvar
  49   ;;
  50
  51   (* may be moved inside the bag *)
  52   let mk_clause maxvar nlit plit proofterm =
  53     let foterm_to_lit (acc,literals) ty =
  54       let vars = Terms.vars_of_term ~start_acc:acc ty in
  55       match ty with
  56       | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
  57            let o = Order.compare_terms l r in
  58            (vars,(Terms.Equation (l, r, ty, o),true)::literals)
  59       | _ -> (vars,(Terms.Predicate ty,true)::literals)
  60     in
  61     let varlist = Terms.vars_of_term proofterm in
  62     let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
  63     let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in
  64     let proof = Terms.Exact proofterm in
  65     fresh_clause maxvar (0, nlit, plit, varlist, proof)
  66   ;;
  67
  68   let mk_passive_clause cl =
  69     (Order.compute_clause_weight cl, cl)
  70   ;;
  71
  72   let mk_passive_goal g =
  73     (Order.compute_clause_weight g, g)
  74   ;;
  75
  76   let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) =
  77     if w1 = w2 then id1 - id2
  78     else w1 - w2
  79   ;;
  80
  81   let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) =
  82     id1 - id2
  83   ;;
  84
  85   let are_alpha_eq_cl cl1 cl2 =
  86     let (_,nlit1,plit1,_,_) = cl1 in
  87     let (_,nlit2,plit2,_,_) = cl2 in
  88     let alpha_eq (lit1,_) (lit2,_) =
  89        let get_term lit =
  90        match lit with
  91           | Terms.Predicate _ -> assert false
  92           | Terms.Equation (l,r,ty,_) ->
  93               Terms.Node [Terms.Leaf B.eqP; ty; l ; r]
  94        in
  95        try ignore(Unif.alpha_eq (get_term lit1) (get_term lit2)) ; true
  96        with FoUnif.UnificationFailure _ -> false
  97     in
  98        try (List.for_all2 alpha_eq nlit1 nlit2 && List.for_all2 alpha_eq plit1 plit2)
  99        with Invalid_argument _ -> false
 100     ;;
 101
 102   let vars_of_clause (id,nlit,plit,_,pr) =
 103     let vars_of_lit acc lit =
 104       match lit with
 105        | (Terms.Predicate t,_) -> Terms.vars_of_term ~start_acc:acc t
 106        | (Terms.Equation (l,r,ty,o),_) ->
 107             Terms.vars_of_term ~start_acc:(Terms.vars_of_term ~start_acc:acc l) r
 108     in
 109     List.fold_left vars_of_lit [] (nlit@plit)
 110 ;;
 111
 112 end