unicode_fol_kit.Node

class unicode_fol_kit.Node

Bases: object

Base class for all AST nodes.

__init__()

Methods

__init__()
atoms()	Return all Atom nodes in pre-order (duplicates kept; comparisons included).
count([cls])	Count nodes in the tree; if cls is given, only nodes of that type.
depth()	Return the height of the tree; a leaf node has depth 1.
from_dict(d)	Deserialise a node from a dictionary produced by to_dict.
map_children(fn)	Rebuild this node with fn applied to each immediate Node child.
subformulas()	Yield every sub-node that is a formula (i.e. not an atomic term).
to_dict()	Serialise this node to a JSON-compatible dictionary.
to_dot()	Render the AST as a Graphviz DOT digraph string.
to_latex()	Render this node as a LaTeX math-mode string (no surrounding $…$).
to_msfol()	Lower Łukasiewicz operators to classical counterparts; recurse into children.
to_prover9()	Render this node as a Prover9-syntax string.
to_tptp()	Render this node as a TPTP-syntax string.
to_unicode_str()	Render this node back to a parseable Unicode formula string.
to_z3([env])	Translate this node into a Z3 expression using the given environment.
tree_str()	Render the AST as a multi-line ASCII tree using ├──/└── connectors.
variables()	Return the set of logical Variable nodes occurring anywhere (free and bound).
walk()	Yield this node and every descendant in pre-order (depth-first).

to_dict()

Serialise this node to a JSON-compatible dictionary.

Return type:

dict

to_z3(env=None)

Translate this node into a Z3 expression using the given environment.

Parameters:

env (Z3Env)

Return type:

ExprRef

to_prover9()

Render this node as a Prover9-syntax string.

Return type:

str

to_tptp()

Render this node as a TPTP-syntax string.

Return type:

str

static from_dict(d)

Deserialise a node from a dictionary produced by to_dict.

Parameters:

d (dict)

Return type:

Node

to_unicode_str()

Render this node back to a parseable Unicode formula string.

The result, re-parsed in the matching MSFLParser mode, yields a structurally equal AST (parser round-trip). The renderer lives in _msfl_nodes.py (imported lazily to avoid a circular import) because it dispatches over both the FOL nodes here and the MSFL/lambda nodes there.

Return type:

str

to_latex()

Render this node as a LaTeX math-mode string (no surrounding $…$).

Uses the same precedence-driven parenthesisation as to_unicode_str. Symbol/function/predicate names are emitted verbatim (no mathrm wrapping). The renderer lives in _msfl_nodes.py (imported lazily) so it can dispatch over both FOL and MSFL/lambda nodes.

Return type:

str

tree_str()

Render the AST as a multi-line ASCII tree using ├──/└── connectors.

Return type:

str

to_msfol()

Lower Łukasiewicz operators to classical counterparts; recurse into children.

Classical and sort-annotated nodes return a structurally equal copy with children recursed. Fuzzy operator subclasses override this to substitute the corresponding classical node type.

Return type:

Node

map_children(fn)

Rebuild this node with fn applied to each immediate Node child.

The single point of structural recursion. Each dataclass field is handled by kind: a Node field becomes fn(value); a list/tuple field has fn mapped over its Node elements (non-Node elements pass through, container kind preserved); any other field is copied verbatim. The node type and field order are preserved.

Binders (Lambda, Quantifier, SortedQuantifier) carry their bound variable as a plain Node field, so fn is applied to it too; callers that must treat a binder’s scope specially should handle that case explicitly before delegating here. This is the shared engine behind the purely structural recursions (to_msfol, _relativize, beta/eta reduction, scope resolution, …), so a new structural node type is handled automatically without touching each traversal.

Return type:

Node

walk()

Yield this node and every descendant in pre-order (depth-first).

subformulas()

Yield every sub-node that is a formula (i.e. not an atomic term).

Terms (Variable, Constant, Number, Function, SortedConstant, LambdaVar) are excluded; everything else reachable is returned in pre-order.

atoms()

Return all Atom nodes in pre-order (duplicates kept; comparisons included).

variables()

Return the set of logical Variable nodes occurring anywhere (free and bound).

count(cls=None)

Count nodes in the tree; if cls is given, only nodes of that type.

Return type:

int

depth()

Return the height of the tree; a leaf node has depth 1.

Return type:

int

to_dot()

Render the AST as a Graphviz DOT digraph string.

Uses the same label/child view as tree_str (the bound variable of a quantifier is folded into its node label, not shown as a child), so the graph mirrors the ASCII tree. No external dependency: returns the source.

Return type:

str