fix: some checks that were too strict

src/aba/mod.rs

@@ -88,6 +88,10 @@ impl<A: Atom> Aba<A> {
     fn has_assumption(&self, atom: &A) -> bool {
         self.inverses.contains_key(atom)
     }
+
+    fn has_element(&self, element: &A) -> bool {
+        self.universe().any(|e| element == e)
+    }
 }
 
 fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>) -> ClauseList {

src/aba/problems/admissibility.rs

@@ -29,7 +29,7 @@ pub struct VerifyAdmissibleExtension<A: Atom> {
 
 /// Decide whether `assumption` is credulously admissible in an [`Aba`]
 pub struct DecideCredulousAdmissibility<A> {
-    pub assumption: A,
+    pub element: A,
 }
 
 pub fn initial_admissibility_clauses<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> ClauseList {
@@ -222,7 +222,7 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
 
     fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
         let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
-        clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
+        clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
         clauses
     }
 
@@ -231,12 +231,12 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
     }
 
     fn check(&self, aba: &Aba<A>) -> Result {
-        if aba.has_assumption(&self.assumption) {
+        if aba.has_assumption(&self.element) {
             Ok(())
         } else {
             Err(Error::ProblemCheckFailed(format!(
                 "Assumption {:?} not present in ABA framework",
-                self.assumption
+                self.element
             )))
         }
     }

src/aba/problems/complete.rs

@@ -20,7 +20,7 @@ pub struct EnumerateCompleteExtensions<A> {
 
 /// Decide whether `assumption` is credulously complete in an [`Aba`]
 pub struct DecideCredulousComplete<A> {
-    pub assumption: A,
+    pub element: A,
 }
 
 fn initial_complete_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
@@ -101,7 +101,7 @@ impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
 
     fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
         let mut clauses = initial_complete_clauses(aba);
-        clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
+        clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
         clauses
     }
 
@@ -110,12 +110,12 @@ impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
     }
 
     fn check(&self, aba: &Aba<A>) -> Result {
-        if aba.has_assumption(&self.assumption) {
+        if aba.has_element(&self.element) {
             Ok(())
         } else {
             Err(Error::ProblemCheckFailed(format!(
-                "Assumption {:?} not present in ABA framework",
-                self.assumption
+                "Element {:?} not present in ABA framework",
+                self.element
             )))
         }
     }

src/main.rs

@@ -64,15 +64,14 @@ fn __main() -> Result {
             aba::problems::solve(SampleAdmissibleExtension, &aba)?.fmt_iccma()
         }
         args::Problems::DecideCredulousAdmissibility { query } => {
-            aba::problems::solve(DecideCredulousAdmissibility { assumption: query }, &aba)?
-                .fmt_iccma()
+            aba::problems::solve(DecideCredulousAdmissibility { element: query }, &aba)?.fmt_iccma()
         }
         args::Problems::EnumerateComplete => {
             aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), &aba)?
                 .fmt_iccma()
         }
         args::Problems::DecideCredulousComplete { query } => {
-            aba::problems::solve(DecideCredulousComplete { assumption: query }, &aba)?.fmt_iccma()
+            aba::problems::solve(DecideCredulousComplete { element: query }, &aba)?.fmt_iccma()
         }
     }?;
     let mut stdout = std::io::stdout().lock();