module M : Map.S with type key = int
type 'a bag = int (* max ID *)
- * (('a unit_clause * bool * int) M.t)
+ * (('a clause * bool * int) M.t)
(* also gives a fresh ID to the clause *)
val add_to_bag :
- 'a unit_clause -> 'a bag ->
- 'a bag * 'a unit_clause
+ 'a clause -> 'a bag ->
+ 'a bag * 'a clause
val replace_in_bag :
- 'a unit_clause * bool * int -> 'a bag ->
+ 'a clause * bool * int -> 'a bag ->
'a bag
val get_from_bag :
- int -> 'a bag -> 'a unit_clause * bool * int
+ int -> 'a bag -> 'a clause * bool * int
val empty_bag : 'a bag
module type Blob =
sig
(* Blob is the type for opaque leaves:
- * - checking equlity should be efficient
+ * - checking equality should be efficient
* - atoms have to be equipped with a total order relation
*)
type t
* *)
val pp : t -> string
- type input
- val embed : input -> t foterm
- (* saturate [proof] [type] -> [proof] * [type] *)
- val saturate : input -> input -> t foterm * t foterm
-
end