(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
let debug s = prerr_endline (Lazy.force s) ;;
-let debug _ = ();;
+(* let debug _ = ();; *)
let monster = 100;;
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)
module AgePassiveSet = Set.Make(AgeOrderedPassives)
- 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
+ let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
+ let (w,cl) = Clauses.mk_passive_clause cl in
+ let cl = (w+bonus_weight,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
+ let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
+ let (w,g) = Clauses.mk_passive_goal g in
+ let g = (w+bonus_weight,g) in
WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
;;
passives_w,passives_a
;;
- let add_passive_clauses ?(no_weight=false)
+ let add_passive_clauses ?(bonus_weight=0)
(passives_w,passives_a) new_clauses =
let new_clauses_w,new_clauses_a =
- List.fold_left (add_passive_clause ~no_weight)
+ List.fold_left (add_passive_clause ~bonus_weight)
(WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
in
(WeightPassiveSet.union new_clauses_w passives_w,
AgePassiveSet.union new_clauses_a passives_a)
;;
- let add_passive_goals ?(no_weight=false)
+ let add_passive_goals ?(bonus_weight=0)
(passives_w,passives_a) new_clauses =
let new_clauses_w,new_clauses_a =
- List.fold_left (add_passive_goal ~no_weight)
+ List.fold_left (add_passive_goal ~bonus_weight)
(WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
in
(WeightPassiveSet.union new_clauses_w passives_w,
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
- let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+ let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
let goal = match goals with | [g] -> g | _ -> assert false in
let passives =
- add_passive_clauses ~no_weight:true passive_empty_set hypotheses
+ add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses
in
let g_passives =
- add_passive_goal ~no_weight:true passive_empty_set goal
+ add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal
in
let g_actives = [] in
let actives = [], IDX.DT.empty in