Trait satoxid::ConstraintRepr

pub trait ConstraintRepr<V: SatVar>: Constraint<V> {
    fn encode_constraint_implies_repr<S: Backend>(
        self, 
        repr: Option<i32>, 
        solver: &mut S, 
        varmap: &mut VarMap<V>
    ) -> i32;

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

Trait used to express a constraint which can imply another variable, a so called representative (repr).

If no repr is supplied (None) then the methods have to choose their own repr. It can either be a fresh generated variable using varmap, but sometimes the structure of the constraint provides a suitable candidate. The used repr is returned by the methods. If a repr was provided when calling the methods the same repr has to be returned. If the constraint isn’t satisified the whole generated encoding has to be satisfiable regardless what value repr is.

Required methods

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.

Provided methods

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.

Implementors

impl<I, V> ConstraintRepr<V> for Or<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

impl<V, C> ConstraintRepr<V> for Not<C> where
    V: SatVar,
    C: ConstraintRepr<V>, 

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

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

impl<V, C, T> ConstraintRepr<V> for If<C, T> where
    V: SatVar,
    C: ConstraintRepr<V>,
    T: ConstraintRepr<V>, 

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

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

impl<V, I> ConstraintRepr<V> for And<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

impl<V, I> ConstraintRepr<V> for AtLeastK<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

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

impl<V, I> ConstraintRepr<V> for AtMostK<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

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

impl<V, I> ConstraintRepr<V> for Equal<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

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

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

impl<V, L> ConstraintRepr<V> for L where
    V: SatVar,
    L: Debug + Clone + Into<VarType<V>>, 

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

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

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

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

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

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

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

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

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