Grcov report - rewriter

1

//! Common utilities and types for rewriters.

2

use super::{

3

    RuleEffect,

4

    expression_zipper::expression_ctx,

5

    resolve_rules::{ResolveRulesError, RuleData},

6

};

7

use crate::ast::{

8

    DeclarationPtr, Expression, Model, Name, SymbolTable,

9

    pretty::{pretty_value_letting_declaration, pretty_variable_declaration, pretty_vec},

10

};

11

use crate::settings::{

12

    Heuristic, default_rule_trace_enabled, heuristic, next_heuristic_all_index,

13

    next_heuristic_interactive_index, next_heuristic_random_index, rule_trace_aggregates_enabled,

14

    rule_trace_enabled,

15

};

16

17

use itertools::Itertools;

18

use std::collections::BTreeMap;

19

use std::fmt::Debug;

20

use std::sync::Arc;

21

use thiserror::Error;

22

use tracing::{debug, trace};

23

24

#[derive(Debug, Clone)]

25

pub struct RuleResult<'a> {

26

    pub rule_data: RuleData<'a>,

27

    pub effect: RuleEffect,

28

29

30

#[derive(Clone, Copy, Debug)]

31

pub(crate) enum RuleAttemptStatus {

32

    Success,

33

    Failure,

34

35

36

impl RuleAttemptStatus {

37

6339252

    pub(crate) fn as_str(self) -> &'static str {

38

6339252

        match self {

39

115964

            Self::Success => "success",

40

6223288

            Self::Failure => "fail",

41

42

6339252

43

44

45

pub(crate) trait RuleAttemptObserver {

46

    fn attempted(

47

        &mut self,

48

        priority: u16,

49

        rule: &RuleData<'_>,

50

        expression: &Expression,

51

        status: RuleAttemptStatus,

52

);

53

54

55

/// Observer used when rule-attempt tracing is disabled.

56

///

57

/// Rewrite loops are generic over their observer, so this empty implementation is inlined and

58

/// removed from the monomorphised hot path: disabled tracing performs no per-attempt dispatch,

59

/// formatting, allocation, or enabled-level check.

60

pub(crate) struct NoopObserver;

61

62

impl RuleAttemptObserver for NoopObserver {

63

    #[inline(always)]

64

2681352528

    fn attempted(

65

2681352528

        &mut self,

66

2681352528

        _priority: u16,

67

2681352528

        _rule: &RuleData<'_>,

68

2681352528

        _expression: &Expression,

69

2681352528

        _status: RuleAttemptStatus,

70

2681352528

) {

71

2681352528

72

73

74

1076947

fn expression_ast_depth(expression: &Expression) -> usize {

75

1076947

    let mut child_depth = 0;

76

1076947

    expression.for_each_expr_child(&mut |child| {

77

1071261

        child_depth = child_depth.max(expression_ast_depth(child));

78

1071261

});

79

1076947

    1 + child_depth

80

1076947

81

82

5686

fn effect_ast_depth(effect: &RuleEffect) -> usize {

83

5686

    std::iter::once(&effect.new_expression)

84

5686

        .chain(effect.new_top.iter())

85

5686

        .map(expression_ast_depth)

86

5686

        .max()

87

5686

        .unwrap_or(0)

88

5686

89

90

5686

fn rule_result_compact_depth(result: &RuleResult<'_>) -> usize {

91

    // Deferred effects deliberately cannot be materialised speculatively. Prefer a concrete

92

    // effect when compactness can actually be measured.

93

5686

    if result.effect.is_deferred() {

94

        usize::MAX

95

    } else {

96

5686

        effect_ast_depth(&result.effect)

97

98

5686

99

100

/// Chooses between rules applicable at the same priority and focus.

101

64704825

pub(crate) fn choose_rule_result_index<'a, 'b>(

102

64704825

    results: impl ExactSizeIterator<Item = &'b RuleResult<'a>>,

103

64704825

) -> usize

104

64704825

where

105

64704825

    'a: 'b,

106

107

64704825

    let results: Vec<_> = results.collect();

108

    debug_assert!(!results.is_empty());

109

64704825

    if results.len() == 1 {

110

64700356

        return 0;

111

4469

112

4469

    match heuristic() {

113

        Heuristic::First => 0,

114

        Heuristic::Random => next_heuristic_random_index(results.len()),

115

2843

        Heuristic::Compact => results

116

2843

            .iter()

117

2843

            .enumerate()

118

2843

            .min_by(|(_, left), (_, right)| {

119

2843

                rule_result_compact_depth(left)

120

2843

                    .cmp(&rule_result_compact_depth(right))

121

                    .then_with(|| left.rule_data.rule.name.cmp(right.rule_data.rule.name))

122

2843

})

123

            .map(|(index, _)| index)

124

2843

            .unwrap_or(0),

125

        Heuristic::Interactive => {

126

1

            let names: Vec<_> = results

127

1

                .iter()

128

2

                .map(|result| result.rule_data.rule.name)

129

                .collect();

130

1

            next_heuristic_interactive_index(&names)

131

132

        Heuristic::All => {

133

1625

            let names: Vec<_> = results

134

1625

                .iter()

135

3250

                .map(|result| result.rule_data.rule.name)

136

                .collect();

137

1625

            next_heuristic_all_index(&names)

138

139

140

64704825

141

142

pub type VariableDeclarationSnapshot = BTreeMap<Name, String>;

143

144

/// Pretty-prints every local variable declaration for rule-trace before/after diffs.

145

///

146

/// This is intentionally expensive (string formatting of domains). Callers must only invoke it

147

/// when the default human-readable rule trace needs declaration diffs.

148

82013

pub fn snapshot_variable_declarations(symbols: &SymbolTable) -> VariableDeclarationSnapshot {

149

82013

    symbols

150

82013

        .clone()

151

82013

        .into_iter_local()

152

1336542

        .filter_map(|(name, _)| {

153

1336542

            pretty_variable_declaration(symbols, &name).map(|declaration| (name, declaration))

154

1336542

})

155

        .collect()

156

82013

157

158

/// Captures a Root declaration snapshot only when the default rule-trace sink is enabled.

159

///

160

/// Failed rule attempts and aggregate/verbose-only tracing must not pay for pretty-printing.

161

/// The effect has not been applied yet, so a post-success call is still a valid "before" snapshot.

162

64709291

pub fn root_variable_snapshot_for_default_trace(

163

64709291

    expr: &Expression,

164

64709291

    symbols: &SymbolTable,

165

64709291

) -> Option<VariableDeclarationSnapshot> {

166

64709291

    if !matches!(expr, Expression::Root(_, _)) {

167

50201373

        return None;

168

14507918

169

14507918

    if !(rule_trace_enabled() && default_rule_trace_enabled()) {

170

14466912

        return None;

171

41006

172

41006

    Some(snapshot_variable_declarations(symbols))

173

64709291

174

175

/// Snapshots variable declarations after applying a rule's symbol-table changes.

176

41006

pub fn snapshot_symbols_after_effect(

177

41006

    symbols: &SymbolTable,

178

41006

    effect: &RuleEffect,

179

41006

) -> VariableDeclarationSnapshot {

180

41006

    let mut merged = symbols.clone();

181

41006

    effect.preview_declaration_updates(&mut merged);

182

41006

    merged.extend(effect.symbols.clone());

183

41006

    snapshot_variable_declarations(&merged)

184

41006

185

186

/// Logs, to the main log, and the human readable traces used by the exhaustive tester, that the

187

/// rule has been applied to the expression

188

64704822

pub fn log_rule_application(

189

64704822

    result: &RuleResult,

190

64704822

    initial_expression: &Expression,

191

64704822

    initial_symbols: &SymbolTable,

192

64704822

    variable_declaration_snapshots: Option<(

193

64704822

        &VariableDeclarationSnapshot,

194

64704822

        &VariableDeclarationSnapshot,

195

64704822

)>,

196

64704822

) {

197

64704822

    let red = &result.effect;

198

64704822

    let rule = result.rule_data.rule;

199

200

64704822

    if tracing::enabled!(target: "conjure::rule_application", tracing::Level::DEBUG) {

201

        // A reduction can only modify either constraints or clauses, not both. So the same

202

        // field can represent both (or be empty if neither changed).

203

115732

        let new_top = if !red.new_top.is_empty() {

204

828

            pretty_vec(&red.new_top)

205

        } else {

206

114904

            pretty_vec(&red.new_sat_decisions)

207

};

208

209

        debug!(

210

            target: "conjure::rule_application",

211

115732

            rule = rule.name,

212

115732

            rule_sets = ?rule.rule_sets,

213

115732

            before = %initial_expression,

214

115732

            after = %red.new_expression,

215

            %new_top,

216

115732

            "applied rule"

217

);

218

64589090

219

220

64704822

    if rule_trace_enabled() && default_rule_trace_enabled() {

221

802258

        let new_constraints_str = if !red.new_top.is_empty() {

222

40603

            let mut exprs: Vec<String> = vec![];

223

40603

            for expr in &red.new_top {

224

70491

                exprs.push(format!("  {expr}"));

225

226

40603

            let exprs = exprs.iter().join("\n");

227

40603

            format!("new constraints:\n{exprs}\n")

228

761655

        } else if !red.new_sat_decisions.is_empty() {

229

27898

            let mut exprs: Vec<String> = vec![];

230

27898

            for clause in &red.new_sat_decisions {

231

30943

                exprs.push(format!("  {clause}"));

232

233

27898

            let exprs = exprs.iter().join("\n");

234

27898

            format!("new SAT encoding decisions:\n{exprs}\n")

235

        } else {

236

733757

            String::new()

237

};

238

239

        let (new_variables_str, updated_variables_str) =

240

802258

            if let Some((before, after)) = variable_declaration_snapshots {

241

41005

                let mut new_variables = Vec::new();

242

41005

                let mut updated_variables = Vec::new();

243

244

41005

                for (name, declaration_after) in after {

245

660108

                    match before.get(name) {

246

63755

                        None => new_variables.push(format!("  {declaration_after}")),

247

596353

                        Some(declaration_before) if declaration_before != declaration_after => {

248

377

                            updated_variables

249

377

                                .push(format!("  {declaration_before} ~~> {declaration_after}"));

250

251

595976

                        _ => {}

252

253

254

255

41005

                let new_variables_str = if new_variables.is_empty() {

256

15954

                    String::new()

257

                } else {

258

25051

                    format!("new variables:\n{}\n", new_variables.join("\n"))

259

};

260

261

41005

                let updated_variables_str = if updated_variables.is_empty() {

262

40715

                    String::new()

263

                } else {

264

290

                    format!("\nupdated variables:\n{}\n", updated_variables.join("\n"))

265

};

266

267

41005

                (new_variables_str, updated_variables_str)

268

            } else {

269

                // empty if no new variables

270

761253

                let mut vars: Vec<String> = vec![];

271

761253

                for var_name in red.added_symbols(initial_symbols) {

272

                    // Representing a constant introduces value lettings rather than decision

273

                    // variables, so a rule can add either kind. A trace is diagnostic output, so

274

                    // anything neither renderer knows is skipped rather than brought down.

275

146678

                    if let Some(declaration) = pretty_variable_declaration(&red.symbols, &var_name)

276

957

                        .or_else(|| pretty_value_letting_declaration(&red.symbols, &var_name))

277

278

146678

                        vars.push(format!("  {declaration}"));

279

280

281

761253

                let new_variables_str = if vars.is_empty() {

282

671727

                    String::new()

283

                } else {

284

89526

                    format!("new variables:\n{}\n", vars.join("\n"))

285

};

286

761253

                (new_variables_str, String::new())

287

};

288

289

802258

        trace!(

290

            target: "rule_engine_rule_trace",

291

            "{}\n   ~~> {} ({:?})\n{}\n{}{}{}\n--\n",

292

802258

            initial_expression,

293

802258

            rule.name,

294

802258

            rule.rule_sets,

295

802258

            red.new_expression,

296

802258

            new_variables_str,

297

802258

            updated_variables_str,

298

802258

            new_constraints_str

299

);

300

63902564

301

302

64704822

    if rule_trace_enabled() && rule_trace_aggregates_enabled() {

303

55075889

        trace!(

304

            target: "rule_engine_rule_trace_aggregates",

305

55075889

            rule_name = rule.name,

306

55075889

            "Applied rule"

307

);

308

9628933

309

64704822

310

311

type LettingCtxFn = Arc<dyn Fn(Expression) -> Expression>;

312

type ApplicableLettingRule<'a> = (

313

    RuleResult<'a>,

314

    u16,

315

    Expression,

316

    DeclarationPtr,

317

    LettingCtxFn,

318

);

319

320

107

pub(crate) fn try_rewrite_value_letting_once<O: RuleAttemptObserver>(

321

107

    model: &mut Model,

322

107

    rules_grouped: &Vec<(u16, Vec<RuleData<'_>>)>,

323

107

    observer: &mut O,

324

107

) -> Option<Name> {

325

107

    let symbols = model.symbols();

326

107

    let mut results: Vec<ApplicableLettingRule<'_>> = vec![];

327

328

107

    'top: for (priority, rules) in rules_grouped.iter() {

329

5800

        for (_, decl) in symbols.iter_local() {

330

35032

            let Some(letting_expr) = decl.as_value_letting().map(|expr| expr.clone()) else {

331

33640

                continue;

332

};

333

334

1392

            for (expr, ctx) in expression_ctx(letting_expr) {

335

1392

                let expr = expr.clone();

336

1392

                let ctx = ctx.clone();

337

338

1392

                for rd in rules {

339

6432

                    match rd.rule.apply(&expr, &symbols) {

340

                        Ok(effect) => {

341

                            observer.attempted(*priority, rd, &expr, RuleAttemptStatus::Success);

342

                            results.push((

343

                                RuleResult {

344

                                    rule_data: rd.clone(),

345

                                    effect,

346

},

347

                                *priority,

348

                                expr.clone(),

349

                                decl.clone(),

350

                                ctx.clone(),

351

));

352

353

                        Err(_) => {

354

6432

                            observer.attempted(*priority, rd, &expr, RuleAttemptStatus::Failure)

355

356

357

358

359

1392

                if !results.is_empty() {

360

                    break 'top;

361

1392

362

363

364

365

366

107

    if results.is_empty() {

367

107

        return None;

368

369

    let selected = choose_rule_result_index(results.iter().map(|(result, ..)| result));

370

    let (result, _, expr, decl, ctx) = results.swap_remove(selected);

371

372

    let effect = result.effect.materialise(&symbols);

373

    let result = RuleResult {

374

        rule_data: result.rule_data,

375

        effect,

376

};

377

378

    log_rule_application(&result, &expr, &symbols, None);

379

380

    let rewritten_expr = ctx(result.effect.new_expression.clone());

381

    drop(symbols);

382

    result.effect.apply(model);

383

384

    let mut decl = decl;

385

    *decl

386

        .as_value_letting_mut()

387

        .expect("declaration should still be a value letting") = rewritten_expr;

388

389

    model.symbols_mut().refresh_local_binding_hashes();

390

391

    Some(decl.name().clone())

392

107

393

394

/// Represents errors that can occur during the model rewriting process.

395

#[derive(Debug, Error)]

396

pub enum RewriteError {

397

    #[error("{0}")]

398

    UniformRepresentation(String),

399

    #[error("Error resolving rules {0}")]

400

    ResolveRulesError(ResolveRulesError),

401

402

403

impl From<ResolveRulesError> for RewriteError {

404

    fn from(error: ResolveRulesError) -> Self {

405

        RewriteError::ResolveRulesError(error)

406

407

408

409

#[cfg(test)]

410

mod tests {

411

    use super::*;

412

    use crate::ast::{Literal, Metadata, Moo};

413

    use crate::rule_engine::{ApplicationError, Rule, RuleSet};

414

    use crate::settings::{

415

        Heuristic, begin_heuristic_all_choices, heuristic, heuristic_all_choices,

416

        set_default_rule_trace_enabled, set_heuristic, set_heuristic_responses,

417

        set_rule_trace_enabled,

418

};

419

420

    fn test_rule_set_applies(_: &crate::settings::SolverFamily) -> bool {

421

        true

422

423

424

    fn never_apply(_: &Expression, _: &SymbolTable) -> Result<RuleEffect, ApplicationError> {

425

        Err(ApplicationError::RuleNotApplicable)

426

427

428

    static TEST_RULE_SET: RuleSet<'static> =

429

        RuleSet::new("heuristic-test", &[], test_rule_set_applies);

430

    static FIRST_RULE: Rule<'static> =

431

        Rule::new("first-rule", never_apply, &[("heuristic-test", 1)]);

432

    static SECOND_RULE: Rule<'static> =

433

        Rule::new("second-rule", never_apply, &[("heuristic-test", 1)]);

434

435

6

    fn heuristic_result(

436

6

        rule: &'static Rule<'static>,

437

6

        expression: Expression,

438

6

    ) -> RuleResult<'static> {

439

6

        RuleResult {

440

6

            rule_data: RuleData {

441

6

                rule,

442

6

                priority: 1,

443

6

                rule_set: &TEST_RULE_SET,

444

6

},

445

6

            effect: RuleEffect::pure(expression),

446

6

447

6

448

449

    struct HeuristicGuard(Heuristic);

450

451

    impl HeuristicGuard {

452

3

        fn set(value: Heuristic) -> Self {

453

3

            let guard = Self(heuristic());

454

3

            set_heuristic(value);

455

3

            guard

456

3

457

458

459

    impl Drop for HeuristicGuard {

460

3

        fn drop(&mut self) {

461

3

            set_heuristic(self.0);

462

3

463

464

465

    /// Restores process-local rule-trace flags after a test mutates them.

466

    struct RuleTraceFlagGuard {

467

        rule_trace: bool,

468

        default_rule_trace: bool,

469

470

471

    impl RuleTraceFlagGuard {

472

        /// Saves the current flags and applies `rule_trace` / `default_rule_trace`.

473

2

        fn set(rule_trace: bool, default_rule_trace: bool) -> Self {

474

2

            let guard = Self {

475

2

                rule_trace: rule_trace_enabled(),

476

2

                default_rule_trace: default_rule_trace_enabled(),

477

2

};

478

2

            set_rule_trace_enabled(rule_trace);

479

2

            set_default_rule_trace_enabled(default_rule_trace);

480

2

            guard

481

2

482

483

484

    impl Drop for RuleTraceFlagGuard {

485

2

        fn drop(&mut self) {

486

2

            set_rule_trace_enabled(self.rule_trace);

487

2

            set_default_rule_trace_enabled(self.default_rule_trace);

488

2

489

490

491

    #[test]

492

1

    fn root_snapshot_skipped_when_default_rule_trace_disabled() {

493

1

        let _guard = RuleTraceFlagGuard::set(true, false);

494

1

        let root = Expression::Root(Metadata::new(), vec![Literal::Bool(true).into()]);

495

1

        let symbols = SymbolTable::new();

496

1

        assert!(root_variable_snapshot_for_default_trace(&root, &symbols).is_none());

497

1

498

499

    #[test]

500

1

    fn root_snapshot_taken_only_for_root_when_default_rule_trace_enabled() {

501

1

        let _guard = RuleTraceFlagGuard::set(true, true);

502

1

        let root = Expression::Root(Metadata::new(), vec![Literal::Bool(true).into()]);

503

1

        let leaf: Expression = Literal::Bool(true).into();

504

1

        let symbols = SymbolTable::new();

505

1

        assert!(root_variable_snapshot_for_default_trace(&root, &symbols).is_some());

506

1

        assert!(root_variable_snapshot_for_default_trace(&leaf, &symbols).is_none());

507

1

508

509

    #[test]

510

1

    fn compact_heuristic_chooses_shallower_rule_effect() {

511

1

        let _guard = HeuristicGuard::set(Heuristic::Compact);

512

1

        let leaf: Expression = Literal::Bool(true).into();

513

1

        let deep = Expression::Not(Metadata::new(), Moo::new(leaf.clone()));

514

1

        let results = [

515

1

            heuristic_result(&FIRST_RULE, deep),

516

1

            heuristic_result(&SECOND_RULE, leaf),

517

1

];

518

1

        assert_eq!(choose_rule_result_index(results.iter()), 1);

519

1

520

521

    #[test]

522

1

    fn all_heuristic_records_equally_applicable_rules() {

523

1

        let _guard = HeuristicGuard::set(Heuristic::All);

524

1

        begin_heuristic_all_choices(vec![1]);

525

1

        let results = [

526

1

            heuristic_result(&FIRST_RULE, Literal::Bool(true).into()),

527

1

            heuristic_result(&SECOND_RULE, Literal::Bool(false).into()),

528

1

];

529

1

        assert_eq!(choose_rule_result_index(results.iter()), 1);

530

1

        assert_eq!(

531

1

            heuristic_all_choices()[0].options,

532

1

            vec!["first-rule".to_string(), "second-rule".to_string()]

533

);

534

1

535

536

    #[test]

537

1

    fn interactive_heuristic_uses_one_based_responses() {

538

1

        let _guard = HeuristicGuard::set(Heuristic::Interactive);

539

1

        set_heuristic_responses(vec![2]);

540

1

        let results = [

541

1

            heuristic_result(&FIRST_RULE, Literal::Bool(true).into()),

542

1

            heuristic_result(&SECOND_RULE, Literal::Bool(false).into()),

543

1

];

544

1

        assert_eq!(choose_rule_result_index(results.iter()), 1);

545

1

546