Module Parse_tptp

module Parse_tptp: sig .. end

type token =

`\|`	`XOR`
`\|`	`WILDCARD`
`\|`	`VLINE`
`\|`	`UPPER_WORD of string`
`\|`	`UNDERSCORE`
`\|`	`TYPE_TY`
`\|`	`TRUE`
`\|`	`TFF`
`\|`	`STAR`
`\|`	`SINGLE_QUOTED of string`
`\|`	`RIGHT_PAREN`
`\|`	`RIGHT_BRACKET`
`\|`	`REAL of string`
`\|`	`RATIONAL of string`
`\|`	`NOT_EQUAL`
`\|`	`NOTVLINE`
`\|`	`NOTAND`
`\|`	`NOT`
`\|`	`LOWER_WORD of string`
`\|`	`LEFT_PAREN`
`\|`	`LEFT_IMPLY`
`\|`	`LEFT_BRACKET`
`\|`	`INTEGER of string`
`\|`	`INCLUDE`
`\|`	`IMPLY`
`\|`	`GENTZEN_ARROW`
`\|`	`FORALL_TY`
`\|`	`FORALL`
`\|`	`FOF`
`\|`	`FALSE`
`\|`	`EXISTS`
`\|`	`EQUIV`
`\|`	`EQUAL`
`\|`	`EOI`
`\|`	`DOT`
`\|`	`DOLLAR_WORD of string`
`\|`	`DOLLAR_DOLLAR_WORD of string`
`\|`	`DISTINCT_OBJECT of string`
`\|`	`COMMA`
`\|`	`COLUMN`
`\|`	`CNF`
`\|`	`ARROW`
`\|`	`AND`

exception Error

val parse_term : (Lexing.lexbuf -> token) ->
       Lexing.lexbuf -> Libzipperposition.STerm.t

val parse_formula : (Lexing.lexbuf -> token) ->
       Lexing.lexbuf -> Libzipperposition.STerm.t

val parse_declarations : (Lexing.lexbuf -> token) ->
       Lexing.lexbuf -> Libzipperposition.STerm.t Ast_tptp.declaration list

val parse_declaration : (Lexing.lexbuf -> token) ->
       Lexing.lexbuf -> Libzipperposition.STerm.t Ast_tptp.declaration

val parse_answer_tuple : (Lexing.lexbuf -> token) ->
       Lexing.lexbuf -> Libzipperposition.STerm.t list list