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