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::ldd::LDDFunction;

11

use oxidd::ldd::LDDManagerRef;

12

use oxidd::ldd::Value;

13

use oxidd::util::Borrowed;

14

use oxidd::util::OptBool;

15

use oxidd::util::OutOfMemory;

16

use oxidd_core::function::EdgeOfFunc;

17

use oxidd_core::util::EdgeDropGuard;

18

use oxidd_rules_bdd::simple::BDDTerminal;

19

use rustc_hash::FxHashMap;

20

21

use crate::collect_children;

22

use crate::height;

23

24

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

25

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

26

/// bits.

27

///

28

/// # Details

29

///

30

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

31

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

32

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

33

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

34

/// exist in the given BDD manager.

35

3690

pub fn ldd_to_bdd(

36

3690

    _ldd_manager_ref: &LDDManagerRef,

37

3690

    bdd_manager_ref: &BDDManagerRef,

38

3690

    ldd: &LDDFunction,

39

3690

    bits_per_layer: &LDDFunction,

40

3690

    bit_variables: &[VarNo],

41

3690

) -> Result<BDDFunction, OutOfMemory> {

42

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

43

    // need the bits_per_layer and bit_variables in the cache.

44

3690

    let mut cache = FxHashMap::default();

45

46

3690

    bdd_manager_ref.with_manager_shared(|bdd_manager| -> Result<BDDFunction, OutOfMemory> {

47

3690

        Ok(BDDFunction::from_edge(

48

3690

            bdd_manager,

49

3690

            ldd_to_bdd_edge(bdd_manager, &mut cache, ldd, bits_per_layer, bit_variables)?,

50

))

51

3690

})

52

3690

53

54

/// Recursive implementation of [ldd_to_bdd].

55

#[allow(clippy::mutable_key_type)]

56

607782

pub fn ldd_to_bdd_edge<'id>(

57

607782

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

58

607782

    cache: &mut FxHashMap<LDDFunction, BDDFunction>,

59

607782

    ldd: &LDDFunction,

60

607782

    bits_per_layer: &LDDFunction,

61

607782

    bit_variables: &[VarNo],

62

607782

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

63

    // Base cases

64

607782

    if ldd.is_empty() {

65

247543

        return bdd_manager.get_terminal(BDDTerminal::False);

66

360239

67

360239

    if ldd.is_empty_vector() {

68

15186

        return bdd_manager.get_terminal(BDDTerminal::True);

69

345053

70

71

345053

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

72

43007

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

73

302046

74

75

302046

    let (value, down, right) = ldd.node().expect("ldd is an inner node");

76

302046

    let (bits_value, bits_down, _bits_right) = bits_per_layer.node().expect("bits_per_layer is an inner node");

77

78

    // Right branch does not consume variables at this layer

79

302046

    let right_bdd = EdgeDropGuard::new(

80

302046

        bdd_manager,

81

302046

        ldd_to_bdd_edge(bdd_manager, cache, &right, bits_per_layer, bit_variables)?,

82

);

83

84

302046

    let needed_bits = bits_value as usize;

85

302046

    assert!(

86

302046

        bit_variables.len() >= needed_bits,

87

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

88

        bit_variables.len()

89

);

90

91

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

92

302046

    let mut down_bdd = EdgeDropGuard::new(

93

302046

        bdd_manager,

94

302046

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

95

);

96

97

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

98

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

99

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

100

302046

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

101

905215

    for i in 0..bits_value {

102

905215

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

103

905215

        let var_no = bit_variables[bit as usize];

104

905215

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

105

905215

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

106

            // bit is 1

107

301036

            down_bdd = EdgeDropGuard::new(

108

301036

                bdd_manager,

109

301036

                BDDFunction::ite_edge(bdd_manager, &var, &down_bdd, &f_edge)?,

110

);

111

        } else {

112

            // bit is 0

113

604179

            down_bdd = EdgeDropGuard::new(

114

604179

                bdd_manager,

115

604179

                BDDFunction::ite_edge(bdd_manager, &var, &f_edge, &down_bdd)?,

116

);

117

118

119

120

302046

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

121

302046

    cache.insert(ldd.clone(), BDDFunction::from_edge_ref(bdd_manager, &result));

122

302046

    Ok(result)

123

607782

124

125

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

126

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

127

100

pub fn bdd_to_ldd(

128

100

    ldd_manager_ref: &LDDManagerRef,

129

100

    manager_ref: &BDDManagerRef,

130

100

    bdd: &BDDFunction,

131

100

    variables: &[VarNo],

132

100

    bits_per_layer: &[Value],

133

100

    current_bit: Value,

134

100

    current_value: Value,

135

100

) -> Result<LDDFunction, OutOfMemory> {

136

100

    let mut cache = FxHashMap::default();

137

    // Hold both manager locks for the whole recursion: every LDD node is built with the lock-free

138

    // `*_edge` constructors, so the entire conversion runs under a single shared lock per manager.

139

100

    manager_ref.with_manager_shared(|manager| {

140

100

        ldd_manager_ref.with_manager_shared(|ldd_manager| {

141

100

            let edge = bdd.as_edge(manager);

142

100

            bdd_to_ldd_edge(

143

100

                ldd_manager,

144

100

                manager,

145

100

                &mut cache,

146

100

                edge.borrowed(),

147

100

                variables,

148

100

                bits_per_layer,

149

100

                current_bit,

150

100

                current_value,

151

152

100

})

153

100

})

154

100

155

156

/// Recursive implementation of [bdd_to_ldd].

157

#[allow(clippy::mutable_key_type)]

158

#[allow(clippy::too_many_arguments)]

159

15812

pub fn bdd_to_ldd_edge<'id, 'ldd>(

160

15812

    ldd_manager: &<LDDFunction as Function>::Manager<'ldd>,

161

15812

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

162

15812

    cache: &mut FxHashMap<(BDDFunction, usize, Value, Value), LDDFunction>,

163

15812

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

164

15812

    variables: &[VarNo],

165

15812

    bits_per_layer: &[Value],

166

15812

    current_bit: Value,

167

15812

    current_value: Value,

168

15812

) -> Result<LDDFunction, OutOfMemory> {

169

15812

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

170

11200

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

171

4612

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

172

            // Base cases

173

4612

            match terminal {

174

                BDDTerminal::False => {

175

3331

                    return LDDFunction::empty_set(ldd_manager);

176

177

                BDDTerminal::True => {

178

1281

                    if variables.is_empty() {

179

882

                        return LDDFunction::singleton(ldd_manager, &[current_value]);

180

399

181

182

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

183

                    // Cache this because the True terminal can be reached via many shared BDD paths.

184

399

                    let cache_key = (

185

399

                        BDDFunction::from_edge_ref(manager, &*bdd),

186

399

                        variables.len(),

187

399

                        current_bit,

188

399

                        current_value,

189

399

);

190

399

                    if let Some(cached) = cache.get(&cache_key) {

191

184

                        return Ok(cached.clone());

192

215

193

194

215

                    let num_bits = bits_per_layer

195

215

                        .first()

196

215

                        .copied()

197

215

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

198

199

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

200

215

                    let result = if num_bits == current_bit {

201

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

202

                        let down =

203

                            bdd_to_ldd_edge(ldd_manager, manager, cache, bdd, variables, &bits_per_layer[1..], 0, 0)?;

204

                        let right = LDDFunction::empty_set(ldd_manager)?;

205

                        LDDFunction::make_node(ldd_manager, current_value, &down, &right)?

206

                    } else {

207

215

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

208

215

                        let high = bdd_to_ldd_edge(

209

215

                            ldd_manager,

210

215

                            manager,

211

215

                            cache,

212

215

                            bdd.borrowed(),

213

215

                            &variables[1..],

214

215

                            bits_per_layer,

215

                            current_bit + 1,

216

215

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

217

)?;

218

215

                        let low = bdd_to_ldd_edge(

219

215

                            ldd_manager,

220

215

                            manager,

221

215

                            cache,

222

215

                            bdd,

223

215

                            &variables[1..],

224

215

                            bits_per_layer,

225

215

                            current_bit + 1,

226

215

                            current_value,

227

)?;

228

215

                        LDDFunction::union_edge(ldd_manager, &high, &low)?

229

};

230

231

215

                    cache.insert(cache_key, result.clone());

232

215

                    return Ok(result);

233

234

235

236

};

237

238

    // Cache lookup: shared BDD subgraphs are expanded independently each time without this,

239

    // causing exponential blowup when the same inner node is reachable via multiple paths.

240

11200

    let cache_key = (

241

11200

        BDDFunction::from_edge_ref(manager, &*bdd),

242

11200

        variables.len(),

243

11200

        current_bit,

244

11200

        current_value,

245

11200

);

246

11200

    if let Some(cached) = cache.get(&cache_key) {

247

2306

        return Ok(cached.clone());

248

8894

249

250

    // Read the bits required per layer

251

8894

    let num_bits = bits_per_layer

252

8894

        .first()

253

8894

        .copied()

254

8894

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

255

256

8894

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

257

8894

    let result = if *variable_level < bdd_node.level() {

258

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

259

327

        if num_bits == current_bit {

260

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

261

81

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

262

81

            let right = LDDFunction::empty_set(ldd_manager)?;

263

81

            LDDFunction::make_node(ldd_manager, current_value, &down, &right)?

264

        } else {

265

246

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

266

246

            let high = bdd_to_ldd_edge(

267

246

                ldd_manager,

268

246

                manager,

269

246

                cache,

270

246

                bdd.borrowed(),

271

246

                &variables[1..],

272

246

                bits_per_layer,

273

246

                current_bit + 1,

274

246

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

275

)?;

276

246

            let low = bdd_to_ldd_edge(

277

246

                ldd_manager,

278

246

                manager,

279

246

                cache,

280

246

                bdd,

281

246

                &variables[1..],

282

246

                bits_per_layer,

283

246

                current_bit + 1,

284

246

                current_value,

285

)?;

286

246

            LDDFunction::union_edge(ldd_manager, &high, &low)?

287

288

    } else {

289

8567

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

290

8567

        if num_bits == current_bit {

291

            // We reached the last bit for this layer

292

2425

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

293

2425

            let right = LDDFunction::empty_set(ldd_manager)?;

294

2425

            LDDFunction::make_node(ldd_manager, current_value, &down, &right)?

295

        } else {

296

6142

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

297

6142

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

298

299

            // Recurse for high and low cofactors

300

6142

            let high = bdd_to_ldd_edge(

301

6142

                ldd_manager,

302

6142

                manager,

303

6142

                cache,

304

6142

                bdd_high,

305

6142

                &variables[1..],

306

6142

                bits_per_layer,

307

6142

                current_bit + 1,

308

6142

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

309

)?;

310

6142

            let low = bdd_to_ldd_edge(

311

6142

                ldd_manager,

312

6142

                manager,

313

6142

                cache,

314

6142

                bdd_low,

315

6142

                &variables[1..],

316

6142

                bits_per_layer,

317

6142

                current_bit + 1,

318

6142

                current_value,

319

)?;

320

321

6142

            LDDFunction::union_edge(ldd_manager, &high, &low)?

322

323

};

324

325

8894

    cache.insert(cache_key, result.clone());

326

8894

    Ok(result)

327

15812

328

329

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

330

3286

pub fn compute_highest(storage: &LDDManagerRef, ldd: &LDDFunction) -> Vec<u32> {

331

3286

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

332

3286

    compute_highest_rec(&mut result, ldd, 0);

333

3286

    result

334

3286

335

336

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

337

/// [ldd_to_bdd].

338

pub struct ValuesIter<'a> {

339

    bits: &'a [OptBool],

340

    num_of_bits: &'a [u32],

341

    offset: usize,

342

    index: usize,

343

344

345

impl<'a> ValuesIter<'a> {

346

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

347

        Self {

348

            bits,

349

            num_of_bits,

350

            offset: 0,

351

            index: 0,

352

353

354

355

356

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

357

    type Item = u64;

358

359

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

360

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

361

            return None;

362

363

364

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

365

        // Clamp the slice to the available bits so the iterator always yields exactly

366

        // num_of_bits.len() items, honoring the ExactSizeIterator contract even on

367

        // truncated input.

368

        let start = self.offset.min(self.bits.len());

369

        let end = (self.offset + nb).min(self.bits.len());

370

        let value = to_value(&self.bits[start..end]);

371

        self.offset += nb;

372

        self.index += 1;

373

        Some(value)

374

375

376

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

377

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

378

        (remaining, Some(remaining))

379

380

381

382

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

383

384

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

385

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

386

204912

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

387

204912

    let mut value = 0u64;

388

614920

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

389

614920

        if *bit == OptBool::True {

390

            // Bits beyond the 64-bit range cannot be represented in a u64; ignore them

391

            // rather than overflowing the shift (checked_shl yields None for bit_pos >= 64).

392

182265

            if let Some(mask) = 1u64.checked_shl(bit_pos as u32) {

393

182265

                value |= mask;

394

182265

395

432655

396

397

398

204912

    value

399

204912

400

401

/// Helper function for compute_highest

402

1091604

fn compute_highest_rec(result: &mut [u32], set: &LDDFunction, depth: usize) {

403

1091604

    let (value, down, right) = match set.node() {

404

        // Terminals (empty set / empty vector) have no contribution.

405

547445

        None => return,

406

544159

        Some(node) => node,

407

};

408

409

544159

    compute_highest_rec(result, &right, depth);

410

544159

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

411

412

544159

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

413

1091604

414

415

/// Calculate minimum bits needed to represent the value

416

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

417

6449

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

418

6449

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

419

6449

420

421

/// Calculate minimum bits needed to represent the value

422

4178

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

423

4178

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

424

4178

425

426

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

427

704

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

428

5645

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

429

704

430

431

#[cfg(test)]

432

mod tests {

433

    use oxidd::Manager;

434

    use oxidd::ManagerRef;

435

    use oxidd::ldd::LDDFunction;

436

437

    use merc_utilities::random_test;

438

439

    use crate::FormatConfigSet;

440

    use crate::LddDisplay;

441

    use crate::bdd_to_ldd;

442

    use crate::compute_bits;

443

    use crate::compute_highest;

444

    use crate::from_iter;

445

    use crate::ldd_to_bdd;

446

    use crate::random_vector_set;

447

    use crate::required_bits;

448

449

    #[test]

450

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

451

1

    fn test_random_compute_highest() {

452

100

        random_test(100, |rng| {

453

100

            let manager = oxidd::ldd::new_manager(2048, 1024, 1);

454

100

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

455

100

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

456

100

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

457

458

100

            let highest = compute_highest(&manager, &ldd);

459

100

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

460

300

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

461

                // Determine the highest value for every vector

462

1179

                for value in set.iter() {

463

1179

                    assert!(

464

1179

                        *h >= value[i],

465

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

466

i,

467

h,

468

                        value[i]

469

);

470

471

472

473

100

            let bits = compute_bits(&highest);

474

100

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

475

476

300

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

477

300

                let expected_bits = required_bits(highest[i]);

478

300

                assert_eq!(

479

                    *b, expected_bits,

480

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

481

                    i, b, expected_bits

482

);

483

484

100

})

485

1

486

487

    #[test]

488

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

489

1

    fn test_random_ldd_to_bdd() {

490

100

        random_test(100, |rng| {

491

100

            let manager = oxidd::ldd::new_manager(2048, 1024, 1);

492

100

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

493

494

100

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

495

100

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

496

497

100

            let highest = compute_highest(&manager, &ldd);

498

100

            let bits = compute_bits(&highest);

499

100

            let bits_dd = manager

500

100

                .with_manager_shared(|m| LDDFunction::singleton(m, &bits))

501

100

                .unwrap();

502

503

100

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

504

505

100

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

506

100

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

507

100

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

508

100

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

509

100

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

510

100

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

511

100

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

512

513

100

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

514

100

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

515

100

});

516

1

517