Struct satoxid::Encoder

pub struct Encoder<V, S> {
    pub backend: S,
    pub varmap: VarMap<V>,
    pub debug: bool,
}

The Encoder type contains all data used for the encoding.

Fields

backend: S

varmap: VarMap<V>

debug: bool

Implementations

impl<V: SatVar, S: Default> Encoder<V, S>

pub fn new() -> Self

Creates a new encoder.

pub fn with_debug() -> Self

Creates a new encoder and will print out every encoded constraint.

impl<V, B> Encoder<V, B> where
    V: SatVar,
    B: Backend, 

pub fn with_backend(backend: B) -> Self

Create a new Encoder using backend as the Backend.

pub fn add_constraint<C: Constraint<V>>(&mut self, constraint: C)

Encode a constraint.

pub fn add_constraint_implies_repr<C: ConstraintRepr<V>>(
    &mut self,
    constraint: C
) -> VarType<V>

Encode a constraint such that a variable represents it. If the constraint in the solved model is true, the return variable (repr) will also be true. Otherwise there it doesn’t constrain repr which can either be true or false.

pub fn add_constraint_equals_repr<C: ConstraintRepr<V>>(
    &mut self,
    constraint: C
) -> VarType<V>

Encode a constraint such that a variable represents it. Like add_constraint_implies_repr but the value of repr will equal the constraint satisfied. So if constraint wasn’t satisfied, repr will be false.

impl<V: SatVar, S: Solver> Encoder<V, S>

pub fn solve(&mut self) -> Option<Model<V>>

Solve the encoded problem. If problem is unsat then None is returned. Otherwise a model of the problem is returned.