sig
  module Variable : Id.Generator
  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_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
  module Variable_queue :
    sig
      type elt = Variable.t
      type t
      val create : elt -> t
      val length : t -> int
      val is_empty : t -> bool
      val mem : t -> elt -> bool
      val head : t -> elt
      val enqueue : t -> elt -> unit
      val dequeue : t -> elt
      val drop : t -> unit
      val priority : t -> elt -> float
      val inc_priority : t -> elt -> float -> unit
      val scale : t -> float -> unit
    end
  module Literal : Id.T
  module Literal_map :
    sig
      type key = Literal.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 Literal_set :
    sig
      type elt = Literal.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
  val variable : Literal.t -> Variable.t
  val is_positive : Literal.t -> bool
  val literal : Variable.t -> Literal.t
  val negation : Literal.t -> Literal.t
end

---

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