Struct Formula 

pub struct Formula(pub Vec<Clause>);

A formula; it’s a list of conjoined clauses

Tuple Fields

0: Vec<Clause>

Implementations

impl Formula

pub fn empty() -> Formula

An empty formula

pub fn new(clauses: Vec<Clause>) -> Formula

A new formula with the given vector of clauses

pub fn add(&mut self, clause: Clause)

Add a clause to the current formula

pub fn filter_clauses(&self, model: &Model) -> Formula

Return a formula only containing true literals in each clause

pub fn find_implicant(&self, model: &Model) -> HashSet<i32>

Obtain an implicant of the formula based on the model

pub fn iter(&self) -> impl Iterator<Item = &Clause>

pub fn concat(&self, clause: &Clause) -> Self

pub fn concat_mut(&mut self, clause: &Clause) -> &mut Self

pub fn distribute(&self, formula: &Formula) -> Self

pub fn distribute_mut(&mut self, formula: &Formula) -> &mut Self

Trait Implementations

impl Clone for Formula

fn clone(&self) -> Formula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl Display for Formula

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

Formats the value using the given formatter.

impl Hash for Formula

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 IntoIterator for Formula

type Item = Clause

The type of the elements being iterated over.

type IntoIter = IntoIter<Clause>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Formula

fn eq(&self, other: &Formula) -> 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 Eq for Formula

impl StructuralPartialEq for Formula