sig
  class type dpll =
    object
      method add_clause : Term.term list -> unit
      method add_interface_variable : Term.term -> unit
      method backjump : unit
      method backjump_possible : bool
      method conflict_detected : bool
      method decide : unit
      method decision_level : int
      method decision_possible : bool
      method forget_some_learned_clauses : unit
      method get_literal : Term.term
      method get_literal_possible : bool
      method infer : unit
      method inference_possible : bool
      method is_interface_literal : Term.term -> bool
      method is_true : Term.term -> bool
      method level : Term.term -> int
      method literal_to_explain : Term.term
      method num_clauses : int
      method num_conflicts : int
      method num_decisions : int
      method num_externally_set : int
      method num_inferences : int
      method num_learneds : int
      method num_vars : int
      method owns_constant : Term.term -> bool
      method proxy : Term.term -> Term.term
      method restart : unit
      method satisfied : bool
      method set_conflict_clause : Term.term list -> unit
      method set_literal : Term.term -> unit
      method set_literal_explanation : Term.term list -> unit
      method unsatisfiable : bool
      method variables : Term.Term_set.t
    end
  class type theory =
    object
      method add_interface_variable : Term.term -> unit
      method backjump : int -> unit
      method conflict_clause : Term.term list
      method conflict_detected : bool
      method decision_level : int
      method final_check : unit
      method get_lemma : Term.term list
      method get_lemma_possible : bool
      method get_literal : Term.term
      method get_literal_possible : bool
      method increment_level : unit
      method infer : unit
      method inference_possible : bool
      method is_interface_literal : Term.term -> bool
      method is_true : Term.term -> bool
      method literal_explanation : Term.term -> Term.term list
      method owns_constant : Term.term -> bool
      method proxy : Term.term -> Term.term
      method restart : unit
      method set_literal : Term.term -> unit
      method variables : Term.Term_set.t
    end
  class type solver =
    object method add_clause : Term.term list -> unit method solve : bool end
end

---

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