Struct satoxid::constraints::ExactlyK

pub struct ExactlyK<I> {
    pub lits: I,
    pub k: u32,
}

This constraint encodes the requirement that exactly k of lits are true.

Fields

lits: I

k: u32

Trait Implementations

impl<I: Clone> Clone for ExactlyK<I>

fn clone(&self) -> ExactlyK<I>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<V, I> Constraint<V> for ExactlyK<I> where
    V: SatVar,
    I: Iterator + Clone,
    I::Item: Into<VarType<V>> + Debug, 

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

Encode Self as an constraint using solver.

impl<V, I> ConstraintRepr<V> for ExactlyK<I> where
    V: SatVar,
    I: Iterator + Clone,
    I::Item: Into<VarType<V>> + Debug, 

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.

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<S: Backend>(
    self,
    repr: Option<i32>,
    solver: &mut S,
    varmap: &mut VarMap<V>
) -> i32

Encode that repr is true if the constraint is satisfied. The semantics are less restrictive for to allow for cheaper encoding. No guarantees are given about the constraints of repr if the constraint is false. Usually it has either the semantics of implies_repr or equals_repr.

impl<I> Debug for ExactlyK<I> where
    I: Iterator + Clone,
    I::Item: Debug, 

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

Formats the value using the given formatter.