Struct ModelCounter 

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

A structure used to count the models of a DecisionDNNF.

The algorithm takes a time polynomial in the size of the Decision-DNNF.

Example

use decdnnf_rs::{DecisionDNNF, ModelCounter};

fn count_models(ddnnf: &DecisionDNNF) {
    let model_counter = ModelCounter::new(ddnnf, false);
    println!("the formula has {} models", model_counter.global_count());
}

Implementations

impl<'a> ModelCounter<'a>

pub fn new(ddnnf: &'a DecisionDNNF, partial_models: bool) -> Self

Builds a new model counter given a formula.

This function can both count the number of full or partial models.

pub fn set_assumptions(&mut self, assumptions: &[Literal])

Set assumption literals, reducing the number of models.

The only models to be considered are the ones that contain all the literals marked as assumptions. The set of assumptions must involved at most once each variable.

Panics

This function panics if the set of assumptions involves the same variable multiple times.

pub fn global_count(&self) -> &Integer

Returns the number of counted elements of the whole formula.

pub fn ddnnf(&self) -> &DecisionDNNF

Returns the DecisionDNNF which elements are counted.

pub fn count_from(&self, index: NodeIndex) -> &Integer

Returns the number of counted elements of the subfomula rooted at the node which index is given.

Panics

This function panics if the provided node index is greater or equal to the number of nodes of the formula.

pub fn partial_models(&self) -> bool

Returns a Boolean value indicating if partial models are computed (false is returns in case full models are computed).