val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
- (* 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
val mk_passive_clause :
- B.t Terms.unit_clause -> B.t Terms.passive_clause
+ B.t Terms.clause -> B.t Terms.passive_clause
val mk_passive_goal :
- B.t Terms.unit_clause -> B.t Terms.passive_clause
+ B.t Terms.clause -> B.t Terms.passive_clause
- val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
- val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
+ val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
+ val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
- val fresh_unit_clause :
- int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
+ val fresh_clause :
+ int -> B.t Terms.clause -> B.t Terms.clause * int
(* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
val relocate :