sig
  module Variable :
    sig
      type t = int
      val invalid : t
      val is_valid : t -> bool
      val equal : t -> t -> bool
      val hash : t -> int
      val compare : t -> t -> int
      type generator
      val new_generator : unit -> generator
      val fresh : generator -> t
      val count : generator -> int
      val iter : (t -> unit) -> generator -> unit
      val fold : ('a -> t -> 'a) -> 'a -> generator -> 'a
    end
  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 type L =
    sig
      type number
      type t = Dl_core.Variable.t * Dl_core.Variable.t * Dl_core.L.number
      val equal : Dl_core.L.t -> Dl_core.L.t -> bool
      val hash : Dl_core.L.t -> int
    end
  module type T =
    sig
      type num
      module Literal :
        sig
          type number = num
          type t = Variable.t * Variable.t * number
          val equal : t -> t -> bool
          val hash : t -> int
        end
      type literal = Dl_core.T.Literal.t
      type t
      val negation : Dl_core.T.literal -> Dl_core.T.literal
      val new_solver : unit -> Dl_core.T.t
      val fresh_variable : Dl_core.T.t -> Dl_core.Variable.t
      val add_literal : Dl_core.T.t -> Dl_core.T.literal -> unit
      val conflict_detected : Dl_core.T.t -> bool
      val inference_possible : Dl_core.T.t -> bool
      val get_literal_possible : Dl_core.T.t -> bool
      val get_lemma_possible : Dl_core.T.t -> bool
      val decision_level : Dl_core.T.t -> int
      val increment_level : Dl_core.T.t -> unit
      val set_literal : Dl_core.T.t -> Dl_core.T.literal -> unit
      val get_literal : Dl_core.T.t -> Dl_core.T.literal
      val get_lemma : Dl_core.T.t -> Dl_core.T.literal list
      val infer : Dl_core.T.t -> unit
      val explain_conflict : Dl_core.T.t -> Dl_core.T.literal list
      val explain :
        Dl_core.T.t -> Dl_core.T.literal -> Dl_core.T.literal list
      val backtrack : Dl_core.T.t -> int -> unit
      val is_true : Dl_core.T.t -> Dl_core.T.literal -> bool
      val potential : Dl_core.T.t -> Dl_core.T.num Dl_core.Variable_map.t
    end
  module Make :
    functor (N : Dl_number.T) ->
      sig
        type num = N.t
        module Literal :
          sig
            type number = num
            type t = Variable.t * Variable.t * number
            val equal : t -> t -> bool
            val hash : t -> int
          end
        type literal = Literal.t
        type t
        val negation : literal -> literal
        val new_solver : unit -> t
        val fresh_variable : t -> Variable.t
        val add_literal : t -> literal -> unit
        val conflict_detected : t -> bool
        val inference_possible : t -> bool
        val get_literal_possible : t -> bool
        val get_lemma_possible : t -> bool
        val decision_level : t -> int
        val increment_level : t -> unit
        val set_literal : t -> literal -> unit
        val get_literal : t -> literal
        val get_lemma : t -> literal list
        val infer : t -> unit
        val explain_conflict : t -> literal list
        val explain : t -> literal -> literal list
        val backtrack : t -> int -> unit
        val is_true : t -> literal -> bool
        val potential : t -> num Variable_map.t
      end
end

---

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