feat: enable proof logging in appropriate test cases (#154)

Only logs the proof; does not check at the moment

Author: maartenflippo

pumpkin-macros/src/lib.rs

@@ -35,9 +35,7 @@ pub fn cumulative(item: TokenStream) -> TokenStream {
                         stringcase::snake_case(&argument[2..].split("-").skip(1).join("_"))
                     })
                     .join("_");
-                let options = quote! {
-                    #(#options),*
-                };
+
                 let test_name = format_ident!(
                     "{}",
                     stringcase::snake_case(
@@ -53,12 +51,18 @@ pub fn cumulative(item: TokenStream) -> TokenStream {
                     )
                 );
                 let stream: TokenStream = quote! {
-                        mzn_test!(
-                            #test_name,
-                            "cumulative",
-                            vec!["--cumulative-propagation-method", &stringcase::kebab_case(#propagation_method),"--cumulative-explanation-type", #explanation_type, #options]
-                        );
-                    }
+                    mzn_test!(
+                        #test_name,
+                        "cumulative",
+                        vec![
+                            "--cumulative-propagation-method".to_string(),
+                            stringcase::kebab_case(#propagation_method),
+                            "--cumulative-explanation-type".to_string(),
+                            #explanation_type.to_string(),
+                            #(#options.to_string()),*
+                        ]
+                    );
+                }
                 .into();
                 output.extend(stream);
             }
@@ -102,9 +106,6 @@ pub fn cumulative_synchronised(item: TokenStream) -> TokenStream {
                 .iter()
                 .map(|argument| stringcase::snake_case(&argument[2..].split("-").skip(1).join("_")))
                 .join("_");
-            let options = quote! {
-                #(#options),*
-            };
             let test_name = format_ident!(
                 "{}",
                 stringcase::snake_case(
@@ -128,8 +129,20 @@ pub fn cumulative_synchronised(item: TokenStream) -> TokenStream {
                     check_statistic_equality(
                         "cumulative",
                         "mzn_constraints",
-                        vec!["--cumulative-propagation-method", &stringcase::kebab_case(stringify!(#first_name)),"--cumulative-explanation-type", #explanation_type, #options],
-                        vec!["--cumulative-propagation-method", &stringcase::kebab_case(stringify!(#second_name)),"--cumulative-explanation-type", #explanation_type, #options],
+                        vec![
+                            "--cumulative-propagation-method".to_string(),
+                            stringcase::kebab_case(stringify!(#first_name)),
+                            "--cumulative-explanation-type".to_string(),
+                            #explanation_type.to_string(),
+                            #(#options.to_string()),*
+                        ],
+                        vec![
+                            "--cumulative-propagation-method".to_string(),
+                            stringcase::kebab_case(stringify!(#second_name)),
+                            "--cumulative-explanation-type".to_string(),
+                            #explanation_type.to_string(),
+                            #(#options.to_string()),*
+                        ],
                         &format!("equality_{}_{}_{}", #first_name, #explanation_type, #option_string),
                         &format!("equality_{}_{}_{}", #second_name, #explanation_type, #option_string),
                     );

pumpkin-solver/tests/helpers/mod.rs

@@ -42,10 +42,10 @@ pub(crate) fn run_solver(instance_path: impl AsRef<Path>, with_proof: bool) -> F
     run_solver_with_options(instance_path, with_proof, std::iter::empty(), None)
 }
 
-pub(crate) fn run_solver_with_options<'a>(
+pub(crate) fn run_solver_with_options(
     instance_path: impl AsRef<Path>,
     with_proof: bool,
-    args: impl IntoIterator<Item = &'a str>,
+    args: impl IntoIterator<Item = String>,
     prefix: Option<&str>,
 ) -> Files {
     let args = args.into_iter().collect::<Vec<_>>();
@@ -57,7 +57,7 @@ pub(crate) fn run_solver_with_options<'a>(
     let solver = PathBuf::from(env!("CARGO_BIN_EXE_pumpkin-solver"));
 
     let add_extension = |extension: &str| -> PathBuf {
-        if let Some(prefix) = prefix {
+        if let Some(prefix) = prefix.and_then(|s| if s.is_empty() { None } else { Some(s) }) {
             instance_path.with_extension(format!("{prefix}.{extension}"))
         } else {
             instance_path.with_extension(extension)
@@ -184,15 +184,19 @@ pub(crate) fn verify_proof(files: Files, checker_output: &Output) -> std::io::Re
     files.cleanup()
 }
 
-pub(crate) fn run_mzn_test<const ORDERED: bool>(instance_name: &str, folder_name: &str) {
-    run_mzn_test_with_options::<ORDERED>(instance_name, folder_name, vec![], "")
+pub(crate) fn run_mzn_test<const ORDERED: bool>(
+    instance_name: &str,
+    folder_name: &str,
+    test_type: TestType,
+) -> String {
+    run_mzn_test_with_options::<ORDERED>(instance_name, folder_name, test_type, vec![], "")
 }
 
 pub(crate) fn check_statistic_equality(
     instance_name: &str,
     folder_name: &str,
-    mut options_first: Vec<&str>,
-    mut options_second: Vec<&str>,
+    mut options_first: Vec<String>,
+    mut options_second: Vec<String>,
     prefix_first: &str,
     prefix_second: &str,
 ) {
@@ -201,8 +205,8 @@ pub(crate) fn check_statistic_equality(
         env!("CARGO_MANIFEST_DIR")
     );
 
-    options_first.push("-sa");
-    options_second.push("-sa");
+    options_first.push("-sa".to_owned());
+    options_second.push("-sa".to_owned());
 
     let files_first = run_solver_with_options(
         instance_path.clone(),
@@ -246,12 +250,20 @@ pub(crate) fn check_statistic_equality(
     )
 }
 
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub(crate) enum TestType {
+    Unsatisfiable,
+    SolutionEnumeration,
+    Optimality,
+}
+
 pub(crate) fn run_mzn_test_with_options<const ORDERED: bool>(
     instance_name: &str,
     folder_name: &str,
-    mut options: Vec<&str>,
+    test_type: TestType,
+    mut options: Vec<String>,
     prefix: &str,
-) {
+) -> String {
     let instance_path = format!(
         "{}/tests/{folder_name}/{instance_name}.fzn",
         env!("CARGO_MANIFEST_DIR")
@@ -262,22 +274,39 @@ pub(crate) fn run_mzn_test_with_options<const ORDERED: bool>(
         env!("CARGO_MANIFEST_DIR")
     );
 
-    options.push("-a");
+    if matches!(
+        test_type,
+        TestType::SolutionEnumeration | TestType::Optimality
+    ) {
+        // Both for optimisation and enumeration do we want to log all encountered solutions.
+        options.push("-a".to_owned());
+    }
 
-    let files = run_solver_with_options(instance_path, false, options, Some(prefix));
+    let files = run_solver_with_options(
+        instance_path,
+        matches!(test_type, TestType::Unsatisfiable | TestType::Optimality),
+        options,
+        Some(prefix),
+    );
 
     let output = std::fs::read_to_string(files.log_file).expect("Failed to read solver output");
 
-    let expected_file =
-        std::fs::read_to_string(snapshot_path).expect("Failed to read expected solution file.");
+    if test_type == TestType::Unsatisfiable {
+        assert!(output.contains("=====UNSATISFIABLE====="));
+    } else {
+        let expected_file =
+            std::fs::read_to_string(snapshot_path).expect("Failed to read expected solution file.");
 
-    let actual_solutions = output
-        .parse::<Solutions<ORDERED>>()
-        .expect("Valid solution");
+        let actual_solutions = output
+            .parse::<Solutions<ORDERED>>()
+            .expect("Valid solution");
 
-    let expected_solutions = expected_file
-        .parse::<Solutions<ORDERED>>()
-        .expect("Valid solution");
+        let expected_solutions = expected_file
+            .parse::<Solutions<ORDERED>>()
+            .expect("Valid solution");
+
+        assert_eq!(actual_solutions, expected_solutions, "Did not find the elements {:?} in the expected solution and the expected solution contained {:?} while the actual solution did not.", actual_solutions.assignments.iter().filter(|solution| !expected_solutions.assignments.contains(solution)).collect::<Vec<_>>(), expected_solutions.assignments.iter().filter(|solution| !actual_solutions.assignments.contains(solution)).collect::<Vec<_>>());
+    }
 
-    assert_eq!(actual_solutions, expected_solutions, "Did not find the elements {:?} in the expected solution and the expected solution contained {:?} while the actual solution did not.", actual_solutions.assignments.iter().filter(|solution| !expected_solutions.assignments.contains(solution)).collect::<Vec<_>>(), expected_solutions.assignments.iter().filter(|solution| !actual_solutions.assignments.contains(solution)).collect::<Vec<_>>());
+    output
 }

pumpkin-solver/tests/mzn_constraint_test.rs

@@ -3,6 +3,7 @@
 mod helpers;
 use helpers::check_statistic_equality;
 use helpers::run_mzn_test_with_options;
+use helpers::TestType;
 use pumpkin_macros::cumulative;
 use pumpkin_macros::cumulative_synchronised;
 
@@ -14,12 +15,14 @@ macro_rules! mzn_test {
     ($name:ident, $file:expr, $options:expr) => {
         #[test]
         fn $name() {
-            run_mzn_test_with_options::<false>(
+            let output = run_mzn_test_with_options::<false>(
                 $file,
                 "mzn_constraints",
+                TestType::SolutionEnumeration,
                 $options,
                 stringify!($name),
             );
+            assert!(output.ends_with("==========\n"));
         }
     };
 }

pumpkin-solver/tests/mzn_infeasible_test.rs

@@ -2,7 +2,8 @@
 
 mod helpers;
 
-use helpers::run_solver_with_options;
+use helpers::run_mzn_test;
+use helpers::TestType;
 
 macro_rules! mzn_infeasible_test {
     ($name:ident) => {
@@ -15,13 +16,5 @@ macro_rules! mzn_infeasible_test {
 mzn_infeasible_test!(prop_stress);
 
 pub fn run_mzn_infeasible_test(instance_name: &str, folder_name: &str) {
-    let instance_path = format!(
-        "{}/tests/{folder_name}/{instance_name}.fzn",
-        env!("CARGO_MANIFEST_DIR")
-    );
-
-    let files = run_solver_with_options(instance_path, false, ["-a"], None);
-
-    let output = std::fs::read_to_string(files.log_file).expect("Failed to read solver output");
-    assert!(output.ends_with("=====UNSATISFIABLE=====\n"));
+    let _ = run_mzn_test::<false>(instance_name, folder_name, TestType::Unsatisfiable);
 }

pumpkin-solver/tests/mzn_optimization_test.rs

@@ -3,12 +3,15 @@
 mod helpers;
 
 use helpers::run_mzn_test;
+use helpers::TestType;
 
 macro_rules! mzn_optimization_test {
     ($name:ident) => {
         #[test]
         fn $name() {
-            run_mzn_test::<false>(stringify!($name), "mzn_optimization");
+            let output =
+                run_mzn_test::<false>(stringify!($name), "mzn_optimization", TestType::Optimality);
+            assert!(output.ends_with("==========\n"));
         }
     };
 }

pumpkin-solver/tests/mzn_search_test.rs

@@ -3,12 +3,17 @@
 mod helpers;
 
 use helpers::run_mzn_test;
+use helpers::TestType;
 
 macro_rules! mzn_search_ordered {
     ($name:ident) => {
         #[test]
         fn $name() {
-            run_mzn_test::<true>(stringify!($name), "mzn_search");
+            let _ = run_mzn_test::<true>(
+                stringify!($name),
+                "mzn_search",
+                TestType::SolutionEnumeration,
+            );
         }
     };
 }
@@ -17,7 +22,11 @@ macro_rules! mzn_search_unordered {
     ($name:ident) => {
         #[test]
         fn $name() {
-            run_mzn_test::<false>(stringify!($name), "mzn_search");
+            let _ = run_mzn_test::<false>(
+                stringify!($name),
+                "mzn_search",
+                TestType::SolutionEnumeration,
+            );
         }
     };
 }