- in
- let module PassiveSet = Set.Make(OrderedPassives)
- in
- let add_passive_clause passives cl =
- PassiveSet.add (Utils.mk_passive_clause cl) passives
- in
- let timeout = Unix.gettimeofday () +. amount_of_time in
-
- (* TODO : fairness condition *)
- let select passives g_passives =
- if PassiveSet.is_empty passives then begin
- assert (not (PassiveSet.is_empty g_passives));
- let g_cl = PassiveSet.min_elt g_passives in
- (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
+
+ 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
+ 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
+ WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+ ;;
+
+ let remove_passive_clause (passives_w,passives_a) cl =
+ let passives_w = WeightPassiveSet.remove cl passives_w in
+ let passives_a = AgePassiveSet.remove cl passives_a in
+ passives_w,passives_a
+ ;;
+
+ let add_passive_clauses ?(no_weight=false)
+ (passives_w,passives_a) new_clauses =
+ let new_clauses_w,new_clauses_a =
+ List.fold_left (add_passive_clause ~no_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)
+ (passives_w,passives_a) new_clauses =
+ let new_clauses_w,new_clauses_a =
+ List.fold_left (add_passive_goal ~no_weight)
+ (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
+ in
+ (WeightPassiveSet.union new_clauses_w passives_w,
+ AgePassiveSet.union new_clauses_a passives_a)
+ ;;
+
+ let is_passive_set_empty (passives_w,passives_a) =
+ if (WeightPassiveSet.is_empty passives_w) then begin
+ assert (AgePassiveSet.is_empty passives_a); true
+ end else begin
+ assert (not (AgePassiveSet.is_empty passives_a)); false
+ end
+ ;;
+
+ let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w
+
+ let passive_empty_set =
+ (WeightPassiveSet.empty,AgePassiveSet.empty)
+ ;;
+
+ let pick_min_passive ~use_age (passives_w,passives_a) =
+ if use_age then AgePassiveSet.min_elt passives_a
+ else WeightPassiveSet.min_elt passives_w
+ ;;
+
+ let mk_clause bag maxvar (t,ty) =
+ let (proof,ty) = B.saturate t ty in
+ let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
+ let bag, c = Terms.add_to_bag c bag in
+ (bag, maxvar), c
+ ;;
+
+ let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+ let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
+ (* TODO : global age over facts and goals (without comparing weights) *)
+ let select ~use_age passives g_passives =
+ if is_passive_set_empty passives then begin
+ if (is_passive_set_empty g_passives) then
+ raise (Stop GaveUp) (* we say we are incomplete *)
+ else
+ let g_cl = pick_min_passive ~use_age:use_age g_passives in
+ (true,g_cl,passives,remove_passive_clause g_passives g_cl)