val empty_state : state
val bag_of_state :state -> bag
val replace_bag : state -> bag -> state
+ (* we suppose input has been already saturated *)
val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
val forward_infer_step :