feat: drop obsolete rules using trim function on ABA instances

This is a small step on the journey to get rid of loops, but will only
remove trivial loops that can never be reached.

src/aba/mod.rs

@@ -1,3 +1,30 @@
+//! # Assumption-based Argumentation
+//!
+//! All relevant tools for solving problems around assumption-based argumentation.
+//!
+//! ## Example
+//! ```
+//! # use aba2sat::aba::Aba;
+//! # use aba2sat::aba::problems::solve;
+//! # use aba2sat::aba::problems::admissibility::VerifyAdmissibleExtension;
+//! let aba =
+//!     // Start with an empty framework
+//!     Aba::default()
+//!         // Add an assumption 'a' with inverse 'p'
+//!         .with_assumption('a', 'p')
+//!         // Add an assumption 'b' with inverse 'q'
+//!         .with_assumption('b', 'q')
+//!         // Add a rule to derive 'p' (the inverse of 'a') from 'b'
+//!         .with_rule('p', ['b']);
+//!
+//!
+//! // Solve the problem whether the set of assumptions {'b'} is admissible
+//! let result =
+//!     solve(VerifyAdmissibleExtension { assumptions: vec!['b'] }, &aba).unwrap();
+//!
+//! // The result should be true
+//! assert!(result)
+//! ```
 use std::collections::{HashMap, HashSet};
 
 use crate::{
@@ -7,9 +34,12 @@ use crate::{
 
 pub mod problems;
 
-#[derive(Debug, Default, PartialEq)]
+pub type Rule<A> = (A, HashSet<A>);
+pub type RuleList<A> = Vec<Rule<A>>;
+
+#[derive(Debug, Default, Clone, PartialEq)]
 pub struct Aba<A: Atom> {
-    pub rules: Vec<(A, HashSet<A>)>,
+    pub rules: RuleList<A>,
     pub inverses: HashMap<A, A>,
 }
 
@@ -20,14 +50,6 @@ pub struct Theory<A: Atom>(A);
 pub struct TheoryHelper<A: Atom>(usize, A);
 
 impl<A: Atom> Aba<A> {
-    #[cfg(test)]
-    pub fn new() -> Self {
-        Aba {
-            rules: vec![],
-            inverses: HashMap::new(),
-        }
-    }
-
     pub fn with_assumption(mut self, assumption: A, inverse: A) -> Self {
         self.inverses.insert(assumption, inverse);
         self
@@ -55,9 +77,7 @@ impl<A: Atom> Aba<A> {
         self.inverses.contains_key(a)
     }
 
-    /**
+    /// Translate the ABA into base rules / definitions for SAT solving
-     * Translate the ABA into base rules / definitions for SAT solving
-     */
     pub fn derive_clauses(&self) -> ClauseList {
         let mut clauses = ClauseList::new();
         self.derive_rule_clauses().collect_into(&mut clauses);
@@ -77,6 +97,37 @@ impl<A: Atom> Aba<A> {
             .len()
     }
 
+    /// Filtered list of rules
+    ///
+    /// Iterates over all rules, marking reachable elements until
+    /// no additional rule can be applied. Then removes every
+    /// rule that contains any unreachable atom and returns the rest
+    pub fn trim(&mut self) {
+        // Begin with all assumptions marked as reachable
+        let mut reachable: HashSet<_> = self.assumptions().cloned().collect();
+        // Calculate all reachable elements
+        loop {
+            let mut marked_any = false;
+            for (head, body) in &self.rules {
+                if reachable.contains(head) {
+                    continue;
+                }
+                if body.iter().all(|atom| reachable.contains(atom)) {
+                    marked_any = true;
+                    reachable.insert(head.clone());
+                }
+            }
+            if !marked_any {
+                break;
+            }
+        }
+        // Remove all rules that contain any unreachable atom
+        self.rules.retain(|(head, body)| {
+            // Both the head and all elements from the body must be reachable
+            reachable.contains(head) && body.iter().all(|atom| reachable.contains(atom))
+        });
+    }
+
     fn derive_rule_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
         theory_helper::<Theory<_>, _>(self)
     }

src/aba/problems/mod.rs

@@ -57,19 +57,33 @@ pub struct SetTheory<A: Atom>(A);
 #[derive(Debug)]
 pub struct SetTheoryHelper<A: Atom>(usize, A);
 
-pub fn solve<A: Atom, P: Problem<A>>(problem: P, aba: &Aba<A>) -> Result<P::Output> {
+pub fn solve<A: Atom, P: Problem<A>>(problem: P, mut aba: Aba<A>) -> Result<P::Output> {
-    problem.check(aba)?;
+    // Trim the ABA, this is always safe
-    let clauses = aba.derive_clauses();
+    aba.trim();
-    let additional_clauses = problem.additional_clauses(aba);
+    // Let the problem perform additional checks before starting the solver
+    problem.check(&aba)?;
+    // Create a map that will keep track of the translation between
+    // atoms as we know them and their SAT representation
     let mut map = Mapper::new();
+    // Instantiate a new SAT solver instance
     let mut sat: Solver = Solver::default();
+    // Derive clauses from the ABA
+    let clauses = aba.derive_clauses();
+    // Append additional clauses as defined by the problem
+    let additional_clauses = problem.additional_clauses(&aba);
+    // Convert the total of our derived clauses using the mapper
+    // and feed the solver with the result
     map.as_raw_iter(&clauses)
         .for_each(|raw| sat.add_clause(raw));
+    // Do the same with the additional clauses that the problem defined
     map.as_raw_iter(&additional_clauses)
         .for_each(|raw| sat.add_clause(raw));
+    // A single solver call to determine the solution
     if let Some(sat_result) = sat.solve() {
+        // If the solver didn't panic, convert our result into the output
+        // using our problem instance
         Ok(problem.construct_output(SolverState {
-            aba,
+            aba: &aba,
             sat_result,
             solver: &sat,
             map: &map,
@@ -81,39 +95,62 @@ pub fn solve<A: Atom, P: Problem<A>>(problem: P, aba: &Aba<A>) -> Result<P::Outp
 
 pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
     mut problem: P,
-    aba: &Aba<A>,
+    mut aba: Aba<A>,
 ) -> Result<P::Output> {
-    problem.check(aba)?;
+    // Trim the ABA, this is always safe
+    aba.trim();
+    // Let the problem perform additional checks before starting the solver
+    problem.check(&aba)?;
+    // Create a map that will keep track of the translation between
+    // atoms as we know them and their SAT representation
     let mut map = Mapper::new();
+    // Instantiate a new SAT solver instance
     let mut sat: Solver = Solver::default();
-    let mut iteration = 0;
+    // Derive clauses from the ABA
     let clauses = aba.derive_clauses();
+    // Convert the total of our derived clauses using the mapper
+    // and feed the solver with the result
     map.as_raw_iter(&clauses)
         .for_each(|raw| sat.add_clause(raw));
+    // Keep track of the iteration we're in, this is a multishot solve
+    let mut iteration = 0;
+    // Enter the main loop
     let final_result = loop {
-        let additional_clauses = problem.additional_clauses(aba, iteration);
+        // Derive additional clauses from the problem instance, these
+        // may change for every iteration
+        let additional_clauses = problem.additional_clauses(&aba, iteration);
+        // Feed the clauses into our mapper and add the output to our running solver instance
         map.as_raw_iter(&additional_clauses)
             .for_each(|raw| sat.add_clause(raw));
+        // Call the solver for the next result
         let sat_result = sat.solve().ok_or(Error::SatCallInterrupted)?;
         #[cfg(debug_assertions)]
         if sat_result {
             let rec = map.reconstruct(&sat).collect::<Vec<_>>();
             eprintln!("{rec:#?}");
         }
+        // Call our problem to ask whether we should continue. This is the point
+        // where the problem instance can exit the loop our mutate inner state
+        // with the solver feedback and continue
         let control = problem.feedback(SolverState {
-            aba,
+            aba: &aba,
             sat_result,
             solver: &sat,
             map: &map,
         });
+        // Exit if the problem instance requested it
         if control == LoopControl::Stop {
             break sat_result;
         }
+        // Or continue into the next iteration
         iteration += 1;
     };
+    // This point will only be reached if the problem instance
+    // is happy with the iterations. Call it one final time to
+    // construct the output using the final results
     Ok(problem.construct_output(
         SolverState {
-            aba,
+            aba: &aba,
             sat_result: final_result,
             solver: &sat,
             map: &map,

src/main.rs

@@ -53,25 +53,24 @@ fn __main() -> Result {
             VerifyAdmissibleExtension {
                 assumptions: set.into_iter().collect(),
             },
-            &aba,
+            aba,
         )?
         .fmt_iccma(),
         args::Problems::EnumerateAdmissibility => {
-            aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)?
+            aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)?
                 .fmt_iccma()
         }
         args::Problems::SampleAdmissibility => {
-            aba::problems::solve(SampleAdmissibleExtension, &aba)?.fmt_iccma()
+            aba::problems::solve(SampleAdmissibleExtension, aba)?.fmt_iccma()
         }
         args::Problems::DecideCredulousAdmissibility { query } => {
-            aba::problems::solve(DecideCredulousAdmissibility { element: query }, &aba)?.fmt_iccma()
+            aba::problems::solve(DecideCredulousAdmissibility { element: query }, aba)?.fmt_iccma()
         }
         args::Problems::EnumerateComplete => {
-            aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), &aba)?
+            aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), aba)?.fmt_iccma()
-                .fmt_iccma()
         }
         args::Problems::DecideCredulousComplete { query } => {
-            aba::problems::solve(DecideCredulousComplete { element: query }, &aba)?.fmt_iccma()
+            aba::problems::solve(DecideCredulousComplete { element: query }, aba)?.fmt_iccma()
         }
     }?;
     let mut stdout = std::io::stdout().lock();

src/tests/mod.rs

@@ -2,16 +2,14 @@ use std::collections::HashSet;
 
 use crate::aba::{
     problems::{
-        admissibility::{
+        admissibility::{EnumerateAdmissibleExtensions, VerifyAdmissibleExtension},
-            DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, VerifyAdmissibleExtension,
-        },
         conflict_free::ConflictFreeness,
     },
     Aba,
 };
 
 fn simple_aba_example_1() -> Aba<char> {
-    Aba::new()
+    Aba::default()
         .with_assumption('a', 'r')
         .with_assumption('b', 's')
         .with_assumption('c', 't')
@@ -39,7 +37,7 @@ fn simple_conflict_free_verification() {
         .for_each(|(assumptions, expectation)| {
             eprintln!("Checking set {assumptions:?}");
             let result =
-                crate::aba::problems::solve(ConflictFreeness { assumptions }, &aba).unwrap();
+                crate::aba::problems::solve(ConflictFreeness { assumptions }, aba.clone()).unwrap();
             assert!(result == expectation);
         })
 }
@@ -58,7 +56,7 @@ fn simple_admissible_verification() {
         .for_each(|(assumptions, expectation)| {
             eprintln!("Checking set {assumptions:?}");
             let result =
-                crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: assumptions.clone() }, &aba).unwrap();
+                crate::aba::problems::solve(VerifyAdmissibleExtension { assumptions: assumptions.clone() }, aba.clone()).unwrap();
             assert!(
                 result == expectation,
                 "Expected {expectation} from solver, but got {result} while checking {assumptions:?}"
@@ -71,7 +69,7 @@ fn simple_admissible_example() {
     let aba = simple_aba_example_1();
     let expected: Vec<HashSet<char>> = vec![set!(), set!('b'), set!('b', 'c'), set!('c')];
     let result =
-        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)
+        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
             .unwrap();
     for elem in &expected {
         assert!(
@@ -92,7 +90,7 @@ fn simple_admissible_example_with_defense() {
     let aba = simple_aba_example_1().with_rule('t', vec!['a', 'b']);
     let expected: Vec<HashSet<char>> = vec![set!(), set!('a', 'b'), set!('b'), set!('b', 'c')];
     let result =
-        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)
+        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
             .unwrap();
     for elem in &expected {
         assert!(
@@ -110,7 +108,7 @@ fn simple_admissible_example_with_defense() {
 
 #[test]
 fn simple_admissible_atomic() {
-    let aba = Aba::new()
+    let aba = Aba::default()
         .with_assumption('a', 'p')
         .with_assumption('b', 'q')
         .with_assumption('c', 'r')
@@ -119,7 +117,7 @@ fn simple_admissible_atomic() {
     let expected: Vec<HashSet<char>> =
         vec![set!(), set!('b'), set!('c'), set!('a', 'c'), set!('b', 'c')];
     let result =
-        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)
+        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
             .unwrap();
     for elem in &expected {
         assert!(
@@ -138,7 +136,7 @@ fn simple_admissible_atomic() {
 #[test]
 fn a_chain_with_no_beginning() {
     // found this while grinding against ASPforABA (5aa9201)
-    let aba = Aba::new()
+    let aba = Aba::default()
         .with_assumption('a', 'b')
         .with_assumption('b', 'c')
         .with_rule('c', ['a', 'd'])
@@ -146,7 +144,7 @@ fn a_chain_with_no_beginning() {
     let expected: Vec<HashSet<char>> = vec![set!(), set!('b')];
     // 'a' cannot be defended against b since c is not derivable
     let result =
-        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), &aba)
+        crate::aba::problems::multishot_solve(EnumerateAdmissibleExtensions::default(), aba)
             .unwrap();
     for elem in &expected {
         assert!(