Struct biodivine_sketchbook::algorithms::fo_logic::fol_tree::FolTreeNode

pub struct FolTreeNode {
    pub formula_str: String,
    pub height: u32,
    pub node_type: NodeType,
}

A single node in a syntax tree of a FOL formula.

Each node tracks its: - height; A positive integer starting from 0 (for term nodes). - node_type; A collection of node data represented through NodeType. - subform_str; A canonical string representation of the FOL formula, which is used for uniqueness testing during simplification and canonization.

Fields

formula_str: String

height: u32

node_type: NodeType

Implementations

impl FolTreeNode

pub fn from_tokens(tokens: &[FolToken]) -> Result<FolTreeNode, String>

“Parse” a new FolTreeNode from a list of FolToken objects.

Note that this is a very “low-level” function. Unless you know what you are doing, you should probably use some of the functions in crate::algorithms::fo_logic::parser instead.

pub fn mk_quantifier( child: FolTreeNode, var: &str, op: Quantifier, ) -> FolTreeNode

Create a “quantifier” FolTreeNode from the given arguments.

See also NodeType::Quantifier.

pub fn mk_unary(child: FolTreeNode, op: UnaryOp) -> FolTreeNode

Create a “unary” FolTreeNode from the given arguments.

See also NodeType::Unary.

pub fn mk_binary( left: FolTreeNode, right: FolTreeNode, op: BinaryOp, ) -> FolTreeNode

Create a “binary” FolTreeNode from the given arguments.

See also NodeType::Binary.

pub fn mk_constant(constant_val: bool) -> FolTreeNode

Create a FolTreeNode representing a Boolean constant.

See also NodeType::Terminal and Atom::True / Atom::False.

pub fn mk_variable(var_name: &str) -> FolTreeNode

Create a FolTreeNode representing a variable.

See also NodeType::Terminal and Atom::Var.

fn mk_atom(atom: Atom) -> FolTreeNode

A helper function which creates a new FolTreeNode for the given Atom value.

pub fn mk_function( name: &str, inner_nodes: Vec<FolTreeNode>, is_update: bool, ) -> FolTreeNode

Create a FolTreeNode representing a function symbol applied to given arguments.

impl FolTreeNode

pub fn from_fn_update( fn_update: FnUpdate, bn_context: &BooleanNetwork, ) -> FolTreeNode

Recursively obtain the FolTreeNode from a similar FnUpdate object of the [biodivine_lib_param_bn] library that is used internally for update functions. The provided BN gives context for variable and parameter IDs.

pub fn substitute_variable( &self, var: &str, expression: &FolTreeNode, ) -> FolTreeNode

Create a copy of this FolTreeNode with every occurrence of variable var substituted for FolTreeNode expression.

You must ensure that no conflicts arise with quantification. For instance, this should be safe in case you are not substituting to quantified variables.

impl FolTreeNode

pub fn as_str(&self) -> &str

Trait Implementations

impl Clone for FolTreeNode

fn clone(&self) -> FolTreeNode

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for FolTreeNode

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for FolTreeNode

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for FolTreeNode

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for FolTreeNode

fn eq(&self, other: &FolTreeNode) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for FolTreeNode

impl StructuralPartialEq for FolTreeNode