/* Copyright (c) Microsoft Corporation */

quote(mli,"
(**
  Summary: \[ [ parse_smtlib_string_x c str sort_names sorts decl_names decls ] \]

  Parse the given string using the SMT-LIB parser. 

  The symbol table of the parser can be initialized using the given sorts and declarations. 
  The symbols in the arrays [sort_names] and [decl_names] don't need to match the names
  of the sorts and declarations in the arrays [sorts] and [decls]. This is an useful feature
  since we can use arbitrary names to reference sorts and declarations defined using the API.

  - {b See also}: {!parse_smtlib_file_x}
*)
val parse_smtlib_string_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)

(**
  Summary: Similar to {!parse_smtlib_string_x}, but reads the benchmark from a file.

  - {b See also}: {!parse_smtlib_string_x}
*)
val parse_smtlib_file_x: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> (ast array * ast array * func_decl array)

(**
  Summary: \[ [ parse_smtlib_string_formula c ... ] \] calls [(parse_smtlib_string c ...)] and returns the single formula produced.

  - {b See also}: {!parse_smtlib_file_formula}
  - {b See also}: {!parse_smtlib_string_x}
*)
val parse_smtlib_string_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast

(**
  Summary: \[ [ parse_smtlib_file_formula c ... ] \] calls [(parse_smtlib_file c ...)] and returns the single formula produced.

  - {b See also}: {!parse_smtlib_string_formula}
  - {b See also}: {!parse_smtlib_file_x}
*)
val parse_smtlib_file_formula: context -> string -> symbol array -> sort array -> symbol array -> func_decl array -> ast
");
