Grcov report - integration

1

#![allow(clippy::expect_used)]

2

use conjure_cp::bug;

3

use conjure_cp::rule_engine::get_rules_grouped;

4

5

use conjure_cp::defaults::DEFAULT_RULE_SETS;

6

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

7

use conjure_cp::rule_engine::rewrite_naive;

8

use conjure_cp::solver::Solver;

9

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

10

use conjure_cp_cli::utils::testing::{normalize_solutions_for_comparison, read_human_rule_trace};

11

use itertools::Itertools;

12

use std::collections::BTreeMap;

13

use std::env;

14

use std::error::Error;

15

use std::fs;

16

use std::fs::File;

17

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

18

use tree_morph::{helpers::select_panic, prelude::*};

19

20

#[cfg(feature = "smt")]

21

use conjure_cp::solver::adaptors::smt::TheoryConfig;

22

23

use std::sync::Arc;

24

use std::sync::RwLock;

25

26

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

27

use conjure_cp::context::Context;

28

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

29

use conjure_cp::rule_engine::resolve_rule_sets;

30

use conjure_cp::settings::{

31

    Parser, QuantifiedExpander, Rewriter, SolverFamily, set_comprehension_expander,

32

    set_current_parser, set_current_rewriter, set_current_solver_family,

33

};

34

use conjure_cp_cli::utils::conjure::solutions_to_json;

35

use conjure_cp_cli::utils::conjure::{get_solutions, get_solutions_from_conjure};

36

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

37

use conjure_cp_cli::utils::testing::{read_solutions_json, save_solutions_json};

38

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

39

use conjure_cp_rules;

40

use pretty_assertions::assert_eq;

41

use tests_integration::TestConfig;

42

43

#[derive(Clone, Copy, Debug)]

44

struct RunCase<'a> {

45

    parser: Parser,

46

    rewriter: Rewriter,

47

    comprehension_expander: QuantifiedExpander,

48

    solver: SolverFamily,

49

    case_name: &'a str,

50

51

52

632

fn run_case_label(

53

632

    path: &str,

54

632

    essence_base: &str,

55

632

    extension: &str,

56

632

    run_case: RunCase<'_>,

57

632

) -> String {

58

632

    format!(

59

        "test_dir={path}, model={essence_base}.{extension}, parser={}, rewriter={}, comprehension_expander={}, solver={}",

60

        run_case.parser, run_case.rewriter, run_case.comprehension_expander, run_case.solver

61

62

632

63

64

545

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

65

545

    let accept = env::var("ACCEPT").unwrap_or("false".to_string()) == "true";

66

67

545

    if accept {

68

        clean_test_dir_for_accept(path, essence_base, extension)?;

69

545

70

71

545

    let file_config: TestConfig =

72

545

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

73

545

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

74

        } else {

75

            Default::default()

76

};

77

78

545

    let config = file_config;

79

80

545

    let validate_with_conjure = config.validate_with_conjure;

81

82

545

    let parsers = config

83

545

        .configured_parsers()

84

545

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

85

545

    let rewriters = config

86

545

        .configured_rewriters()

87

545

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

88

545

    let comprehension_expanders = config

89

545

        .configured_comprehension_expanders()

90

545

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

91

545

    let solvers = config

92

545

        .configured_solvers()

93

545

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

94

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

95

545

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

96

545

    let conjure_solutions = if accept && validate_with_conjure {

97

        eprintln!("[integration] loading Conjure reference solutions for {model_path}");

98

        Some(Arc::new(

99

            get_solutions_from_conjure(&model_path, Default::default()).map_err(|err| {

100

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

101

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

102

))

103

            })?,

104

))

105

    } else {

106

545

        if accept && !validate_with_conjure {

107

            eprintln!("[integration] skipping Conjure validation for {model_path}");

108

545

109

545

        None

110

};

111

112

583

    for parser in parsers {

113

583

        for rewriter in rewriters.clone() {

114

631

            for comprehension_expander in comprehension_expanders.clone() {

115

632

                for solver in solvers.clone() {

116

632

                    let case_name = run_case_name(parser, rewriter, comprehension_expander);

117

632

                    let run_case = RunCase {

118

632

                        parser,

119

632

                        rewriter,

120

632

                        comprehension_expander,

121

632

                        solver,

122

632

                        case_name: case_name.as_str(),

123

632

};

124

632

                    let file = File::create(format!(

125

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

126

                        run_case.case_name,

127

632

                        run_case.solver.as_str()

128

                    ))?;

129

632

                    let subscriber = Arc::new(

130

632

                        tracing_subscriber::registry().with(

131

632

                            fmt::layer()

132

632

                                .with_writer(file)

133

632

                                .with_level(false)

134

632

                                .without_time()

135

632

                                .with_target(false)

136

632

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

137

53417

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

138

53417

                                    meta.target() == "rule_engine_human"

139

53417

                                })),

140

),

141

142

632

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

143

632

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

144

632

                    eprintln!("[integration] running {run_label}");

145

632

                    tracing::subscriber::with_default(subscriber, || {

146

632

                        integration_test_inner(

147

632

                            path,

148

632

                            essence_base,

149

632

                            extension,

150

632

                            run_case,

151

632

                            conjure_solutions.clone(),

152

632

                            accept,

153

154

632

})

155

632

                    .map_err(|err| std::io::Error::other(format!("{run_label}: {err}")))?;

156

157

158

159

160

161

544

    Ok(())

162

545

163

164

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

165

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

166

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

167

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

168

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

169

///

170

/// This function operates in multiple stages:

171

///

172

/// - **Parsing Stage**

173

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

174

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

175

///

176

/// - **Rewrite Stage**

177

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

178

///

179

/// - **Solution Stage**

180

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

181

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

182

///

183

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

184

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

185

///

186

/// # Arguments

187

///

188

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

189

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

190

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

191

///

192

/// # Errors

193

///

194

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

195

#[allow(clippy::unwrap_used)]

196

632

fn integration_test_inner(

197

632

    path: &str,

198

632

    essence_base: &str,

199

632

    extension: &str,

200

632

    run_case: RunCase<'_>,

201

632

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

202

632

    accept: bool,

203

632

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

204

632

    let parser = run_case.parser;

205

632

    let rewriter = run_case.rewriter;

206

632

    let comprehension_expander = run_case.comprehension_expander;

207

632

    let solver_fam = run_case.solver;

208

632

    let case_name = run_case.case_name;

209

210

632

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

211

212

632

    set_current_parser(parser);

213

632

    set_current_rewriter(rewriter);

214

632

    set_comprehension_expander(comprehension_expander);

215

632

    set_current_solver_family(solver_fam);

216

217

    // File path

218

632

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

219

220

    // Stage 1a/1b: Parse the model using the selected parser.

221

632

    let parsed_model = match parser {

222

        Parser::TreeSitter => {

223

46

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

224

46

            ctx.file_name = Some(format!("{path}/{essence_base}.{extension}"));

225

46

            parse_essence_file_native(&file_path, context.clone())?

226

227

586

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

228

};

229

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

230

632

    let mut extra_rules = vec![];

231

232

632

    if let SolverFamily::Sat(sat_encoding) = solver_fam {

233

2

        extra_rules.push(sat_encoding.as_rule_set());

234

630

235

236

632

    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();

237

632

    rules_to_load.extend(extra_rules);

238

239

632

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

240

241

632

    let mut model = parsed_model;

242

243

632

    let rewritten_model = match rewriter {

244

632

        Rewriter::Naive => rewrite_naive(&model, &rule_sets, false)?,

245

        Rewriter::Morph => {

246

            let submodel = &mut model;

247

            let rules_grouped = get_rules_grouped(&rule_sets)

248

                .unwrap_or_else(|_| bug!("get_rule_priorities() failed!"))

249

                .into_iter()

250

                .map(|(_, rule)| rule.into_iter().map(|f| f.rule).collect_vec())

251

                .collect_vec();

252

253

            let engine = EngineBuilder::new()

254

                .set_selector(select_panic)

255

                .append_rule_groups(rules_grouped)

256

                .build();

257

            let (expr, symbol_table) =

258

                engine.morph(submodel.root().clone(), submodel.symbols().clone());

259

260

            *submodel.symbols_mut() = symbol_table;

261

            submodel.replace_root(expr);

262

            model.clone()

263

264

};

265

632

    let solver_input_file = None;

266

267

632

    let solver = match solver_fam {

268

540

        SolverFamily::Minion => Solver::new(Minion::default()),

269

2

        SolverFamily::Sat(_) => Solver::new(Sat::default()),

270

        #[cfg(feature = "smt")]

271

90

        SolverFamily::Smt(_) => Solver::new(Smt::default()),

272

};

273

274

632

    let solutions = {

275

632

        let solved = get_solutions(solver, rewritten_model, 0, &solver_input_file)?;

276

632

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

277

632

        solved

278

};

279

280

    // Stage 3b: Check solutions against Conjure when ACCEPT=true and validation is enabled.

281

632

    if accept && conjure_solutions.is_some() {

282

        let conjure_solutions = conjure_solutions

283

            .as_deref()

284

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

285

286

        let username_solutions = normalize_solutions_for_comparison(&solutions);

287

        let conjure_solutions = normalize_solutions_for_comparison(conjure_solutions);

288

289

        let mut conjure_solutions_json = solutions_to_json(&conjure_solutions);

290

        let mut username_solutions_json = solutions_to_json(&username_solutions);

291

292

        conjure_solutions_json.sort_all_objects();

293

        username_solutions_json.sort_all_objects();

294

295

        assert_eq!(

296

            username_solutions_json, conjure_solutions_json,

297

            "Solutions (<) do not match conjure (>)!"

298

);

299

632

300

301

    // When ACCEPT=true, copy all generated files to expected

302

632

    if accept {

303

        // Always overwrite these ones. Unlike the rest, we don't need to selectively do these

304

        // based on the test results, so they don't get done later.

305

306

        copy_generated_to_expected(path, case_name, "solutions", "json", Some(solver_fam))?;

307

308

        copy_human_trace_generated_to_expected(path, case_name, solver_fam)?;

309

632

310

311

    // Check Stage 3a (solutions)

312

632

    match solver_fam {

313

        SolverFamily::Minion => {

314

540

            let expected_solutions_json =

315

540

                read_solutions_json(path, case_name, "expected", SolverFamily::Minion)?;

316

540

            let username_solutions_json = solutions_to_json(&solutions);

317

540

            assert_eq!(username_solutions_json, expected_solutions_json);

318

319

        SolverFamily::Sat(_) => {

320

2

            let expected_solutions_json = read_solutions_json(

321

2

                path,

322

2

                case_name,

323

2

                "expected",

324

2

                SolverFamily::Sat(Default::default()),

325

)?;

326

2

            let username_solutions_json = solutions_to_json(&solutions);

327

2

            assert_eq!(username_solutions_json, expected_solutions_json);

328

329

        #[cfg(feature = "smt")]

330

        SolverFamily::Smt(_) => {

331

90

            let expected_solutions_json = read_solutions_json(

332

90

                path,

333

90

                case_name,

334

90

                "expected",

335

90

                SolverFamily::Smt(TheoryConfig::default()),

336

)?;

337

90

            let username_solutions_json = solutions_to_json(&solutions);

338

90

            assert_eq!(username_solutions_json, expected_solutions_json);

339

340

341

342

    // TODO: Implement rule trace validation for morph

343

632

    match rewriter {

344

        Rewriter::Morph => {}

345

        Rewriter::Naive => {

346

632

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

347

632

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

348

349

632

            assert_eq!(

350

                expected, generated,

351

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

352

);

353

354

355

356

631

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

357

358

631

    Ok(())

359

631

360

361

632

fn run_case_name(

362

632

    parser: Parser,

363

632

    rewriter: Rewriter,

364

632

    comprehension_expander: QuantifiedExpander,

365

632

) -> String {

366

632

    format!("{parser}-{rewriter}-{comprehension_expander}")

367

632

368

369

fn clean_test_dir_for_accept(

370

    path: &str,

371

    essence_base: &str,

372

    extension: &str,

373

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

374

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

375

376

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

377

        let entry = entry?;

378

        let file_name = entry.file_name();

379

        let file_name = file_name.to_string_lossy();

380

        let entry_path = entry.path();

381

382

        if file_name == input_filename || file_name == "config.toml" {

383

            continue;

384

385

386

        if entry_path.is_dir() {

387

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

388

        } else {

389

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

390

391

392

393

    Ok(())

394

395

396

fn copy_human_trace_generated_to_expected(

397

    path: &str,

398

    test_name: &str,

399

    solver: SolverFamily,

400

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

401

    let solver_name = solver.as_str();

402

    std::fs::copy(

403

        format!("{path}/{test_name}-{solver_name}-generated-rule-trace.txt"),

404

        format!("{path}/{test_name}-{solver_name}-expected-rule-trace.txt"),

405

)?;

406

    Ok(())

407

408

409

fn copy_generated_to_expected(

410

    path: &str,

411

    test_name: &str,

412

    stage: &str,

413

    extension: &str,

414

    solver: Option<SolverFamily>,

415

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

416

    let marker = solver.map_or("agnostic", |s| s.as_str());

417

418

    std::fs::copy(

419

        format!("{path}/{test_name}-{marker}.generated-{stage}.{extension}"),

420

        format!("{path}/{test_name}-{marker}.expected-{stage}.{extension}"),

421

)?;

422

    Ok(())

423

424

425

#[test]

426

2

fn assert_conjure_present() {

427

2

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

428

2

429

430

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