additional docs and renames

src/aba/mod.rs

@@ -78,7 +78,7 @@ impl<A: Atom> Aba<A> {
     }
 
     fn derive_rule_clauses(&self) -> impl Iterator<Item = Clause> + '_ {
-        inference_helper::<Theory<_>, _>(self)
+        theory_helper::<Theory<_>, _>(self)
     }
 
     fn rule_heads(&self) -> impl Iterator<Item = &A> + '_ {
@@ -101,9 +101,15 @@ fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>)
     clauses
 }
 
-pub fn inference_helper<I: TheoryAtom<A> + IntoLiteral, A: Atom>(
+/// Generate the logic for theory derivation in the given [`Aba`]
+///
+/// This will need a valid [`TheoryAtom`] that will be used to construct the logic
+// TODO: describe how this is done
+pub fn theory_helper<I: TheoryAtom<A> + IntoLiteral, A: Atom>(
     aba: &Aba<A>,
 ) -> impl Iterator<Item = Clause> + '_ {
+    // The combined list of rules, such that every
+    // head is unique and possible contains a list of bodies
     let mut rules_combined =
         aba.rules
             .iter()
@@ -111,20 +117,29 @@ pub fn inference_helper<I: TheoryAtom<A> + IntoLiteral, A: Atom>(
                 rules.entry(head).or_default().push(body);
                 rules
             });
+    // All atoms that can be derived by rules
     let rule_heads: HashSet<_> = aba.rule_heads().collect();
-    // For every non-assumption, that is not derivable add a rule without a body
+    // For every non-assumption, that is not derivable add a rule without a body,
+    // such that it cannot be derived at all. This is to prevent the solver from
+    // guessing this atom on it's own
     aba.universe()
         .filter(|atom| !aba.has_assumption(atom))
         .filter(|atom| !rule_heads.contains(atom))
         .map(|atom| (atom, vec![]))
         .collect_into(&mut rules_combined);
+    // All combined rules
+    // These are heads with any number of bodies, possibly none
     rules_combined
         .into_iter()
         .flat_map(|(head, bodies)| match &bodies[..] {
+            // No bodies, add a clause that prevents the head from accuring in the theory
             [] => {
                 vec![Clause::from(vec![I::new(head.clone()).neg()])]
             }
+            // A single body only, this is equivalent to a head that can only be derived by a single rule
             [body] => body_to_clauses::<I, _>(I::new(head.clone()).pos(), body),
+            // n bodies, we'll need to take extra care to allow any number of bodies to derive this
+            // head without logic errors
             bodies => {
                 let mut clauses = vec![];
                 bodies

src/aba/problems/admissibility.rs

@@ -2,7 +2,7 @@
 use std::collections::HashSet;
 
 use crate::{
-    aba::{inference_helper, Aba, Theory},
+    aba::{theory_helper, Aba, Theory},
     clauses::{Atom, Clause, ClauseList},
     error::Error,
     literal::{IntoLiteral, TheoryAtom},
@@ -43,12 +43,12 @@ pub struct SetTheoryHelper<A: Atom>(usize, A);
 fn initial_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
     let mut clauses = vec![];
     // Create inference for the problem set
-    inference_helper::<SetTheory<_>, _>(aba).collect_into(&mut clauses);
+    theory_helper::<SetTheory<_>, _>(aba).collect_into(&mut clauses);
     // Attack the inference of the aba, if an attack exists
     for (assumption, inverse) in &aba.inverses {
         [
             // For any assumption `a` and it's inverse `b`:
-            //   Inference(a) <=> not SetInference(b)
+            //   a in th(A) <=> b not in th(S)
             Clause::from(vec![
                 Theory::new(assumption.clone()).pos(),
                 SetTheory::new(inverse.clone()).pos(),
@@ -59,14 +59,14 @@ fn initial_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
             ]),
             // Prevent attacks from the opponent to the selected set
             // For any assumption `a` and it's inverse `b`:
-            //   Inference(b) and SetInference(a) => bottom
+            //   b in th(A) and a in th(S) => bottom
             Clause::from(vec![
                 Theory::new(inverse.clone()).neg(),
                 SetTheory::new(assumption.clone()).neg(),
             ]),
             // Prevent self-attacks
             // For any assumption `a` and it's inverse `b`:
-            //   SetInference(a) and SetInference(b) => bottom
+            //   a in th(S) and b in th(S) => bottom
             Clause::from(vec![
                 SetTheory::new(assumption.clone()).neg(),
                 SetTheory::new(inverse.clone()).neg(),

src/literal.rs

@@ -41,7 +41,7 @@ impl<T: Any + Debug + Sized> IntoLiteral for T {
 /// ([`Literal`]) A literal that can be used to construct the logic behind
 /// the theory of a (sub-)set of assumptions (`th(S)`) in an [`Aba`](crate::aba::Aba).
 ///
-/// See [`crate::aba::inference_helper`].
+/// See [`crate::aba::theory_helper`].
 pub trait TheoryAtom<A: Atom>: Sized + IntoLiteral {
     /// Helper type
     type Helper: IntoLiteral;