Grcov report - ldd_to

1

use oxidd::BooleanFunction;

2

use oxidd::Edge;

3

use oxidd::Function;

4

use oxidd::HasLevel;

5

use oxidd::Manager;

6

use oxidd::ManagerRef;

7

use oxidd::VarNo;

8

use oxidd::bdd::BDDFunction;

9

use oxidd::bdd::BDDManagerRef;

10

use oxidd::util::Borrowed;

11

use oxidd::util::OptBool;

12

use oxidd::util::OutOfMemory;

13

use oxidd_core::function::EdgeOfFunc;

14

use oxidd_core::util::EdgeDropGuard;

15

use oxidd_rules_bdd::simple::BDDTerminal;

16

use rustc_hash::FxHashMap;

17

18

use merc_ldd::DataRef;

19

use merc_ldd::Ldd;

20

use merc_ldd::LddRef;

21

use merc_ldd::Storage;

22

use merc_ldd::Value;

23

use merc_ldd::height;

24

use merc_ldd::union;

25

26

use crate::collect_children;

27

28

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

29

/// same set by bitblasting the vector elements using the given variables as

30

/// bits.

31

///

32

/// # Details

33

///

34

/// The `bits_per_layer` should be a singleton LDD containing the result of

35

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

36

/// by node, and introducing bit number of BDD variables (given by

37

/// `bit_variables`) for each layer in the LDD. These variables *must* already

38

/// exist in the given BDD manager.

39

#[allow(clippy::mutable_key_type)]

40

2912

pub fn ldd_to_bdd(

41

2912

    storage: &mut Storage,

42

2912

    manager_ref: &BDDManagerRef,

43

2912

    ldd: &LddRef<'_>,

44

2912

    bits_per_layer: &LddRef<'_>,

45

2912

    bit_variables: &[VarNo],

46

2912

) -> Result<BDDFunction, OutOfMemory> {

47

    // For LDDs we can assume that nodes in one layer are unique, so we don't

48

    // need the bits_per_layer and bit_variables in the cache.

49

2912

    let mut cache = FxHashMap::default();

50

51

2912

    manager_ref.with_manager_shared(|manager| -> Result<BDDFunction, OutOfMemory> {

52

2912

        Ok(BDDFunction::from_edge(

53

2912

            manager,

54

2912

            ldd_to_bdd_edge(storage, manager, &mut cache, ldd, bits_per_layer, bit_variables)?,

55

))

56

2912

})

57

2912

58

59

/// Recursive implementation of [ldd_to_bdd].

60

#[allow(clippy::mutable_key_type)]

61

818420

pub fn ldd_to_bdd_edge<'id>(

62

818420

    storage: &mut Storage,

63

818420

    manager: &<BDDFunction as Function>::Manager<'id>,

64

818420

    cache: &mut FxHashMap<Ldd, BDDFunction>,

65

818420

    ldd: &LddRef<'_>,

66

818420

    bits_per_layer: &LddRef<'_>,

67

818420

    bit_variables: &[VarNo],

68

818420

) -> Result<EdgeOfFunc<'id, BDDFunction>, OutOfMemory> {

69

    // Base cases

70

818420

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

71

346994

        return manager.get_terminal(BDDTerminal::False);

72

471426

73

471426

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

74

13215

        return manager.get_terminal(BDDTerminal::True);

75

458211

76

77

458211

    if let Some(cached) = cache.get(ldd) {

78

50457

        return Ok(manager.clone_edge(cached.as_edge(manager)));

79

407754

80

81

407754

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

82

407754

    let DataRef(bits_value, bits_down, _bits_right) = storage.get_ref(bits_per_layer);

83

84

    // Right branch does not consume variables at this layer

85

407754

    let right_bdd = EdgeDropGuard::new(

86

407754

        manager,

87

407754

        ldd_to_bdd_edge(storage, manager, cache, &right, bits_per_layer, bit_variables)?,

88

);

89

90

    // Ensure we have enough variables for this layer

91

407754

    let needed_bits = bits_value as usize;

92

407754

    if bit_variables.len() < needed_bits {

93

        panic!(

94

            "Insufficient variables: need {needed_bits}, have {} for current layer",

95

            bit_variables.len()

96

);

97

407754

98

99

    // Recurse on down with the remaining variables after consuming this layer

100

407754

    let mut down_bdd = EdgeDropGuard::new(

101

407754

        manager,

102

407754

        ldd_to_bdd_edge(storage, manager, cache, &down, &bits_down, &bit_variables[needed_bits..])?,

103

);

104

105

    // Encode current value using the variables for this layer (MSB to LSB)

106

    // Current layer variables: vars[0..bits_value]

107

    // The `ite` is necessary since the variables are not in sorted order.

108

407754

    let f_edge = EdgeDropGuard::new(manager, manager.get_terminal(BDDTerminal::False)?);

109

1222884

    for i in 0..bits_value {

110

1222884

        let bit = bits_value - i - 1; // MSB first

111

1222884

        let var_no = bit_variables[bit as usize];

112

1222884

        let var = EdgeDropGuard::new(manager, BDDFunction::var_edge(manager, var_no)?);

113

1222884

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

114

            // bit is 1

115

407228

            down_bdd = EdgeDropGuard::new(manager, BDDFunction::ite_edge(manager, &var, &down_bdd, &f_edge)?);

116

        } else {

117

            // bit is 0

118

815656

            down_bdd = EdgeDropGuard::new(manager, BDDFunction::ite_edge(manager, &var, &f_edge, &down_bdd)?);

119

120

121

122

407754

    let result = BDDFunction::or_edge(manager, &down_bdd, &right_bdd)?;

123

407754

    cache.insert(storage.protect(ldd), BDDFunction::from_edge_ref(manager, &result));

124

407754

    Ok(result)

125

818420

126

127

/// Converts a BDD representing a set of bitblasted vectors back into an LDD

128

/// representing the same set, i.e., the inverse of [ldd_to_bdd].

129

100

pub fn bdd_to_ldd(

130

100

    storage: &mut Storage,

131

100

    manager_ref: &BDDManagerRef,

132

100

    bdd: &BDDFunction,

133

100

    variables: &[VarNo],

134

100

    bits_per_layer: &[Value],

135

100

    current_bit: Value,

136

100

    current_value: Value,

137

100

) -> Result<Ldd, OutOfMemory> {

138

100

    manager_ref.with_manager_shared(|manager| {

139

100

        let edge = bdd.as_edge(manager);

140

100

        bdd_to_ldd_edge(

141

100

            storage,

142

100

            manager,

143

100

            edge.borrowed(),

144

100

            variables,

145

100

            bits_per_layer,

146

100

            current_bit,

147

100

            current_value,

148

149

100

})

150

100

151

152

/// Recursive implementation of [bdd_to_ldd].

153

26882

pub fn bdd_to_ldd_edge<'id>(

154

26882

    storage: &mut Storage,

155

26882

    manager: &<BDDFunction as Function>::Manager<'id>,

156

26882

    bdd: Borrowed<EdgeOfFunc<'id, BDDFunction>>,

157

26882

    variables: &[VarNo],

158

26882

    bits_per_layer: &[Value],

159

26882

    current_bit: Value,

160

26882

    current_value: Value,

161

26882

) -> Result<Ldd, OutOfMemory> {

162

26882

    let bdd_node = match manager.get_node(&bdd) {

163

14138

        oxidd::Node::Inner(node) => node,

164

12744

        oxidd::Node::Terminal(terminal) => {

165

            // Base cases

166

12744

            match terminal {

167

                BDDTerminal::False => {

168

8013

                    return Ok(storage.empty_set().clone());

169

170

                BDDTerminal::True => {

171

4731

                    if !variables.is_empty() {

172

                        // If there are still variables left, we must generate don't cares for the remaining layers

173

582

                        let num_bits = bits_per_layer

174

582

                            .first()

175

582

                            .copied()

176

582

                            .expect("Missing bits per layer for current layer");

177

178

                        // There are don't care variables in this BDD that have been skipped, so generate both branches.

179

582

                        if num_bits == current_bit {

180

                            // We reached the last bit for this layer, variable still belongs to next layer.

181

                            let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?;

182

                            let right = storage.empty_set().clone();

183

                            return Ok(storage.insert(current_value, &down, &right));

184

582

185

186

582

                        debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer");

187

582

                        let high = bdd_to_ldd_edge(

188

582

                            storage,

189

582

                            manager,

190

582

                            bdd.borrowed(),

191

582

                            &variables[1..],

192

582

                            bits_per_layer,

193

582

                            current_bit + 1,

194

582

                            current_value | (1 << (num_bits - current_bit - 1)),

195

)?;

196

582

                        let low = bdd_to_ldd_edge(

197

582

                            storage,

198

582

                            manager,

199

582

                            bdd,

200

582

                            &variables[1..],

201

582

                            bits_per_layer,

202

582

                            current_bit + 1,

203

582

                            current_value,

204

)?;

205

582

                        return Ok(union(storage, &high, &low));

206

4149

207

208

4149

                    return Ok(storage.insert_singleton(current_value));

209

210

211

212

};

213

214

    // TODO: Implement caching

215

216

    // Read the bits required per layer

217

14138

    let num_bits = bits_per_layer

218

14138

        .first()

219

14138

        .copied()

220

14138

        .expect("Missing bits per layer for current layer");

221

222

14138

    let variable_level = variables.first().expect("Missing variable for current layer");

223

14138

    if *variable_level < bdd_node.level() {

224

        // There are don't care variables in this BDD that have been skipped, so generate both branches without cofactors.

225

453

        if num_bits == current_bit {

226

            // We reached the last bit for this layer, variable still belongs to next layer.

227

83

            let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?;

228

83

            let right = storage.empty_set().clone();

229

83

            return Ok(storage.insert(current_value, &down, &right));

230

370

231

232

370

        debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer");

233

370

        let high = bdd_to_ldd_edge(

234

370

            storage,

235

370

            manager,

236

370

            bdd.borrowed(),

237

370

            &variables[1..],

238

370

            bits_per_layer,

239

370

            current_bit + 1,

240

370

            current_value | (1 << (num_bits - current_bit - 1)),

241

)?;

242

370

        let low = bdd_to_ldd_edge(

243

370

            storage,

244

370

            manager,

245

370

            bdd,

246

370

            &variables[1..],

247

370

            bits_per_layer,

248

370

            current_bit + 1,

249

370

            current_value,

250

)?;

251

370

        return Ok(union(storage, &high, &low));

252

13685

253

254

13685

    debug_assert_eq!(*variable_level, bdd_node.level(), "Levels do not match");

255

13685

    if num_bits == current_bit {

256

        // We reached the last bit for this layer

257

2575

        let down = bdd_to_ldd_edge(storage, manager, bdd, variables, &bits_per_layer[1..], 0, 0)?;

258

2575

        let right = storage.empty_set().clone();

259

2575

        Ok(storage.insert(current_value, &down, &right))

260

    } else {

261

11110

        debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer");

262

11110

        debug_assert!(current_bit < num_bits, "Current bit exceeds number of bits for layer");

263

11110

        let (bdd_high, bdd_low) = collect_children(bdd_node);

264

265

        // Recurse for high and low cofactors

266

11110

        let high = bdd_to_ldd_edge(

267

11110

            storage,

268

11110

            manager,

269

11110

            bdd_high,

270

11110

            &variables[1..],

271

11110

            bits_per_layer,

272

11110

            current_bit + 1,

273

11110

            current_value | (1 << (num_bits - current_bit - 1)),

274

)?;

275

11110

        let low = bdd_to_ldd_edge(

276

11110

            storage,

277

11110

            manager,

278

11110

            bdd_low,

279

11110

            &variables[1..],

280

11110

            bits_per_layer,

281

11110

            current_bit + 1,

282

11110

            current_value,

283

)?;

284

285

11110

        Ok(union(storage, &high, &low))

286

287

26882

288

289

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

290

2611

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

291

2611

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

292

2611

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

293

2611

    result

294

2611

295

296

/// Iterator that yields values reconstructed from a bit cube, from a BDD obtained by

297

/// [ldd_to_bdd].

298

pub struct ValuesIter<'a> {

299

    bits: &'a [OptBool],

300

    num_of_bits: &'a [u32],

301

    offset: usize,

302

    index: usize,

303

304

305

impl<'a> ValuesIter<'a> {

306

    pub fn new(bits: &'a [OptBool], num_of_bits: &'a [u32]) -> Self {

307

        Self {

308

            bits,

309

            num_of_bits,

310

            offset: 0,

311

            index: 0,

312

313

314

315

316

impl<'a> Iterator for ValuesIter<'a> {

317

    type Item = u64;

318

319

    fn next(&mut self) -> Option<Self::Item> {

320

        if self.index >= self.num_of_bits.len() {

321

            return None;

322

323

324

        let nb = self.num_of_bits[self.index] as usize;

325

        if self.offset + nb > self.bits.len() {

326

            // Malformed input; stop iterating.

327

            return None;

328

329

330

        let value = to_value(&self.bits[self.offset..self.offset + nb]);

331

        self.offset += nb;

332

        self.index += 1;

333

        Some(value)

334

335

336

    fn size_hint(&self) -> (usize, Option<usize>) {

337

        let remaining = self.num_of_bits.len().saturating_sub(self.index);

338

        (remaining, Some(remaining))

339

340

341

342

impl<'a> ExactSizeIterator for ValuesIter<'a> {}

343

344

/// Reconstruct the value represented by the bits as encoded by

345

/// [crate::ldd_to_bdd]. So most significant bit first.

346

pub fn to_value(bits: &[OptBool]) -> u64 {

347

    let mut value = 0u64;

348

    for (bit_pos, bit) in bits.iter().rev().enumerate() {

349

        if *bit == OptBool::True {

350

            value |= 1 << bit_pos;

351

352

353

354

    value

355

356

357

/// Helper function for compute_highest

358

1016285

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

359

1016285

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

360

509448

        return;

361

506837

362

363

506837

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

364

506837

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

365

506837

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

366

367

506837

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

368

1016285

369

370

/// Calculate minimum bits needed to represent the value

371

/// Use 1 bit if value is 0 to ensure at least 1 bit is written

372

5312

pub fn required_bits(value: u32) -> u32 {

373

5312

    (u32::BITS - value.leading_zeros()).max(1)

374

5312

375

376

/// Calculate minimum bits needed to represent the value

377

2558

pub fn required_bits_64(value: u64) -> u32 {

378

2558

    (u64::BITS - value.leading_zeros()).max(1)

379

2558

380

381

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

382

601

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

383

4611

    highest.iter().map(|&h| required_bits(h)).collect()

384

601

385

386

#[cfg(test)]

387

mod tests {

388

    use merc_ldd::LddDisplay;

389

    use merc_ldd::from_iter;

390

    use merc_ldd::random_vector_set;

391

    use merc_ldd::singleton;

392

    use merc_utilities::random_test;

393

    use oxidd::Manager;

394

    use oxidd::ManagerRef;

395

396

    use crate::FormatConfigSet;

397

398

    use super::*;

399

400

    #[test]

401

1

    fn test_random_compute_highest() {

402

100

        random_test(100, |rng| {

403

100

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

404

100

            let mut storage = Storage::new();

405

100

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

406

100

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

407

408

100

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

409

100

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

410

300

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

411

                // Determine the highest value for every vector

412

1188

                for value in set.iter() {

413

1188

                    assert!(

414

1188

                        *h >= value[i],

415

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

416

i,

417

h,

418

                        value[i]

419

);

420

421

422

423

100

            let bits = compute_bits(&highest);

424

100

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

425

426

300

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

427

300

                let expected_bits = required_bits(highest[i]);

428

300

                assert_eq!(

429

                    *b, expected_bits,

430

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

431

                    i, b, expected_bits

432

);

433

434

100

})

435

1

436

437

    #[test]

438

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

439

1

    fn test_random_ldd_to_bdd() {

440

100

        random_test(100, |rng| {

441

100

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

442

443

100

            let mut storage = Storage::new();

444

100

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

445

100

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

446

447

100

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

448

100

            let bits = compute_bits(&highest);

449

100

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

450

451

100

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

452

453

100

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

454

100

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

455

100

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

456

100

            let vars = manager_ref.with_manager_exclusive(|manager| manager.add_vars(total_bits).collect::<Vec<_>>());

457

100

            let bdd = ldd_to_bdd(&mut storage, &manager_ref, &ldd, &bits_dd, &vars).unwrap();

458

100

            println!("resulting BDD: {}", FormatConfigSet(&bdd));

459

100

            let resulting_ldd = bdd_to_ldd(&mut storage, &manager_ref, &bdd, &vars, &bits, 0, 0).unwrap();

460

461

100

            println!("resulting LDD: {}", LddDisplay::new(&storage, &resulting_ldd));

462

100

            assert_eq!(ldd, resulting_ldd, "Converted LDD does not match original");

463

100

});

464

1

465