feat: enable proof logging in appropriate test cases

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(
@@ -129,8 +130,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/src/engine/constraint_satisfaction_solver.rs

@@ -1174,11 +1174,11 @@ impl ConstraintSatisfactionSolver {
                 );
                 propagator.propagate(context)
             };
-            if self.assignments.get_decision_level() == 0
-                && self.internal_parameters.proof_log.is_logging_inferences()
-            {
+
+            if self.assignments.get_decision_level() == 0 {
                 self.log_root_propagation_to_proof(num_trail_entries_before, tag);
             }
+
             match propagation_status {
                 Ok(_) => {
                     // Notify other propagators of the propagations and continue.
@@ -1187,23 +1187,7 @@ impl ConstraintSatisfactionSolver {
                 Err(inconsistency) => match inconsistency {
                     // A propagator did a change that resulted in an empty domain.
                     Inconsistency::EmptyDomain => {
-                        let empty_domain_reason =
-                            ConstraintSatisfactionSolver::compute_reason_for_empty_domain(
-                                &mut self.assignments,
-                                &mut self.reason_store,
-                                &mut self.propagators,
-                            );
-
-                        // TODO: As a temporary solution, we remove the last trail element.
-                        // This way we guarantee that the assignment is consistent, which is needed
-                        // for the conflict analysis data structures. The proper alternative would
-                        // be to forbid the assignments from getting into an inconsistent state.
-                        self.assignments.remove_last_trail_element();
-
-                        let stored_conflict_info = StoredConflictInfo::EmptyDomain {
-                            conflict_nogood: empty_domain_reason,
-                        };
-                        self.state.declare_conflict(stored_conflict_info);
+                        self.prepare_for_conflict_resolution();
                         break;
                     }
                     // A propagator-specific reason for the current conflict.
@@ -1265,6 +1249,10 @@ impl ConstraintSatisfactionSolver {
         start_trail_index: usize,
         tag: Option<NonZero<u32>>,
     ) {
+        if !self.internal_parameters.proof_log.is_logging_inferences() {
+            return;
+        }
+
         for trail_idx in start_trail_index..self.assignments.num_trail_entries() {
             let entry = self.assignments.get_trail_entry(trail_idx);
             let reason_ref = entry
@@ -1314,11 +1302,15 @@ impl ConstraintSatisfactionSolver {
                     continue;
                 }
 
-                if let Some(step_id) = self.unit_nogood_step_ids.get(&trail_entry.predicate) {
-                    self.internal_parameters.proof_log.add_propagation(*step_id);
-                } else {
-                    unreachable!()
-                }
+                let possible_step_id = self.unit_nogood_step_ids.get(&trail_entry.predicate);
+                let Some(step_id) = possible_step_id else {
+                    panic!(
+                        "Getting unit nogood step id for {:?} but it does not exist.",
+                        trail_entry.predicate
+                    );
+                };
+
+                self.internal_parameters.proof_log.add_propagation(*step_id);
             }
 
             // Log the nogood which adds the root-level knowledge to the proof.
@@ -1424,6 +1416,8 @@ impl ConstraintSatisfactionSolver {
     }
 
     pub fn add_nogood(&mut self, nogood: Vec<Predicate>) -> Result<(), ConstraintOperationError> {
+        let num_trail_entries = self.assignments.num_trail_entries();
+
         let mut propagation_context = PropagationContextMut::new(
             &mut self.stateful_assignments,
             &mut self.assignments,
@@ -1432,21 +1426,54 @@ impl ConstraintSatisfactionSolver {
             Self::get_nogood_propagator_id(),
         );
         let nogood_propagator_id = Self::get_nogood_propagator_id();
-        ConstraintSatisfactionSolver::add_nogood_to_nogood_propagator(
+
+        let addition_result = ConstraintSatisfactionSolver::add_nogood_to_nogood_propagator(
             &mut self.propagators[nogood_propagator_id],
             nogood,
             &mut propagation_context,
-        )?;
+        );
+
+        if addition_result.is_err() {
+            self.prepare_for_conflict_resolution();
+            self.log_root_propagation_to_proof(num_trail_entries, None);
+            self.complete_proof();
+            return Err(ConstraintOperationError::InfeasibleNogood);
+        }
+
+        self.log_root_propagation_to_proof(num_trail_entries, None);
+
         // temporary hack for the nogood propagator that does propagation from scratch
         self.propagator_queue.enqueue_propagator(PropagatorId(0), 0);
         self.propagate();
+
+        self.log_root_propagation_to_proof(num_trail_entries, None);
+
         if self.state.is_infeasible() {
             Err(ConstraintOperationError::InfeasibleState)
         } else {
             Ok(())
         }
     }
 
+    fn prepare_for_conflict_resolution(&mut self) {
+        let empty_domain_reason = ConstraintSatisfactionSolver::compute_reason_for_empty_domain(
+            &mut self.assignments,
+            &mut self.reason_store,
+            &mut self.propagators,
+        );
+
+        // TODO: As a temporary solution, we remove the last trail element.
+        // This way we guarantee that the assignment is consistent, which is needed
+        // for the conflict analysis data structures. The proper alternative would
+        // be to forbid the assignments from getting into an inconsistent state.
+        self.assignments.remove_last_trail_element();
+
+        let stored_conflict_info = StoredConflictInfo::EmptyDomain {
+            conflict_nogood: empty_domain_reason,
+        };
+        self.state.declare_conflict(stored_conflict_info);
+    }
+
     fn add_nogood_to_nogood_propagator(
         nogood_propagator: &mut dyn Propagator,
         nogood: Vec<Predicate>,

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<_>>();
@@ -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,7 +274,21 @@ 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());
+    }
+
+    if matches!(test_type, TestType::Unsatisfiable | TestType::Optimality) {
+        options.push("--proof".to_owned());
+        options.push(format!(
+            "{}/tests/{folder_name}/{instance_name}.drcp",
+            env!("CARGO_MANIFEST_DIR")
+        ));
+    }
 
     let files = run_solver_with_options(instance_path, false, options, Some(prefix));
 
@@ -280,4 +306,6 @@ pub(crate) fn run_mzn_test_with_options<const ORDERED: bool>(
         .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<_>>());
+
+    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,6 @@ 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");
+    let output = run_mzn_test::<false>(instance_name, folder_name, TestType::Unsatisfiable);
     assert!(output.ends_with("=====UNSATISFIABLE=====\n"));
 }

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"));
         }
     };
 }