Struct Clause 

pub struct Clause(pub Vec<i32>);

A clause; it’s a list of disjoined literals

Tuple Fields

0: Vec<i32>

Implementations

impl Clause

pub fn empty() -> Self

An empty clause

pub fn new(lits: Vec<i32>) -> Self

A new clause with specified literals

pub fn single(lit: i32) -> Self

A singleton clause

pub fn lits(&self) -> &[i32]

Obtain a slice of the literals

pub fn evaluate(&self, model: &Model) -> bool

Given a model, check whether the current clause is true.

pub fn find_true_vars(&self, model: &Model) -> Vec<i32>

Return a list of true literals

pub fn filter_true_vars(&self, model: &Model, set: &HashSet<i32>) -> Vec<i32>

Return a list of true literals that are not in the given set

pub fn filter_vars(&self, model: &Model) -> Clause

Return a list of true literals as a clause

c.f. Self::find_true_vars

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

Return an iterator for the literals

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

Concatenate two clauses

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

Concatenate a given clause by modifying the self clause

pub fn add(&mut self, lit: i32) -> &mut Self

Add a new literal to the clause

Trait Implementations

impl Clone for Clause

fn clone(&self) -> Clause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Clause

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

Formats the value using the given formatter.

impl Display for Clause

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

Formats the value using the given formatter.

impl Hash for Clause

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 Clause

type Item = i32

The type of the elements being iterated over.

type IntoIter = IntoIter<i32>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Clause

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

impl StructuralPartialEq for Clause