Struct ModelFinder 

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

A structure used to find models in a DecisionDNNF.

Queries can involved assumption literals; in this case, the only models under consideration are the ones that involve such literals. In case models exists but none include those assumptions, then the query will return that no model exist.

Example

use decdnnf_rs::{Literal, ModelFinder};

let ddnnf = gimme_ddnnf();
let model_finder = ModelFinder::new(&ddnnf);
if let Some(model) = model_finder.find_model() {
    println!("the formula has models; here is one:");
    for l in model {
        print!("{l} ");
    }
    println!();
    if model_finder.find_model_under_assumptions(&[Literal::from(-1)]).is_some() {
        println!("some of them involve the literal -1");
    }
    if model_finder.find_model_under_assumptions(&[Literal::from(1)]).is_some() {
        println!("some of them involve the literal 1");
    }
} else {
    println!("the formula has no model");
}

Implementations

impl<'a> ModelFinder<'a>

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

Builds a new model finder given a DecisionDNNF.

pub fn find_model(&self) -> Option<Vec<Literal>>

Search for a model.

pub fn find_model_under_assumptions( &self, assumptions: &[Literal], ) -> Option<Vec<Literal>>

Search for a model compatible with the provided assumptions.

Panics

The literals must refer to existing variables. In case the variable index of a literal is higher than the highest variable index in the formula, this function panics.