Grcov report - exhaustive

1

#![allow(clippy::expect_used)]

2

use git_version as _;

3

4

use conjure_cp::defaults::DEFAULT_RULE_SETS;

5

use conjure_cp::parse::tree_sitter::parse_essence_file_native;

6

use conjure_cp::rule_engine::rewrite_model;

7

use conjure_cp::solver::Solver;

8

use conjure_cp::solver::adaptors::*;

9

use conjure_cp_cli::utils::testing::{

10

    DEFAULT_TEXT_SNAPSHOT_CHARACTER_LIMIT, normalize_solutions_for_comparison,

11

    read_default_rule_trace, truncate_to_first_chars,

12

};

13

use serde_json::Value as JsonValue;

14

use std::collections::{BTreeMap, BTreeSet};

15

use std::error::Error;

16

use std::fs;

17

use std::fs::File;

18

use std::io::Read;

19

use std::path::Path;

20

use std::process::{Child, Command, Stdio};

21

use std::time::{Duration, Instant};

22

use tracing_subscriber::{Layer, filter::EnvFilter, filter::FilterFn, fmt, layer::SubscriberExt};

23

24

#[cfg(unix)]

25

use std::os::unix::process::CommandExt;

26

use std::sync::Arc;

27

use std::sync::RwLock;

28

29

use conjure_cp::ast::{Literal, Model, Name, SatEncodingDecision};

30

use conjure_cp::context::Context;

31

use conjure_cp::instantiate::{instantiate_model, validate_instantiation_conditions};

32

use conjure_cp::parse::tree_sitter::parse_essence_file;

33

use conjure_cp::rule_engine::resolve_rule_sets;

34

use conjure_cp::settings::{

35

    Channelling, Heuristic, HeuristicChoice, Parser, QuantifiedExpander, Rewriter, SolverFamily,

36

    begin_heuristic_all_choices, heuristic_all_choices, set_channelling,

37

    set_comprehension_expander, set_current_parser, set_current_rewriter,

38

    set_current_solver_family, set_default_rule_trace_enabled, set_heuristic, set_heuristic_seed,

39

    set_minion_discrete_threshold, set_rule_attempt_trace_enabled,

40

    set_rule_trace_aggregates_enabled, set_rule_trace_enabled,

41

};

42

use conjure_cp_cli::utils::conjure::{

43

    ConjureSolveCaptureOptions, get_solutions_from_conjure_with_stats, get_solutions_with_timings,

44

};

45

use conjure_cp_cli::utils::rule_trace::RuleApplicationCounter;

46

use conjure_cp_cli::utils::simplified_json::{

47

    domains_from_model, param_model_from_assignments, params_from_simplified_json_str,

48

};

49

use conjure_cp_cli::utils::testing::save_stats_json;

50

use conjure_cp_cli::utils::testing::{read_solutions_essence, save_solutions_essence};

51

#[allow(clippy::single_component_path_imports, unused_imports)]

52

use conjure_cp_rules;

53

use pretty_assertions::assert_eq;

54

use test_suite::AcceptMode;

55

use test_suite::TestConfig;

56

use test_suite::diagnostics::{

57

    DIAGNOSTICS_DIR, FailureRecord, clear_diagnostics, conjure_artifacts_dir, copy_file_if_exists,

58

    oxide_artifacts_dir, write_failure_record, write_oxide_failure_text,

59

};

60

use test_suite::golden_files::assert_no_redundant_expected_files;

61

use test_suite::test_config::TraceLevel;

62

use test_suite::test_config::{

63

    NumberOfSolutions, RecordedConjureStats, RecordedRuleTraceStats, RecordedRunConfig,

64

    RecordedRunStats, read_stats_or_default, replace_config_run_stats, reset_stats_for_run,

65

    round_expected_time, stats_path, upsert_conjure_timing_stats, upsert_expected_time_stats,

66

    upsert_status_stats, upsert_tool_status_stats,

67

};

68

69

#[path = "support/solution_snapshots.rs"]

70

mod solution_snapshots;

71

use solution_snapshots::{SharedSolutionSnapshot, render_shared_solutions};

72

73

const DISABLE_TRACING_ENV: &str = "CONJURE_OXIDE_TEST_DISABLE_TRACING";

74

75

#[derive(Clone, Copy, Debug)]

76

struct RunCase<'a> {

77

    parser: Parser,

78

    rewriter: Rewriter,

79

    comprehension_expander: QuantifiedExpander,

80

    solver: SolverFamily,

81

    extra_rule_sets: &'a [String],

82

    heuristic: Heuristic,

83

    channelling: Channelling,

84

    seed: u64,

85

    solver_seed: u32,

86

    choice_path: &'a [usize],

87

    case_name: &'a str,

88

89

90

/// What one exhaustive run produced, beyond pass/fail.

91

struct RunOutcome {

92

    /// The run's solutions, normalised for comparison, when they are the model's complete

93

    /// solution set: the search ran to exhaustion and kept no intermediate optimisation steps.

94

    /// Every such run of one fixture solves the same problem, so they must all agree.

95

    comparable_solutions: Option<Vec<BTreeMap<Name, Literal>>>,

96

97

98

/// The first run of a fixture to report a complete solution set, which every later run must match.

99

struct ReferenceSolutions {

100

    run_label: String,

101

    solutions: Vec<BTreeMap<Name, Literal>>,

102

103

104

/// Checks that a run found the same solution set as the fixture's first comparable run.

105

///

106

/// Each run's expected solutions are only compared against that run's own recording, so a

107

/// modelling choice that loses (or invents) solutions would otherwise be accepted silently whenever

108

/// Conjure validation is skipped. Different representations print the same value in different

109

/// orders, so the comparison is on normalised solutions.

110

40423

fn check_solutions_agree(

111

40423

    reference: &mut Option<ReferenceSolutions>,

112

40423

    run_label: String,

113

40423

    solutions: Vec<BTreeMap<Name, Literal>>,

114

40423

) -> Result<(), Box<dyn Error>> {

115

40423

    let Some(reference) = reference.as_ref() else {

116

555

        *reference = Some(ReferenceSolutions {

117

555

            run_label,

118

555

            solutions,

119

555

});

120

555

        return Ok(());

121

};

122

39868

    if reference.solutions == solutions {

123

39868

        return Ok(());

124

125

126

    const SHOWN: usize = 10;

127

    let describe = |missing_from: &[BTreeMap<Name, Literal>], present_in: &[_]| {

128

        let missing: Vec<String> = present_in

129

            .iter()

130

            .filter(|solution| !missing_from.contains(solution))

131

            .map(|solution: &BTreeMap<Name, Literal>| {

132

                solution

133

                    .iter()

134

                    .map(|(name, value)| format!("{name} = {value}"))

135

                    .collect::<Vec<_>>()

136

                    .join(", ")

137

})

138

            .collect();

139

        let more = missing.len().saturating_sub(SHOWN);

140

        let mut lines: Vec<String> = missing

141

            .into_iter()

142

            .take(SHOWN)

143

            .map(|line| format!("    {line}"))

144

            .collect();

145

        if more > 0 {

146

            lines.push(format!("    ... and {more} more"));

147

148

        lines.join("\n")

149

};

150

    Err(std::io::Error::other(format!(

151

        "{run_label} found {} solutions but {} found {}; runs of one model must agree.\n  \

152

         only in {}:\n{}\n  only in {}:\n{}",

153

        solutions.len(),

154

        reference.run_label,

155

        reference.solutions.len(),

156

        reference.run_label,

157

        describe(&solutions, &reference.solutions),

158

        run_label,

159

        describe(&reference.solutions, &solutions),

160

))

161

    .into())

162

40423

163

164

591

fn run_exhaustive_test_with_timeout<F>(

165

591

    test_name: &str,

166

591

    test_dir: &str,

167

591

    run_test: F,

168

591

) -> Result<(), Box<dyn Error>>

169

591

where

170

591

    F: FnOnce() -> Result<(), Box<dyn Error>>,

171

172

591

    let Some(timeout) = test_case_timeout()? else {

173

591

        return run_test();

174

};

175

176

    if std::env::var_os("CONJURE_OXIDE_TEST_TIMEOUT_CHILD").is_some() {

177

        return run_test();

178

179

180

    let mut command = Command::new(std::env::current_exe()?);

181

    command

182

        .arg(test_name)

183

        .arg("--exact")

184

        // The outer harness has already selected this test, including explicit ignored runs.

185

        .arg("--include-ignored")

186

        .env("CONJURE_OXIDE_TEST_TIMEOUT_CHILD", "1")

187

        .stdin(Stdio::null())

188

        .stdout(Stdio::piped())

189

        .stderr(Stdio::piped());

190

    pass_exhaustive_test_env(&mut command);

191

192

    #[cfg(unix)]

193

    command.process_group(0);

194

195

    let mut child = command.spawn()?;

196

    let stdout = child_output_reader(child.stdout.take());

197

    let stderr = child_output_reader(child.stderr.take());

198

    let started_at = Instant::now();

199

200

    loop {

201

        if let Some(status) = child.try_wait()? {

202

            if status.success() {

203

                return Ok(());

204

205

206

            let child_output = format_child_output(stdout, stderr);

207

            return Err(

208

                format!("timed child test {test_name} failed with {status}{child_output}").into(),

209

);

210

211

212

        if started_at.elapsed() >= timeout {

213

            terminate_timed_child(&mut child)?;

214

            let child_output = format_child_output(stdout, stderr);

215

            if AcceptMode::from_env().accepts_outputs() {

216

                upsert_status_stats(

217

                    &stats_path(Path::new(test_dir)),

218

                    &format!("timeout({})", timeout.as_secs()),

219

)?;

220

221

            let _ = write_failure_record(

222

                Path::new(test_dir),

223

                &FailureRecord {

224

                    stage: "timeout".to_string(),

225

                    message: format!(

226

                        "test {test_name} exceeded TEST_CASE_TIMEOUT={}s{child_output}",

227

                        timeout.as_secs()

228

),

229

                    run_label: None,

230

},

231

);

232

            return Err(format!(

233

                "test {test_name} exceeded TEST_CASE_TIMEOUT={}s{child_output}",

234

                timeout.as_secs(),

235

236

            .into());

237

238

239

        std::thread::sleep(Duration::from_millis(100));

240

241

591

242

243

/// Starts a background reader for a piped child-process stream.

244

fn child_output_reader(

245

    output: Option<impl Read + Send + 'static>,

246

) -> Option<std::thread::JoinHandle<Vec<u8>>> {

247

    output.map(|mut output| {

248

        std::thread::spawn(move || {

249

            let mut buffer = Vec::new();

250

            let _ = output.read_to_end(&mut buffer);

251

            buffer

252

})

253

})

254

255

256

/// Formats captured child-process output for failure reports.

257

fn format_child_output(

258

    stdout: Option<std::thread::JoinHandle<Vec<u8>>>,

259

    stderr: Option<std::thread::JoinHandle<Vec<u8>>>,

260

) -> String {

261

    let stdout = join_child_output(stdout);

262

    let stderr = join_child_output(stderr);

263

    let stdout = cleaned_child_output(&stdout);

264

    let stderr = cleaned_child_output(&stderr);

265

266

    match (stdout.is_empty(), stderr.is_empty()) {

267

        (true, true) => String::new(),

268

        (false, true) => format!("\n\nchild stdout:\n{stdout}"),

269

        (true, false) => format!("\n\nchild stderr:\n{stderr}"),

270

        (false, false) => format!("\n\nchild stdout:\n{stdout}\n\nchild stderr:\n{stderr}"),

271

272

273

274

/// Collects bytes read by a child-output reader thread.

275

fn join_child_output(handle: Option<std::thread::JoinHandle<Vec<u8>>>) -> Vec<u8> {

276

    handle

277

        .and_then(|handle| handle.join().ok())

278

        .unwrap_or_default()

279

280

281

/// Removes noisy libtest status lines from captured child-process output.

282

fn cleaned_child_output(output: &[u8]) -> String {

283

    String::from_utf8_lossy(output)

284

        .lines()

285

        .filter(|line| line.trim() != "running 1 test")

286

        .collect::<Vec<_>>()

287

        .join("\n")

288

        .trim()

289

        .to_owned()

290

291

292

#[cfg(unix)]

293

fn terminate_timed_child(child: &mut Child) -> Result<(), Box<dyn Error>> {

294

    let process_group = format!("-{}", child.id());

295

    let _ = Command::new("kill")

296

        .arg("-TERM")

297

        .arg(&process_group)

298

        .status();

299

300

    std::thread::sleep(Duration::from_millis(500));

301

    if child.try_wait()?.is_none() {

302

        let _ = Command::new("kill")

303

            .arg("-KILL")

304

            .arg(&process_group)

305

            .status();

306

307

308

    let _ = child.wait();

309

    Ok(())

310

311

312

#[cfg(not(unix))]

313

fn terminate_timed_child(child: &mut Child) -> Result<(), Box<dyn Error>> {

314

    child.kill()?;

315

    let _ = child.wait();

316

    Ok(())

317

318

319

591

fn test_case_timeout() -> Result<Option<Duration>, Box<dyn Error>> {

320

591

    match std::env::var("TEST_CASE_TIMEOUT") {

321

        Ok(value) => {

322

            let seconds = value.parse::<u64>().map_err(|err| {

323

                format!("invalid TEST_CASE_TIMEOUT value '{value}', expected seconds: {err}")

324

            })?;

325

            Ok(Some(Duration::from_secs(seconds)))

326

327

591

        Err(std::env::VarError::NotPresent) => Ok(None),

328

        Err(err) => Err(Box::new(err)),

329

330

591

331

332

fn pass_exhaustive_test_env(command: &mut Command) {

333

    for key in [

334

        "TEST_CASE_TIMEOUT",

335

        "ACCEPT",

336

        "MAX_EXPECTED_TIME",

337

        DISABLE_TRACING_ENV,

338

] {

339

        if let Ok(value) = std::env::var(key) {

340

            command.env(key, value);

341

342

343

344

345

1550

fn test_tracing_disabled() -> bool {

346

1550

    match std::env::var(DISABLE_TRACING_ENV) {

347

        Ok(value) => !matches!(value.as_str(), "" | "0" | "false" | "False" | "FALSE"),

348

1550

        Err(std::env::VarError::NotPresent) => false,

349

        Err(std::env::VarError::NotUnicode(_)) => true,

350

351

1550

352

353

41783

fn run_case_label(

354

41783

    path: &str,

355

41783

    essence_base: &str,

356

41783

    extension: &str,

357

41783

    run_case: RunCase<'_>,

358

41783

) -> String {

359

41783

    format!(

360

41783

        "test_dir={path}, model={essence_base}.{extension}, parser={}, rewriter={}, comprehension_expander={}, heuristic={}, seed={}, channelling={}, solver={}, solver_seed={}",

361

41783

        run_case.parser,

362

41783

        run_case.rewriter,

363

41783

        run_case.comprehension_expander,

364

41783

        run_case.heuristic,

365

41783

        run_case.seed,

366

41783

        run_case.channelling,

367

41783

        run_case.solver.as_str(),

368

41783

        run_case.solver_seed

369

370

41783

371

372

42374

fn param_file_in_test_dir(path: &str) -> Option<String> {

373

42374

    let entries = fs::read_dir(path).ok()?;

374

42374

    let paths = entries

375

42374

        .filter_map(Result::ok)

376

8184896

        .map(|entry| entry.path())

377

        .collect::<Vec<_>>();

378

42374

    paths

379

42374

        .iter()

380

7215263

        .find(|path| path.extension().is_some_and(|ext| ext == "param"))

381

36770

        .or_else(|| {

382

6882282

            paths.iter().find(|path| {

383

6882282

                path.file_name()

384

6882282

                    .is_some_and(|name| name == "input.param.json")

385

6882282

})

386

36770

})

387

5900

        .map(|path| path.to_string_lossy().to_string())

388

42374

389

390

591

fn exhaustive_test(path: &str, essence_base: &str, extension: &str) -> Result<(), Box<dyn Error>> {

391

591

    let result = exhaustive_test_inner_with_status(path, essence_base, extension);

392

393

591

    if result.is_ok() {

394

591

        let _ = clear_diagnostics(Path::new(path));

395

396

397

591

    if AcceptMode::from_env().accepts_outputs() {

398

        let status = if result.is_ok() { "ok" } else { "fail" };

399

        upsert_status_stats(&stats_path(Path::new(path)), status)?;

400

591

401

402

591

    result

403

591

404

405

591

fn exhaustive_test_inner_with_status(

406

591

    path: &str,

407

591

    essence_base: &str,

408

591

    extension: &str,

409

591

) -> Result<(), Box<dyn Error>> {

410

591

    let accept_mode = AcceptMode::from_env();

411

591

    let accept = accept_mode.accepts_outputs();

412

591

    let started_at = Instant::now();

413

414

    let file_config: TestConfig =

415

591

        if let Ok(config_contents) = fs::read_to_string(format!("{path}/config.toml")) {

416

591

            toml::from_str(&config_contents).unwrap()

417

        } else {

418

            Default::default()

419

};

420

421

591

    if accept {

422

        clean_test_dir_for_accept(

423

            path,

424

            essence_base,

425

            extension,

426

            file_config.uses_shared_solution_snapshot(),

427

)?;

428

591

429

430

591

    let run_stats = read_stats_or_default(&stats_path(Path::new(path)))?;

431

591

    if accept {

432

        reset_stats_for_run(&stats_path(Path::new(path)))?;

433

591

434

591

    let config = file_config;

435

436

591

    let skip_conjure_validation = config.should_skip_conjure_validation();

437

591

    let minion_discrete_threshold = config.minion_discrete_threshold;

438

591

    let number_of_solutions = config.number_of_solutions;

439

591

    let solver_solution_limit = number_of_solutions.as_solver_limit();

440

591

    let keep_intermediate_solutions = config.keep_intermediate_solutions;

441

442

591

    let parsers = config

443

591

        .configured_parsers()

444

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

445

591

    let rewriters = config

446

591

        .configured_rewriters()

447

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

448

591

    let comprehension_expanders = config

449

591

        .configured_comprehension_expanders()

450

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

451

591

    let solvers = config

452

591

        .configured_solvers()

453

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;

454

591

    let seed = config.seed;

455

591

    let solver_seed = config.solver_seed;

456

591

    let distinguish_rewriter = rewriters.len() > 1;

457

458

    // Conjure output depends only on the input model, so cache it once per test case.

459

591

    let model_path = format!("{path}/{essence_base}.{extension}");

460

591

    let param_file = param_file_in_test_dir(path);

461

591

    let stats_path = stats_path(Path::new(path));

462

591

    let mut conjure_captured = false;

463

591

    let conjure_solutions = if accept

464

        && !skip_conjure_validation

465

        && let Some(solver_solution_limit) = solver_solution_limit

466

467

        let conjure_run = match get_solutions_from_conjure_with_stats(

468

            &model_path,

469

            param_file.as_deref(),

470

            Default::default(),

471

            solver_solution_limit,

472

            ConjureSolveCaptureOptions {

473

                artifact_dir: Some(conjure_artifacts_dir(Path::new(path))),

474

                savilerow_options: Some("-O0".to_string()),

475

},

476

) {

477

            Ok(conjure_run) => {

478

                conjure_captured = true;

479

                upsert_tool_status_stats(&stats_path, "conjure", "ok")?;

480

                conjure_run

481

482

            Err(err) => {

483

                upsert_tool_status_stats(&stats_path, "conjure", "fail")?;

484

                record_exhaustive_failure(

485

                    path,

486

                    FailureRecord {

487

                        stage: "conjure".to_string(),

488

                        message: err.to_string(),

489

                        run_label: None,

490

},

491

                    number_of_solutions,

492

                    false,

493

);

494

                return Err(std::io::Error::other(format!(

495

                    "failed to fetch Conjure reference solutions for {model_path}: {err}"

496

))

497

                .into());

498

499

};

500

501

        Some((Arc::new(conjure_run.solutions), conjure_run.timings))

502

    } else {

503

591

        None

504

};

505

591

    let conjure_solution_values = conjure_solutions

506

591

        .as_ref()

507

        .map(|(solutions, _)| Arc::clone(solutions));

508

591

    let conjure_timings = conjure_solutions.and_then(|(_, timings)| timings);

509

591

    let mut allowed_expected_files = BTreeSet::new();

510

591

    let mut reference_solutions = None;

511

591

    let shared_solutions_enabled = config.uses_shared_solution_snapshot();

512

591

    let shared_expected_name = format!("{essence_base}.expected.solutions");

513

591

    if shared_solutions_enabled {

514

566

        allowed_expected_files.insert(shared_expected_name.clone());

515

25

516

591

    let mut shared_solutions = SharedSolutionSnapshot::default();

517

518

591

    let mut first_config_error = None;

519

591

    for comprehension_expander in comprehension_expanders {

520

591

        for parser in parsers.iter().copied() {

521

592

            for rewriter in rewriters.clone() {

522

592

                for solver in solvers.iter().copied() {

523

1550

                    let configured_trace_level = config.configured_trace_level_for(solver);

524

1550

                    let trace_level = if test_tracing_disabled() {

525

                        TraceLevel::None

526

                    } else {

527

1550

                        configured_trace_level

528

};

529

1550

                    let rule_trace_snapshots_enabled = trace_level == TraceLevel::Full;

530

1550

                    let rule_trace_aggregates_enabled = trace_level == TraceLevel::Aggregate;

531

1550

                    let heuristics = config.configured_heuristics_for(solver).map_err(|err| {

532

                        std::io::Error::new(std::io::ErrorKind::InvalidInput, err)

533

                    })?;

534

                    let channelling_settings =

535

1550

                        config.configured_channelling_for(solver).map_err(|err| {

536

                            std::io::Error::new(std::io::ErrorKind::InvalidInput, err)

537

                        })?;

538

                    let distinguish_heuristic =

539

1550

                        heuristics.len() > 1 || heuristics.first() != Some(&Heuristic::All);

540

1550

                    let distinguish_channelling = channelling_settings.len() > 1

541

1550

                        || channelling_settings.first() != Some(&Channelling::No);

542

1550

                    for heuristic in heuristics.iter().copied() {

543

1562

                        for channelling in channelling_settings.iter().copied() {

544

1562

                            let run_config = RecordedRunConfig {

545

1562

                                parser: parser.to_string(),

546

1562

                                rewriter: rewriter.to_string(),

547

1562

                                comprehension_expander: comprehension_expander.to_string(),

548

1562

                                heuristic: heuristic.to_string(),

549

1562

                                channelling: channelling.to_string(),

550

1562

                                seed,

551

1562

                                solver_seed,

552

1562

                                solver: solver.as_str(),

553

1562

};

554

1562

                            let mut model_rows = Vec::new();

555

1562

                            let config_result = (|| -> Result<(), Box<dyn Error>> {

556

1562

                                let base_case_name = run_case_name(

557

1562

                                    parser,

558

1562

                                    rewriter,

559

1562

                                    comprehension_expander,

560

1562

                                    heuristic,

561

1562

                                    channelling,

562

1562

                                    seed,

563

1562

                                    solver_seed,

564

1562

                                    distinguish_rewriter,

565

1562

                                    distinguish_heuristic,

566

1562

                                    distinguish_channelling,

567

1562

);

568

1562

                                let mut choice_path = Vec::new();

569

1562

                                let mut model_index = 0usize;

570

                                loop {

571

41783

                                    let case_name = if heuristic == Heuristic::All {

572

41573

                                        format!("{base_case_name}-model-{model_index:03}")

573

                                    } else {

574

210

                                        base_case_name.clone()

575

};

576

41783

                                    let run_case = RunCase {

577

41783

                                        parser,

578

41783

                                        rewriter,

579

41783

                                        comprehension_expander,

580

41783

                                        solver,

581

41783

                                        extra_rule_sets: &config.extra_rule_sets,

582

41783

                                        heuristic,

583

41783

                                        channelling,

584

41783

                                        seed,

585

41783

                                        solver_seed,

586

41783

                                        choice_path: &choice_path,

587

41783

                                        case_name: case_name.as_str(),

588

41783

};

589

41783

                                    allowed_expected_files.extend(

590

41783

                                        expected_exhaustive_files_for_case(

591

41783

                                            run_case.case_name,

592

41783

                                            solver,

593

41783

                                            configured_trace_level,

594

41783

                                            solver_solution_limit.is_some()

595

41776

                                                && !shared_solutions_enabled,

596

),

597

);

598

41783

                                    let mut row = model_run_identity(

599

41783

                                        run_case,

600

41783

                                        minion_discrete_threshold,

601

41783

                                        number_of_solutions,

602

41783

);

603

41783

                                    row.model_index = model_index;

604

41783

                                    let model_rule_counts = RuleApplicationCounter::default();

605

41783

                                    let result = execute_exhaustive_run(

606

41783

                                        path,

607

41783

                                        essence_base,

608

41783

                                        extension,

609

41783

                                        run_case,

610

41783

                                        minion_discrete_threshold,

611

41783

                                        number_of_solutions,

612

41783

                                        keep_intermediate_solutions,

613

41783

                                        conjure_solution_values.clone(),

614

41783

                                        accept,

615

41783

                                        rule_trace_snapshots_enabled,

616

41783

                                        rule_trace_aggregates_enabled.then_some(&model_rule_counts),

617

41783

                                        &mut row,

618

41783

                                        shared_solutions_enabled,

619

41783

                                        &mut shared_solutions,

620

41783

);

621

41783

                                    let stats_result = (|| -> Result<(), Box<dyn Error>> {

622

41783

                                        if accept

623

                                            && (rule_trace_snapshots_enabled

624

                                                || rule_trace_aggregates_enabled)

625

626

                                            let aggregates = if rule_trace_snapshots_enabled {

627

                                                collect_rule_trace_aggregates(

628

                                                    Path::new(path),

629

                                                    &case_name,

630

                                                    solver,

631

)?

632

                                            } else {

633

                                                let rules = model_rule_counts.snapshot();

634

                                                RecordedRuleTraceStats {

635

                                                    total_rule_applications: Some(

636

                                                        rules.values().sum(),

637

),

638

                                                    rules,

639

                                                    ..RecordedRuleTraceStats::default()

640

641

};

642

                                            row.rule_trace = aggregates;

643

                                            row.rule_trace.total_rule_attempts =

644

                                                Some(collect_rule_attempts(

645

                                                    Path::new(path),

646

                                                    &case_name,

647

                                                    solver,

648

                                                )?);

649

41783

650

41783

                                        Ok(())

651

                                    })();

652

                                    let result =

653

41783

                                        result.and_then(|outcome| stats_result.map(|()| outcome));

654

41783

                                    let outcome = match result {

655

41783

                                        Ok(outcome) => outcome,

656

                                        Err(err) => {

657

                                            row.status = "fail".to_owned();

658

                                            model_rows.push(row);

659

                                            return Err(err);

660

661

};

662

41783

                                    model_rows.push(row);

663

41783

                                    if let Some(solutions) = outcome.comparable_solutions {

664

40423

                                        let agreement = check_solutions_agree(

665

40423

                                            &mut reference_solutions,

666

40423

                                            format!("{}-{}", run_case.case_name, solver.as_str()),

667

40423

                                            solutions,

668

40423

);

669

40423

                                        if agreement.is_err() {

670

                                            model_rows

671

                                                .last_mut()

672

                                                .expect("model row was just recorded")

673

                                                .status = "fail".to_owned();

674

40423

675

40423

                                        agreement?;

676

1360

677

678

41783

                                    if heuristic != Heuristic::All {

679

210

                                        break;

680

41573

681

41573

                                    let decisions = heuristic_all_choices();

682

41573

                                    let Some(next_path) = next_all_choice_path(&decisions) else {

683

1352

                                        break;

684

};

685

40221

                                    choice_path = next_path;

686

40221

                                    model_index += 1;

687

688

1562

                                Ok(())

689

                            })();

690

691

1562

                            if accept {

692

                                replace_config_run_stats(&stats_path, &run_config, model_rows)?;

693

1562

694

695

1562

                            if let Err(err) = config_result

696

                                && first_config_error.is_none()

697

698

                                first_config_error = Some(err);

699

1562

700

701

702

703

704

705

706

707

591

    let oxide_result = if let Some(err) = first_config_error {

708

        Err(err)

709

    } else {

710

591

        (|| -> Result<(), Box<dyn Error>> {

711

591

            assert_no_redundant_expected_files(Path::new(path), &allowed_expected_files, None)?;

712

591

            if !accept {

713

591

                shared_solutions.finish(&Path::new(path).join(&shared_expected_name), false)?;

714

715

591

            Ok(())

716

        })()

717

};

718

719

591

    if let Err(err) = &oxide_result {

720

        record_exhaustive_failure(

721

            path,

722

            FailureRecord {

723

                stage: "oxide".to_string(),

724

                message: err.to_string(),

725

                run_label: None,

726

},

727

            number_of_solutions,

728

            conjure_captured,

729

);

730

591

731

732

591

    oxide_result?;

733

734

591

    if accept_mode.records_expected_time() {

735

        let observed_expected_time = round_expected_time(started_at.elapsed());

736

        if let Some(expected_time) =

737

            accept_mode.expected_time_to_record(run_stats.expected_time, observed_expected_time)

738

739

            upsert_expected_time_stats(&stats_path, expected_time)?;

740

741

591

742

743

591

    if accept

744

        && !skip_conjure_validation

745

        && let Some(conjure_timings) = conjure_timings

746

747

        upsert_conjure_timing_stats(

748

            &stats_path,

749

            RecordedConjureStats {

750

                conjure_wall_clock_time: conjure_timings.wall_clock_time_s,

751

                conjure_translation_time: conjure_timings.translation_time_s,

752

                conjure_driver_translation_time: conjure_timings.conjure_translation_time_s,

753

                savilerow_translation_time: conjure_timings.savilerow_translation_time_s,

754

                conjure_solve_time: conjure_timings.solve_time_s,

755

},

756

)?;

757

591

758

759

591

    if accept {

760

        shared_solutions.finish(&Path::new(path).join(&shared_expected_name), true)?;

761

591

762

763

591

    Ok(())

764

591

765

766

/// Runs an exhaustive test for a given Conjure model by:

767

/// 1. Parsing the model from an Essence file.

768

/// 2. Rewriting the model according to predefined rule sets.

769

/// 3. Solving the model using the Minion solver and validating the solutions.

770

/// 4. Comparing generated rule traces with expected outputs.

771

///

772

/// Set `CONJURE_OXIDE_TEST_DISABLE_TRACING=1` to skip rule trace generation and validation during

773

/// timing runs.

774

///

775

/// This function operates in multiple stages:

776

///

777

/// - **Parsing Stage**

778

///   - **Stage 1a (Default)**: Reads the Essence model file and verifies that it parses correctly using `parser = "tree-sitter"`.

779

///   - **Stage 1b (Optional)**: Reads the Essence model file and verifies that it parses correctly using `parser = "via-conjure"`.

780

///

781

/// - **Rewrite Stage**

782

///   - **Stage 2a**: Applies a set of rules to the parsed model and validates the result.

783

///

784

/// - **Solution Stage**

785

///   - **Stage 3a (Default)**: Uses Minion to solve the model and save the solutions.

786

///   - **Stage 3b (ACCEPT only)**: Compares solutions against Conjure-generated solutions.

787

///

788

/// - **Rule Trace Validation Stage**

789

///   - **Stage 4a (Default)**: Checks that the generated rules match expected traces.

790

///

791

/// # Arguments

792

///

793

/// * `path` - The file path where the Essence model and other resources are located.

794

/// * `essence_base` - The base name of the Essence model file.

795

/// * `extension` - The file extension for the Essence model.

796

///

797

/// # Errors

798

///

799

/// Returns an error if any stage fails due to a mismatch with expected results or file I/O issues.

800

#[allow(clippy::unwrap_used)]

801

#[allow(clippy::too_many_arguments)]

802

41783

fn execute_exhaustive_run(

803

41783

    path: &str,

804

41783

    essence_base: &str,

805

41783

    extension: &str,

806

41783

    run_case: RunCase<'_>,

807

41783

    minion_discrete_threshold: usize,

808

41783

    number_of_solutions: NumberOfSolutions,

809

41783

    keep_intermediate_solutions: bool,

810

41783

    conjure_solutions: Option<Arc<Vec<BTreeMap<Name, Literal>>>>,

811

41783

    accept: bool,

812

41783

    rule_trace_snapshots_enabled: bool,

813

41783

    rule_counts: Option<&RuleApplicationCounter>,

814

41783

    model_stats: &mut RecordedRunStats,

815

41783

    shared_solutions_enabled: bool,

816

41783

    shared_solutions: &mut SharedSolutionSnapshot,

817

41783

) -> Result<RunOutcome, Box<dyn Error>> {

818

41783

    let run_label = run_case_label(path, essence_base, extension, run_case);

819

41783

    let default_rule_trace_enabled = matches!(run_case.rewriter, Rewriter::Rewrite(_));

820

41783

    set_rule_trace_enabled(rule_trace_snapshots_enabled || rule_counts.is_some());

821

41783

    set_default_rule_trace_enabled(rule_trace_snapshots_enabled && default_rule_trace_enabled);

822

41783

    set_rule_attempt_trace_enabled(false);

823

41783

    set_rule_trace_aggregates_enabled(rule_counts.is_some());

824

41783

    let run_test = || {

825

41783

        exhaustive_test_inner(

826

41783

            path,

827

41783

            essence_base,

828

41783

            extension,

829

41783

            run_case,

830

41783

            minion_discrete_threshold,

831

41783

            number_of_solutions,

832

41783

            keep_intermediate_solutions,

833

41783

            conjure_solutions,

834

41783

            accept,

835

41783

            rule_trace_snapshots_enabled,

836

41783

            model_stats,

837

41783

            shared_solutions_enabled,

838

41783

            shared_solutions,

839

41783

840

41783

};

841

41783

    let result = if rule_trace_snapshots_enabled {

842

1573

        let file = File::create(format!(

843

1573

            "{path}/{}-{}-generated-rule-trace.txt",

844

1573

            run_case.case_name,

845

1573

            run_case.solver.as_str()

846

1573

        ))?;

847

1573

        let subscriber = Arc::new(

848

1573

            tracing_subscriber::registry().with(

849

1573

                fmt::layer()

850

1573

                    .with_writer(file)

851

1573

                    .with_level(false)

852

1573

                    .without_time()

853

1573

                    .with_target(false)

854

1573

                    .with_filter(EnvFilter::new("rule_engine_rule_trace=trace"))

855

16396

                    .with_filter(FilterFn::new(|meta| {

856

16396

                        meta.target() == "rule_engine_rule_trace"

857

16396

                    })),

858

),

859

        ) as Arc<dyn tracing::Subscriber + Send + Sync>;

860

1573

        tracing::subscriber::with_default(subscriber, run_test)

861

40210

    } else if let Some(counts) = rule_counts {

862

39845

        let subscriber = tracing_subscriber::registry().with(counts.clone().with_filter(

863

717312

            FilterFn::new(|meta| meta.target() == "rule_engine_rule_trace_aggregates"),

864

));

865

39845

        tracing::subscriber::with_default(subscriber, run_test)

866

    } else {

867

365

        run_test()

868

};

869

870

41783

    if result.is_err() {

871

        record_choice_path(run_case, model_stats);

872

41783

873

41783

    result.map_err(|err| {

874

        let message = format!("{run_label}: {err}");

875

        copy_oxide_run_artifacts(path, run_case, &message);

876

        let _ = try_capture_oxide_minion(

877

            path,

878

            essence_base,

879

            extension,

880

            run_case,

881

            minion_discrete_threshold,

882

);

883

        std::io::Error::other(message).into()

884

})

885

41783

886

887

41783

fn exhaustive_test_inner(

888

41783

    path: &str,

889

41783

    essence_base: &str,

890

41783

    extension: &str,

891

41783

    run_case: RunCase<'_>,

892

41783

    minion_discrete_threshold: usize,

893

41783

    number_of_solutions: NumberOfSolutions,

894

41783

    keep_intermediate_solutions: bool,

895

41783

    conjure_solutions: Option<Arc<Vec<BTreeMap<Name, Literal>>>>,

896

41783

    accept: bool,

897

41783

    rule_trace_snapshots_enabled: bool,

898

41783

    model_stats: &mut RecordedRunStats,

899

41783

    shared_solutions_enabled: bool,

900

41783

    shared_solutions: &mut SharedSolutionSnapshot,

901

41783

) -> Result<RunOutcome, Box<dyn Error>> {

902

41783

    let parser = run_case.parser;

903

41783

    let rewriter = run_case.rewriter;

904

41783

    let comprehension_expander = run_case.comprehension_expander;

905

41783

    let solver_fam = run_case.solver;

906

41783

    let case_name = run_case.case_name;

907

908

41783

    let context: Arc<RwLock<Context<'static>>> = Default::default();

909

910

41783

    set_current_parser(parser);

911

41783

    set_current_rewriter(rewriter);

912

41783

    set_comprehension_expander(comprehension_expander);

913

41783

    set_current_solver_family(solver_fam);

914

41783

    set_minion_discrete_threshold(Some(minion_discrete_threshold));

915

41783

    set_heuristic(run_case.heuristic);

916

41783

    set_heuristic_seed(run_case.seed);

917

41783

    set_channelling(run_case.channelling);

918

41783

    if run_case.heuristic == Heuristic::All {

919

41573

        begin_heuristic_all_choices(run_case.choice_path.to_vec());

920

210

921

922

41783

    let translation_started_at = Instant::now();

923

924

    // Stage 1a/1b: Parse the problem model and apply an optional param file.

925

41783

    let parsed_model = parse_unified_problem_model(

926

41783

        path,

927

41783

        essence_base,

928

41783

        extension,

929

41783

        parser,

930

41783

        param_file_in_test_dir(path).as_deref(),

931

41783

        context.clone(),

932

41783

)?;

933

    // Stage 2a: Rewrite the model using the rule engine

934

41783

    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();

935

41783

    rules_to_load.extend(run_case.extra_rule_sets.iter().map(String::as_str));

936

937

41783

    let rule_sets = resolve_rule_sets(solver_fam, &rules_to_load)?;

938

    // Solver-time rewrites -- dominance-blocking constraints, say -- read the rule sets back off

939

    // the model's context, so record them there as the CLI does.

940

941

41783

        let mut context = context.write().unwrap();

942

41783

        context.rule_sets = rule_sets.clone();

943

944

945

41783

    let model = parsed_model;

946

947

41783

    let Rewriter::Rewrite(config) = rewriter;

948

41783

    let rewritten_model = rewrite_model(&model, &rule_sets, config)?;

949

    // `x` enumerates translation-time modelling decisions. Solver-time CDP rewrites must not add

950

    // branches to that model portfolio.

951

41783

    if run_case.heuristic == Heuristic::All {

952

41573

        set_heuristic(Heuristic::First);

953

210

954

41783

    let translation_time_s = translation_started_at.elapsed().as_secs_f64();

955

41783

    record_choice_path(run_case, model_stats);

956

41783

    record_model_choices(&rewritten_model, model_stats);

957

41783

    model_stats.translation_time = Some(translation_time_s);

958

959

41783

    let solver_started_at = Instant::now();

960

41783

    let solutions = if let Some(number_of_solutions) = number_of_solutions.as_solver_limit() {

961

41776

        let solver_input_file = None;

962

41776

        let solver = match solver_fam {

963

            SolverFamily::Minion => {

964

915

                Solver::new(Minion::default().with_solver_seed(run_case.solver_seed))

965

966

40000

            SolverFamily::Sat => Solver::new(Sat::default().with_solver_seed(run_case.solver_seed)),

967

861

            SolverFamily::Z3 => Solver::new(Smt::default().with_solver_seed(run_case.solver_seed)),

968

};

969

41776

        let (solved, measured) = get_solutions_with_timings(

970

41776

            solver,

971

41776

            rewritten_model,

972

41776

            number_of_solutions,

973

41776

            keep_intermediate_solutions,

974

41776

            &solver_input_file,

975

41776

            false,

976

41776

)?;

977

41776

        let output_started_at = Instant::now();

978

41776

        save_solutions_essence(&solved, path, case_name, solver_fam)?;

979

41776

        model_stats.backend_time = Some(measured.backend_time_s);

980

41776

        model_stats.search_time = Some(measured.search_time_s);

981

41776

        model_stats.solution_processing_time =

982

41776

            Some(measured.solution_processing_time_s + output_started_at.elapsed().as_secs_f64());

983

41776

        Some(solved)

984

    } else {

985

7

        None

986

};

987

41783

    let solve_time_s = solver_started_at.elapsed().as_secs_f64();

988

41783

    model_stats.solve_time = number_of_solutions.as_solver_limit().map(|_| solve_time_s);

989

990

    // Stage 3b: Check solutions against Conjure when accept mode is enabled and validation is enabled.

991

41783

    if accept && conjure_solutions.is_some() && solutions.is_some() {

992

        let conjure_solutions = conjure_solutions

993

            .as_deref()

994

            .expect("conjure solutions should be present when Conjure validation is enabled");

995

        let solutions = solutions

996

            .as_deref()

997

            .expect("oxide solutions should be present when solver ran");

998

999

        if search_was_truncated(

1000

            number_of_solutions,

1001

            solutions.len().max(conjure_solutions.len()),

1002

) {

1003

            // The search stopped at the configured limit, so each tool holds an arbitrary subset

1004

            // of the solution set. Only the number of solutions found is comparable.

1005

            assert_eq!(

1006

                solutions.len(),

1007

                conjure_solutions.len(),

1008

                "Oxide found {} solutions but Conjure found {} (number-of-solutions = {}, so only \

1009

                 the counts are compared)",

1010

                solutions.len(),

1011

                conjure_solutions.len(),

1012

                solution_limit_description(number_of_solutions),

1013

);

1014

        } else {

1015

            let oxide_solutions = normalize_solutions_for_comparison(solutions);

1016

            let conjure_solutions = normalize_solutions_for_comparison(conjure_solutions);

1017

1018

            assert_eq!(

1019

                oxide_solutions, conjure_solutions,

1020

                "Oxide solutions (<) do not match Conjure solutions (>)!"

1021

);

1022

1023

41783

1024

1025

    // Shared complete searches publish a single golden after every configuration succeeds.

1026

41783

    if shared_solutions_enabled && let Some(solutions) = &solutions {

1027

40895

        shared_solutions.record(

1028

40895

            &format!("{case_name}-{}", solver_fam.as_str()),

1029

40895

            render_shared_solutions(solutions),

1030

40895

)?;

1031

888

1032

1033

    // Limited searches retain their per-run snapshots.

1034

41783

    if accept {

1035

        if solutions.is_some() && !shared_solutions_enabled {

1036

            let solver_name = solver_fam.as_str();

1037

            fs::copy(

1038

                format!("{path}/{case_name}-{solver_name}.generated.solutions"),

1039

                format!("{path}/{case_name}-{solver_name}.expected.solutions"),

1040

)?;

1041

1042

        if rule_trace_snapshots_enabled {

1043

            copy_human_trace_generated_to_expected(path, case_name, solver_fam)?;

1044

1045

41783

1046

1047

    // Check Stage 3a (solutions). Compare the Essence artefacts as written — do not re-render

1048

    // through `normalize_solutions_for_comparison`, which blanks matrix index domains.

1049

41783

    if solutions.is_some() && !shared_solutions_enabled {

1050

881

        let expected_solutions = read_solutions_essence(path, case_name, "expected", solver_fam)?;

1051

881

        let generated_solutions = read_solutions_essence(path, case_name, "generated", solver_fam)?;

1052

1053

881

        let expected_count = count_essence_solutions(&expected_solutions);

1054

881

        let generated_count = count_essence_solutions(&generated_solutions);

1055

1056

881

        if search_was_truncated(number_of_solutions, expected_count.max(generated_count)) {

1057

            // Solutions are enumerated in solver order, so a truncated search can legitimately

1058

            // return a different subset from the one recorded in the expected artefact. Only the

1059

            // number of solutions found is comparable.

1060

806

            assert_eq!(

1061

806

                generated_count,

1062

806

                expected_count,

1063

                "Generated {generated_count} solutions but expected {expected_count} \

1064

                 (number-of-solutions = {}, so only the counts are compared)",

1065

                solution_limit_description(number_of_solutions),

1066

);

1067

        } else {

1068

75

            assert_eq!(generated_solutions, expected_solutions);

1069

1070

40902

1071

1072

41783

    if rule_trace_snapshots_enabled {

1073

1573

        let generated = read_default_rule_trace(path, case_name, "generated", &solver_fam)?;

1074

1573

        let expected = read_default_rule_trace(path, case_name, "expected", &solver_fam)?;

1075

1076

1573

        assert_eq!(

1077

1573

            expected, generated,

1078

            "Generated rule trace does not match the expected trace!"

1079

);

1080

40210

1081

1082

41783

    save_stats_json(context, path, case_name, solver_fam)?;

1083

1084

    // Only a complete solution set is comparable across runs: a truncated search keeps an

1085

    // arbitrary subset, and optimisation (or dominance) runs may legitimately settle on different

1086

    // optimal solutions or report different intermediate steps.

1087

41783

    let comparable_solutions = solutions

1088

41776

        .filter(|solutions| {

1089

41776

            model.objective.is_none()

1090

41045

                && model.dominance.is_none()

1091

40427

                && !keep_intermediate_solutions

1092

40427

                && !search_was_truncated(number_of_solutions, solutions.len())

1093

41776

})

1094

40423

        .map(|solutions| normalize_solutions_for_comparison(&solutions));

1095

1096

41783

    Ok(RunOutcome {

1097

41783

        comparable_solutions,

1098

41783

})

1099

41783

1100

1101

/// Record the full realised portfolio path before solver-time rewrites can change it.

1102

41783

fn model_run_identity(

1103

41783

    run: RunCase<'_>,

1104

41783

    threshold: usize,

1105

41783

    limit: NumberOfSolutions,

1106

41783

) -> RecordedRunStats {

1107

41783

    RecordedRunStats {

1108

41783

        parser: run.parser.to_string(),

1109

41783

        rewriter: run.rewriter.to_string(),

1110

41783

        comprehension_expander: run.comprehension_expander.to_string(),

1111

41783

        heuristic: run.heuristic.to_string(),

1112

41783

        channelling: run.channelling.to_string(),

1113

41783

        seed: run.seed,

1114

41783

        solver_seed: run.solver_seed,

1115

41783

        solver: run.solver.as_str().to_owned(),

1116

41783

        case_name: run.case_name.to_owned(),

1117

41783

        minion_discrete_threshold: (run.solver == SolverFamily::Minion).then_some(threshold),

1118

41783

        solution_limit: limit.as_solver_limit(),

1119

41783

        status: "ok".to_owned(),

1120

41783

        ..Default::default()

1121

41783

1122

41783

1123

1124

41783

fn record_choice_path(run: RunCase<'_>, row: &mut RecordedRunStats) {

1125

41783

    if run.heuristic == Heuristic::All {

1126

41573

        let choices = heuristic_all_choices();

1127

137775

        row.choice_path = choices.iter().map(|choice| choice.selected).collect();

1128

41573

        row.choices = choices

1129

41573

            .iter()

1130

137775

            .map(|choice| choice.options[choice.selected].clone())

1131

            .collect();

1132

210

1133

41783

1134

1135

41783

fn record_model_choices(model: &Model, row: &mut RecordedRunStats) {

1136

41783

    row.representations = model

1137

41783

        .symbols()

1138

41783

        .iter_local()

1139

21441424

        .flat_map(|(_, decl)| {

1140

21441424

            decl.reprs()

1141

21441424

                .iter()

1142

180631

                .map(|(name, _)| name.to_owned())

1143

                .collect::<Vec<_>>()

1144

21441424

})

1145

        .collect::<BTreeSet<_>>()

1146

        .into_iter()

1147

        .collect();

1148

41783

    let mut families: BTreeMap<&str, BTreeSet<String>> = BTreeMap::new();

1149

    macro_rules! record {

1150

        ($family:literal, $selection:expr) => {

1151

            if let Some(selection) = $selection {

1152

                families

1153

                    .entry($family)

1154

                    .or_default()

1155

                    .insert(selection.algorithm.to_string());

1156

1157

};

1158

1159

41783

    for decision in model.sat_decisions() {

1160

20971483

        match decision {

1161

97346

            SatEncodingDecision::AtMostOne { encoding, .. } => record!("amo", encoding),

1162

9221

            SatEncodingDecision::Cardinality { encoding, .. } => record!("cardinality", encoding),

1163

            SatEncodingDecision::CountRelation {

1164

                encoding,

1165

                amo_encoding,

1166

..

1167

            } => {

1168

7700

                record!("cardinality", encoding);

1169

7700

                record!("amo", amo_encoding);

1170

1171

            SatEncodingDecision::PseudoBoolean { encoding, .. }

1172

            | SatEncodingDecision::IntegerRelation { encoding, .. }

1173

305962

            | SatEncodingDecision::Objective { encoding, .. } => record!("pb", encoding),

1174

            SatEncodingDecision::AllDifferent {

1175

                encoding,

1176

                amo_encoding,

1177

                pb_encoding,

1178

..

1179

            } => {

1180

5125

                record!("alldifferent", encoding);

1181

5125

                record!("amo", amo_encoding);

1182

5125

                record!("pb", pb_encoding);

1183

1184

            SatEncodingDecision::Table {

1185

                encoding,

1186

                pb_encoding,

1187

..

1188

            } => {

1189

6034

                record!("table", encoding);

1190

6034

                record!("pb", pb_encoding);

1191

1192

            SatEncodingDecision::Element {

1193

                encoding,

1194

                pb_encoding,

1195

..

1196

            } => {

1197

9627

                record!("element", encoding);

1198

9627

                record!("pb", pb_encoding);

1199

1200

20530468

            _ => {}

1201

1202

1203

41783

    row.sat_encoding_amo = families

1204

41783

        .remove("amo")

1205

41783

        .unwrap_or_default()

1206

41783

        .into_iter()

1207

41783

        .collect();

1208

41783

    row.sat_encoding_cardinality = families

1209

41783

        .remove("cardinality")

1210

41783

        .unwrap_or_default()

1211

41783

        .into_iter()

1212

41783

        .collect();

1213

41783

    row.sat_encoding_pb = families

1214

41783

        .remove("pb")

1215

41783

        .unwrap_or_default()

1216

41783

        .into_iter()

1217

41783

        .collect();

1218

41783

    row.sat_encoding_table = families

1219

41783

        .remove("table")

1220

41783

        .unwrap_or_default()

1221

41783

        .into_iter()

1222

41783

        .collect();

1223

41783

    row.sat_encoding_element = families

1224

41783

        .remove("element")

1225

41783

        .unwrap_or_default()

1226

41783

        .into_iter()

1227

41783

        .collect();

1228

41783

    row.sat_encoding_alldifferent = families

1229

41783

        .remove("alldifferent")

1230

41783

        .unwrap_or_default()

1231

41783

        .into_iter()

1232

41783

        .collect();

1233

41783

1234

1235

/// Reports whether the search stopped early because it hit a numeric `number-of-solutions` limit.

1236

///

1237

/// Once the search is cut short, the solutions found are an arbitrary subset of the full solution

1238

/// set: two runs that enumerate in different orders keep different subsets of the same size. Set

1239

/// comparisons are meaningless in that case, so callers fall back to comparing counts. `count` is

1240

/// the largest number of solutions any of the runs being compared found; a run that finished below

1241

/// the limit searched exhaustively, and its solutions remain comparable.

1242

41308

fn search_was_truncated(number_of_solutions: NumberOfSolutions, count: usize) -> bool {

1243

41308

    match number_of_solutions {

1244

885

        NumberOfSolutions::Limit(limit) if limit > 0 => count >= limit as usize,

1245

40423

        _ => false,

1246

1247

41308

1248

1249

/// Describes the configured solution limit for assertion messages.

1250

fn solution_limit_description(number_of_solutions: NumberOfSolutions) -> String {

1251

    match number_of_solutions {

1252

        NumberOfSolutions::All => "all".to_string(),

1253

        NumberOfSolutions::Limit(limit) => limit.to_string(),

1254

        NumberOfSolutions::Skip => "skip".to_string(),

1255

1256

1257

1258

/// Counts the solutions in a rendered Essence solutions artefact.

1259

1762

fn count_essence_solutions(rendered: &str) -> usize {

1260

1762

    rendered

1261

1762

        .lines()

1262

11896

        .filter(|line| line.starts_with("$ Solution:"))

1263

        .count()

1264

1762

1265

1266

1562

fn run_case_name(

1267

1562

    parser: Parser,

1268

1562

    rewriter: Rewriter,

1269

1562

    comprehension_expander: QuantifiedExpander,

1270

1562

    heuristic: Heuristic,

1271

1562

    channelling: Channelling,

1272

1562

    seed: u64,

1273

1562

    solver_seed: u32,

1274

1562

    distinguish_rewriter: bool,

1275

1562

    distinguish_heuristic: bool,

1276

1562

    distinguish_channelling: bool,

1277

1562

) -> String {

1278

1562

    let mut name = format!("{parser}-{comprehension_expander}");

1279

1562

    if distinguish_rewriter {

1280

        name.push_str(&format!("-{rewriter}"));

1281

1562

1282

1562

    if distinguish_heuristic {

1283

210

        name.push_str(&format!("-heuristic-{heuristic}"));

1284

1352

1285

1562

    if heuristic == Heuristic::Random {

1286

        name.push_str(&format!("-seed-{seed}"));

1287

1562

1288

1562

    if solver_seed != 0 {

1289

        name.push_str(&format!("-solver-seed-{solver_seed}"));

1290

1562

1291

1562

    if distinguish_channelling {

1292

1134

        name.push_str(&format!("-channelling-{channelling}"));

1293

428

1294

1562

    name

1295

1562

1296

1297

/// Advances a depth-first mixed-radix branch path using the choices observed during the latest

1298

/// replay. Earlier branches are replayed from a freshly parsed model, so no mutable AST state is

1299

/// shared between generated models.

1300

41573

fn next_all_choice_path(decisions: &[HeuristicChoice]) -> Option<Vec<usize>> {

1301

41573

    for decision_index in (0..decisions.len()).rev() {

1302

48703

        let decision = &decisions[decision_index];

1303

48703

        if decision.selected + 1 >= decision.options.len() {

1304

8482

            continue;

1305

40221

1306

40221

        let mut next: Vec<_> = decisions[..decision_index]

1307

40221

            .iter()

1308

89072

            .map(|decision| decision.selected)

1309

            .collect();

1310

40221

        next.push(decision.selected + 1);

1311

40221

        return Some(next);

1312

1313

1352

    None

1314

41573

1315

1316

/// Returns the expected snapshot files for an executed exhaustive run case.

1317

41783

fn expected_exhaustive_files_for_case(

1318

41783

    case_name: &str,

1319

41783

    solver: SolverFamily,

1320

41783

    trace_level: TraceLevel,

1321

41783

    per_run_solutions: bool,

1322

41783

) -> BTreeSet<String> {

1323

41783

    let solver_name = solver.as_str();

1324

41783

    let mut files = BTreeSet::new();

1325

41783

    if per_run_solutions {

1326

881

        files.insert(format!("{case_name}-{solver_name}.expected.solutions"));

1327

40902

1328

41783

    if trace_level == TraceLevel::Full {

1329

1573

        files.insert(format!("{case_name}-{solver_name}-expected-rule-trace.txt"));

1330

40210

1331

41783

    files

1332

41783

1333

1334

fn collect_rule_trace_aggregates(

1335

    path: &Path,

1336

    case_name: &str,

1337

    solver: SolverFamily,

1338

) -> Result<RecordedRuleTraceStats, std::io::Error> {

1339

    let mut aggregates = RecordedRuleTraceStats::default();

1340

    let trace_path = path.join(format!(

1341

        "{case_name}-{}-generated-rule-trace.txt",

1342

        solver.as_str()

1343

));

1344

    let trace = fs::read_to_string(trace_path)?;

1345

    let mut applications = 0;

1346

    for line in trace.lines() {

1347

        let Some((_, rule_and_sets)) = line.split_once("~~>") else {

1348

            continue;

1349

};

1350

        let rule_name = rule_and_sets

1351

            .trim()

1352

            .split_once(' ')

1353

            .map_or_else(|| rule_and_sets.trim(), |(rule, _)| rule);

1354

        if rule_name.is_empty() {

1355

            continue;

1356

1357

        applications += 1;

1358

        *aggregates.rules.entry(rule_name.to_string()).or_insert(0) += 1;

1359

1360

    aggregates.total_rule_applications = Some(applications);

1361

    Ok(aggregates)

1362

1363

1364

fn collect_rule_attempts(

1365

    path: &Path,

1366

    case_name: &str,

1367

    solver: SolverFamily,

1368

) -> Result<u64, std::io::Error> {

1369

    let stats_path = path.join(format!("{case_name}-{}-stats.json", solver.as_str()));

1370

    let contents = match fs::read_to_string(stats_path) {

1371

        Ok(contents) => contents,

1372

        // Failed runs may not have reached the stats-writing stage.

1373

        Err(err) if err.kind() == std::io::ErrorKind::NotFound => return Ok(0),

1374

        Err(err) => return Err(err),

1375

};

1376

    let stats: JsonValue = serde_json::from_str(&contents)

1377

        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidData, err))?;

1378

    Ok(stats

1379

        .get("stats")

1380

        .and_then(|stats| stats.get("rewriterRuns"))

1381

        .and_then(JsonValue::as_array)

1382

        .into_iter()

1383

        .flatten()

1384

        .filter_map(|run| {

1385

            run.get("rewriterRuleApplicationAttempts")

1386

                .and_then(JsonValue::as_u64)

1387

})

1388

        .sum())

1389

1390

1391

fn clean_test_dir_for_accept(

1392

    path: &str,

1393

    essence_base: &str,

1394

    extension: &str,

1395

    preserve_shared_solutions: bool,

1396

) -> Result<(), std::io::Error> {

1397

    let input_filename = format!("{essence_base}.{extension}");

1398

1399

    for entry in std::fs::read_dir(path)? {

1400

        let entry = entry?;

1401

        let file_name = entry.file_name();

1402

        let file_name = file_name.to_string_lossy();

1403

        let entry_path = entry.path();

1404

1405

        if file_name == input_filename

1406

            || file_name == "config.toml"

1407

            // Preserve the shared golden until all configurations pass acceptance.

1408

            || (preserve_shared_solutions

1409

                && file_name == format!("{essence_base}.expected.solutions"))

1410

            || file_name == "stats.toml"

1411

            || file_name == DIAGNOSTICS_DIR

1412

            || file_name == "input.param.json"

1413

            || entry_path.extension().is_some_and(|ext| ext == "param")

1414

1415

            continue;

1416

1417

1418

        if entry_path.is_dir() {

1419

            std::fs::remove_dir_all(entry_path)?;

1420

        } else {

1421

            std::fs::remove_file(entry_path)?;

1422

1423

1424

1425

    Ok(())

1426

1427

1428

fn copy_human_trace_generated_to_expected(

1429

    path: &str,

1430

    test_name: &str,

1431

    solver: SolverFamily,

1432

) -> Result<(), std::io::Error> {

1433

    let solver_name = solver.as_str();

1434

1435

    let generated_path = format!("{path}/{test_name}-{solver_name}-generated-rule-trace.txt");

1436

    let expected_path = format!("{path}/{test_name}-{solver_name}-expected-rule-trace.txt");

1437

    let generated_trace = fs::read_to_string(generated_path)?;

1438

    if generated_trace.chars().count() <= DEFAULT_TEXT_SNAPSHOT_CHARACTER_LIMIT {

1439

        fs::write(expected_path, generated_trace)?;

1440

        return Ok(());

1441

1442

1443

    let expected_trace =

1444

        truncate_to_first_chars(&generated_trace, DEFAULT_TEXT_SNAPSHOT_CHARACTER_LIMIT);

1445

    fs::write(expected_path, format!("{expected_trace}\n"))?;

1446

    Ok(())

1447

1448

1449

fn record_exhaustive_failure(

1450

    test_dir: &str,

1451

    record: FailureRecord,

1452

    number_of_solutions: NumberOfSolutions,

1453

    conjure_captured: bool,

1454

) {

1455

    let Some((essence_base, extension)) = essence_file_in_test_dir(test_dir) else {

1456

        return;

1457

};

1458

    let model_path = format!("{test_dir}/{essence_base}.{extension}");

1459

    let param_file = param_file_in_test_dir(test_dir);

1460

    let test_path = Path::new(test_dir);

1461

    let _ = write_failure_record(test_path, &record);

1462

    if !conjure_captured && let Some(number_of_solutions) = number_of_solutions.as_solver_limit() {

1463

        let _ = capture_conjure_reference(

1464

            test_path,

1465

            &model_path,

1466

            param_file.as_deref(),

1467

            number_of_solutions,

1468

);

1469

1470

1471

1472

fn capture_conjure_reference(

1473

    test_dir: &Path,

1474

    model_path: &str,

1475

    param_file: Option<&str>,

1476

    number_of_solutions: i32,

1477

) -> Result<(), Box<dyn Error>> {

1478

    let out_dir = conjure_artifacts_dir(test_dir);

1479

    fs::create_dir_all(&out_dir)?;

1480

    let context: Arc<RwLock<Context<'static>>> = Default::default();

1481

    get_solutions_from_conjure_with_stats(

1482

        model_path,

1483

        param_file,

1484

        context,

1485

        number_of_solutions,

1486

        ConjureSolveCaptureOptions {

1487

            artifact_dir: Some(out_dir),

1488

            savilerow_options: Some("-O0".to_string()),

1489

},

1490

)?;

1491

    Ok(())

1492

1493

1494

41783

fn parse_unified_problem_model(

1495

41783

    path: &str,

1496

41783

    essence_base: &str,

1497

41783

    extension: &str,

1498

41783

    parser: Parser,

1499

41783

    param_file: Option<&str>,

1500

41783

    context: Arc<RwLock<Context<'static>>>,

1501

41783

) -> Result<Model, Box<dyn Error>> {

1502

41783

    let file_path = format!("{path}/{essence_base}.{extension}");

1503

1504

1505

41783

        let mut ctx = context.as_ref().write().unwrap();

1506

41783

        ctx.essence_file_name = Some(file_path.clone());

1507

41783

        ctx.param_file_name = param_file.map(str::to_string);

1508

1509

1510

41783

    let problem_model = match parser {

1511

41779

        Parser::TreeSitter => parse_essence_file_native(&file_path, context.clone())?,

1512

4

        Parser::ViaConjure => parse_essence_file(&file_path, context.clone())?,

1513

};

1514

1515

41783

    let Some(param_path) = param_file else {

1516

35984

        let mut problem_model = problem_model;

1517

35984

        validate_instantiation_conditions(&mut problem_model)?;

1518

35984

        return Ok(problem_model);

1519

};

1520

1521

5799

    let param_model = if param_path.ends_with(".json") {

1522

292

        let domains = domains_from_model(&problem_model);

1523

        let assignments =

1524

292

            params_from_simplified_json_str(&fs::read_to_string(param_path)?, &domains)?;

1525

292

        param_model_from_assignments(assignments, &domains, context)

1526

    } else {

1527

5507

        match parser {

1528

5507

            Parser::TreeSitter => parse_essence_file_native(param_path, context)?,

1529

            Parser::ViaConjure => parse_essence_file(param_path, context)?,

1530

1531

};

1532

1533

5799

    Ok(instantiate_model(problem_model, param_model)?)

1534

41783

1535

1536

fn essence_file_in_test_dir(test_dir: &str) -> Option<(String, String)> {

1537

    fs::read_dir(test_dir).ok().and_then(|entries| {

1538

        entries.filter_map(Result::ok).find_map(|entry| {

1539

            let path = entry.path();

1540

            let extension = path.extension()?.to_str()?;

1541

            if extension != "essence" {

1542

                return None;

1543

1544

            Some((

1545

                path.file_stem()?.to_str()?.to_string(),

1546

                extension.to_string(),

1547

))

1548

})

1549

})

1550

1551

1552

fn copy_oxide_run_artifacts(path: &str, run_case: RunCase<'_>, message: &str) {

1553

    let test_dir = Path::new(path);

1554

    let _ = write_oxide_failure_text(test_dir, run_case.case_name, message);

1555

    let solver = run_case.solver.as_str();

1556

    let case_name = run_case.case_name;

1557

    let oxide_dir = oxide_artifacts_dir(test_dir);

1558

    let _ = copy_file_if_exists(

1559

        &test_dir.join(format!("{case_name}-{solver}-generated-rule-trace.txt")),

1560

        &oxide_dir.join(format!("{case_name}-{solver}-generated-rule-trace.txt")),

1561

);

1562

    let _ = copy_file_if_exists(

1563

        &test_dir.join(format!("{case_name}-{solver}.generated.solutions")),

1564

        &oxide_dir.join(format!("{case_name}-{solver}.generated.solutions")),

1565

);

1566

1567

1568

fn try_capture_oxide_minion(

1569

    path: &str,

1570

    essence_base: &str,

1571

    extension: &str,

1572

    run_case: RunCase<'_>,

1573

    minion_discrete_threshold: usize,

1574

) -> Result<(), Box<dyn Error>> {

1575

    if !matches!(run_case.solver, SolverFamily::Minion) {

1576

        return Ok(());

1577

1578

1579

    let context: Arc<RwLock<Context<'static>>> = Default::default();

1580

    set_current_parser(run_case.parser);

1581

    set_current_rewriter(run_case.rewriter);

1582

    set_comprehension_expander(run_case.comprehension_expander);

1583

    set_current_solver_family(run_case.solver);

1584

    set_minion_discrete_threshold(Some(minion_discrete_threshold));

1585

    set_heuristic(run_case.heuristic);

1586

    set_heuristic_seed(run_case.seed);

1587

    set_channelling(run_case.channelling);

1588

    if run_case.heuristic == Heuristic::All {

1589

        begin_heuristic_all_choices(run_case.choice_path.to_vec());

1590

1591

1592

    let parsed_model = parse_unified_problem_model(

1593

        path,

1594

        essence_base,

1595

        extension,

1596

        run_case.parser,

1597

        param_file_in_test_dir(path).as_deref(),

1598

        context.clone(),

1599

)?;

1600

1601

    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();

1602

    rules_to_load.extend(run_case.extra_rule_sets.iter().map(String::as_str));

1603

    let rule_sets = resolve_rule_sets(run_case.solver, &rules_to_load)?;

1604

1605

    let Rewriter::Rewrite(config) = run_case.rewriter;

1606

    let rewritten_model = rewrite_model(&parsed_model, &rule_sets, config)?;

1607

1608

    let minion_path = oxide_artifacts_dir(Path::new(path)).join(format!(

1609

        "{}-{}.minion",

1610

        run_case.case_name,

1611

        run_case.solver.as_str()

1612

));

1613

    if let Some(parent) = minion_path.parent() {

1614

        fs::create_dir_all(parent)?;

1615

1616

    let solver = Solver::new(Minion::default().with_solver_seed(run_case.solver_seed))

1617

        .load_model(rewritten_model)?;

1618

    let mut file: Box<dyn std::io::Write> = Box::new(File::create(&minion_path)?);

1619

    solver.write_solver_input_file(&mut file)?;

1620

    Ok(())

1621

1622

1623

#[test]

1624

1

fn assert_conjure_present() {

1625

1

    conjure_cp_cli::find_conjure::conjure_executable().unwrap();

1626

1

1627

1628

include!(concat!(env!("OUT_DIR"), "/gen_tests.rs"));