Struct Formula

pub struct Formula { /* private fields */ }

A parsed formula, in a tree format which is convenient to perform unifications

Implementations

impl Formula

pub fn from_float(label: Label, typecode: TypeCode) -> Self

Creates a formula with just a variable

pub const fn labels_iter(&self) -> LabelIter<'_>

Iterates through the labels of a formula, depth-first, pre-order. Items are the label, and a boolean indicating whether the current label is a variable or not.

pub const fn as_ref<'a>(&'a self, db: &'a Database) -> FormulaRef<'a>

Augment a formula with a database reference, to produce a FormulaRef. The resulting object implements Display, Debug, and IntoIterator.

pub fn dump(&self, nset: &Nameset)

Debug only, dumps the internal structure of the formula.

pub const fn get_typecode(&self) -> TypeCode

Returns the typecode of this formula

pub fn is_singleton(&self) -> bool

Returns whether this formula consists in a single token.

pub fn get_by_path(&self, path: &[usize]) -> Option<Label>

Returns the label obtained when following the given path. Each element of the path gives the index of the child to retrieve. For example, the empty

pub fn unify( &self, other: &Formula, substitutions: &mut Substitutions, ) -> Result<(), UnificationError>

Unify this formula with the given formula model If successful, the provided substitutions are completed with the substitutions which needs to be made in other in order to match this formula.

pub fn substitute(&self, substitutions: &Substitutions) -> Formula

Perform substitutions This returns a new Formula object, built from this formula, where all instances of the variables specified in the substitutions are replaced by the corresponding formulas.

pub fn replace(&self, old_sub_fmla: &Formula, new_sub_fmla: &Formula) -> Formula

Replace all instances of old_sub_fmla in this formula by new_sub_fmla. Where substitute works on variables only, this

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl Default for Formula

fn default() -> Formula

Returns the “default value” for a type.

impl PartialEq for Formula

fn eq(&self, other: &Self) -> 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.