sig
  module Variable : Id.Generator
  type literal =
      Equality of Variable.t * Variable.t
    | Disequality of Variable.t * Variable.t
  val invalid_literal : Cc_literal.literal
  val is_valid_literal : Cc_literal.literal -> bool
  val equal : Cc_literal.literal -> Cc_literal.literal -> bool
  val negation : Cc_literal.literal -> Cc_literal.literal
  type lemma =
      RoK of Variable.t * Variable.t * Variable.t
    | Row1 of Variable.t * Variable.t * Variable.t
    | Row2 of Variable.t * Variable.t * Variable.t * Variable.t
    | Ext of Variable.t * Variable.t
  module Variable_map :
    sig
      type key = Variable.t
      type 'a t
      val size : 'a t -> int
      val create : 'a -> 'a t
      val is_empty : 'a t -> bool
      val mem : 'a t -> key -> bool
      val find : 'a t -> key -> 'a
      val add : 'a t -> key -> 'a -> unit
      val replace : 'a t -> key -> 'a -> unit
      val copy : 'a t -> 'a t
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val iter_const : ('a -> key -> 'b -> unit) -> 'a -> 'b t -> unit
      val fold : ('a -> key -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val fold_const :
        ('a -> 'b -> key -> 'c -> 'b) -> 'a -> 'b -> 'c t -> 'b
      val modify : ('a -> 'a) -> 'a t -> unit
      val modify_const : ('a -> 'b -> 'b) -> 'a -> 'b t -> unit
      val set_all : 'a t -> 'a -> unit
    end
  module Variable_hash :
    sig
      type key = Variable.t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  module Variable_map2 :
    sig
      type key0 = Variable.t
      type key1 = Variable.t
      type 'a t
      val create : int -> int -> 'a t
      val mem : 'a t -> key0 -> key1 -> bool
      val find : 'a t -> key0 -> key1 -> 'a
      val set : 'a t -> key0 -> key1 -> 'a -> unit
      val remove : 'a t -> key0 -> key1 -> unit
    end
  module Variable_set :
    sig
      type elt = Variable.t
      type t
      val create : unit -> t
      val size : t -> int
      val is_empty : t -> bool
      val mem : t -> elt -> bool
      val add : t -> elt -> unit
      val remove : t -> elt -> unit
      val clear : t -> unit
      val iter : (elt -> unit) -> t -> unit
      val iter_const : ('a -> elt -> unit) -> 'a -> t -> unit
      val fold : ('a -> elt -> 'a) -> 'a -> t -> 'a
      val fold_const : ('a -> 'b -> elt -> 'b) -> 'a -> 'b -> t -> 'b
    end
end

---

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.