Grcov report - ldd_to

1

use oxidd::BooleanFunction;

2

use oxidd::ManagerRef;

3

use oxidd::bdd::BDDFunction;

4

use oxidd::bdd::BDDManagerRef;

5

6

use merc_ldd::DataRef;

7

use merc_ldd::LddRef;

8

use merc_ldd::Storage;

9

use merc_ldd::height;

10

use merc_utilities::MercError;

11

12

pub fn ldd_to_bdd_simple(

13

    storage: &mut Storage,

14

    manager_ref: &BDDManagerRef,

15

    ldd: &LddRef<'_>,

16

) -> Result<BDDFunction, MercError> {

17

    let highest = compute_highest(storage, ldd);

18

    let bits = compute_bits(&highest);

19

    let bits_dd = merc_ldd::singleton(storage, &bits);

20

21

    ldd_to_bdd(storage, manager_ref, ldd, &bits_dd, 0)

22

23

24

/// Converts an LDD representing a set of vectors into a BDD representing the

25

/// same set by bitblasting the vector elements.

26

///

27

/// # Details

28

///

29

/// The bits should be a singleton LDD containing the result of

30

/// [`compute_bits`]. The conversion works recursively by processing the LDD

31

/// node by node, and introducing bits number of BDD variables for each layer in

32

/// the LDD. Note that `first_variable` indicates the level of the first

33

/// variable, and the next bits are placed at consecutive BDD layers. These

34

/// variables *must* already exist in the given BDD manager.

35

2208

pub fn ldd_to_bdd(

36

2208

    storage: &mut Storage,

37

2208

    manager_ref: &BDDManagerRef,

38

2208

    ldd: &LddRef<'_>,

39

2208

    bits: &LddRef<'_>,

40

2208

    first_variable: u32,

41

2208

) -> Result<BDDFunction, MercError> {

42

    // Base cases

43

2208

    if **storage.empty_set() == *ldd {

44

756

        return Ok(manager_ref.with_manager_shared(|manager| BDDFunction::f(manager)));

45

1452

46

1452

    if **storage.empty_vector() == *ldd {

47

398

        return Ok(manager_ref.with_manager_shared(|manager| BDDFunction::t(manager)));

48

1054

49

50

    // TODO: Implement caching

51

1054

    let DataRef(value, down, right) = storage.get_ref(ldd);

52

1054

    let DataRef(bits_value, bits_down, _bits_right) = storage.get_ref(bits); // Is singleton so right is ignored.

53

54

1054

    let right = ldd_to_bdd(storage, manager_ref, &right, bits, first_variable)?;

55

1054

    let mut down = ldd_to_bdd(storage, manager_ref, &down, &bits_down, first_variable + bits_value)?;

56

57

    // Encode current value

58

2687

    for i in 0..bits_value {

59

        // encode with high bit first

60

2687

        let bit = bits_value - i - 1;

61

2687

        if value & (1 << i) != 0 {

62

            // bit is 1

63

1091

            down = manager_ref.with_manager_shared(|manager| {

64

1091

                BDDFunction::var(manager, first_variable + bit)?.ite(&BDDFunction::f(manager), &down)

65

1091

            })?;

66

        } else {

67

            // bit is 0

68

1596

            down = manager_ref.with_manager_shared(|manager| {

69

1596

                BDDFunction::var(manager, first_variable + bit)?.ite(&down, &BDDFunction::f(manager))

70

1596

            })?;

71

72

73

74

1054

    Ok(down.or(&right)?)

75

2208

76

77

/// Computes the highest value for every layer in the LDD

78

200

fn compute_highest(storage: &mut Storage, ldd: &LddRef<'_>) -> Vec<u32> {

79

200

    let mut result = vec![0; height(storage, ldd)];

80

200

    compute_highest_rec(storage, &mut result, ldd, 0);

81

200

    result

82

200

83

84

/// Helper function for compute_highest

85

4468

fn compute_highest_rec(storage: &mut Storage, result: &mut [u32], set: &LddRef<'_>, depth: usize) {

86

4468

    if set == storage.empty_set() || set == storage.empty_vector() {

87

2334

        return;

88

2134

89

90

2134

    let DataRef(value, down, right) = storage.get_ref(set);

91

2134

    compute_highest_rec(storage, result, &right, depth);

92

2134

    compute_highest_rec(storage, result, &down, depth + 1);

93

94

2134

    result[depth] = result[depth].max(value);

95

4468

96

97

/// Computes the number of bits required to represent the highest value at each layer.

98

200

fn compute_bits(highest: &[u32]) -> Vec<u32> {

99

600

    highest.iter().map(|&h| u32::BITS - h.leading_zeros()).collect()

100

200

101

102

#[cfg(test)]

103

mod tests {

104

    use merc_ldd::fmt_node;

105

    use merc_ldd::from_iter;

106

    use merc_ldd::random_vector_set;

107

    use merc_ldd::singleton;

108

    use merc_utilities::random_test;

109

110

    use crate::create_variables;

111

112

    use super::*;

113

114

    #[test]

115

1

    fn test_random_compute_highest() {

116

100

        random_test(100, |rng| {

117

100

            let set = random_vector_set(rng, 4, 3, 5);

118

100

            let mut storage = Storage::new();

119

100

            let ldd = from_iter(&mut storage, set.iter());

120

100

            println!("LDD: {}", fmt_node(&storage, &ldd));

121

122

100

            let highest = compute_highest(&mut storage, &ldd);

123

100

            println!("Highest: {:?}", highest);

124

300

            for (i, h) in highest.iter().enumerate() {

125

                // Determine the highest value for every vector

126

1191

                for value in set.iter() {

127

1191

                    assert!(

128

1191

                        *h >= value[i],

129

                        "The highest value for depth {} is {}, but vector has value {}",

130

i,

131

h,

132

                        value[i]

133

);

134

135

136

137

100

            let bits = compute_bits(&highest);

138

100

            println!("Bits: {:?}", bits);

139

140

300

            for (i, b) in bits.iter().enumerate() {

141

300

                let expected_bits = if highest[i] == 0 {

142

1

143

                } else {

144

299

                    u32::BITS - highest[i].leading_zeros()

145

};

146

300

                assert_eq!(

147

                    *b, expected_bits,

148

                    "The number of bits for depth {} is {}, but expected {}",

149

                    i, b, expected_bits

150

);

151

152

100

})

153

1

154

155

    #[test]

156

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

157

1

    fn test_random_ldd_to_bdd() {

158

100

        random_test(100, |rng| {

159

100

            let set = random_vector_set(rng, 4, 3, 5);

160

161

100

            let mut storage = Storage::new();

162

100

            let ldd = from_iter(&mut storage, set.iter());

163

100

            println!("LDD: {}", fmt_node(&storage, &ldd));

164

165

100

            let highest = compute_highest(&mut storage, &ldd);

166

100

            let bits = compute_bits(&highest);

167

100

            let bits_dd = singleton(&mut storage, &bits);

168

169

100

            let manager_ref = oxidd::bdd::new_manager(2048, 1024, 1);

170

171

100

            let total_bits: u32 = bits.iter().sum();

172

100

            println!("Total bits: {}", total_bits);

173

100

            let _variables = create_variables(&manager_ref, total_bits).unwrap();

174

175

100

            let _bdd = ldd_to_bdd(&mut storage, &manager_ref, &ldd, &bits_dd, 0).unwrap();

176

100

});

177

1

178