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
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"