1
use merc_utilities::MercError;
2
use oxidd::BooleanFunction;
3
use oxidd::ManagerRef;
4
use oxidd::bdd::BDDFunction;
5
use oxidd::bdd::BDDManagerRef;
6
use oxidd::util::OptBool;
7
use rand::Rng;
8

            
9
/// Generate `num_vectors` random bitvectors of length `num_vars`.
10
6790
pub fn random_bitvectors(rng: &mut impl Rng, num_vars: usize, num_vectors: usize) -> Vec<Vec<OptBool>> {
11
6790
    let mut vectors = Vec::new();
12
6790
    for _ in 0..rng.random_range(0..num_vectors) {
13
326448
        let mut vec = Vec::new();
14
326448
        for _ in 0..num_vars {
15
983276
            vec.push(if rng.random_bool(0.5) {
16
491654
                OptBool::True
17
            } else {
18
491622
                OptBool::False
19
            });
20
        }
21
326448
        vectors.push(vec);
22
    }
23
6790
    vectors
24
6790
}
25

            
26
/// Create a BDD from the given bitvector.
27
6790
pub fn bdd_from_iter<'a>(
28
6790
    manager_ref: &BDDManagerRef,
29
6790
    variables: &[BDDFunction],
30
6790
    vectors: impl Iterator<Item = &'a Vec<OptBool>>,
31
6790
) -> Result<BDDFunction, MercError> {
32
6790
    let mut bdd = manager_ref.with_manager_shared(|manager| BDDFunction::f(manager));
33
326448
    for bits in vectors {
34
326448
        let mut cube = manager_ref.with_manager_shared(|manager| BDDFunction::t(manager));
35
        // Create a cube for this bitvector
36
983276
        for (i, bit) in bits.iter().enumerate() {
37
983276
            let var = variables[i].clone();
38
983276
            let literal = match *bit {
39
491654
                OptBool::True => var,
40
491622
                OptBool::False => var.not()?,
41
                OptBool::None => continue,
42
            };
43
983276
            cube = cube.and(&literal)?;
44
        }
45

            
46
326448
        bdd = bdd.or(&cube)?;
47
    }
48

            
49
6790
    Ok(bdd)
50
6790
}
51

            
52
/// Create a random BDD over the given variables with the given number of cubes.
53
6590
pub fn random_bdd(
54
6590
    manager_ref: &BDDManagerRef,
55
6590
    rng: &mut impl Rng,
56
6590
    variables: &[BDDFunction],
57
6590
) -> Result<BDDFunction, MercError> {
58
6590
    let bitvectors = random_bitvectors(rng, variables.len(), 100);
59
6590
    bdd_from_iter(manager_ref, variables, bitvectors.iter())
60
6590
}