sig
  module M :
    sig
      val check : ?tnf:bool -> Structure.structure -> Formula.formula -> bool
      val evaluate :
        ?tnf:bool ->
        Structure.structure -> Formula.formula -> Assignments.assignment_set
      val evaluate_partial :
        ?tnf:bool ->
        Structure.structure ->
        Assignments.assignment_set ->
        Formula.formula -> Assignments.assignment_set
      val evaluate_real :
        string ->
        Formula.real_expr ->
        Structure.structure -> Assignments.assignment_set
      val get_real_val :
        ?asg:Assignments.assignment_set ->
        Formula.real_expr -> Structure.structure -> float
      val set_timeout : (unit -> bool) -> unit
      val clear_timeout : unit -> unit
    end
  val register_dnf_param : int Pervasives.ref
  val eval_counter : int Pervasives.ref
  val clear_cache : unit -> unit
  val so_to_qbf :
    ?ids:(string * int array, int) Hashtbl.t ->
    ?rev_ids:(int, string * int array) Hashtbl.t ->
    ?assigned:(Formula.var * int) list ->
    Structure.structure ->
    Formula.formula ->
    QBF.qbf * (string * int array, int) Hashtbl.t *
    (int, string * int array) Hashtbl.t
  val find_so :
    ?maximize:bool ->
    ?logtime:float ->
    ?logprefix:string ->
    ?tnf:bool ->
    Structure.structure -> Formula.formula -> Structure.structure * bool
  val add_def_rels :
    Structure.structure ->
    (string * string list * Formula.formula) list -> Structure.structure
  val add_def_funs :
    Structure.structure ->
    (string * string * Formula.real_expr) list -> Structure.structure
end