Struct OrFreeVariables 

pub struct OrFreeVariables { /* private fields */ }

A structure used to handle efficiently the free variables located at disjunction nodes.

This structures allows to store polarity associated with these variables, since they are stored as literals.

Implementations

impl OrFreeVariables

pub fn set_negative_literals(&mut self)

Sets the polarity associated with the literals as negative for all the free variables.

pub fn iter_child_free_vars_lengths( &self, var: usize, ) -> impl Iterator<Item = usize> + '_

Given a disjunction node index, iterates over the number of free variables each child has.

pub fn child_free_vars(&self, var: usize, child_index: usize) -> &[Literal]

Returns a slice of the free variables of a given disjunction node child.

pub fn iter_child_free_vars( &self, var: usize, ) -> impl Iterator<Item = &[Literal]> + '_

Iterates over the free variables of the children of a given disjunction.

pub fn child_free_vars_mut( &mut self, var: usize, child_index: usize, ) -> &mut [Literal]

Iterates mutably over the free variables of a given disjunction node child.

Trait Implementations

impl Clone for OrFreeVariables

fn clone(&self) -> OrFreeVariables

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for OrFreeVariables

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

Formats the value using the given formatter.