Struct DirectAccessEngine 

pub struct DirectAccessEngine<'a> { /* private fields */ }

An object that, given an (internally computed) complete order on the models of a DecisionDNNF, allows to return the k-th model.

The order of the models is given by the structure of the formula. This implies that given the same formula the order will remain the same at each call, but it will change when considering an equivalent formula which has a different structure.

Implementations

impl<'a> DirectAccessEngine<'a>

pub fn new(model_counter: &'a ModelCounter<'a>) -> Self

Builds a new DirectAccessEngine given a ModelCounter.

The formula under consideration is the one of the model counter.

impl DirectAccessEngine<'_>

pub fn n_models(&self) -> &Integer

Returns the number of models of the formula.

pub fn model(&self, n: Integer) -> Option<Vec<Option<Literal>>>

Returns the model at the given index.

pub fn model_with_graph( &self, n: Integer, ) -> Option<(Vec<Option<Literal>>, Vec<usize>)>

Returns the model at the given index, along its model graph.

If the index is higher than the number of models, None is returned.

pub fn ddnnf(&self) -> &DecisionDNNF

Returns the underlying ddnnf.