Struct libprop_sat_solver::tableaux_solver::theory::Theory

pub struct Theory { /* fields omitted */ }

A Theory is a set of alternative PropositionalFormulas.

It corresponds to one particular branch of the tableau tree.

Methods

impl Theory

pub fn new() -> Self

Construct an empty theory.

pub fn from_propositional_formula(formula: PropositionalFormula) -> Self

Construct a Theory from a given propositional formula.

pub fn formulas(&self) -> impl Iterator<Item = &PropositionalFormula>

Get the formulas.

pub fn add(&mut self, formula: PropositionalFormula)

Add a propositional formula to the theory iff the theory does not already contain the formula.

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).

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) for k propositional variables appearing in literals.

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.

pub fn swap_formula(
    &mut self,
    existing: &PropositionalFormula,
    replacement: PropositionalFormula
)

Replace existing formula with a new formula.

pub fn swap_formula2(
    &mut self,
    existing: &PropositionalFormula,
    replacements: (PropositionalFormula, PropositionalFormula)
)

Replace existing formula with two new formulas.

Trait Implementations

impl Clone for Theory

fn clone(&self) -> Theory

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Theory

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

Formats the value using the given formatter.

impl PartialEq<Theory> for Theory

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

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

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

This method tests for !=.

impl StructuralPartialEq for Theory