sig
  type status = Sat | Unsat | Unknown
  type attribute =
      Name of string
    | Sorts of string list
    | Funs of Constant.t list
    | Preds of Constant.t list
    | Definition of string
    | Axioms of Term.term list
    | Theory of Smtlib_attribute.attribute list
    | Language of string
    | Extensions of string
    | Logic of Smtlib_attribute.attribute list
    | Assumption of Term.term
    | Formula of Term.term
    | Status of Smtlib_attribute.status
    | Notes of string
    | Annotation of (string * string option)
  val assumptions : Smtlib_attribute.attribute list -> Term.term list
  val formula : Smtlib_attribute.attribute list -> Term.term
  val status : Smtlib_attribute.attribute list -> Smtlib_attribute.status
  val name : Smtlib_attribute.attribute list -> string
  val logic :
    Smtlib_attribute.attribute list -> Smtlib_attribute.attribute list
end

---

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