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_morph, rewrite_naive};
7
use conjure_cp::solver::Solver;
8
use conjure_cp::solver::adaptors::*;
9
use conjure_cp_cli::utils::testing::{normalize_solutions_for_comparison, read_default_rule_trace};
10
use std::collections::{BTreeMap, BTreeSet};
11
use std::error::Error;
12
use std::fs;
13
use std::fs::File;
14
use std::path::Path;
15
use std::time::Instant;
16
use tracing_subscriber::{Layer, filter::EnvFilter, filter::FilterFn, fmt, layer::SubscriberExt};
17

            
18
use std::sync::Arc;
19
use std::sync::RwLock;
20

            
21
use conjure_cp::ast::{Literal, Name};
22
use conjure_cp::context::Context;
23
use conjure_cp::parse::tree_sitter::parse_essence_file;
24
use conjure_cp::rule_engine::resolve_rule_sets;
25
use conjure_cp::settings::{
26
    Parser, QuantifiedExpander, Rewriter, SolverFamily, set_comprehension_expander,
27
    set_current_parser, set_current_rewriter, set_current_solver_family,
28
    set_default_rule_trace_enabled, set_minion_discrete_threshold,
29
    set_rule_trace_aggregates_enabled, set_rule_trace_enabled, set_rule_trace_verbose_enabled,
30
};
31
use conjure_cp_cli::utils::conjure::solutions_to_json;
32
use conjure_cp_cli::utils::conjure::{get_solutions, get_solutions_from_conjure};
33
use conjure_cp_cli::utils::testing::save_stats_json;
34
use conjure_cp_cli::utils::testing::{read_solutions_json, save_solutions_json};
35
#[allow(clippy::single_component_path_imports, unused_imports)]
36
use conjure_cp_rules;
37
use pretty_assertions::assert_eq;
38
use test_suite::AcceptMode;
39
use test_suite::TestConfig;
40
use test_suite::golden_files::assert_no_redundant_expected_files;
41
use test_suite::test_config::{round_expected_time, upsert_expected_time_config};
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
2271
fn run_case_label(
53
2271
    path: &str,
54
2271
    essence_base: &str,
55
2271
    extension: &str,
56
2271
    run_case: RunCase<'_>,
57
2271
) -> String {
58
2271
    format!(
59
        "test_dir={path}, model={essence_base}.{extension}, parser={}, rewriter={}, comprehension_expander={}, solver={}",
60
        run_case.parser,
61
        run_case.rewriter,
62
        run_case.comprehension_expander,
63
2271
        run_case.solver.as_str()
64
    )
65
2271
}
66

            
67
298
fn integration_test(path: &str, essence_base: &str, extension: &str) -> Result<(), Box<dyn Error>> {
68
298
    let accept_mode = AcceptMode::from_env();
69
298
    let accept = accept_mode.accepts_outputs();
70
298
    let started_at = Instant::now();
71

            
72
298
    if accept {
73
        clean_test_dir_for_accept(path, essence_base, extension)?;
74
298
    }
75

            
76
298
    let file_config: TestConfig =
77
298
        if let Ok(config_contents) = fs::read_to_string(format!("{path}/config.toml")) {
78
298
            toml::from_str(&config_contents).unwrap()
79
        } else {
80
            Default::default()
81
        };
82

            
83
298
    let config = file_config;
84

            
85
298
    let validate_with_conjure = config.validate_with_conjure;
86
298
    let minion_discrete_threshold = config.minion_discrete_threshold;
87

            
88
298
    let parsers = config
89
298
        .configured_parsers()
90
298
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
91
298
    let rewriters = config
92
298
        .configured_rewriters()
93
298
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
94
298
    let comprehension_expanders = config
95
298
        .configured_comprehension_expanders()
96
298
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
97
298
    let solvers = config
98
298
        .configured_solvers()
99
298
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
100

            
101
    // Conjure output depends only on the input model, so cache it once per test case.
102
298
    let model_path = format!("{path}/{essence_base}.{extension}");
103
298
    let conjure_solutions = if accept && validate_with_conjure {
104
        eprintln!("[integration] loading Conjure reference solutions for {model_path}");
105
        Some(Arc::new(
106
            get_solutions_from_conjure(&model_path, None, Default::default()).map_err(|err| {
107
                std::io::Error::other(format!(
108
                    "failed to fetch Conjure reference solutions for {model_path}: {err}"
109
                ))
110
            })?,
111
        ))
112
    } else {
113
298
        if accept && !validate_with_conjure {
114
            eprintln!("[integration] skipping Conjure validation for {model_path}");
115
298
        }
116
298
        None
117
    };
118
298
    let mut allowed_expected_files = BTreeSet::new();
119

            
120
579
    for parser in parsers.iter().copied() {
121
1139
        for rewriter in rewriters.clone() {
122
1265
            for comprehension_expander in comprehension_expanders.clone() {
123
2271
                for solver in solvers.clone() {
124
2271
                    let case_name = run_case_name(parser, rewriter, comprehension_expander);
125
2271
                    let run_case = RunCase {
126
2271
                        parser,
127
2271
                        rewriter,
128
2271
                        comprehension_expander,
129
2271
                        solver,
130
2271
                        case_name: case_name.as_str(),
131
2271
                    };
132
2271
                    let file = File::create(format!(
133
                        "{path}/{}-{}-generated-rule-trace.txt",
134
                        run_case.case_name,
135
2271
                        run_case.solver.as_str()
136
                    ))?;
137
2271
                    let subscriber = Arc::new(
138
2271
                        tracing_subscriber::registry().with(
139
2271
                            fmt::layer()
140
2271
                                .with_writer(file)
141
2271
                                .with_level(false)
142
2271
                                .without_time()
143
2271
                                .with_target(false)
144
2271
                                .with_filter(EnvFilter::new("rule_engine_rule_trace=trace"))
145
50983
                                .with_filter(FilterFn::new(|meta| {
146
50983
                                    meta.target() == "rule_engine_rule_trace"
147
50983
                                })),
148
                        ),
149
                    )
150
2271
                        as Arc<dyn tracing::Subscriber + Send + Sync>;
151
2271
                    let run_label = run_case_label(path, essence_base, extension, run_case);
152
2271
                    eprintln!("[integration] running {run_label}");
153
2271
                    let default_rule_trace_enabled = matches!(rewriter, Rewriter::Naive);
154
2271
                    set_rule_trace_enabled(true);
155
2271
                    set_default_rule_trace_enabled(default_rule_trace_enabled);
156
2271
                    set_rule_trace_verbose_enabled(false);
157
2271
                    set_rule_trace_aggregates_enabled(false);
158
2271
                    tracing::subscriber::with_default(subscriber, || {
159
2271
                        integration_test_inner(
160
2271
                            path,
161
2271
                            essence_base,
162
2271
                            extension,
163
2271
                            run_case,
164
2271
                            minion_discrete_threshold,
165
2271
                            conjure_solutions.clone(),
166
2271
                            accept,
167
                        )
168
2271
                    })
169
2271
                    .map_err(|err| std::io::Error::other(format!("{run_label}: {err}")))?;
170
2271
                    allowed_expected_files.extend(expected_integration_files_for_case(
171
2271
                        run_case.case_name,
172
2271
                        solver,
173
                    ));
174
                }
175
            }
176
        }
177
    }
178

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

            
181
298
    if accept_mode.records_expected_time() {
182
        let observed_expected_time = round_expected_time(started_at.elapsed());
183
        let config_path = Path::new(path).join("config.toml");
184
        if let Some(expected_time) =
185
            accept_mode.expected_time_to_record(config.expected_time, observed_expected_time)
186
        {
187
            upsert_expected_time_config(&config_path, expected_time)?;
188
        }
189
298
    }
190

            
191
298
    Ok(())
192
298
}
193

            
194
/// Runs an integration test for a given Conjure model by:
195
/// 1. Parsing the model from an Essence file.
196
/// 2. Rewriting the model according to predefined rule sets.
197
/// 3. Solving the model using the Minion solver and validating the solutions.
198
/// 4. Comparing generated rule traces with expected outputs.
199
///
200
/// This function operates in multiple stages:
201
///
202
/// - **Parsing Stage**
203
///   - **Stage 1a (Default)**: Reads the Essence model file and verifies that it parses correctly using `parser = "tree-sitter"`.
204
///   - **Stage 1b (Optional)**: Reads the Essence model file and verifies that it parses correctly using `parser = "via-conjure"`.
205
///
206
/// - **Rewrite Stage**
207
///   - **Stage 2a**: Applies a set of rules to the parsed model and validates the result.
208
///
209
/// - **Solution Stage**
210
///   - **Stage 3a (Default)**: Uses Minion to solve the model and save the solutions.
211
///   - **Stage 3b (ACCEPT only)**: Compares solutions against Conjure-generated solutions.
212
///
213
/// - **Rule Trace Validation Stage**
214
///   - **Stage 4a (Default)**: Checks that the generated rules match expected traces.
215
///
216
/// # Arguments
217
///
218
/// * `path` - The file path where the Essence model and other resources are located.
219
/// * `essence_base` - The base name of the Essence model file.
220
/// * `extension` - The file extension for the Essence model.
221
///
222
/// # Errors
223
///
224
/// Returns an error if any stage fails due to a mismatch with expected results or file I/O issues.
225
#[allow(clippy::unwrap_used)]
226
2271
fn integration_test_inner(
227
2271
    path: &str,
228
2271
    essence_base: &str,
229
2271
    extension: &str,
230
2271
    run_case: RunCase<'_>,
231
2271
    minion_discrete_threshold: usize,
232
2271
    conjure_solutions: Option<Arc<Vec<BTreeMap<Name, Literal>>>>,
233
2271
    accept: bool,
234
2271
) -> Result<(), Box<dyn Error>> {
235
2271
    let parser = run_case.parser;
236
2271
    let rewriter = run_case.rewriter;
237
2271
    let comprehension_expander = run_case.comprehension_expander;
238
2271
    let solver_fam = run_case.solver;
239
2271
    let case_name = run_case.case_name;
240

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

            
243
2271
    set_current_parser(parser);
244
2271
    set_current_rewriter(rewriter);
245
2271
    set_comprehension_expander(comprehension_expander);
246
2271
    set_current_solver_family(solver_fam);
247
2271
    set_minion_discrete_threshold(minion_discrete_threshold);
248

            
249
    // File path
250
2271
    let file_path = format!("{path}/{essence_base}.{extension}");
251

            
252
    // Stage 1a/1b: Parse the model using the selected parser.
253
2271
    let parsed_model = match parser {
254
        Parser::TreeSitter => {
255
1349
            let mut ctx = context.as_ref().write().unwrap();
256
1349
            ctx.essence_file_name = Some(format!("{path}/{essence_base}.{extension}"));
257
1349
            parse_essence_file_native(&file_path, context.clone())?
258
        }
259
922
        Parser::ViaConjure => parse_essence_file(&file_path, context.clone())?,
260
    };
261
    // Stage 2a: Rewrite the model using the rule engine
262
2271
    let mut extra_rules = vec![];
263

            
264
2271
    if let SolverFamily::Sat(sat_encoding) = solver_fam {
265
706
        extra_rules.push(sat_encoding.as_rule_set());
266
1565
    }
267

            
268
2271
    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();
269
2271
    rules_to_load.extend(extra_rules);
270

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

            
273
2271
    let model = parsed_model;
274

            
275
2271
    let rewritten_model = match rewriter {
276
1163
        Rewriter::Naive => rewrite_naive(&model, &rule_sets, false)?,
277
1108
        Rewriter::Morph(config) => rewrite_morph(model, &rule_sets, false, config),
278
    };
279
2271
    let solver_input_file = None;
280
2271
    let solver = match solver_fam {
281
1089
        SolverFamily::Minion => Solver::new(Minion::default()),
282
706
        SolverFamily::Sat(_) => Solver::new(Sat::default()),
283

            
284
476
        SolverFamily::Smt(_) => Solver::new(Smt::default()),
285
    };
286

            
287
2271
    let solutions = {
288
2271
        let solved = get_solutions(solver, rewritten_model, 0, &solver_input_file, false)?;
289
2271
        save_solutions_json(&solved, path, case_name, solver_fam)?;
290
2271
        solved
291
    };
292

            
293
    // Stage 3b: Check solutions against Conjure when accept mode is enabled and validation is enabled.
294
2271
    if accept && conjure_solutions.is_some() {
295
        let conjure_solutions = conjure_solutions
296
            .as_deref()
297
            .expect("conjure solutions should be present when Conjure validation is enabled");
298

            
299
        let username_solutions = normalize_solutions_for_comparison(&solutions);
300
        let conjure_solutions = normalize_solutions_for_comparison(conjure_solutions);
301

            
302
        let mut conjure_solutions_json = solutions_to_json(&conjure_solutions);
303
        let mut username_solutions_json = solutions_to_json(&username_solutions);
304

            
305
        conjure_solutions_json.sort_all_objects();
306
        username_solutions_json.sort_all_objects();
307

            
308
        assert_eq!(
309
            username_solutions_json, conjure_solutions_json,
310
            "Solutions (<) do not match conjure (>)!"
311
        );
312
2271
    }
313

            
314
    // When accept mode is enabled, copy all generated files to expected
315
2271
    if accept {
316
        // Always overwrite these ones. Unlike the rest, we don't need to selectively do these
317
        // based on the test results, so they don't get done later.
318
        copy_generated_to_expected(path, case_name, "solutions", "json", solver_fam)?;
319
        copy_human_trace_generated_to_expected(path, case_name, solver_fam)?;
320
2271
    }
321

            
322
    // Check Stage 3a (solutions)
323
2271
    let expected_solutions_json = read_solutions_json(path, case_name, "expected", solver_fam)?;
324
2271
    let username_solutions_json = solutions_to_json(&solutions);
325
2271
    assert_eq!(username_solutions_json, expected_solutions_json);
326

            
327
    // TODO: Implement rule trace validation for morph
328
2271
    match rewriter {
329
1108
        Rewriter::Morph(_) => {}
330
        Rewriter::Naive => {
331
1163
            let generated = read_default_rule_trace(path, case_name, "generated", &solver_fam)?;
332
1163
            let expected = read_default_rule_trace(path, case_name, "expected", &solver_fam)?;
333

            
334
1163
            assert_eq!(
335
                expected, generated,
336
                "Generated rule trace does not match the expected trace!"
337
            );
338
        }
339
    }
340

            
341
2271
    save_stats_json(context, path, case_name, solver_fam)?;
342

            
343
2271
    Ok(())
344
2271
}
345

            
346
2271
fn run_case_name(
347
2271
    parser: Parser,
348
2271
    rewriter: Rewriter,
349
2271
    comprehension_expander: QuantifiedExpander,
350
2271
) -> String {
351
2271
    format!("{parser}-{rewriter}-{comprehension_expander}")
352
2271
}
353

            
354
/// Returns the expected snapshot files for an executed integration run case.
355
2271
fn expected_integration_files_for_case(case_name: &str, solver: SolverFamily) -> BTreeSet<String> {
356
2271
    let solver_name = solver.as_str();
357
2271
    BTreeSet::from([
358
2271
        format!("{case_name}-{solver_name}.expected-solutions.json"),
359
2271
        format!("{case_name}-{solver_name}-expected-rule-trace.txt"),
360
2271
    ])
361
2271
}
362

            
363
fn clean_test_dir_for_accept(
364
    path: &str,
365
    essence_base: &str,
366
    extension: &str,
367
) -> Result<(), std::io::Error> {
368
    let input_filename = format!("{essence_base}.{extension}");
369

            
370
    for entry in std::fs::read_dir(path)? {
371
        let entry = entry?;
372
        let file_name = entry.file_name();
373
        let file_name = file_name.to_string_lossy();
374
        let entry_path = entry.path();
375

            
376
        if file_name == input_filename || file_name == "config.toml" {
377
            continue;
378
        }
379

            
380
        if entry_path.is_dir() {
381
            std::fs::remove_dir_all(entry_path)?;
382
        } else {
383
            std::fs::remove_file(entry_path)?;
384
        }
385
    }
386

            
387
    Ok(())
388
}
389

            
390
fn copy_human_trace_generated_to_expected(
391
    path: &str,
392
    test_name: &str,
393
    solver: SolverFamily,
394
) -> Result<(), std::io::Error> {
395
    let solver_name = solver.as_str();
396

            
397
    std::fs::copy(
398
        format!("{path}/{test_name}-{solver_name}-generated-rule-trace.txt"),
399
        format!("{path}/{test_name}-{solver_name}-expected-rule-trace.txt"),
400
    )?;
401
    Ok(())
402
}
403

            
404
fn copy_generated_to_expected(
405
    path: &str,
406
    test_name: &str,
407
    stage: &str,
408
    extension: &str,
409
    solver: SolverFamily,
410
) -> Result<(), std::io::Error> {
411
    let marker = solver.as_str();
412

            
413
    std::fs::copy(
414
        format!("{path}/{test_name}-{marker}.generated-{stage}.{extension}"),
415
        format!("{path}/{test_name}-{marker}.expected-{stage}.{extension}"),
416
    )?;
417
    Ok(())
418
}
419

            
420
#[test]
421
1
fn assert_conjure_present() {
422
1
    conjure_cp_cli::find_conjure::conjure_executable().unwrap();
423
1
}
424

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