feat: new failing test

scripts/validate.sh

@@ -16,7 +16,7 @@ print_help_and_exit() {
   printf "          The additional argument for the problem\n"
   printf "  -f, --file\n"
   printf "          The file containing the problem in ABA format\n"
-  printf "  --file-dir\n"
+  printf "  --files-from\n"
   printf "          Use the following dir to read files, specify a single file with --file instead\n"
   exit 1
 }
@@ -43,7 +43,7 @@ run_dc_co() {
 
 POSITIONAL_ARGS=()
 ASPFORABA=ASPforABA
-ABA2SAT=aba2sat
+ABA2SAT=result/bin/aba2sat
 ABA_FILE=
 ABA_FILE_DIR=
 ABA_FILE_EXT=aba

src/aba/problems/mod.rs

@@ -81,6 +81,11 @@ pub fn solve<A: Atom, P: Problem<A>>(problem: P, mut aba: Aba<A>) -> Result<P::O
         .for_each(|raw| sat.add_clause(raw));
     // A single solver call to determine the solution
     if let Some(sat_result) = sat.solve() {
+        #[cfg(debug_assertions)]
+        if sat_result {
+            let rec = map.reconstruct(&sat).collect::<Vec<_>>();
+            eprintln!("{rec:#?}");
+        }
         // If the solver didn't panic, convert our result into the output
         // using our problem instance
         Ok(problem.construct_output(SolverState {

src/tests/mod.rs

@@ -3,6 +3,7 @@ use std::collections::HashSet;
 use crate::aba::{
     problems::{
         admissibility::{EnumerateAdmissibleExtensions, VerifyAdmissibleExtension},
+        complete::{DecideCredulousComplete, EnumerateCompleteExtensions},
         conflict_free::ConflictFreeness,
     },
     Aba,
@@ -159,3 +160,16 @@ fn a_chain_with_no_beginning() {
         );
     }
 }
+
+#[test]
+fn loops_and_conflicts() {
+    let aba = Aba::default()
+        .with_assumption('a', 'b')
+        .with_rule('b', ['a'])
+        .with_rule('b', ['c'])
+        .with_rule('c', ['b'])
+        .with_rule('d', ['b']);
+    let result =
+        crate::aba::problems::solve(DecideCredulousComplete { element: 'd' }, aba).unwrap();
+    assert!(!result, "d cannot be credulous complete");
+}