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 tests_integration::AcceptMode;
39
use tests_integration::TestConfig;
40
use tests_integration::golden_files::assert_no_redundant_expected_files;
41
use tests_integration::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
2275
fn run_case_label(
53
2275
    path: &str,
54
2275
    essence_base: &str,
55
2275
    extension: &str,
56
2275
    run_case: RunCase<'_>,
57
2275
) -> String {
58
2275
    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
2275
        run_case.solver.as_str()
64
    )
65
2275
}
66

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

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

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

            
83
299
    let config = file_config;
84

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

            
88
299
    let parsers = config
89
299
        .configured_parsers()
90
299
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
91
299
    let rewriters = config
92
299
        .configured_rewriters()
93
299
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
94
299
    let comprehension_expanders = config
95
299
        .configured_comprehension_expanders()
96
299
        .map_err(|err| std::io::Error::new(std::io::ErrorKind::InvalidInput, err))?;
97
299
    let solvers = config
98
299
        .configured_solvers()
99
299
        .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
299
    let model_path = format!("{path}/{essence_base}.{extension}");
103
299
    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
299
        if accept && !validate_with_conjure {
114
            eprintln!("[integration] skipping Conjure validation for {model_path}");
115
299
        }
116
299
        None
117
    };
118
299
    let mut allowed_expected_files = BTreeSet::new();
119

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

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

            
181
299
    if accept_mode.records_expected_time() {
182
        let expected_time = round_expected_time(started_at.elapsed());
183
        let config_path = Path::new(path).join("config.toml");
184
        upsert_expected_time_config(&config_path, expected_time)?;
185
299
    }
186

            
187
299
    Ok(())
188
299
}
189

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

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

            
239
2275
    set_current_parser(parser);
240
2275
    set_current_rewriter(rewriter);
241
2275
    set_comprehension_expander(comprehension_expander);
242
2275
    set_current_solver_family(solver_fam);
243
2275
    set_minion_discrete_threshold(minion_discrete_threshold);
244

            
245
    // File path
246
2275
    let file_path = format!("{path}/{essence_base}.{extension}");
247

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

            
260
2275
    if let SolverFamily::Sat(sat_encoding) = solver_fam {
261
706
        extra_rules.push(sat_encoding.as_rule_set());
262
1569
    }
263

            
264
2275
    let mut rules_to_load = DEFAULT_RULE_SETS.to_vec();
265
2275
    rules_to_load.extend(extra_rules);
266

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

            
269
2275
    let model = parsed_model;
270

            
271
2275
    let rewritten_model = match rewriter {
272
1165
        Rewriter::Naive => rewrite_naive(&model, &rule_sets, false)?,
273
1110
        Rewriter::Morph(config) => rewrite_morph(model, &rule_sets, false, config),
274
    };
275
2275
    let solver_input_file = None;
276
2275
    let solver = match solver_fam {
277
1093
        SolverFamily::Minion => Solver::new(Minion::default()),
278
706
        SolverFamily::Sat(_) => Solver::new(Sat::default()),
279

            
280
476
        SolverFamily::Smt(_) => Solver::new(Smt::default()),
281
    };
282

            
283
2275
    let solutions = {
284
2275
        let solved = get_solutions(solver, rewritten_model, 0, &solver_input_file, false)?;
285
2275
        save_solutions_json(&solved, path, case_name, solver_fam)?;
286
2275
        solved
287
    };
288

            
289
    // Stage 3b: Check solutions against Conjure when accept mode is enabled and validation is enabled.
290
2275
    if accept && conjure_solutions.is_some() {
291
        let conjure_solutions = conjure_solutions
292
            .as_deref()
293
            .expect("conjure solutions should be present when Conjure validation is enabled");
294

            
295
        let username_solutions = normalize_solutions_for_comparison(&solutions);
296
        let conjure_solutions = normalize_solutions_for_comparison(conjure_solutions);
297

            
298
        let mut conjure_solutions_json = solutions_to_json(&conjure_solutions);
299
        let mut username_solutions_json = solutions_to_json(&username_solutions);
300

            
301
        conjure_solutions_json.sort_all_objects();
302
        username_solutions_json.sort_all_objects();
303

            
304
        assert_eq!(
305
            username_solutions_json, conjure_solutions_json,
306
            "Solutions (<) do not match conjure (>)!"
307
        );
308
2275
    }
309

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

            
318
    // Check Stage 3a (solutions)
319
2275
    let expected_solutions_json = read_solutions_json(path, case_name, "expected", solver_fam)?;
320
2275
    let username_solutions_json = solutions_to_json(&solutions);
321
2275
    assert_eq!(username_solutions_json, expected_solutions_json);
322

            
323
    // TODO: Implement rule trace validation for morph
324
2275
    match rewriter {
325
1110
        Rewriter::Morph(_) => {}
326
        Rewriter::Naive => {
327
1165
            let generated = read_default_rule_trace(path, case_name, "generated", &solver_fam)?;
328
1165
            let expected = read_default_rule_trace(path, case_name, "expected", &solver_fam)?;
329

            
330
1165
            assert_eq!(
331
                expected, generated,
332
                "Generated rule trace does not match the expected trace!"
333
            );
334
        }
335
    }
336

            
337
2275
    save_stats_json(context, path, case_name, solver_fam)?;
338

            
339
2275
    Ok(())
340
2275
}
341

            
342
2275
fn run_case_name(
343
2275
    parser: Parser,
344
2275
    rewriter: Rewriter,
345
2275
    comprehension_expander: QuantifiedExpander,
346
2275
) -> String {
347
2275
    format!("{parser}-{rewriter}-{comprehension_expander}")
348
2275
}
349

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

            
359
fn clean_test_dir_for_accept(
360
    path: &str,
361
    essence_base: &str,
362
    extension: &str,
363
) -> Result<(), std::io::Error> {
364
    let input_filename = format!("{essence_base}.{extension}");
365

            
366
    for entry in std::fs::read_dir(path)? {
367
        let entry = entry?;
368
        let file_name = entry.file_name();
369
        let file_name = file_name.to_string_lossy();
370
        let entry_path = entry.path();
371

            
372
        if file_name == input_filename || file_name == "config.toml" {
373
            continue;
374
        }
375

            
376
        if entry_path.is_dir() {
377
            std::fs::remove_dir_all(entry_path)?;
378
        } else {
379
            std::fs::remove_file(entry_path)?;
380
        }
381
    }
382

            
383
    Ok(())
384
}
385

            
386
fn copy_human_trace_generated_to_expected(
387
    path: &str,
388
    test_name: &str,
389
    solver: SolverFamily,
390
) -> Result<(), std::io::Error> {
391
    let solver_name = solver.as_str();
392

            
393
    std::fs::copy(
394
        format!("{path}/{test_name}-{solver_name}-generated-rule-trace.txt"),
395
        format!("{path}/{test_name}-{solver_name}-expected-rule-trace.txt"),
396
    )?;
397
    Ok(())
398
}
399

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

            
409
    std::fs::copy(
410
        format!("{path}/{test_name}-{marker}.generated-{stage}.{extension}"),
411
        format!("{path}/{test_name}-{marker}.expected-{stage}.{extension}"),
412
    )?;
413
    Ok(())
414
}
415

            
416
#[test]
417
1
fn assert_conjure_present() {
418
1
    conjure_cp_cli::find_conjure::conjure_executable().unwrap();
419
1
}
420

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