unicode_fol_kit.from_z3

unicode_fol_kit.from_z3(expr, _scope=None)

Convert a Z3 expression (z3.ExprRef) into a toolkit Node.

The inverse of Node.to_z3(); meaning-preserving (see the module docstring for the inherent Z3 lossiness around free variables / constants / numbers).

Raises:

TypeError – on a Z3 construct with no first-order toolkit counterpart.

Return type:

Node