pp.cmi: terms.cmi
foSubst.cmi: terms.cmi
+foUtils.cmi: terms.cmi
+foUnif.cmi: terms.cmi
orderings.cmi: terms.cmi
-foUtils.cmi: terms.cmi orderings.cmi
+clauses.cmi: orderings.cmi
index.cmi: terms.cmi orderings.cmi
-foUnif.cmi: terms.cmi orderings.cmi
superposition.cmi: terms.cmi orderings.cmi index.cmi
stats.cmi: terms.cmi orderings.cmi
paramod.cmi: terms.cmi orderings.cmi
pp.cmx: terms.cmx pp.cmi
foSubst.cmo: terms.cmi foSubst.cmi
foSubst.cmx: terms.cmx foSubst.cmi
-orderings.cmo: terms.cmi pp.cmi orderings.cmi
-orderings.cmx: terms.cmx pp.cmx orderings.cmi
-foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi
-foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
- index.cmi
-index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
- index.cmi
-foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi
-foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi
+foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi
+orderings.cmo: terms.cmi pp.cmi foUnif.cmi foSubst.cmi orderings.cmi
+orderings.cmx: terms.cmx pp.cmx foUnif.cmx foSubst.cmx orderings.cmi
+clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi clauses.cmi
+clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx clauses.cmi
+index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi
+index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi
superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
foUnif.cmi foSubst.cmi superposition.cmi
superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
foUnif.cmx foSubst.cmx superposition.cmi
-stats.cmo: terms.cmi stats.cmi
-stats.cmx: terms.cmx stats.cmi
+stats.cmo: terms.cmi pp.cmi stats.cmi
+stats.cmx: terms.cmx pp.cmx stats.cmi
paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
foUtils.cmi foUnif.cmi paramod.cmi
paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
INTERFACE_FILES = \
terms.mli pp.mli foSubst.mli \
- orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
+ foUtils.mli foUnif.mli orderings.mli \
+ clauses.mli index.mli superposition.mli \
stats.mli paramod.mli nCicBlob.mli cicBlob.mli nCicProof.mli \
nCicParamod.mli
aux false false l
;;
-module Founif (B : Orderings.Blob) = struct
+module FoUnif (B : Terms.Blob) = struct
module Subst = FoSubst
module U = FoUtils.Utils(B)
exception UnificationFailure of string Lazy.t;;
-module Founif (B : Orderings.Blob) :
+module FoUnif (B : Terms.Blob) :
sig
val unification:
| _,[] -> 1
;;
-module Utils (B : Orderings.Blob) = struct
+module Utils (B : Terms.Blob) = struct
module Subst = FoSubst;;
- module Order = B;;
let rec eq_foterm x y =
x == y ||
| Terms.Equation _, Terms.Predicate _ -> 1
;;
- let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
- let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
-
let relocate maxvar varlist subst =
List.fold_right
(fun i (maxvar, varlist, s) ->
varlist (maxvar+1, [], subst)
;;
- let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
- let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
- let apply_subst_on_lit = function
- | Terms.Equation (l,r,ty,o) ->
- let l = Subst.apply_subst subst l in
- let r = Subst.apply_subst subst r in
- let ty = Subst.apply_subst subst ty in
- Terms.Equation (l,r,ty,o)
- | Terms.Predicate p ->
- let p = Subst.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 (Subst.apply_subst subst t)
- | Terms.Step (rule,c1,c2,dir,pos,s) ->
- Terms.Step(rule,c1,c2,dir,pos,Subst.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
val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int
-module Utils (B : Orderings.Blob) :
+module Utils (B : Terms.Blob) :
sig
val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool
val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int
val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
- (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
- val mk_clause :
- int ->
- B.t Terms.foterm list -> (* negative literals in clause *)
- B.t Terms.foterm list -> (* positive literals in clause *)
- B.t Terms.foterm ->
- B.t Terms.clause * int
-
- val mk_passive_clause :
- B.t Terms.clause -> B.t Terms.passive_clause
-
- val mk_passive_goal :
- B.t Terms.clause -> B.t Terms.passive_clause
-
- 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
-
- (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
- val relocate :
- int -> int list -> B.t Terms.substitution ->
- int * int list * B.t Terms.substitution
-
- val compare_passive_clauses_weight :
- B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
-
- val compare_passive_clauses_age :
- B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
+ val relocate : int -> int list -> B.t Terms.substitution
+ -> int * int list * B.t Terms.substitution
end
module Index(B : Orderings.Blob) = struct
module U = FoUtils.Utils(B)
+ module Clauses = Clauses.Clauses(B)
module ClauseOT =
struct
let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) =
let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
- if c <> 0 then c else U.compare_clause uc1 uc2
+ if c <> 0 then c else Clauses.compare_clause uc1 uc2
;;
end
| _ -> assert false
;;
+let are_invertible relocate alpha_eq l r =
+ let varlist = Terms.vars_of_term l in
+ let maxvar = List.fold_left max 0 varlist in
+ let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+ let l = FoSubst.apply_subst subst l in
+ try (ignore(alpha_eq l r);true) with
+ FoUnif.UnificationFailure _ -> false;;
+
module NRKBO (B : Terms.Blob) = struct
let name = "nrkbo"
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
-exception UnificationFailure of string Lazy.t;;
-
-
-(* DUPLICATE CODE FOR TESTS (see FoUnif) *)
- let alpha_eq s t =
- let rec equiv subst s t =
- let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
- and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
-
- in
- match s, t with
- | s, t when eq_foterm s t -> subst
- | Terms.Var i, Terms.Var j
- when (not (List.exists (fun (_,k) -> k=t) subst)) ->
- let subst = FoSubst.build_subst i t subst in
- subst
- | Terms.Node l1, Terms.Node l2 -> (
- try
- List.fold_left2
- (fun subst' s t -> equiv subst' s t)
- subst l1 l2
- with Invalid_argument _ ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- )
- | _, _ ->
- raise (UnificationFailure (lazy "Inference.unification.unif"))
- in
- equiv FoSubst.id_subst s t
-;;
-
-let relocate maxvar varlist subst =
- List.fold_right
- (fun i (maxvar, varlist, s) ->
- maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
- varlist (maxvar+1, [], subst)
- ;;
-
- let are_invertible l r =
- let varlist = Terms.vars_of_term l in
- let maxvar = List.fold_left max 0 varlist in
- let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
- let l = FoSubst.apply_subst subst l in
- try (ignore(alpha_eq l r);true) with
- UnificationFailure _ -> false
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
let compute_clause_weight = compute_clause_weight;;
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
include B
module Pp = Pp.Pp(B)
+ module Unif = FoUnif.FoUnif(B)
+ module Utils = FoUtils.Utils(B)
let eq_foterm = eq_foterm B.eq;;
+ let are_invertible = are_invertible Utils.relocate Unif.alpha_eq;;
+
let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
exception Stop of szsontology
type bag = B.t Terms.bag * int
module Pp = Pp.Pp (B)
- module FU = FoUnif.Founif(B)
+ module FU = FoUnif.FoUnif(B)
module IDX = Index.Index(B)
module Sup = Superposition.Superposition(B)
module Utils = FoUtils.Utils(B)
module Order = B
+ module Clauses = Clauses.Clauses(B)
module WeightOrderedPassives =
struct
type t = B.t Terms.passive_clause
- let compare = Utils.compare_passive_clauses_weight
+ let compare = Clauses.compare_passive_clauses_weight
end
module AgeOrderedPassives =
struct
type t = B.t Terms.passive_clause
- let compare = Utils.compare_passive_clauses_age
+ let compare = Clauses.compare_passive_clauses_age
end
module WeightPassiveSet = Set.Make(WeightOrderedPassives)
let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
let cl = if no_weight then (0,cl)
- else Utils.mk_passive_clause cl in
+ else Clauses.mk_passive_clause cl in
WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
;;
let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
let g = if no_weight then (0,g)
- else Utils.mk_passive_goal g in
+ else Clauses.mk_passive_goal g in
WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
;;
let bag = Terms.empty_bag in
let maxvar = 0 in
let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
- let c,maxvar = Utils.mk_clause maxvar nlit plit t in
+ let c,maxvar = Clauses.mk_clause maxvar nlit plit t in
let bag,c = Terms.add_to_bag c bag in
(bag,maxvar,c::l)
in
module Superposition (B : Orderings.Blob) =
struct
module IDX = Index.Index(B)
- module Unif = FoUnif.Founif(B)
+ module Unif = FoUnif.FoUnif(B)
module Subst = FoSubst
module Order = B
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
+ module Clauses = Clauses.Clauses(B)
exception Success of B.t Terms.bag * int * B.t Terms.clause
current :: alist, IDX.index_clause atable current
in
debug (lazy "Indexed");
- let fresh_current, maxvar = Utils.fresh_clause maxvar current in
+ let fresh_current, maxvar = Clauses.fresh_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
let bag, fresh_current = Terms.add_to_bag fresh_current bag in
projects / helm.git / commitdiff