model.boolean

Attributes

k

Classes

`ParseTree`	A class that parses and represents a propositional formula in a tree structure.
`PropFormulaNN`	A neural network model representing a propositional formula that is constructed

Module Contents

class model.boolean.ParseTree(expr=None)

A class that parses and represents a propositional formula in a tree structure.

node

The node of the ParseTree.

Type:: str

subtrees

The subtrees of the ParseTree.

Type:: list[ParseTree]

height

The height of the ParseTree relative to the root.

Type:: int

Initializes a ParseTree instance.

If no expression is given, then all the attributes will be set to None. If an expression is given, the expression will be parsed, where its node and subtrees will be extracted accordingly. Also, the height of the ParseTree and its subtrees will be determined.

If this ParseTree instance is the root of the entire expression, then the horizontal position of the ParseTree and its subtrees will be assigned.

Parameters:: expr (str, optional) – The expression to be parsed. Defaults to None.

get_leafs()

Retrieves the list of all leafs nodes in the ParseTree.

Returns:

List of all ParseTree instances contianing: leaf nodes/atomic variables of ParseTree.

Return type:

list[ParseTree]

get_height_subtrees(target_height)

Returns the list of all subtrees with the specified height within the ParseTree.

Parameters:

target_height (int) – The target height of interest.

Returns:

A list of ParseTree instances with the specified height relative: to the root.

Return type:

List[ParseTree]

__repr__()

Returns the string representation of the ParseTree.

Returns:: The string representation of the node.
Return type:: str

_get_height()

Returns the height of the ParseTree.

A ParseTree with a single node and no subtree will have height 0.

Returns:: The height of the ParseTree.
Return type:: int

_fill_height_gaps(): Adds trees between nodes such that the height difference between each node is kept at 1.

_create_identity_trees(subtree)

Creates ParseTrees that carry the idenity operation.

Parameters:

subtree (ParseTree) – The subtree to connect with using intermediate identity trees.

Returns:

The first ParseTree that is connected with the target subtree: through the chain of intermidate identity trees.

Return type:

ParseTree

_parse(expr)

Parses string expression of a propositional formula to identify its current node/operator and the subtrees/subformulas for its sub-expressions.

Parameters:: expr (sympy.Expr) – The expression to be parsed.
Returns:: A tuple containing the current node and its subtrees.
Return type:: tuple[str, list[ParseTree]]

class model.boolean.PropFormulaNN(formula_expr: sympy.core.function.FunctionClass, atoms: Tuple)

Bases: torch.nn.Sequential

A neural network model representing a propositional formula that is constructed using only NOT (~), OR (|), AND (&) with syntax from SymPy.

It takes inputs where -1 represents False and +1 represents True.

Inherits from:: torch.nn.Sequential: Parent class for implementing neural networks with modules defined in a sequential manner.

parse_tree

The ParseTree representation of the formula.

Type:: ParseTree

atoms

The unique atoms in the formula. The ordering of this tuple matters in determining the ordering of the input to the network.

Type:: tuple[str]

Initializes a PropFormulaNN instance and generates all the torch.nn.Linear layers necessary to construct the neural network.

Parameters:

formula_expr (sympy.core.function.FunctionClass) – The expression representing the propositional formula. Constructed using only syntax from SymPy with the operators NOT (~), OR (|), AND (&).
atoms (tuple[str]) – A tuple of unique atoms in the formula.

parse_tree

atoms

_init_layers() → List[torch.nn.Module]

Initializes all the layers of the neural network into a list of nn.Module.

The layers are initialized and created in ascending order of height in the ParseTree representation of the formula.

Returns:: List of neural network layers.
Return type:: list[torch.nn.Module]

_atom_layer() → torch.nn.Module

Initializes the first layer of the neural network that duplicates and reorders the input propositional atoms based on their ordering in the ParseTree.

Returns:: Linear layer that duplicates and reorders the input atoms.
Return type:: torch.nn.Linear

_get_height_layers(height: int) → List[torch.nn.Module]

Retrieves layers corresponding to a specific height in the ParseTree.

Parameters:

height (int) – The specified height within the ParseTree representatation.

Returns:

List of neural network layers for the nodes that are located: at the given height in the ParseTree representation.

Return type:

list[torch.nn.Module]

_init_binary_operator_layers(subtree_ls: List[ParseTree]) → List[torch.nn.Module]

Initializes the all the layers associated with carrying out the operators involved in the given list of subtrees.

It assumes that the given list of subtrees contains at least one that involves a binary operator/connective.

Parameters:: subtree_ls (list[ParseTree]) – List of ParseTree instances with the same height in the full ParseTree that includes binary operators.
Returns:: List of neural network layers for binary operators.
Return type:: list[torch.nn.Module]

_binary_operator_block(arg_num_ls: List[int], subtree_ls: List[ParseTree], first_block: bool = False) → List[torch.nn.Module]

Creates a block of layers that simpliefies the subexpression for the given list of subtrees by applying the binary operator/connective once whenever possible.

The binary operator/connective from the same subtree can be applied simultaneously as long as the number of arguments inputted to it permits (i.e. divisible by two).

Parameters:

arg_num_ls (list[int]) – List of number of arguments that the operator/node of each subtrees takes.
subtree_ls (list[ParseTree]) – List of subtrees with the same height in the ParseTree.
first_block (bool) – Indicates if this is the first block of the layers for this collection of subtrees with the same height.

Returns:

List of neural network layers in a single block.

Return type:

list[torch.nn.Module]

_identity_weights() → Tuple[torch.Tensor, torch.Tensor]

Generates the weights for the two nn.Linear layers in an identity block.

Returns:: Inter and out layer weights for an identity block.
Return type:: tuple[torch.Tensor, torch.Tensor]

_and_or_weights(sub_inter_dim: int, operator: str) → Tuple[torch.Tensor, torch.Tensor]

Generates weights for the two nn.Linear layers in an AND or OR block.

Parameters:

sub_inter_dim (int) – Dimension of the intermediate layer.
operator (str) – The operator type (AND or OR).

Returns:

Inter and out layer weights for an AND or OR block.

Return type:

tuple[torch.Tensor, torch.Tensor]

_init_unary_operator_layer(subtree_ls: List[ParseTree]) → List[torch.nn.Module]

Initializes the all the layers associated with carrying out the operators involved in the given list of subtrees.

It assumes that the given list of subtrees contains only unary operators.

Parameters:: subtree_ls (list[ParseTree]) – List of ParseTree instances with the same height in the full ParseTree that only has unary operators.
Returns:: List of neural network layers for unary operators.
Return type:: list[torch.nn.Module]

_count_binary_operators(subtree_ls: List[ParseTree]) → int

Counts the occurrences of binary operators in the given list of ParseTree instances.

Parameters:: subtree_ls (list[ParseTree]) – List of ParseTree instances with the same height in the full ParseTree.
Returns:: Count of binary operators.
Return type:: int

_post_block_arg_num_ls(arg_num_ls: List[int]) → List[int]

Returns the list of number of arguments of each subtree after a binary operator block of layers.

Parameters:: arg_num_ls (list[int]) – List of numbers of arguments for each subtree.
Returns:: Number of arguments for each subtree after a block.
Return type:: list[int]

model.boolean.k