- (* mk_unit_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
- val mk_unit_clause :
- int -> B.t Terms.foterm -> B.t Terms.foterm ->
- B.t Terms.unit_clause * int
+ (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
+ val mk_clause :
+ int ->
+ B.t Terms.foterm list -> (* negative literals in clause *)
+ B.t Terms.foterm list -> (* positive literals in clause *)
+ B.t Terms.foterm ->
+ B.t Terms.clause * int