sig
(* bag, maxvar, meeting point *)
- exception Success of
- B.t Terms.bag
- * int
- * B.t Terms.unit_clause
- * B.t Terms.substitution
+ exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
(* The returned active set is the input one + the selected clause *)
val infer_right :
B.t Terms.bag ->
int ->
B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+
+
val keep_simplified:
B.t Terms.unit_clause ->
Index.Index(B).active_set ->
B.t Terms.unit_clause ->
bool
- val are_alpha_eq :
- B.t Terms.unit_clause ->
- B.t Terms.unit_clause ->
- bool
+
end