Struct biodivine_lib_bdd::BddPartialValuation

pub struct BddPartialValuation(/* private fields */);

Describes assignment of some arbitrary number of Bdd variables.

A partial valuation can be used to quickly construct simple conjunctive/disjunctive clauses. It also exactly describes one path in a Bdd and hence can be used as an intermediate value when traversing the valuations of a Bdd.

Implementations

impl BddPartialValuation

pub fn empty() -> BddPartialValuation

Creates an empty valuation without any variables set.

Examples found in repository

examples/bench_restrict.rs (line 16)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    let mut file = std::fs::File::open(args[1].as_str()).unwrap();
    let bdd = Bdd::read_as_bytes(&mut file).unwrap();
    println!("Loaded: {} as Bdd({})", args[1].as_str(), bdd.size());

    let mut support = Vec::from_iter(bdd.support_set());

    for k in 1..5 {
        // Fix variables randomly.
        let mut reduction = BddPartialValuation::empty();
        let mut rng = StdRng::seed_from_u64(0);
        support.sort(); // Don't leak previous shuffled state.
        support.shuffle(&mut rng);

        for var in &support[0..k] {
            reduction[*var] = Some(rng.gen_bool(0.5));
        }

        // Run restriction.
        for _ in 0..5 {
            let start = Instant::now();
            let result = bdd.restrict(&reduction.to_values());
            println!(
                "Result: Bdd({}) in {}ms",
                result.size(),
                (Instant::now() - start).as_millis()
            );
        }
    }
}

pub fn is_empty(&self) -> bool

True if the valuation contains no values.

pub fn cardinality(&self) -> u16

Return the number of fixed variables in this valuation.

pub fn last_fixed_variable(&self) -> Option<BddVariable>

Return the identifier of the last fixed variable in this valuation. Returns None if no variable is fixed.

pub fn from_values(values: &[(BddVariable, bool)]) -> BddPartialValuation

Create a partial valuation from a list of variables and values.

The order of variables in the slice can be arbitrary. The operation does not perform any uniqueness checking. If the slice contains multiple copies of the same variable, the last value is accepted.

pub fn to_values(&self) -> Vec<(BddVariable, bool)>

Consume this valuation and turn it into a vector of values which are stored in it.

Examples found in repository

examples/bench_restrict.rs (line 28)

fn main() {
    let args = std::env::args().collect::<Vec<_>>();
    let mut file = std::fs::File::open(args[1].as_str()).unwrap();
    let bdd = Bdd::read_as_bytes(&mut file).unwrap();
    println!("Loaded: {} as Bdd({})", args[1].as_str(), bdd.size());

    let mut support = Vec::from_iter(bdd.support_set());

    for k in 1..5 {
        // Fix variables randomly.
        let mut reduction = BddPartialValuation::empty();
        let mut rng = StdRng::seed_from_u64(0);
        support.sort(); // Don't leak previous shuffled state.
        support.shuffle(&mut rng);

        for var in &support[0..k] {
            reduction[*var] = Some(rng.gen_bool(0.5));
        }

        // Run restriction.
        for _ in 0..5 {
            let start = Instant::now();
            let result = bdd.restrict(&reduction.to_values());
            println!(
                "Result: Bdd({}) in {}ms",
                result.size(),
                (Instant::now() - start).as_millis()
            );
        }
    }
}

pub fn get_value(&self, id: BddVariable) -> Option<bool>

Get a value stored for the given variable id, if any.

pub fn has_value(&self, id: BddVariable) -> bool

Returns true if this valuation has the value of id variable set.

pub fn set_value(&mut self, id: BddVariable, value: bool)

Update value of the given id variable.

pub fn unset_value(&mut self, id: BddVariable)

Remove value of a variable from this valuation.

If the value was not set, this operation has no effect.

pub fn extends(&self, valuation: &BddPartialValuation) -> bool

Returns true if the values set in this partial valuation match the values fixed in the other given valuation. I.e. the two valuations agree on fixed values in valuation.

In other words this >= valuation in terms of specificity.

Trait Implementations

impl Clone for BddPartialValuation

fn clone(&self) -> BddPartialValuation

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for BddPartialValuation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for BddPartialValuation

fn default() -> Self

Returns the “default value” for a type.

impl From<BddValuation> for BddPartialValuation

fn from(value: BddValuation) -> Self

Converts to this type from the input type.

impl Hash for BddPartialValuation

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Index<BddVariable> for BddPartialValuation

type Output = Option<bool>

The returned type after indexing.

fn index(&self, index: BddVariable) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<BddVariable> for BddPartialValuation

fn index_mut(&mut self, index: BddVariable) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl PartialEq for BddPartialValuation

fn eq(&self, other: &Self) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl TryFrom<BddPartialValuation> for BddValuation

If possible, convert the given partial valuation to valuation with the same number of variables. Partial valuation must contain values of all variables.

type Error = ()

The type returned in the event of a conversion error.

fn try_from(value: BddPartialValuation) -> Result<Self, Self::Error>

Performs the conversion.

impl Eq for BddPartialValuation