Struct libprop_sat_solver::tableaux_solver::tableau::Tableau

pub struct Tableau { /* fields omitted */ }

A Tableau is a collection of Theory-ies. This corresponds to the entire propositional tableau tree, where each Theory is a branch (from the root node to each leaf).

For example, given the tableau (tree)

    (a^b)
    /   \
   a     b

There are two branches (hence two Theory-ies):

1. { (a^b), a }
2. { (a^b), b }

Methods

impl Tableau

pub fn new() -> Self

Construct a new Tableau with no theories.

pub fn from_starting_propositional_formula(
    formula: PropositionalFormula
) -> Self

Construct a Tableau with the starting root node being the given propositional formula.

pub fn is_empty(&self) -> bool

Check if the Tableau contains no Theory-ies.

pub fn pop_theory(&mut self) -> Option<Theory>

Retrieve a Theory from the Tableau.

pub fn push_theory(&mut self, theory: Theory)

Add a Theory to the Tableau.

pub fn contains(&self, theory: &Theory) -> bool

Check if the Tableau already contains the Theory.

Trait Implementations

impl Clone for Tableau

fn clone(&self) -> Tableau

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Tableau

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

Formats the value using the given formatter.

impl PartialEq<Tableau> for Tableau

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl StructuralPartialEq for Tableau