type bag = t Terms.bag * int
type state
val empty_state : state
+ val size_of_state : state -> int*int
val bag_of_state : state -> bag
val replace_bag: state -> bag -> state
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
(bag, maxvar), c
;;
- let mk_clause bag maxvar (t,ty) =
- let (proof,ty) = B.saturate t ty in
+(*
+ let mk_clause bag maxvar (proof,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_passive (bag,maxvar) = mk_unit_clause bag maxvar;;
- let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+ let mk_goal (bag,maxvar) = mk_unit_clause bag maxvar;;
let initialize_goal (bag,maxvar,actives,passives,_,_) t =
let (bag,maxvar), g = mk_unit_clause bag maxvar t in
let g_passives = g_passive_empty_set in
- (* if the goal is not an equation we returns an empty
+ (* if the goal is not an equation we return an empty
passive set *)
let g_passives =
if Terms.is_eq_clause g then add_passive_goal g_passives g
add_passive_goals g_passives new_goals
;;
+ let size_of_state (_,_,(a,_),p,_,_) = List.length a, passive_set_cardinal p;;
+
let debug_status (_,_,actives,passives,g_actives,g_passives) =
lazy
((Printf.sprintf "Number of active goals : %d\n"