Struct Formula 

pub struct Formula<B, U, A>
where
    B: Symbolic,
    U: Symbolic,
    A: Symbolic,
{
    pub tree: Tree<B, U, A>,
    pub zipper: Zipper<B, U, A>,
}

The primary generic struct for logical formulas that implement both unary and binary operators. The struct is generic over the type of binary operators B, unary operators U, and the atoms A, and assumes all three are very cheap (e.g. fieldless enums, integers) and therefore implement Copy. It’s possible this requirement will be relaxed in future versions for the atoms ‘A’, in case there’s a need for very complex atoms (i.e. arbitrarily large relations).

This is a zipper implementation of binary/unary trees which represent logical formulae. This means that a Formula is not just a tree, but a tree and a particular location in that tree, represented by the zipper; please read the source material for more if you want to understand how this works. At the basic level you may assume that .*_unzip, methods go ‘down’ the tree while .*_zip methods go up. If the formula is fully zipped (i.e. by calling top_zip) the tree is in fact the whole formula, with Zipper::Top stored as a sentinel zipper.

The implementation therefore always operates/mutates the formula at its current location in the tree, so if you want to operate on the very ‘top’ of the formula you must call top_zip first. The only exception to this is methods that start with .top_, which you may assume call top_zip before performing mutations.

The mutating methods therefore change different properties about the formula but leave the ‘location’ of the formula, i.e. the current .tree, untouched or as untouched as possible, so that these mutations can be done repeatedly as part of, for example, an inorder_traverse_mut. It can be hard to understand this abstractly so it’s best to read the documentation for concrete transforming methods like combine or distribute_right for a clearer view.

This implementation does not use the builder pattern, both out of dislike but also because this would be impossible to PyBind if methods took self or require a duplicate implementation.

For builder-style method chaining use the wonderful cascade! macro. The Python wrappers do use a chainable pattern (taking and receiving &mut self) and can of course be used from the Rust API, but the Python API is really designed for Pythonic use and this API for Rust.

Finally, the API is designed for safety in the sense that transformations that are applied are only applied if they’re valid at the current location in the formula and don’t do anything otherwise! This is an opinionated design decision because this crate is fundamentally designed for situations that demand lots of rapid transformation the circumstance when you want to apply a transformation if possible or not do anything, e.g. when converting a formula to conjunctive normal form. Returning Result<T, E> in this situation would inappropriately stop such fast transformation chains and require a lot of branching in code. Nonetheless a trait may be added and implemented for this type which reimplements the methods to allow one to immediately discern if a formula has changed after a method call because there’s no signal something has either happened or failed to (e.g. as would be signaled by returning a Result<T, E> type).

Fields

tree: Tree<B, U, A>

zipper: Zipper<B, U, A>

Implementations

impl<B: Symbolic, U: Symbolic, A: Symbolic> Formula<B, U, A>

This first impl block is for initialization and traversal.

pub fn new(atom: A) -> Self

A new formula that’s just an atom.

pub fn zip(&mut self)

Traverse the current zipper one step, reconstructing the tree, whether you’re in a binary tree (i.e. a left or right zipper) or a unary one (up zipper); doesn’t do anything if you’re at Zipper::Top.

pub fn zip_up(&mut self)

In the subtree of a unary tree, go UP and eat the unary operator back into the tree. That is,

  zipper: (U, Zipper)       zipper: (*Zipper)
                                
           ^        =>         ^
           |                   |
                                
          tree              tree: U
                                  |
                               old_tree

pub fn zip_right(&mut self)

In the left subtree of a binary tree, go “right” and eat the binary operator and right subtree! You’re basically recombining them, like

        zipper: (B, RTree, Zipper)        zipper: (*Zipper)
         /                                      |
        /                            =>         |
      tree: LTree                          tree: B
                                               /   \
                                            LTree  RTree

pub fn zip_left(&mut self)

Just like zip_right except you’re in the right subtree of a binary tree. The destination state is the exact same.

pub fn unzip_right(&mut self)

The inverse of zip_left. Decompose a binary tree and traverse to the right subtree of a binary formula.

pub fn unzip_left(&mut self)

The inverse of zip_right: decompose a binary tree and travel to the left subtree of a binary formula.

pub fn unzip_down(&mut self)

Traverse to the formula contained in a unary tree. The inverse of zip_up.

pub fn top_zip(&mut self)

Unzip the formula, i.e. return to the top node. After this, self.tree contains the whole formula.

pub fn inorder_traverse_mut<F: FnMut(&mut Self) -> Option<()>>( &mut self, func: &mut F, ) -> Option<()>

Inorder traversal starting at the current context. If you want the whole formula simply top_zip first. Takes in a closure which can mutate the formula in place somehow. Returns Option<()> so traversal can be stopped early if needed; in most cases can be ignored.

pub fn preorder_traverse_mut<F: FnMut(&mut Self) -> Option<()>>( &mut self, func: &mut F, ) -> Option<()>

Preorder traversal starting at the current context. Also takes in a closure that can mutate the formula. This is a much more dangerous traversal strategy to call with a transformation method like rotate_right compared to inorder_traverse_mut; the latter will travel to the leaves of a formula and then perform transforms going back up the zipper, whereas this method will apply transformations immediately as it visits each node, having potentially weird consequences if there are in place mutations going on with formulae.

pub fn inorder_traverse<F: FnMut(&Tree<B, U, A>) -> Option<()>>( &self, func: &mut F, ) -> Option<()>

pub fn preorder_traverse<F: FnMut(&Tree<B, U, A>) -> Option<()>>( &self, func: &mut F, ) -> Option<()>

impl<B: Symbolic, U: Symbolic, A: Symbolic> Formula<B, U, A>

This impl is about manipulating and combining formulas.

pub fn combine(&mut self, bin: B, new_tree: Tree<B, U, A>)

Connects to a new formula WITHOUT unzipping, which is why this takes in a tree. Whatever the current .tree is will become the left subtree of a binary tree, where new_tree is the right subtree and they’re connected by bin. This is a very zipper-style impl which might be counter intuitive, and perhaps better illustrated with some poor ASCII art:

         zipper                 zipper: Zipper::Right(bin, new_tree, old_zipper)
                                
           ^        =>            /
           |                    /
                                
          tree               tree

pub fn left_combine(&mut self, bin: B, new_tree: Tree<B, U, A>)

Exactly the same as combine but the new subtree is inserted as a left subtree, so you’re now in the right subtree of a binary tree. And therefore you end up with a Zipper::Left.

pub fn top_combine(&mut self, bin: B, formula: Self)

Combine two formulas with a binary connective. But unzip first.

pub fn top_left_combine(&mut self, bin: B, formula: Self)

top_combine but on the left side.

pub fn unify(&mut self, un: U)

Insert a unary operator in the formula’s current position.

pub fn top_unify(&mut self, un: U)

Insert a unary operator for the whole formula.

pub fn flip(&mut self)

A function which demonstrates some zipper-y fun, if you’re currently at the right or left subtree of a binary formula, i.e. the current zipper is Zipper::Right{..} or Zipper::Left{..}, swap your position with the other subtree (without moving memory). Otherwise, the formula remains the same.

pub fn rotate_left(&mut self)

If it applies in the current context, ‘rotate’ a tree formula, i.e. change precedence between two binary operators, to the left. As an example,

    →                                       
  /   \\
A       ∧          
      /   \
    B       C

        =>

            ∧                               
         //   \
        →       C   
      /   \
    A       B

is an example of a left rotation. Rotations are always performed assuming the current zipper holds the lower-precedence B, i.e. the one higher up in the tree. In the example above, the rotation would be performed on a Formula where the zipper is the \ pictured, holding the → operator. self is left in the same position after rotation, with // denoting the new active zipper.

pub fn rotate_right(&mut self)

If it applies in the current context, ‘rotate’ a tree formula, i.e. change precedence between two binary operators, to the right. As an example,

         ∧                               
      //   \
     →      C   
   /   \
 A       B

              =>

                    →                                       
                  /   \\
                A       ∧          
                      /   \
                    B       C

is an example of a right rotation. More detail available in the documentation of .rotate_left().

pub fn distribute_right(&mut self)

‘Distribute’ a binary operator over the right (binary) subtree. Often used in, for example, creating the conjunctive normal forms of formulae. Easiest to see by example:

        ∧
     /     \\
   p        ∨
         /      \
       q         r

                       =>
                                   ∨
                              /        \\
                           ∧               ∧
                       /       \       /       \
                      p         q     p         r

The dummy formula corresponding to p above gets cloned. Just like with the rotation methods, the above method occurs starting from the higher-precedence operator (lower in the subtree) corresponding to \ being the active zipper, and \ in the second formula describes the active zipper after distribution.

pub fn distribute_left(&mut self)

Distribute a binary operator over the left subtree (corresponding to a right rotation). See distribute_right for more.

pub fn lower_right(&mut self)

Very similar to the .rotate_* methods but with unary operators swapping precedence with binary ones instead. Because of this the .lower_* methods don’t reverse each other unlike the .rotate_* methods. This method unifies the right subformula.

pub fn lower_left(&mut self)

Same as .lower_right() but unifies the left subformula.

pub fn distribute_down(&mut self, new_bin: Option<B>)

Distribute a unary operator over a binary operator. Optionally pass in a new binary operator to root the formula after distribution. Basically like executing lower_left and lower_right at the same time, and optionally swapping the root of the binary tree. If you’re unfamiliar with logic, this method exists because in numerous languages a binary operator will have a ‘dual’ operator that it swaps with when a unary operator is distributed over the two operands.

pub fn push_down(&mut self, new_un: Option<U>)

Swap two unary operators, optionally changing the one that’s been swapped up. This exists because oftentimes unary operators have a ‘dual’ operator which they change to when another unary operator changes precedence with them.

pub fn instantiate(&mut self, formulas: &HashMap<A, Tree<B, U, A>>)

Instantiate an atom in the formula (as usual, starting where you currently are) with another tree subformula. If you want to do this over a whole formula, just call this inside inorder_traverse_mut.

impl<B: Symbolic, U: Symbolic, A: Symbolic> Formula<B, U, A>

This block is about interfacing with tensors.

pub fn tensorize( &self, mapping: &HashMap<Symbol<B, U, A>, usize>, ) -> Result<(Vec<usize>, Vec<Vec<usize>>), ParseError>

Given some arbitrary mapping from symbols to nonnegative integers, encode a formula as a list of integers corresponding to an inorder traversal of the nodes, and another list of the parent-child relationships between the nodes. If the mapping given is not total, return None. The edges are returned in COO format (two lists of pairs, corresponding by index).

pub fn get_atoms(&self) -> HashSet<A>

Store all the atoms that appear in the formula in a HashSet.

pub fn normalize<I: Iterator<Item = A>>(&self, indices: I) -> Option<Self>

Normalize all the atoms in a formula by replacing its atoms with atoms that index their first appearance in an inorder traversal. The indices given are taken from a passed in iterator (over A) on which std::iter::Iterator::next is called precisely once every time a new atom is observed. In case the iterator runs out, returns None.

Trait Implementations

impl<B, U, A> Clone for Formula<B, U, A>

where B: Symbolic + Clone, U: Symbolic + Clone, A: Symbolic + Clone,

fn clone(&self) -> Formula<B, U, A>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<B, U, A> Debug for Formula<B, U, A>

where B: Symbolic + Debug, U: Symbolic + Debug, A: Symbolic + Debug,

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

Formats the value using the given formatter.

impl<B, U, A> Default for Formula<B, U, A>

where B: Symbolic + Default, U: Symbolic + Default, A: Symbolic + Default,

fn default() -> Formula<B, U, A>

Returns the “default value” for a type.

impl<B, U, A> Display for Formula<B, U, A>

where B: Symbolic, U: Symbolic, A: Symbolic,

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

Read string representation starting from current position in formula. THIS WILL NOT PRINT ANY UNZIPPED PARTS OF THE FORMULA. Make sure to Formula::top_zip first if you want the whole formula. Printing is an easy way to see “where” you are in the formula.

impl<B, U, A> From<&Formula<B, U, A>> for Tree<B, U, A>

where B: Symbolic, U: Symbolic, A: Symbolic,

If you’re really lazy I guess!

fn from(value: &Formula<B, U, A>) -> Self

Converts to this type from the input type.

impl<B, U, A> From<Tree<B, U, A>> for Formula<B, U, A>

where B: Symbolic, U: Symbolic, A: Symbolic,

fn from(value: Tree<B, U, A>) -> Self

Converts to this type from the input type.

impl<B, U, A> Hash for Formula<B, U, A>

where B: Symbolic + Hash, U: Symbolic + Hash, A: Symbolic + Hash,

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<B, U, A> Ord for Formula<B, U, A>

where B: Symbolic + Ord, U: Symbolic + Ord, A: Symbolic + Ord,

fn cmp(&self, other: &Formula<B, U, A>) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl<B, U, A> PartialEq for Formula<B, U, A>

where B: Symbolic + PartialEq, U: Symbolic + PartialEq, A: Symbolic + PartialEq,

fn eq(&self, other: &Formula<B, U, A>) -> 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<B, U, A> PartialOrd for Formula<B, U, A>

where B: Symbolic + PartialOrd, U: Symbolic + PartialOrd, A: Symbolic + PartialOrd,

fn partial_cmp(&self, other: &Formula<B, U, A>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

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

Tests less than (for self and other) and is used by the < operator.

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

Tests less than or equal to (for self and other) and is used by the <= operator.

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

Tests greater than (for self and other) and is used by the > operator.

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

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<B, U, A> Eq for Formula<B, U, A>

where B: Symbolic + Eq, U: Symbolic + Eq, A: Symbolic + Eq,

impl<B, U, A> StructuralPartialEq for Formula<B, U, A>

where B: Symbolic, U: Symbolic, A: Symbolic,