Enum PropositionalFormula

pub enum PropositionalFormula {
    Variable(Variable),
    Negation(Option<Box<PropositionalFormula>>),
    Conjunction(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>),
    Disjunction(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>),
    Implication(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>),
    Biimplication(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>),
}

A propositional formula is defined inductively, conforming to the following BNF:

<formula>
    ::= <propositional-variable>
    | ( - <formula> )
    | ( <formula> ^ <formula>)
    | ( <formula> | <formula> )
    | ( <formula> -> <formula> )
    | ( <formula> <-> <formula> )

Notice the requirement for explicit parentheses around the unary and binary operators, which eliminates the requirement for operator precedence due to grammar ambiguity at the cost of being more verbose.

Ownership, Interior Mutability and Optional Sub-formulas

Since we don’t need any fancy multiple-threading or multi-owner business, we’ll stick with the most trivial Box pointer indirection instead of the fancier alternatives:

• Reference-counted smart pointer Rc
• Atomically-reference-counted smart pointer Arc
• Lifetime-bounded references &'a

We do not support interior mutability as we do not need it for our use cases with respect to the propositional formula AST.

We need sub-formulas to be wrapped in Option for construction purposes, so we can build a PropPropositionalFormula during parsing.

No Default

We cannot soundly define a sane default for a PropositionalFormula – even in the base case of a single propositional variable, what would the default propositional variable be?

Variants

Variable(Variable)

Base case: a single propositional variable.

Negation(Option<Box<PropositionalFormula>>)

Unary case: negated formula.

Conjunction(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>)

Binary formula with the main connective being the logical AND connective.

Disjunction(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>)

Binary formula with the main connective being the logical OR operator.

Implication(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>)

Binary formula with the main connective being the implication operator.

Biimplication(Option<Box<PropositionalFormula>>, Option<Box<PropositionalFormula>>)

Binary formula with the main connective being the biimplication operator.

Implementations

impl PropositionalFormula

pub fn variable(v: Variable) -> Self

Construct a new propositional formula from a propositional Variable.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let formula = PropositionalFormula::variable(Variable::new("a"));
println!("{:#?}", formula);

pub fn negated(formula: Box<PropositionalFormula>) -> Self

Construct a new propositional formula from a sub propositional formula with negation.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let sub_formula = PropositionalFormula::variable(Variable::new("a"));
let formula = PropositionalFormula::negated(Box::new(sub_formula.clone()));
println!("{:#?}", formula);

pub fn conjunction( left_sub_formula: Box<PropositionalFormula>, right_sub_formula: Box<PropositionalFormula>, ) -> Self

Construct a new propositional formula from two propositional sub-formulas with a conjunction main connective.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let sub_formula = PropositionalFormula::variable(Variable::new("a"));
let formula = PropositionalFormula::conjunction(Box::new(sub_formula.clone()), Box::new(sub_formula.clone()));
println!("{:#?}", formula);

pub fn disjunction( left_sub_formula: Box<PropositionalFormula>, right_sub_formula: Box<PropositionalFormula>, ) -> Self

Construct a new propositional formula from two propositional sub-formulas with a disjunction main connective.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let sub_formula = PropositionalFormula::variable(Variable::new("a"));
let formula = PropositionalFormula::disjunction(Box::new(sub_formula.clone()), Box::new(sub_formula.clone()));
println!("{:#?}", formula);

pub fn implication( left_sub_formula: Box<PropositionalFormula>, right_sub_formula: Box<PropositionalFormula>, ) -> Self

Construct a new propositional formula from two propositional sub-formulas with an implication main connective.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let sub_formula = PropositionalFormula::variable(Variable::new("a"));
let formula = PropositionalFormula::implication(Box::new(sub_formula.clone()), Box::new(sub_formula.clone()));
println!("{:#?}", formula);

pub fn biimplication( left_sub_formula: Box<PropositionalFormula>, right_sub_formula: Box<PropositionalFormula>, ) -> Self

Construct a new propositional formula from two propositional sub-formulas with a biimplication main connective.

Example

use libprop_sat_solver::formula::{PropositionalFormula, Variable};
let sub_formula = PropositionalFormula::variable(Variable::new("a"));
let formula = PropositionalFormula::biimplication(Box::new(sub_formula.clone()), Box::new(sub_formula.clone()));
println!("{:#?}", formula);

pub fn is_literal(&self) -> bool

Checks if the given PropositionalFormula is a literal (either a propositional variable like p or its negation -p).

Trait Implementations

impl Clone for PropositionalFormula

fn clone(&self) -> PropositionalFormula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PropositionalFormula

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

Formats the value using the given formatter.

impl<V> From<V> for PropositionalFormula

where V: Into<Variable>,

fn from(v: V) -> Self

Converts to this type from the input type.

impl Hash for PropositionalFormula

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for PropositionalFormula

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for PropositionalFormula

fn partial_cmp(&self, other: &PropositionalFormula) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Eq for PropositionalFormula

impl StructuralPartialEq for PropositionalFormula