unicode_fol_kit.parse_smtlib

unicode_fol_kit.parse_smtlib(text)

Parse an SMT-LIB2 string and return its assertions as toolkit Nodes.

Uses Z3’s own SMT-LIB2 parser (z3.parse_smt2_string) to read the assertions, then converts each with from_z3().

Parameters:

text (str) – SMT-LIB2 source (declare-fun / assert … ).

Returns:

A list of Node, one per top-level assert.

Return type:

list