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

---

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