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 t
      val is_empty : 'a t -> bool
      val mem : 'a t -> key -> bool
      val find : 'a t -> key -> 'a
      val add : 'a t -> key -> '-> unit
      val replace : 'a t -> key -> '-> unit
      val copy : 'a t -> 'a t
      val iter : (key -> '-> unit) -> 'a t -> unit
      val iter_const : ('-> key -> '-> unit) -> '-> 'b t -> unit
      val fold : ('-> key -> '-> 'a) -> '-> 'b t -> 'a
      val fold_const :
        ('-> '-> key -> '-> 'b) -> '-> '-> 'c t -> 'b
      val modify : ('-> 'a) -> 'a t -> unit
      val modify_const : ('-> '-> 'b) -> '-> 'b t -> unit
      val set_all : 'a t -> '-> 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 -> '-> 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 -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> '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 -> '-> 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 : ('-> elt -> unit) -> '-> t -> unit
      val fold : ('-> elt -> 'a) -> '-> t -> 'a
      val fold_const : ('-> '-> elt -> 'b) -> '-> '-> t -> 'b
    end
end

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