pub struct Theory { /* private fields */ }
Expand description
A Theory
is a set of alternative PropositionalFormula
s.
It corresponds to one particular branch of the tableau tree.
Implementations§
Source§impl Theory
impl Theory
Sourcepub fn from_propositional_formula(formula: PropositionalFormula) -> Self
pub fn from_propositional_formula(formula: PropositionalFormula) -> Self
Construct a Theory
from a given propositional formula.
Sourcepub fn formulas(&self) -> impl Iterator<Item = &PropositionalFormula>
pub fn formulas(&self) -> impl Iterator<Item = &PropositionalFormula>
Get the formulas.
Sourcepub fn add(&mut self, formula: PropositionalFormula)
pub fn add(&mut self, formula: PropositionalFormula)
Add a propositional formula to the theory iff the theory does not already contain the formula.
Sourcepub fn is_fully_expanded(&self) -> bool
pub fn is_fully_expanded(&self) -> bool
Checks if the Theory
is fully expanded, i.e. each propositional_formula in the given
Theory
is a literal (e.g. p
, -(p)
, a propositional variable or its negation).
Sourcepub fn has_contradictions(&self) -> bool
pub fn has_contradictions(&self) -> bool
Checks if a Theory
contains contradictions. That is, if the Theory
contains a literal
p
AND its negation -p
.
§Space and Time Complexity
This function uses a HashMap
(specifically, a map from some &str
to the tuple
(has_literal, has_negation): (bool, bool)
. As soon as we encounter the case where
has_literal && has_negation
then we have found a contradiction.
- Worst-case time complexity:
O(n)
because we iterate through all of the formulas for the given theory. - Worst-case space complexity:
O(k)
fork
propositional variables appearing in literals.
Sourcepub fn get_non_literal_formula(&mut self) -> Option<PropositionalFormula>
pub fn get_non_literal_formula(&mut self) -> Option<PropositionalFormula>
Get a non-literal formula (not a propositional variable or its negation) from the current
Theory
.
Sourcepub fn swap_formula(
&mut self,
existing: &PropositionalFormula,
replacement: PropositionalFormula,
)
pub fn swap_formula( &mut self, existing: &PropositionalFormula, replacement: PropositionalFormula, )
Replace existing formula with a new formula.
Sourcepub fn swap_formula2(
&mut self,
existing: &PropositionalFormula,
replacements: (PropositionalFormula, PropositionalFormula),
)
pub fn swap_formula2( &mut self, existing: &PropositionalFormula, replacements: (PropositionalFormula, PropositionalFormula), )
Replace existing formula with two new formulas.