Struct satoxid::constraints::SameCardinality

pub struct SameCardinality<V> { /* fields omitted */ }

Constraint to ensure that several sets of literals have all the same number of true literals.

Implementations

impl<V> SameCardinality<V>

pub fn new() -> Self

pub fn add_lits<I>(&mut self, lits: I) -> &mut Self where
    I: Iterator,
    I::Item: Into<VarType<V>>, 

Trait Implementations

impl<V: Clone> Clone for SameCardinality<V>

fn clone(&self) -> SameCardinality<V>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<V: SatVar> Constraint<V> for SameCardinality<V>

fn encode<S: Backend>(self, solver: &mut S, varmap: &mut VarMap<V>)

Encode Self as an constraint using solver.

impl<V: SatVar> ConstraintRepr<V> for SameCardinality<V>

fn encode_constraint_implies_repr<S: Backend>(
    self,
    repr: Option<i32>,
    solver: &mut S,
    varmap: &mut VarMap<V>
) -> i32

Encode if Self is satisified, that repr is true. Otherwise repr is not constrained and can be true or false.

fn encode_constraint_equals_repr<S: Backend>(
    self,
    repr: Option<i32>,
    solver: &mut S,
    varmap: &mut VarMap<V>
) -> i32

Encode if and only if Self is satisified, that repr is true.

fn encode_constraint_repr_cheap<B: Backend>(
    self,
    repr: Option<i32>,
    backend: &mut B,
    varmap: &mut VarMap<V>
) -> i32

Encode that repr is true if the constraint is satisfied. The implementation can decide if it has the semantics of encode_constraint_implies_repr or encode_constraint_equals_repr, depending on what is cheaper to encode.

impl<V: Debug> Debug for SameCardinality<V>

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

Formats the value using the given formatter.