unicode_fol_kit.parse_prover9_problem

unicode_fol_kit.parse_prover9_problem(text)

Parse a whole Prover9 / LADR input file into a list of Prover9Formula.

Reads set / clear / assign / op directives (recognised and skipped), formulas(LIST). … end_of_list. blocks, and bare top-level formula. statements (% line comments are ignored). Each formula is returned tagged with its list name as role ("" for a bare top-level formula), in source order.

Statements are scanned deterministically (split on the terminating ., with a . inside a decimal number kept), and each formula is parsed by parse_prover9(). A formulas(...) header with no matching end_of_list., a stray end_of_list., or a malformed header is a hard error — unlike a grammar that could silently reinterpret an unterminated list as bare formulas.

Parameters:

text (str) – the contents of a Prover9 problem file.

Returns:

A list of Prover9Formula (role, formula) records.

Raises:

Prover9ParsingError – if the text is not a well-formed Prover9 problem (within the supported subset; an individual formula is parsed by parse_prover9()).

Return type:

list