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