Grcov report - util.rs

1

use std::collections::HashSet;

2

3

use oxidd::Edge;

4

use oxidd::Function;

5

use oxidd::HasLevel;

6

use oxidd::InnerNode;

7

use oxidd::LevelNo;

8

use oxidd::Manager;

9

use oxidd::ManagerRef;

10

use oxidd::Node;

11

use oxidd::VarNo;

12

use oxidd::bdd::BDDFunction;

13

use oxidd::bdd::BDDManagerRef;

14

use oxidd::util::Borrowed;

15

use oxidd::util::OutOfMemory;

16

use oxidd_core::function::EdgeOfFunc;

17

use oxidd_core::util::EdgeDropGuard;

18

use rustc_hash::FxHashMap;

19

20

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

21

pub type BDDSupport = BDDFunction;

22

23

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

24

///

25

/// # Details

26

///

27

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

28

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

29

///

30

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

31

25

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

32

25

    let mut result = HashSet::new();

33

25

    manager_ref.with_manager_shared(|manager| {

34

25

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

35

25

});

36

25

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

37

25

38

39

/// Recursive implementation of [support].

40

321

fn support_edge<'id>(

41

321

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

42

321

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

43

321

    result: &mut HashSet<VarNo>,

44

321

) {

45

321

    match manager.get_node(&function) {

46

173

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

47

148

        Node::Inner(node) => {

48

148

            result.insert(node.level());

49

148

50

148

            // Recurse into cofactors

51

148

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

52

148

            support_edge(manager, low, result);

53

148

            support_edge(manager, high, result);

54

148

55

56

321

57

58

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

59

60

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

61

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

62

///

63

/// # Details

64

///

65

/// In general substitution is defined as follows,

66

///

67

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

68

///

69

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

70

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

71

/// implementation, as follows:

72

///

73

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

74

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

75

///

76

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

77

/// performs the renaming.

78

3326

pub fn variable_rename(

79

3326

    manager_ref: &BDDManagerRef,

80

3326

    function: &BDDFunction,

81

3326

    substitution: &Substitution,

82

3326

) -> Result<BDDFunction, OutOfMemory> {

83

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

84

99052

    for (from, to) in substitution {

85

99052

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

86

87

88

3326

    let mut cache = FxHashMap::default();

89

90

3326

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

91

3326

        Ok(BDDFunction::from_edge(

92

3326

            manager,

93

3326

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

94

))

95

3326

})

96

3326

97

98

/// Implementation of [variable_rename].

99

14425690

pub fn variable_rename_edge<'id>(

100

14425690

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

101

14425690

    cache: &mut FxHashMap<BDDFunction, BDDFunction>,

102

14425690

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

103

14425690

    substitution: &Substitution,

104

14425690

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

105

14425690

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

106

6044601

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

107

8381089

        Node::Inner(node) => node,

108

};

109

110

8381089

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

111

311148

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

112

8069941

113

114

8069941

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

115

        None => {

116

            // No variables to substitute, so remains identity.

117

15951

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

118

119

8053990

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

120

};

121

122

8053990

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

123

2608383

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

124

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

125

2608383

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

126

2608383

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

127

128

2608383

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

129

251637

            Node::Inner(node) => {

130

251637

                if node.level() == *to {

131

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

132

82621

                    collect_children(node).0

133

                } else {

134

169016

                    high.borrowed()

135

136

137

2356746

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

138

};

139

140

2608383

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

141

450107

            Node::Inner(node) => {

142

450107

                if node.level() == *to {

143

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

144

135660

                    collect_children(node).1

145

                } else {

146

314447

                    low.borrowed()

147

148

149

2158276

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

150

};

151

152

2608383

        reduce(

153

2608383

            manager,

154

2608383

            *to,

155

2608383

            manager.clone_edge(&high_high),

156

2608383

            manager.clone_edge(&low_low),

157

158

5445607

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

159

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

160

1685616

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

161

    } else {

162

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

163

3759991

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

164

3759991

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

165

3759991

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

166

167

3759991

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

168

}?;

169

170

8053990

    cache.insert(

171

8053990

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

172

8053990

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

173

);

174

175

8053990

    Ok(result)

176

14425690

177

178

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

179

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

180

///

181

/// # Details

182

///

183

/// We can derive the following:

184

///

185

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

186

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

187

1930

pub fn variable_rename_reverse(

188

1930

    manager_ref: &BDDManagerRef,

189

1930

    function: &BDDFunction,

190

1930

    substitution: &Substitution

191

1930

) -> Result<BDDFunction, OutOfMemory> {

192

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

193

57200

    for (from, to) in substitution {

194

57200

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

195

196

197

1930

    let mut cache = FxHashMap::default();

198

199

1930

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

200

1930

        Ok(BDDFunction::from_edge(

201

1930

            manager,

202

1930

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

203

))

204

1930

})

205

1930

206

207

/// Implementation of [variable_rename].

208

442029

pub fn variable_rename_reverse_edge<'id, 'a>(

209

442029

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

210

442029

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

211

442029

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

212

442029

    substitution: &'a Substitution,

213

442029

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

214

442029

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

215

194921

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

216

247108

        Node::Inner(node) => node,

217

};

218

219

247108

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

220

247108

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

221

247108

        substitution,

222

247108

    )) {

223

25135

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

224

221973

225

226

221973

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

227

        None => {

228

            // No variables to substitute, identity.

229

51

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

230

231

221922

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

232

};

233

234

221922

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

235

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

236

125469

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

237

238

125469

        let high = EdgeDropGuard::new(

239

125469

            manager,

240

125469

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

241

);

242

125469

        let low = EdgeDropGuard::new(

243

125469

            manager,

244

125469

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

245

);

246

247

125469

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

248

49462

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

249

125430

            _ => high.borrowed(),

250

};

251

125469

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

252

92645

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

253

125430

            _ => low.borrowed(),

254

};

255

256

125469

        reduce(

257

125469

            manager,

258

125469

            *to,

259

125469

            manager.clone_edge(&high_high),

260

125469

            manager.clone_edge(&low_low),

261

262

96453

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

263

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

264

92672

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

265

92672

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

266

92672

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

267

92672

        reduce(manager, *to, high, low)

268

3781

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

269

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

270

3745

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

271

    } else {

272

        // Recurse normally, keeping the substitution.

273

36

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

274

36

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

275

36

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

276

36

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

277

}?;

278

279

221922

    cache.insert(

280

221922

281

221922

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

282

221922

            substitution,

283

221922

),

284

221922

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

285

);

286

287

221922

    Ok(result)

288

442029

289

290

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

291

#[inline]

292

#[must_use]

293

7915933

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

294

7915933

    debug_assert_eq!(N::ARITY, 2);

295

7915933

    let mut it = node.children();

296

7915933

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

297

7915933

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

298

7915933

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

299

7915933

    (f_then, f_else)

300

7915933

301

302

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

303

#[inline(always)]

304

7491835

pub(crate) fn reduce<'id>(

305

7491835

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

306

7491835

    level: LevelNo,

307

7491835

    t: EdgeOfFunc<'id, BDDFunction>,

308

7491835

    e: EdgeOfFunc<'id, BDDFunction>,

309

7491835

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

310

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

311

    // apparently not fully optimized away.

312

7491835

    if t == e {

313

5103942

        manager.drop_edge(e);

314

5103942

        return Ok(t);

315

2387893

316

2387893

    oxidd_core::LevelView::get_or_insert(

317

2387893

        &mut manager.level(level),

318

2387893

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

319

320

7491835

321

322

#[cfg(test)]

323

mod tests {

324

    use merc_utilities::random_test;

325

    use oxidd::BooleanFunction;

326

    use oxidd::FunctionSubst;

327

    use oxidd::Manager;

328

    use oxidd::ManagerRef;

329

    use oxidd::Subst;

330

    use oxidd::bdd::BDDFunction;

331

    use oxidd::util::AllocResult;

332

333

    use crate::FormatConfigSet;

334

    use crate::compute_vars_bdd;

335

    use crate::random_bdd;

336

    use crate::support;

337

    use crate::variable_rename;

338

    use crate::variable_rename_reverse;

339

340

    #[test]

341

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

342

1

    fn test_bdd_variable_rename() {

343

1

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

344

345

1

        let vars: Vec<BDDFunction> = manager_ref

346

1

            .with_manager_exclusive(|manager| {

347

3

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

348

1

})

349

1

            .unwrap();

350

351

1

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

352

1

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

353

1

        assert!(subst.satisfiable());

354

1

355

356

    #[test]

357

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

358

1

    fn test_random_bdd_support() {

359

25

        random_test(25, |rng| {

360

25

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

361

362

25

            let vars = manager_ref

363

25

                .with_manager_exclusive(|manager| {

364

25

                    manager

365

25

                        .add_vars(4)

366

100

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

367

25

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

368

25

})

369

25

                .unwrap();

370

371

25

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

372

25

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

373

374

            // TODO: Verify support correctness

375

25

});

376

1

377

378

    #[test]

379

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

380

1

    fn test_random_bdd_renaming() {

381

25

        random_test(25, |rng| {

382

25

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

383

384

25

            let vars = manager_ref

385

25

                .with_manager_exclusive(|manager| {

386

25

                    manager

387

25

                        .add_vars(4)

388

100

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

389

25

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

390

25

})

391

25

                .unwrap();

392

393

25

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

394

395

25

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

396

25

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

397

25

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

398

399

25

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

400

25

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

401

402

25

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

403

25

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

404

405

25

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

406

25

});

407

1

408

409

    #[test]

410

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

411

1

    fn test_random_bdd_renaming_reverse() {

412

25

        random_test(25, |rng| {

413

25

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

414

415

25

            let vars = manager_ref

416

25

                .with_manager_exclusive(|manager| {

417

25

                    manager

418

25

                        .add_vars(4)

419

100

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

420

25

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

421

25

})

422

25

                .unwrap();

423

424

25

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

425

426

25

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

427

25

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

428

25

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

429

430

25

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

431

25

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

432

433

25

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

434

25

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

435

436

25

            assert!(

437

25

                expected == renamed,

438

                "Renaming with reverse did not match expected substitution"

439

);

440

25

});

441

1

442