Grcov report - util.rs

1

use std::collections::HashSet;

2

3

use std::cmp::Ordering;

4

use std::fmt;

5

6

use merc_io::LargeFormatter;

7

use oxidd::BooleanFunction;

8

use oxidd::Edge;

9

use oxidd::Function;

10

use oxidd::HasLevel;

11

use oxidd::InnerNode;

12

use oxidd::LevelNo;

13

use oxidd::Manager;

14

use oxidd::ManagerRef;

15

use oxidd::Node;

16

use oxidd::VarNo;

17

use oxidd::bdd::BDDFunction;

18

use oxidd::bdd::BDDManagerRef;

19

use oxidd::ldd::LDDFunction;

20

use oxidd::ldd::LDDManagerRef;

21

use oxidd::ldd::Value;

22

use oxidd::util::Borrowed;

23

use oxidd::util::OutOfMemory;

24

use oxidd::util::SatCountCache as OxiddSatCountCache;

25

use oxidd_core::function::EdgeOfFunc;

26

use oxidd_core::util::EdgeDropGuard;

27

use oxidd_core::util::num::F64;

28

use oxidd_rules_ldd::LDDTerminal;

29

use rustc_hash::FxBuildHasher;

30

use rustc_hash::FxHashMap;

31

32

/// The BDD representing the support variables of a BDD function.

33

pub type BDDSupport = BDDFunction;

34

35

/// Result of [`approx_satcount`], either an exact integer count or an f64 approximation.

36

///

37

/// The underlying [`BooleanFunction::sat_count`] initializes its accumulator to

38

/// `2^vars`, so a u64 accumulator overflows once `vars >= 64` regardless of the

39

/// actual count.

40

#[derive(Debug, Clone, Copy, PartialEq)]

41

pub enum SatCount {

42

    Exact(u64),

43

    Approximate(f64),

44

45

46

impl SatCount {

47

    /// The count converted to f64, lossy for [`SatCount::Exact`] values above `2^53`.

48

503

    pub fn as_f64(&self) -> f64 {

49

503

        match self {

50

503

            SatCount::Exact(n) => *n as f64,

51

            SatCount::Approximate(x) => *x,

52

53

503

54

55

    /// The exact count, or `None` if only an f64 approximation is available.

56

    pub fn exact(&self) -> Option<u64> {

57

        match self {

58

            SatCount::Exact(n) => Some(*n),

59

            SatCount::Approximate(_) => None,

60

61

62

63

64

impl fmt::Display for SatCount {

65

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

66

        match self {

67

            SatCount::Exact(n) => write!(f, "{}", LargeFormatter(*n)),

68

            SatCount::Approximate(x) => write!(f, "~{:e}", x),

69

70

71

72

73

/// Reusable cache for [`approx_satcount`], holding both the exact (`u64`) and the

74

/// approximate (`f64`) sub-caches so the same instance can serve calls with

75

/// any number of variables.

76

#[derive(Default)]

77

pub struct SatCountCache {

78

    exact: OxiddSatCountCache<u64, FxBuildHasher>,

79

    approximate: OxiddSatCountCache<F64, FxBuildHasher>,

80

81

82

impl SatCountCache {

83

    /// Create an empty cache.

84

503

    pub fn new() -> Self {

85

503

        Self::default()

86

503

87

88

89

/// Counts the number of satisfying assignments of `bdd` over `vars` variables.

90

///

91

/// Returns an exact [`SatCount::Exact`] when `vars < 64`, and falls back to

92

/// [`SatCount::Approximate`] otherwise (see [`SatCount`] for the reason).

93

503

pub fn approx_satcount(bdd: &BDDFunction, vars: VarNo, cache: &mut SatCountCache) -> SatCount {

94

503

    if vars < 64 {

95

503

        SatCount::Exact(bdd.sat_count::<u64, FxBuildHasher>(vars, &mut cache.exact))

96

    } else {

97

        SatCount::Approximate(bdd.sat_count::<F64, FxBuildHasher>(vars, &mut cache.approximate).0)

98

99

503

100

101

/// Computes the support (set of variables) of the given BDD function.

102

///

103

/// # Details

104

///

105

/// The `support` is the variables on which the `BDD` is defined, and other

106

/// variables are irrelevant or don't care, formally:

107

///

108

/// > support(f) = { x_i | exists x_0, ..., x_{i-1}, x_{i+1}, ..., x_n : f(x_0, ..., x_{i-1}, true, x_{i+1}, ..., x_n) != f(x_0, ..., x_{i-1}, false, x_{i+1}, ..., x_n) }

109

25

pub fn support(manager_ref: &BDDManagerRef, function: &BDDFunction) -> Result<Vec<VarNo>, OutOfMemory> {

110

25

    let mut result = HashSet::new();

111

25

    manager_ref.with_manager_shared(|manager| {

112

25

        support_edge(manager, function.as_edge(manager).borrowed(), &mut result);

113

25

});

114

25

    Ok(result.into_iter().collect())

115

25

116

117

/// Recursive implementation of [support].

118

351

fn support_edge<'id>(

119

351

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

120

351

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

121

351

    result: &mut HashSet<VarNo>,

122

351

) {

123

351

    match manager.get_node(&function) {

124

188

        Node::Terminal(_) => (),

125

163

        Node::Inner(node) => {

126

163

            result.insert(node.level());

127

163

128

163

            // Recurse into cofactors

129

163

            let (high, low) = collect_children(node);

130

163

            support_edge(manager, low, result);

131

163

            support_edge(manager, high, result);

132

163

133

134

351

135

136

pub type Substitution = [(VarNo, VarNo)];

137

138

/// Specialized substitution function for variables renaming that only works for

139

/// `f[x <- x+1]` renamings.

140

///

141

/// # Details

142

///

143

/// In general substitution is defined as follows,

144

///

145

/// > f[x <- g] = (!g ∧ f[x <- false]) ∨ (g ∧ f[x <- true])

146

///

147

/// but its computation can be fairly expensive. Restricting the substitution to

148

/// only renaming variables from 'x' to 'x+1' allows for a more efficient

149

/// implementation, as follows:

150

///

151

/// > `f[x <- x+1] = (!x+1 ∧ f[x <- false]) ∨ (x+1 ∧ f[x <- true])`

152

/// > `            = make_node(x+1, f[x <- true][x+1 <- true], f[x <- false][x+1 <- false])`

153

///

154

/// This function checks whether the inputs satisfy this restriction and then

155

/// performs the renaming.

156

4659

pub fn variable_rename(

157

4659

    manager_ref: &BDDManagerRef,

158

4659

    function: &BDDFunction,

159

4659

    substitution: &Substitution,

160

4659

) -> Result<BDDFunction, OutOfMemory> {

161

    // Every substitution must be from a lower variable to a higher variable.

162

144805

    for (from, to) in substitution {

163

144805

        debug_assert!(from + 1 == *to, "Variable renaming must be from 'x' to 'x+1'");

164

165

166

4659

    let mut cache = FxHashMap::default();

167

168

4659

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

169

4659

        Ok(BDDFunction::from_edge(

170

4659

            manager,

171

4659

            variable_rename_edge(manager, &mut cache, function.as_edge(manager).borrowed(), substitution)?,

172

))

173

4659

})

174

4659

175

176

/// Implementation of [variable_rename].

177

///

178

/// # Cache key

179

///

180

/// The cache is keyed only on the BDD node (not on the substitution slice)

181

/// because `from < to`: as we traverse top-down, any node at level `L` has

182

/// already consumed all entries with `from < L`, either at the matching

183

/// `from`-level node or via the `level > from` branch.  The remaining

184

/// substitution suffix is therefore uniquely determined by the node's level

185

/// alone, so two paths to the same node always arrive with the same slice.

186

6496320

pub fn variable_rename_edge<'id>(

187

6496320

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

188

6496320

    cache: &mut FxHashMap<BDDFunction, BDDFunction>,

189

6496320

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

190

6496320

    substitution: &Substitution,

191

6496320

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

192

6496320

    let node = match manager.get_node(&function) {

193

2386646

        Node::Terminal(terminal) => return manager.get_terminal(terminal),

194

4109674

        Node::Inner(node) => node,

195

};

196

197

4109674

    if let Some(cached) = cache.get(&BDDFunction::from_edge(manager, manager.clone_edge(&function))) {

198

124996

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

199

3984678

200

201

3984678

    let (from, to) = match substitution.first() {

202

        None => {

203

            // No variables to substitute, so remains identity.

204

75041

            return Ok(manager.clone_edge(&function));

205

206

3909637

        Some((from, to)) => (from, to),

207

};

208

209

3909637

    let result = if node.level() == *from {

210

907715

        let (high, low) = collect_children(node);

211

        // Rename variable from 'from' to 'to'.

212

907715

        let high = EdgeDropGuard::new(manager, variable_rename_edge(manager, cache, high, &substitution[1..])?);

213

907715

        let low = EdgeDropGuard::new(manager, variable_rename_edge(manager, cache, low, &substitution[1..])?);

214

215

907715

        let high_high = match manager.get_node(&high) {

216

187550

            Node::Inner(node) => {

217

187550

                if node.level() == *to {

218

                    // This is f[x <- true][x+1 <- true]

219

48854

                    collect_children(node).0

220

                } else {

221

138696

                    high.borrowed()

222

223

224

720165

            Node::Terminal(_terminal) => high.borrowed(),

225

};

226

227

907715

        let low_low = match manager.get_node(&low) {

228

328202

            Node::Inner(node) => {

229

328202

                if node.level() == *to {

230

                    // There are f[x <- false][x+1 <- false]

231

76834

                    collect_children(node).1

232

                } else {

233

251368

                    low.borrowed()

234

235

236

579513

            Node::Terminal(_terminal) => low.borrowed(),

237

};

238

239

907715

        reduce(

240

907715

            manager,

241

907715

            *to,

242

907715

            manager.clone_edge(&high_high),

243

907715

            manager.clone_edge(&low_low),

244

245

3001922

    } else if node.level() > *from {

246

        // We are past the substitution point, so just continue.

247

1327613

        variable_rename_edge(manager, cache, function.borrowed(), &substitution[1..])

248

    } else {

249

        // node.level() < *from, in this case we keep the variable as is.

250

1674309

        let (high, low) = collect_children(node);

251

1674309

        let high = variable_rename_edge(manager, cache, high, substitution)?;

252

1674309

        let low = variable_rename_edge(manager, cache, low, substitution)?;

253

254

1674309

        reduce(manager, node.level(), high, low)

255

}?;

256

257

3909637

    cache.insert(

258

3909637

        BDDFunction::from_edge(manager, manager.clone_edge(&function)),

259

3909637

        BDDFunction::from_edge(manager, manager.clone_edge(&result)),

260

);

261

262

3909637

    Ok(result)

263

6496320

264

265

/// Specialized substitution function for variables renaming that only works for

266

/// `f[x+1 <- x]` renamings, similar to [variable_rename].

267

///

268

/// # Details

269

///

270

/// We can derive the following:

271

///

272

/// > `f[x+1 <- x] = (!x ∧ f[x+1 <- false]) ∨ (x ∧ f[x+1 <- true])`

273

/// > `            = make_node(x, f[x+1 <- true][x <- true] , f[x+1 <- false][x <- false])`

274

1820

pub fn variable_rename_reverse(

275

1820

    manager_ref: &BDDManagerRef,

276

1820

    function: &BDDFunction,

277

1820

    substitution: &Substitution,

278

1820

) -> Result<BDDFunction, OutOfMemory> {

279

    // Every substitution must be from a higher variable to a lower variable.

280

53777

    for (from, to) in substitution {

281

53777

        debug_assert!(*from == to + 1, "Variable renaming must be from 'x+1' to 'x'");

282

283

284

1820

    let mut cache = FxHashMap::default();

285

286

1820

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

287

1820

        Ok(BDDFunction::from_edge(

288

1820

            manager,

289

1820

            variable_rename_reverse_edge(manager, &mut cache, function.as_edge(manager).borrowed(), substitution)?,

290

))

291

1820

})

292

1820

293

294

/// Implementation of [variable_rename_reverse].

295

///

296

/// # Cache key

297

///

298

/// The cache is keyed on `(BDDFunction, &Substitution)` — the node *and* the

299

/// current substitution slice — because `to < from`: the `to`-level appears

300

/// above the `from`-level in the BDD.  A node at level `> from` can be reached

301

/// via two distinct paths:

302

///

303

/// 1. Through a `to`-level node, which consumes the entry and passes

304

///    `substitution[1..]` to its cofactors.

305

/// 2. Directly from an ancestor above `to` that skips the `to`-level (because

306

///    the function doesn't depend on that variable along that path), which

307

///    preserves the full slice.

308

///

309

/// The same BDD node can therefore be visited with different substitution

310

/// slices, so the slice must be part of the cache key to avoid returning a

311

/// stale result.

312

465245

pub fn variable_rename_reverse_edge<'id, 'a>(

313

465245

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

314

465245

    cache: &mut FxHashMap<(BDDFunction, &'a Substitution), BDDFunction>,

315

465245

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

316

465245

    substitution: &'a Substitution,

317

465245

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

318

465245

    let node = match manager.get_node(&function) {

319

203415

        Node::Terminal(terminal) => return manager.get_terminal(terminal),

320

261830

        Node::Inner(node) => node,

321

};

322

323

261830

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

324

261830

        BDDFunction::from_edge(manager, manager.clone_edge(&function)),

325

261830

        substitution,

326

261830

    )) {

327

27386

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

328

234444

329

330

234444

    let (from, to) = match substitution.first() {

331

        None => {

332

            // No variables to substitute, identity.

333

921

            return Ok(manager.clone_edge(&function));

334

335

233523

        Some((from, to)) => (from, to),

336

};

337

338

233523

    let result = if node.level() == *to {

339

        // Build node at level `to` using cofactors of `from` where present.

340

101362

        let (high, low) = collect_children(node);

341

342

101362

        let high = EdgeDropGuard::new(

343

101362

            manager,

344

101362

            variable_rename_reverse_edge(manager, cache, high, &substitution[1..])?,

345

);

346

101362

        let low = EdgeDropGuard::new(

347

101362

            manager,

348

101362

            variable_rename_reverse_edge(manager, cache, low, &substitution[1..])?,

349

);

350

351

101362

        let high_high = match manager.get_node(&high) {

352

41523

            Node::Inner(node) if node.level() == *from => collect_children(node).0,

353

101322

            _ => high.borrowed(),

354

};

355

101362

        let low_low = match manager.get_node(&low) {

356

74002

            Node::Inner(node) if node.level() == *from => collect_children(node).1,

357

101331

            _ => low.borrowed(),

358

};

359

360

101362

        reduce(

361

101362

            manager,

362

101362

            *to,

363

101362

            manager.clone_edge(&high_high),

364

101362

            manager.clone_edge(&low_low),

365

366

132161

    } else if node.level() == *from {

367

        // `x+1` appears: rename this node to level `to`.

368

128502

        let (high, low) = collect_children(node);

369

128502

        let high = variable_rename_reverse_edge(manager, cache, high, &substitution[1..])?;

370

128502

        let low = variable_rename_reverse_edge(manager, cache, low, &substitution[1..])?;

371

128502

        reduce(manager, *to, high, low)

372

3659

    } else if node.level() > *from {

373

        // Past both `to` and `from`, drop this substitution.

374

3621

        variable_rename_reverse_edge(manager, cache, function.borrowed(), &substitution[1..])

375

    } else {

376

        // Recurse normally, keeping the substitution.

377

38

        let (high, low) = collect_children(node);

378

38

        let high = variable_rename_reverse_edge(manager, cache, high, substitution)?;

379

38

        let low = variable_rename_reverse_edge(manager, cache, low, substitution)?;

380

38

        reduce(manager, node.level(), high, low)

381

}?;

382

383

233523

    cache.insert(

384

233523

385

233523

            BDDFunction::from_edge(manager, manager.clone_edge(&function)),

386

233523

            substitution,

387

233523

),

388

233523

        BDDFunction::from_edge(manager, manager.clone_edge(&result)),

389

);

390

391

233523

    Ok(result)

392

465245

393

394

/// Collect the two children (high, low) of a binary node

395

#[inline]

396

#[must_use]

397

6273300

pub(crate) fn collect_children<E: Edge, N: InnerNode<E>>(node: &N) -> (Borrowed<'_, E>, Borrowed<'_, E>) {

398

6273300

    debug_assert_eq!(N::ARITY, 2);

399

6273300

    let mut it = node.children();

400

6273300

    let f_then = it.next().unwrap();

401

6273300

    let f_else = it.next().unwrap();

402

6273300

    debug_assert!(it.next().is_none());

403

6273300

    (f_then, f_else)

404

6273300

405

406

/// Apply the reduction rules, creating a node in `manager` if necessary

407

#[inline(always)]

408

3830975

pub(crate) fn reduce<'id>(

409

3830975

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

410

3830975

    level: LevelNo,

411

3830975

    t: EdgeOfFunc<'id, BDDFunction>,

412

3830975

    e: EdgeOfFunc<'id, BDDFunction>,

413

3830975

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

414

    // We do not use `DiagramRules::reduce()` here, as the iterator is

415

    // apparently not fully optimized away.

416

3830975

    if t == e {

417

1115950

        manager.drop_edge(e);

418

1115950

        return Ok(t);

419

2715025

420

2715025

    oxidd_core::LevelView::get_or_insert(

421

2715025

        &mut manager.level(level),

422

2715025

        <<BDDFunction as Function>::Manager<'id> as Manager>::InnerNode::new(level, [t, e], ()),

423

424

3830975

425

426

/// Returns the height of the LDD tree.

427

3487

pub fn height(manager: &LDDManagerRef, ldd: &LDDFunction) -> usize {

428

3487

    manager.with_manager_shared(|manager| height_edge(manager, ldd.as_edge(manager).borrowed()))

429

3487

430

431

/// The edge variant of [height].

432

37093

pub fn height_edge<'id>(

433

37093

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

434

37093

    ldd: Borrowed<EdgeOfFunc<'id, LDDFunction>>,

435

37093

) -> usize {

436

37093

    match manager.get_node(&ldd) {

437

3487

        Node::Terminal(_) => 0,

438

33606

        Node::Inner(node) => {

439

            // All right siblings share the same height, so only the down chain

440

            // contributes to the height of the LDD.

441

33606

            let (down, _right) = collect_children(node);

442

33606

            1 + height_edge(manager, down)

443

444

445

37093

446

447

/// Returns true iff the set contains the vector.

448

pub fn element_of(manager: &LDDManagerRef, vector: &[Value], ldd: &LDDFunction) -> bool {

449

    manager.with_manager_shared(|manager| element_of_edge(manager, vector, ldd.as_edge(manager).borrowed()))

450

451

452

fn element_of_edge<'id>(

453

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

454

    vector: &[Value],

455

    ldd: Borrowed<EdgeOfFunc<'id, LDDFunction>>,

456

) -> bool {

457

    match manager.get_node(&ldd) {

458

        Node::Terminal(LDDTerminal::True) => vector.is_empty(),

459

        Node::Terminal(LDDTerminal::Empty) => false,

460

        Node::Inner(node) => {

461

            let value = *node.get_value();

462

            let (down, right) = collect_children(node);

463

            match vector.first() {

464

                None => false,

465

                Some(&first) => match value.cmp(&first) {

466

                    Ordering::Less => element_of_edge(manager, vector, right),

467

                    Ordering::Equal => element_of_edge(manager, &vector[1..], down),

468

                    Ordering::Greater => false,

469

},

470

471

472

473

474

475

#[cfg(test)]

476

mod tests {

477

    use merc_utilities::random_test;

478

    use oxidd::BooleanFunction;

479

    use oxidd::FunctionSubst;

480

    use oxidd::Manager;

481

    use oxidd::ManagerRef;

482

    use oxidd::Subst;

483

    use oxidd::bdd::BDDFunction;

484

    use oxidd::util::AllocResult;

485

486

    use crate::FormatConfigSet;

487

    use crate::compute_vars_bdd;

488

    use crate::random_bdd;

489

    use crate::support;

490

    use crate::variable_rename;

491

    use crate::variable_rename_reverse;

492

493

    #[test]

494

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

495

1

    fn test_bdd_variable_rename() {

496

1

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

497

498

1

        let vars: Vec<BDDFunction> = manager_ref

499

1

            .with_manager_exclusive(|manager| {

500

3

                AllocResult::from_iter(manager.add_vars(3).map(|i| BDDFunction::var(manager, i)))

501

1

})

502

1

            .unwrap();

503

504

1

        let res = vars[0].and(&vars[1]).unwrap().or(&vars[2]).unwrap();

505

1

        let subst = variable_rename(&manager_ref, &res, &[(0, 1), (1, 2)]).unwrap();

506

1

        assert!(subst.satisfiable());

507

1

508

509

    #[test]

510

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

511

1

    fn test_random_bdd_support() {

512

25

        random_test(25, |rng| {

513

25

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

514

515

25

            let vars = manager_ref

516

25

                .with_manager_exclusive(|manager| {

517

25

                    manager

518

25

                        .add_vars(4)

519

100

                        .map(|v| BDDFunction::var(manager, v))

520

25

                        .collect::<Result<Vec<BDDFunction>, _>>()

521

25

})

522

25

                .unwrap();

523

524

25

            let function = random_bdd(&manager_ref, rng, &vars, 8).unwrap();

525

25

            let _support = support(&manager_ref, &function).unwrap();

526

527

            // TODO: Verify support correctness

528

25

});

529

1

530

531

    #[test]

532

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

533

1

    fn test_random_bdd_renaming() {

534

25

        random_test(25, |rng| {

535

25

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

536

537

25

            let vars = manager_ref

538

25

                .with_manager_exclusive(|manager| {

539

25

                    manager

540

25

                        .add_vars(4)

541

100

                        .map(|v| BDDFunction::var(manager, v))

542

25

                        .collect::<Result<Vec<BDDFunction>, _>>()

543

25

})

544

25

                .unwrap();

545

546

25

            let function = random_bdd(&manager_ref, rng, &vars, 8).unwrap();

547

548

25

            let to = compute_vars_bdd(&manager_ref, &[1, 3]).unwrap().0;

549

25

            let substitution = Subst::new(&[0, 2], &to);

550

25

            println!("input: {}", FormatConfigSet(&function));

551

552

25

            let expected = function.substitute(&substitution).unwrap();

553

25

            let renamed = variable_rename(&manager_ref, &function, &[(0, 1), (2, 3)]).unwrap();

554

555

25

            println!("expected: {}", FormatConfigSet(&expected));

556

25

            println!("result: {}", FormatConfigSet(&renamed));

557

558

25

            assert!(expected == renamed, "Renaming did not match expected substitution");

559

25

});

560

1

561

562

    #[test]

563

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

564

1

    fn test_random_bdd_renaming_reverse() {

565

25

        random_test(25, |rng| {

566

25

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

567

568

25

            let vars = manager_ref

569

25

                .with_manager_exclusive(|manager| {

570

25

                    manager

571

25

                        .add_vars(4)

572

100

                        .map(|v| BDDFunction::var(manager, v))

573

25

                        .collect::<Result<Vec<BDDFunction>, _>>()

574

25

})

575

25

                .unwrap();

576

577

25

            let function = random_bdd(&manager_ref, rng, &vars, 8).unwrap();

578

579

25

            let to = compute_vars_bdd(&manager_ref, &[0, 2]).unwrap().0;

580

25

            let substitution = Subst::new(&[1, 3], &to);

581

25

            println!("input: {}", FormatConfigSet(&function));

582

583

25

            let expected = function.substitute(&substitution).unwrap();

584

25

            let renamed = variable_rename_reverse(&manager_ref, &function, &[(1, 0), (3, 2)]).unwrap();

585

586

25

            println!("expected: {}", FormatConfigSet(&expected));

587

25

            println!("renamed: {}", FormatConfigSet(&renamed));

588

589

25

            assert!(

590

25

                expected == renamed,

591

                "Renaming with reverse did not match expected substitution"

592

);

593

25

});

594

1

595