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

2236

pub fn ldd_to_bdd(

41

2236

    storage: &mut Storage,

42

2236

    manager_ref: &BDDManagerRef,

43

2236

    ldd: &LddRef<'_>,

44

2236

    bits_per_layer: &LddRef<'_>,

45

2236

    bit_variables: &[VarNo],

46

2236

) -> 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

2236

    let mut cache = FxHashMap::default();

50

51

2236

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

52

2236

        Ok(BDDFunction::from_edge(

53

2236

            manager,

54

2236

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

55

))

56

2236

})

57

2236

58

59

/// Recursive implementation of [ldd_to_bdd].

60

#[allow(clippy::mutable_key_type)]

61

344896

pub fn ldd_to_bdd_edge<'id>(

62

344896

    storage: &mut Storage,

63

344896

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

64

344896

    cache: &mut FxHashMap<Ldd, BDDFunction>,

65

344896

    ldd: &LddRef<'_>,

66

344896

    bits_per_layer: &LddRef<'_>,

67

344896

    bit_variables: &[VarNo],

68

344896

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

69

    // Base cases

70

344896

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

71

140306

        return manager.get_terminal(BDDTerminal::False);

72

204590

73

204590

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

74

9702

        return manager.get_terminal(BDDTerminal::True);

75

194888

76

77

194888

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

78

23558

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

79

171330

80

81

171330

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

82

171330

    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

171330

    let right_bdd = EdgeDropGuard::new(

86

171330

        manager,

87

171330

        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

171330

    let needed_bits = bits_value as usize;

92

171330

    if bit_variables.len() < needed_bits {

93

        panic!(

94

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

95

            bit_variables.len()

96

);

97

171330

98

99

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

100

171330

    let mut down_bdd = EdgeDropGuard::new(

101

171330

        manager,

102

171330

        ldd_to_bdd_edge(

103

171330

            storage,

104

171330

            manager,

105

171330

            cache,

106

171330

            &down,

107

171330

            &bits_down,

108

171330

            &bit_variables[needed_bits..],

109

)?,

110

);

111

112

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

113

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

114

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

115

171330

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

116

512713

    for i in 0..bits_value {

117

512713

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

118

512713

        let var_no = bit_variables[bit as usize];

119

512713

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

120

512713

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

121

            // bit is 1

122

169363

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

123

        } else {

124

            // bit is 0

125

343350

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

126

127

128

129

171330

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

130

171330

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

131

171330

    Ok(result)

132

344896

133

134

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

135

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

136

100

pub fn bdd_to_ldd(

137

100

    storage: &mut Storage,

138

100

    manager_ref: &BDDManagerRef,

139

100

    bdd: &BDDFunction,

140

100

    variables: &[VarNo],

141

100

    bits_per_layer: &[Value],

142

100

    current_bit: Value,

143

100

    current_value: Value,

144

100

) -> Result<Ldd, OutOfMemory> {

145

100

    manager_ref.with_manager_shared(|manager| {

146

100

        let edge = bdd.as_edge(manager);

147

100

        bdd_to_ldd_edge(

148

100

            storage,

149

100

            manager,

150

100

            edge.borrowed(),

151

100

            variables,

152

100

            bits_per_layer,

153

100

            current_bit,

154

100

            current_value,

155

156

100

})

157

100

158

159

/// Recursive implementation of [bdd_to_ldd].

160

26950

pub fn bdd_to_ldd_edge<'id>(

161

26950

    storage: &mut Storage,

162

26950

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

163

26950

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

164

26950

    variables: &[VarNo],

165

26950

    bits_per_layer: &[Value],

166

26950

    current_bit: Value,

167

26950

    current_value: Value,

168

26950

) -> Result<Ldd, OutOfMemory> {

169

26950

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

170

14204

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

171

12746

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

172

            // Base cases

173

12746

            match terminal {

174

                BDDTerminal::False => {

175

8041

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

176

177

                BDDTerminal::True => {

178

4705

                    if !variables.is_empty() {

179

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

180

565

                        let num_bits = bits_per_layer

181

565

                            .first()

182

565

                            .copied()

183

565

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

184

185

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

186

565

                        if num_bits == current_bit {

187

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

188

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

189

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

190

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

191

565

192

193

565

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

194

565

                        let high = bdd_to_ldd_edge(

195

565

                            storage,

196

565

                            manager,

197

565

                            bdd.borrowed(),

198

565

                            &variables[1..],

199

565

                            bits_per_layer,

200

565

                            current_bit + 1,

201

565

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

202

)?;

203

565

                        let low = bdd_to_ldd_edge(

204

565

                            storage,

205

565

                            manager,

206

565

                            bdd,

207

565

                            &variables[1..],

208

565

                            bits_per_layer,

209

565

                            current_bit + 1,

210

565

                            current_value,

211

)?;

212

565

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

213

4140

214

215

4140

                    return Ok(storage.insert_singleton(current_value));

216

217

218

219

};

220

221

    // TODO: Implement caching

222

223

    // Read the bits required per layer

224

14204

    let num_bits = bits_per_layer

225

14204

        .first()

226

14204

        .copied()

227

14204

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

228

229

14204

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

230

14204

    if *variable_level < bdd_node.level() {

231

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

232

439

        if num_bits == current_bit {

233

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

234

79

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

235

79

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

236

79

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

237

360

238

239

360

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

240

360

        let high = bdd_to_ldd_edge(

241

360

            storage,

242

360

            manager,

243

360

            bdd.borrowed(),

244

360

            &variables[1..],

245

360

            bits_per_layer,

246

360

            current_bit + 1,

247

360

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

248

)?;

249

360

        let low = bdd_to_ldd_edge(

250

360

            storage,

251

360

            manager,

252

360

            bdd,

253

360

            &variables[1..],

254

360

            bits_per_layer,

255

360

            current_bit + 1,

256

360

            current_value,

257

)?;

258

360

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

259

13765

260

261

13765

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

262

13765

    if num_bits == current_bit {

263

        // We reached the last bit for this layer

264

2609

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

265

2609

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

266

2609

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

267

    } else {

268

11156

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

269

11156

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

270

11156

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

271

272

        // Recurse for high and low cofactors

273

11156

        let high = bdd_to_ldd_edge(

274

11156

            storage,

275

11156

            manager,

276

11156

            bdd_high,

277

11156

            &variables[1..],

278

11156

            bits_per_layer,

279

11156

            current_bit + 1,

280

11156

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

281

)?;

282

11156

        let low = bdd_to_ldd_edge(

283

11156

            storage,

284

11156

            manager,

285

11156

            bdd_low,

286

11156

            &variables[1..],

287

11156

            bits_per_layer,

288

11156

            current_bit + 1,

289

11156

            current_value,

290

)?;

291

292

11156

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

293

294

26950

295

296

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

297

2033

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

298

2033

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

299

2033

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

300

2033

    result

301

2033

302

303

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

304

/// [ldd_to_bdd].

305

pub struct ValuesIter<'a> {

306

    bits: &'a [OptBool],

307

    num_of_bits: &'a [u32],

308

    offset: usize,

309

    index: usize,

310

311

312

impl<'a> ValuesIter<'a> {

313

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

314

        Self {

315

            bits,

316

            num_of_bits,

317

            offset: 0,

318

            index: 0,

319

320

321

322

323

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

324

    type Item = u64;

325

326

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

327

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

328

            return None;

329

330

331

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

332

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

333

            // Malformed input; stop iterating.

334

            return None;

335

336

337

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

338

        self.offset += nb;

339

        self.index += 1;

340

        Some(value)

341

342

343

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

344

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

345

        (remaining, Some(remaining))

346

347

348

349

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

350

351

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

352

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

353

295837

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

354

295837

    let mut value = 0u64;

355

887695

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

356

887695

        if *bit == OptBool::True {

357

318793

            value |= 1 << bit_pos;

358

568902

359

360

361

295837

    value

362

295837

363

364

/// Helper function for compute_highest

365

623239

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

366

623239

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

367

312636

        return;

368

310603

369

370

310603

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

371

310603

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

372

310603

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

373

374

310603

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

375

623239

376

377

/// Calculate minimum bits needed to represent the value

378

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

379

4236

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

380

4236

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

381

4236

382

383

/// Calculate minimum bits needed to represent the value

384

1244

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

385

1244

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

386

1244

387

388

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

389

503

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

390

3633

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

391

503

392

393

#[cfg(test)]

394

mod tests {

395

    use oxidd::Manager;

396

    use oxidd::ManagerRef;

397

398

    use merc_ldd::LddDisplay;

399

    use merc_ldd::Storage;

400

    use merc_ldd::from_iter;

401

    use merc_ldd::random_vector_set;

402

    use merc_ldd::singleton;

403

    use merc_utilities::random_test;

404

405

    use crate::FormatConfigSet;

406

    use crate::bdd_to_ldd;

407

    use crate::compute_bits;

408

    use crate::compute_highest;

409

    use crate::ldd_to_bdd;

410

    use crate::required_bits;

411

412

    #[test]

413

1

    fn test_random_compute_highest() {

414

100

        random_test(100, |rng| {

415

100

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

416

100

            let mut storage = Storage::new();

417

100

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

418

100

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

419

420

100

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

421

100

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

422

300

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

423

                // Determine the highest value for every vector

424

1188

                for value in set.iter() {

425

1188

                    assert!(

426

1188

                        *h >= value[i],

427

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

428

i,

429

h,

430

                        value[i]

431

);

432

433

434

435

100

            let bits = compute_bits(&highest);

436

100

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

437

438

300

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

439

300

                let expected_bits = required_bits(highest[i]);

440

300

                assert_eq!(

441

                    *b, expected_bits,

442

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

443

                    i, b, expected_bits

444

);

445

446

100

})

447

1

448

449

    #[test]

450

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

451

1

    fn test_random_ldd_to_bdd() {

452

100

        random_test(100, |rng| {

453

100

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

454

455

100

            let mut storage = Storage::new();

456

100

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

457

100

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

458

459

100

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

460

100

            let bits = compute_bits(&highest);

461

100

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

462

463

100

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

464

465

100

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

466

100

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

467

100

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

468

100

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

469

100

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

470

100

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

471

100

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

472

473

100

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

474

100

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

475

100

});

476

1

477