sig
  type 'a tokenizer = Lexing.lexbuf -> 'a
  type ('a, 'b) recognizer =
      'a Smtlib_parser.tokenizer -> Lexing.lexbuf -> 'b
  val initialized : unit -> bool
  val initialize :
    string ->
    'a Smtlib_parser.tokenizer ->
    ('a, Smtlib_attribute.attribute list) Smtlib_parser.recognizer ->
    ('a, Smtlib_attribute.attribute list) Smtlib_parser.recognizer ->
    ('a, Smtlib_attribute.attribute list) Smtlib_parser.recognizer -> unit
  val smtlib_theory_file : string -> string
  val smtlib_logic_file : string -> string
  val parse_theory : string -> Smtlib_attribute.attribute list
  val parse_logic : string -> Smtlib_attribute.attribute list
  val parse_benchmark : string -> Smtlib_attribute.attribute list
end

---

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