kdrag.parsers.tptp.to_z3

kdrag.parsers.tptp.to_z3(tree: Tree, sort: SortRef | None = None) → list[TPTPFormulaEntry]

Transform a TPTP parse tree into Z3 expressions.

>>> import kdrag.parsers.tptp as tptp
>>> tree = tptp.fof_parser.parse("fof(a,axiom, p(a) ).")
>>> entries = tptp.to_z3(tree)
>>> entries[0].name
'a'
>>> entries[0].role
<FormulaRole.AXIOM: 'axiom'>
>>> entries[0].formula
p(a)

Parameters:

tree (Tree)
sort (SortRef | None)

Return type:

list[TPTPFormulaEntry]