1use std::collections::{BTreeMap, HashMap, HashSet};
2use std::fmt::Debug;
3use std::path::Path;
4use std::{io, mem, vec};
5
6use conjure_cp::ast::records::Field;
7use conjure_cp::ast::serde::ObjId;
8use itertools::Itertools as _;
9use std::fs::File;
10use std::hash::Hash;
11use std::io::{BufRead, BufReader};
12use std::sync::{Arc, RwLock};
13use uniplate::Uniplate;
14
15use conjure_cp::ast::pretty::pretty_expression_domain_annotation;
16use conjure_cp::ast::{AbstractLiteral, Expression, GroundDomain, Moo, SerdeModel};
17use conjure_cp::context::Context;
18use serde_json::{Error as JsonError, Value as JsonValue};
19
20use conjure_cp::error::Error;
21
22use crate::utils::conjure::solutions_to_essence;
23use crate::utils::json::sort_json_object;
24use crate::utils::misc::to_set;
25use conjure_cp::Model as ConjureModel;
26use conjure_cp::ast::Name::User;
27use conjure_cp::ast::{Literal, Name};
28use conjure_cp::settings::SolverFamily;
29
30pub const REWRITE_SERIALISED_JSON_MAX_LINES: usize = 1000;
32
33pub const DEFAULT_TEXT_SNAPSHOT_CHARACTER_LIMIT: usize = 1_000_000;
35
36fn model_to_json_with_stable_ids(model: &SerdeModel) -> Result<JsonValue, JsonError> {
41 let id_map = model.collect_stable_id_mapping();
43
44 let mut json = serde_json::to_value(model)?;
46
47 replace_ids(&mut json, &id_map);
49
50 Ok(json)
51}
52
53fn replace_ids(value: &mut JsonValue, id_map: &HashMap<ObjId, ObjId>) {
58 match value {
59 JsonValue::Object(map) => {
60 for (k, v) in map.iter_mut() {
65 if (k == "id" || k == "ptr" || k == "parent")
66 && let Ok(old_id) = serde_json::from_value::<ObjId>(mem::take(v))
67 {
68 let new_id = id_map.get(&old_id).expect("all ids to be in the id map");
69 *v = serde_json::to_value(new_id)
70 .expect("serialization of an ObjId to always succeed");
71 }
72 }
73
74 for val in map.values_mut() {
76 replace_ids(val, id_map);
77 }
78 }
79 JsonValue::Array(arr) => {
80 for item in arr {
81 replace_ids(item, id_map);
82 }
83 }
84 _ => {}
85 }
86}
87
88pub fn assert_eq_any_order<T: Eq + Hash + Debug + Clone>(a: &Vec<Vec<T>>, b: &Vec<Vec<T>>) {
89 assert_eq!(a.len(), b.len());
90
91 let mut a_rows: Vec<HashSet<T>> = Vec::new();
92 for row in a {
93 let hash_row = to_set(row);
94 a_rows.push(hash_row);
95 }
96
97 let mut b_rows: Vec<HashSet<T>> = Vec::new();
98 for row in b {
99 let hash_row = to_set(row);
100 b_rows.push(hash_row);
101 }
102
103 for row in a_rows {
104 assert!(b_rows.contains(&row));
105 }
106}
107
108pub fn serialize_model(model: &ConjureModel) -> Result<String, JsonError> {
109 let serde_model: SerdeModel = model.clone().into();
110
111 let json_with_stable_ids = model_to_json_with_stable_ids(&serde_model)?;
113
114 let sorted_json = sort_json_object(&json_with_stable_ids, false);
116
117 serde_json::to_string_pretty(&sorted_json)
119}
120
121pub fn serialize_domains(model: &ConjureModel) -> Result<String, JsonError> {
122 let mut output = String::new();
123 for constraint in model.constraints() {
124 serialize_domains_expr(constraint, 0, &mut output);
125 }
126 Ok(output)
127}
128
129fn serialize_domains_expr(expr: &Expression, depth: usize, output: &mut String) {
130 let domain = expr
131 .domain_of()
132 .map(|domain| domain.to_string())
133 .unwrap_or_else(|| "<unknown>".to_owned());
134 output.push_str(&" ".repeat(depth));
135 output.push_str(&pretty_expression_domain_annotation(expr, domain));
136 output.push('\n');
137
138 for child in expr.children() {
139 serialize_domains_expr(&child, depth + 1, output);
140 }
141}
142
143pub fn save_model_json(
144 model: &ConjureModel,
145 path: &str,
146 test_name: &str,
147 test_stage: &str,
148 solver: SolverFamily,
149) -> Result<(), std::io::Error> {
150 let marker = solver.as_str();
151 let generated_json_str = serialize_model(model)?;
152 let generated_json_str = maybe_truncate_serialised_json(generated_json_str, test_stage);
153 let filename = format!("{path}/{test_name}-{marker}.generated-{test_stage}.serialised.json");
154 println!("saving: {filename}");
155 std::fs::write(filename, format!("{generated_json_str}\n"))?;
156 Ok(())
157}
158
159pub fn save_stats_json(
160 context: Arc<RwLock<Context<'static>>>,
161 path: &str,
162 test_name: &str,
163 solver: SolverFamily,
164) -> Result<(), std::io::Error> {
165 #[allow(clippy::unwrap_used)]
166 let solver_name = solver.as_str();
167
168 let stats = context.read().unwrap().clone();
169 let generated_json = sort_json_object(&serde_json::to_value(stats)?, false);
170
171 let generated_json_str = serde_json::to_string_pretty(&generated_json)?;
173
174 std::fs::write(
175 format!("{path}/{test_name}-{solver_name}-stats.json"),
176 format!("{generated_json_str}\n"),
177 )?;
178
179 Ok(())
180}
181
182fn read_with_path(path: String) -> Result<String, std::io::Error> {
184 std::fs::read_to_string(&path)
185 .map_err(|e| io::Error::new(e.kind(), format!("{e} (path: {path})")))
186}
187
188pub fn read_model_json(
189 ctx: &Arc<RwLock<Context<'static>>>,
190 path: &str,
191 test_name: &str,
192 prefix: &str,
193 test_stage: &str,
194 solver: SolverFamily,
195) -> Result<ConjureModel, std::io::Error> {
196 let marker = solver.as_str();
197 let filepath = format!("{path}/{test_name}-{marker}.{prefix}-{test_stage}.serialised.json");
198 let expected_json_str = std::fs::read_to_string(filepath)?;
199 let expected_model: SerdeModel = serde_json::from_str(&expected_json_str)?;
200
201 Ok(expected_model.initialise(ctx.clone()).unwrap())
202}
203
204pub fn read_model_json_prefix(
206 path: &str,
207 test_name: &str,
208 prefix: &str,
209 test_stage: &str,
210 solver: SolverFamily,
211 max_lines: usize,
212) -> Result<String, std::io::Error> {
213 let marker = solver.as_str();
214 let filename = format!("{path}/{test_name}-{marker}.{prefix}-{test_stage}.serialised.json");
215 println!("reading: {filename}");
216 read_first_n_lines(filename, max_lines)
217}
218
219pub fn minion_solutions_from_json(
220 serialized: &str,
221) -> Result<Vec<HashMap<Name, Literal>>, anyhow::Error> {
222 let json: JsonValue = serde_json::from_str(serialized)?;
223
224 let json_array = json
225 .as_array()
226 .ok_or(Error::Parse("Invalid JSON".to_owned()))?;
227
228 let mut solutions = Vec::new();
229
230 for solution in json_array {
231 let mut sol = HashMap::new();
232 let solution = solution
233 .as_object()
234 .ok_or(Error::Parse("Invalid JSON".to_owned()))?;
235
236 for (var_name, constant) in solution {
237 let constant = match constant {
238 JsonValue::Number(n) => {
239 let n = n
240 .as_i64()
241 .ok_or(Error::Parse("Invalid integer".to_owned()))?;
242 Literal::Int(n as i32)
243 }
244 JsonValue::Bool(b) => Literal::Bool(*b),
245 _ => return Err(Error::Parse("Invalid constant".to_owned()).into()),
246 };
247
248 sol.insert(User(var_name.into()), constant);
249 }
250
251 solutions.push(sol);
252 }
253
254 Ok(solutions)
255}
256
257pub fn save_solutions_essence(
259 solutions: &[BTreeMap<Name, Literal>],
260 path: &str,
261 test_name: &str,
262 solver: SolverFamily,
263) -> Result<String, std::io::Error> {
264 let rendered = solutions_to_essence(solutions);
265 let solver_name = solver.as_str();
266 let filename = format!("{path}/{test_name}-{solver_name}.generated.solutions");
267 std::fs::write(filename, &rendered)?;
268
269 Ok(rendered)
270}
271
272pub fn read_solutions_essence(
273 path: &str,
274 test_name: &str,
275 prefix: &str,
276 solver: SolverFamily,
277) -> Result<String, anyhow::Error> {
278 let solver_name = solver.as_str();
279 let filename = format!("{path}/{test_name}-{solver_name}.{prefix}.solutions");
280 Ok(read_with_path(filename)?)
281}
282
283pub fn read_default_rule_trace(
285 path: &str,
286 test_name: &str,
287 prefix: &str,
288 solver: &SolverFamily,
289) -> Result<String, std::io::Error> {
290 let solver_name = solver.as_str();
291 let filename = format!("{path}/{test_name}-{solver_name}-{prefix}-rule-trace.txt");
292 Ok(truncate_to_first_chars(
293 &read_with_path(filename)?,
294 DEFAULT_TEXT_SNAPSHOT_CHARACTER_LIMIT,
295 ))
296}
297
298#[doc(hidden)]
299pub fn normalize_solutions_for_comparison(
300 input_solutions: &[BTreeMap<Name, Literal>],
301) -> Vec<BTreeMap<Name, Literal>> {
302 let mut normalized = input_solutions.to_vec();
303
304 for solset in &mut normalized {
305 let keys_to_remove: Vec<Name> = solset
307 .keys()
308 .filter(|k| matches!(k, Name::Machine(_)))
309 .cloned()
310 .collect();
311 for k in keys_to_remove {
312 solset.remove(&k);
313 }
314
315 let mut updates = vec![];
316 for (k, v) in solset.clone() {
317 if let Name::User(_) = k {
318 match v {
319 Literal::Bool(true) => updates.push((k, Literal::Int(1))),
320 Literal::Bool(false) => updates.push((k, Literal::Int(0))),
321 Literal::Int(_) => {}
322 Literal::AbstractLiteral(AbstractLiteral::Matrix(elems, _)) => {
323 let mut matrix =
327 AbstractLiteral::Matrix(elems, Moo::new(GroundDomain::Int(vec![])));
328 matrix = matrix.transform(&move |x: AbstractLiteral<Literal>| match x {
329 AbstractLiteral::Matrix(items, _) => {
330 let items = items
331 .into_iter()
332 .map(|x| match x {
333 Literal::Bool(false) => Literal::Int(0),
334 Literal::Bool(true) => Literal::Int(1),
335 x => x,
336 })
337 .collect_vec();
338
339 AbstractLiteral::Matrix(items, Moo::new(GroundDomain::Int(vec![])))
340 }
341 x => x,
342 });
343 updates.push((k, Literal::AbstractLiteral(matrix)));
344 }
345 Literal::AbstractLiteral(AbstractLiteral::Tuple(elems)) => {
346 let mut tuple = AbstractLiteral::Tuple(elems);
349 tuple = tuple.transform(
350 &(move |x: AbstractLiteral<Literal>| match x {
351 AbstractLiteral::Tuple(items) => {
352 let items = items
353 .into_iter()
354 .map(|x| match x {
355 Literal::Bool(false) => Literal::Int(0),
356 Literal::Bool(true) => Literal::Int(1),
357 x => x,
358 })
359 .collect_vec();
360
361 AbstractLiteral::Tuple(items)
362 }
363 x => x,
364 }),
365 );
366 updates.push((k, Literal::AbstractLiteral(tuple)));
367 }
368 Literal::AbstractLiteral(AbstractLiteral::Record(entries)) => {
369 let mut record = AbstractLiteral::Record(entries);
372 record = record.transform(&move |x: AbstractLiteral<Literal>| match x {
373 AbstractLiteral::Record(entries) => {
374 let entries = entries
375 .into_iter()
376 .map(|x| {
377 let Field { name, value } = x;
378 {
379 let value = match value {
380 Literal::Bool(false) => Literal::Int(0),
381 Literal::Bool(true) => Literal::Int(1),
382 x => x,
383 };
384 Field { name, value }
385 }
386 })
387 .collect_vec();
388
389 AbstractLiteral::Record(entries)
390 }
391 x => x,
392 });
393 updates.push((k, Literal::AbstractLiteral(record)));
394 }
395 Literal::AbstractLiteral(AbstractLiteral::Variant(entry)) => {
396 let mut variant = AbstractLiteral::Variant(entry);
397 variant = variant.transform(&move |x| match x {
398 AbstractLiteral::Variant(entry) => {
399 let Field { name, value } = Moo::unwrap_or_clone(entry);
400 let value = match value {
401 Literal::Bool(false) => Literal::Int(0),
402 Literal::Bool(true) => Literal::Int(1),
403 value => value,
404 };
405 AbstractLiteral::Variant(Moo::new(Field { name, value }))
406 }
407 value => value,
408 });
409 updates.push((k, Literal::AbstractLiteral(variant)));
410 }
411 Literal::AbstractLiteral(AbstractLiteral::Set(members)) => {
412 let set = AbstractLiteral::Set(members).transform(&move |x| match x {
413 AbstractLiteral::Set(members) => {
414 let members = members
415 .into_iter()
416 .map(|x| match x {
417 Literal::Bool(false) => Literal::Int(0),
418 Literal::Bool(true) => Literal::Int(1),
419 x => x,
420 })
421 .collect_vec();
422
423 AbstractLiteral::Set(members)
424 }
425 x => x,
426 });
427 updates.push((k, Literal::AbstractLiteral(set)));
428 }
429 Literal::AbstractLiteral(AbstractLiteral::MSet(members)) => {
430 let mset = AbstractLiteral::MSet(members).transform(&move |x| match x {
431 AbstractLiteral::MSet(members) => {
432 let members = members
433 .into_iter()
434 .map(|x| match x {
435 Literal::Bool(false) => Literal::Int(0),
436 Literal::Bool(true) => Literal::Int(1),
437 x => x,
438 })
439 .collect_vec();
440 AbstractLiteral::MSet(members)
441 }
442 x => x,
443 });
444 updates.push((k, Literal::AbstractLiteral(mset)));
445 }
446 Literal::AbstractLiteral(AbstractLiteral::Sequence(elems)) => {
447 let sequence =
448 AbstractLiteral::Sequence(elems).transform(&move |x| match x {
449 AbstractLiteral::Sequence(elems) => {
450 let elems = elems
451 .into_iter()
452 .map(|x| match x {
453 Literal::Bool(false) => Literal::Int(0),
454 Literal::Bool(true) => Literal::Int(1),
455 x => x,
456 })
457 .collect_vec();
458 AbstractLiteral::Sequence(elems)
459 }
460 x => x,
461 });
462 updates.push((k, Literal::AbstractLiteral(sequence)));
463 }
464 Literal::AbstractLiteral(AbstractLiteral::Function(pairs)) => {
465 let function =
466 AbstractLiteral::Function(pairs).transform(&move |x| match x {
467 AbstractLiteral::Function(pairs) => {
468 let pairs = pairs
469 .into_iter()
470 .map(|(key, value)| {
471 let normalize = |x| match x {
472 Literal::Bool(false) => Literal::Int(0),
473 Literal::Bool(true) => Literal::Int(1),
474 x => x,
475 };
476 (normalize(key), normalize(value))
477 })
478 .collect_vec();
479 AbstractLiteral::Function(pairs)
480 }
481 x => x,
482 });
483 updates.push((k, Literal::AbstractLiteral(function)));
484 }
485 Literal::AbstractLiteral(AbstractLiteral::Relation(tuples)) => {
486 let relation =
487 AbstractLiteral::Relation(tuples).transform(&move |x| match x {
488 AbstractLiteral::Relation(tuples) => {
489 let tuples = tuples
490 .into_iter()
491 .map(|fields| {
492 fields
493 .into_iter()
494 .map(|x| match x {
495 Literal::Bool(false) => Literal::Int(0),
496 Literal::Bool(true) => Literal::Int(1),
497 x => x,
498 })
499 .collect_vec()
500 })
501 .collect_vec();
502 AbstractLiteral::Relation(tuples)
503 }
504 x => x,
505 });
506 updates.push((k, Literal::AbstractLiteral(relation)));
507 }
508 Literal::AbstractLiteral(AbstractLiteral::Partition(parts)) => {
509 let partition =
510 AbstractLiteral::Partition(parts).transform(&move |x| match x {
511 AbstractLiteral::Partition(parts) => {
512 let parts = parts
513 .into_iter()
514 .map(|part| {
515 part.into_iter()
516 .map(|x| match x {
517 Literal::Bool(false) => Literal::Int(0),
518 Literal::Bool(true) => Literal::Int(1),
519 x => x,
520 })
521 .collect_vec()
522 })
523 .collect_vec();
524 AbstractLiteral::Partition(parts)
525 }
526 x => x,
527 });
528 updates.push((k, Literal::AbstractLiteral(partition)));
529 }
530 Literal::AbstractLiteral(AbstractLiteral::Permutation(cycles)) => {
531 let permutation =
532 AbstractLiteral::Permutation(cycles).transform(&move |x| match x {
533 AbstractLiteral::Permutation(cycles) => {
534 let cycles = cycles
535 .into_iter()
536 .map(|cycle| {
537 cycle
538 .into_iter()
539 .map(|x| match x {
540 Literal::Bool(false) => Literal::Int(0),
541 Literal::Bool(true) => Literal::Int(1),
542 x => x,
543 })
544 .collect_vec()
545 })
546 .collect_vec();
547 AbstractLiteral::Permutation(cycles)
548 }
549 x => x,
550 });
551 updates.push((k, Literal::AbstractLiteral(permutation)));
552 }
553 }
554 }
555 }
556
557 for (k, v) in updates {
558 let v = match v {
559 Literal::AbstractLiteral(value) => {
560 Literal::AbstractLiteral(normalize_set_literal_order(value))
561 }
562 value => value,
563 };
564 solset.insert(k, v);
565 }
566 }
567
568 normalized = normalized.into_iter().unique().collect();
570 normalized.sort_by(solution_essence_cmp);
571 normalized
572}
573
574fn solution_essence_cmp(
575 lhs: &BTreeMap<Name, Literal>,
576 rhs: &BTreeMap<Name, Literal>,
577) -> std::cmp::Ordering {
578 lhs.iter()
579 .zip(rhs)
580 .find_map(|((lhs_name, lhs_value), (rhs_name, rhs_value))| {
581 let ordering = lhs_name.cmp(rhs_name);
582 (ordering != std::cmp::Ordering::Equal)
583 .then_some(ordering)
584 .or_else(|| {
585 let ordering = lhs_value.essence_cmp(rhs_value);
586 (ordering != std::cmp::Ordering::Equal).then_some(ordering)
587 })
588 })
589 .unwrap_or_else(|| lhs.len().cmp(&rhs.len()))
590}
591
592fn normalize_set_literal_order(value: AbstractLiteral<Literal>) -> AbstractLiteral<Literal> {
593 value.transform(&|value| match value {
594 AbstractLiteral::Set(mut members) => {
595 members.sort_by(Literal::essence_cmp);
596 AbstractLiteral::Set(members)
597 }
598 AbstractLiteral::MSet(mut members) => {
599 members.sort_by(Literal::essence_cmp);
600 AbstractLiteral::MSet(members)
601 }
602 AbstractLiteral::Function(mut pairs) => {
603 pairs.sort_by(|(k1, _), (k2, _)| Literal::essence_cmp(k1, k2));
604 AbstractLiteral::Function(pairs)
605 }
606 AbstractLiteral::Relation(mut tuples) => {
607 tuples.sort_by(|a, b| {
608 a.iter()
609 .zip(b.iter())
610 .map(|(x, y)| Literal::essence_cmp(x, y))
611 .find(|ord| *ord != std::cmp::Ordering::Equal)
612 .unwrap_or(std::cmp::Ordering::Equal)
613 });
614 AbstractLiteral::Relation(tuples)
615 }
616 AbstractLiteral::Partition(mut parts) => {
617 for part in parts.iter_mut() {
618 part.sort_by(Literal::essence_cmp);
619 }
620 parts.sort_by(|a, b| {
621 a.iter()
622 .zip(b.iter())
623 .map(|(x, y)| Literal::essence_cmp(x, y))
624 .find(|ord| *ord != std::cmp::Ordering::Equal)
625 .unwrap_or_else(|| a.len().cmp(&b.len()))
626 });
627 AbstractLiteral::Partition(parts)
628 }
629 value => value,
630 })
631}
632
633fn maybe_truncate_serialised_json(serialised: String, test_stage: &str) -> String {
634 if test_stage == "rewrite" {
635 truncate_to_first_lines(&serialised, REWRITE_SERIALISED_JSON_MAX_LINES)
636 } else {
637 serialised
638 }
639}
640
641fn truncate_to_first_lines(content: &str, max_lines: usize) -> String {
642 content.lines().take(max_lines).join("\n")
643}
644
645pub fn truncate_to_first_chars(content: &str, max_chars: usize) -> String {
646 match content.char_indices().nth(max_chars) {
647 Some((idx, _)) => content[..idx].to_owned(),
648 None => content.to_owned(),
649 }
650}
651
652fn read_first_n_lines<P: AsRef<Path>>(filename: P, n: usize) -> io::Result<String> {
653 let reader = BufReader::new(File::open(&filename)?);
654 let lines = reader
655 .lines()
656 .chunks(n)
657 .into_iter()
658 .next()
659 .unwrap()
660 .collect::<Result<Vec<_>, _>>()?;
661 Ok(lines.join("\n"))
662}
663
664#[cfg(test)]
665mod tests {
666 use super::*;
667
668 fn set(members: Vec<Literal>) -> Literal {
669 Literal::AbstractLiteral(AbstractLiteral::Set(members))
670 }
671
672 #[test]
673 fn solution_normalization_sorts_nested_set_members_by_essence_order() {
674 let inner_one_two = set(vec![Literal::Int(2), Literal::Int(1)]);
675 let inner_two = set(vec![Literal::Int(2)]);
676 let mut oxide_solution = BTreeMap::new();
677 oxide_solution.insert(
678 Name::User("x".into()),
679 set(vec![inner_two.clone(), inner_one_two.clone()]),
680 );
681 let mut conjure_solution = BTreeMap::new();
682 conjure_solution.insert(
683 Name::User("x".into()),
684 set(vec![inner_one_two, inner_two.clone()]),
685 );
686
687 let normalized_oxide = normalize_solutions_for_comparison(&[oxide_solution]);
688 let normalized_conjure = normalize_solutions_for_comparison(&[conjure_solution]);
689 let expected = set(vec![inner_two, set(vec![Literal::Int(1), Literal::Int(2)])]);
690
691 assert_eq!(normalized_oxide, normalized_conjure);
692 assert_eq!(
693 normalized_oxide[0].get(&Name::User("x".into())),
694 Some(&expected)
695 );
696 }
697}