sig
  type solver
  val new_solver : unit -> Dpll_core.solver
  val fresh_variable : Dpll_core.solver -> Dpll_literal.Variable.t
  val add_clause : Dpll_core.solver -> Dpll_literal.Literal.t list -> unit
  val model : Dpll_core.solver -> Dpll_literal.Literal.t list
  val add_interface_variable :
    Dpll_core.solver -> Dpll_literal.Variable.t -> unit
  val is_interface_variable :
    Dpll_core.solver -> Dpll_literal.Variable.t -> bool
  val decision_level : Dpll_core.solver -> int
  val inference_possible : Dpll_core.solver -> bool
  val get_literal_possible : Dpll_core.solver -> bool
  val conflict_detected : Dpll_core.solver -> bool
  val decision_possible : Dpll_core.solver -> bool
  val backjump_possible : Dpll_core.solver -> bool
  val satisfied : Dpll_core.solver -> bool
  val unsatisfiable : Dpll_core.solver -> bool
  val is_true : Dpll_core.solver -> Dpll_literal.Literal.t -> bool
  val is_decided : Dpll_core.solver -> Dpll_literal.Literal.t -> bool
  val is_inferred : Dpll_core.solver -> Dpll_literal.Literal.t -> bool
  val level : Dpll_core.solver -> Dpll_literal.Literal.t -> int
  val decide : Dpll_core.solver -> unit
  val infer : Dpll_core.solver -> unit
  val set_literal : Dpll_core.solver -> Dpll_literal.Literal.t -> unit
  val get_literal : Dpll_core.solver -> Dpll_literal.Literal.t
  val set_conflict_clause :
    Dpll_core.solver -> Dpll_literal.Literal.t list -> unit
  val literal_to_explain : Dpll_core.solver -> Dpll_literal.Literal.t
  val set_literal_explanation :
    Dpll_core.solver -> Dpll_literal.Literal.t list -> unit
  val backjump : Dpll_core.solver -> unit
  val forget_some_learned_clauses : Dpll_core.solver -> unit
  val restart : Dpll_core.solver -> unit
  val num_vars : Dpll_core.solver -> int
  val num_clauses : Dpll_core.solver -> int
  val num_learneds : Dpll_core.solver -> int
  val num_conflicts : Dpll_core.solver -> int
  val num_decisions : Dpll_core.solver -> int
  val num_inferences : Dpll_core.solver -> int
  val num_externally_set : Dpll_core.solver -> int
end

---

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