Struct pblib_rs::EncodingResult

pub struct EncodingResult { /* private fields */ }

The result of an encoding function.

This structure contains both the clauses generated to encode the constraint and the index of the next free variable id.

Implementations

impl EncodingResult

pub fn clauses(&self) -> &[Vec<i32>]

Returns a reference to the clauses used to encode the constraint.

pub fn next_free_var_id(&self) -> i32

Returns the next free variable id.

Encodings use auxiliary variables almost all the time. Functions that encode constraints ask the first variable id they can use for these auxiliary variables. In return, they tell the caller which is the lowest id that can be used after this encoding, that is, the highest auxiliary variable index plus 1.