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

---

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