pub struct Tableau { /* private fields */ }
Expand description
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):
{ (a^b), a }
{ (a^b), b }
Implementations§
Source§impl Tableau
impl Tableau
Sourcepub fn from_starting_propositional_formula(
formula: PropositionalFormula,
) -> Self
pub fn from_starting_propositional_formula( formula: PropositionalFormula, ) -> Self
Construct a Tableau
with the starting root node being the given propositional formula.
Sourcepub fn pop_theory(&mut self) -> Option<Theory>
pub fn pop_theory(&mut self) -> Option<Theory>
Retrieve a Theory
from the Tableau
.
Sourcepub fn push_theory(&mut self, theory: Theory)
pub fn push_theory(&mut self, theory: Theory)
Add a Theory
to the Tableau
.
Trait Implementations§
impl StructuralPartialEq for Tableau
Auto Trait Implementations§
impl Freeze for Tableau
impl RefUnwindSafe for Tableau
impl Send for Tableau
impl Sync for Tableau
impl Unpin for Tableau
impl UnwindSafe for Tableau
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more