B.t Terms.unit_clause ->
B.t Terms.bag * B.t Terms.unit_clause
- end
+ val one_pass_simplification:
+ B.t Terms.unit_clause ->
+ Index.Index(B).active_set ->
+ B.t Terms.bag ->
+ (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+
+ val keep_simplified:
+ B.t Terms.unit_clause ->
+ Index.Index(B).active_set ->
+ B.t Terms.bag ->
+ (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+ end