improved error output

src/aba/problems/admissibility.rs

@@ -4,7 +4,9 @@ use std::collections::HashSet;
 use crate::{
     aba::{inference_helper, Aba, Theory},
     clauses::{Atom, Clause, ClauseList},
+    error::Error,
     literal::{IntoLiteral, TheoryAtom},
+    Result,
 };
 
 use super::{LoopControl, MultishotProblem, Problem, SolverState};
@@ -25,6 +27,11 @@ pub struct VerifyAdmissibleExtension<A: Atom> {
     pub assumptions: Vec<A>,
 }
 
+/// Decide whether `assumption` is credulously admissible in an [`Aba`]
+pub struct DecideCredulousAdmissibility<A> {
+    pub assumption: A,
+}
+
 /// *(Literal)* `A` is element of `th(S)`
 #[derive(Debug)]
 pub struct SetTheory<A: Atom>(A);
@@ -203,9 +210,43 @@ impl<A: Atom> Problem<A> for VerifyAdmissibleExtension<A> {
         state.sat_result
     }
 
-    fn check(&self, aba: &Aba<A>) -> bool {
+    fn check(&self, aba: &Aba<A>) -> Result {
         // Make sure that every assumption is part of the ABA
-        self.assumptions.iter().all(|a| aba.contains_assumption(a))
+        match self
+            .assumptions
+            .iter()
+            .find(|a| !aba.contains_assumption(a))
+        {
+            Some(assumption) => Err(Error::ProblemCheckFailed(format!(
+                "Assumption {assumption:?} not present in ABA framework"
+            ))),
+            None => Ok(()),
+        }
+    }
+}
+
+impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
+    type Output = bool;
+
+    fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
+        let mut clauses = initial_clauses(aba);
+        clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
+        clauses
+    }
+
+    fn construct_output(self, state: SolverState<'_, A>) -> Self::Output {
+        state.sat_result
+    }
+
+    fn check(&self, aba: &Aba<A>) -> Result {
+        if aba.has_assumption(&self.assumption) {
+            Ok(())
+        } else {
+            Err(Error::ProblemCheckFailed(format!(
+                "Assumption {:?} not present in ABA framework",
+                self.assumption
+            )))
+        }
     }
 }
 

src/aba/problems/conflict_free.rs

@@ -3,7 +3,9 @@ use std::collections::HashSet;
 use crate::{
     aba::{Aba, Theory},
     clauses::{Atom, Clause, ClauseList},
+    error::Error,
     literal::{IntoLiteral, TheoryAtom},
+    Result,
 };
 
 use super::{Problem, SolverState};
@@ -39,8 +41,18 @@ impl<A: Atom> Problem<A> for ConflictFreeness<A> {
         state.sat_result
     }
 
-    fn check(&self, aba: &Aba<A>) -> bool {
+    fn check(&self, aba: &Aba<A>) -> Result {
         // Make sure that every assumption is part of the ABA
-        self.assumptions.iter().all(|a| aba.contains_assumption(a))
+        match self
+            .assumptions
+            .iter()
+            .find(|a| !aba.contains_assumption(a))
+        {
+            Some(assumption) => Err(Error::ProblemCheckFailed(format!(
+                "Assumption {:?} not present in ABA framework",
+                assumption
+            ))),
+            None => Ok(()),
+        }
     }
 }

src/aba/problems/mod.rs

@@ -30,8 +30,8 @@ pub trait Problem<A: Atom> {
     fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList;
     fn construct_output(self, state: SolverState<'_, A>) -> Self::Output;
 
-    fn check(&self, _aba: &Aba<A>) -> bool {
+    fn check(&self, _aba: &Aba<A>) -> Result {
-        true
+        Ok(())
     }
 }
 
@@ -42,33 +42,30 @@ pub trait MultishotProblem<A: Atom> {
     fn feedback(&mut self, state: SolverState<'_, A>) -> LoopControl;
     fn construct_output(self, state: SolverState<'_, A>, total_iterations: usize) -> Self::Output;
 
-    fn check(&self, _aba: &Aba<A>) -> bool {
+    fn check(&self, _aba: &Aba<A>) -> Result {
-        true
+        Ok(())
     }
 }
 
 pub fn solve<A: Atom, P: Problem<A>>(problem: P, aba: &Aba<A>) -> Result<P::Output> {
-    if problem.check(aba) {
+    problem.check(aba)?;
-        let clauses = aba.derive_clauses();
+    let clauses = aba.derive_clauses();
-        let additional_clauses = problem.additional_clauses(aba);
+    let additional_clauses = problem.additional_clauses(aba);
-        let mut map = Mapper::new();
+    let mut map = Mapper::new();
-        let mut sat: Solver = Solver::default();
+    let mut sat: Solver = Solver::default();
-        map.as_raw_iter(&clauses)
+    map.as_raw_iter(&clauses)
-            .for_each(|raw| sat.add_clause(raw));
+        .for_each(|raw| sat.add_clause(raw));
-        map.as_raw_iter(&additional_clauses)
+    map.as_raw_iter(&additional_clauses)
-            .for_each(|raw| sat.add_clause(raw));
+        .for_each(|raw| sat.add_clause(raw));
-        if let Some(sat_result) = sat.solve() {
+    if let Some(sat_result) = sat.solve() {
-            Ok(problem.construct_output(SolverState {
+        Ok(problem.construct_output(SolverState {
-                aba,
+            aba,
-                sat_result,
+            sat_result,
-                solver: &sat,
+            solver: &sat,
-                map: &map,
+            map: &map,
-            }))
+        }))
-        } else {
-            Err(Error::SatCallInterrupted)
-        }
     } else {
-        Err(Error::ProblemCheckFailed)
+        Err(Error::SatCallInterrupted)
     }
 }
 
@@ -76,9 +73,7 @@ pub fn multishot_solve<A: Atom, P: MultishotProblem<A>>(
     mut problem: P,
     aba: &Aba<A>,
 ) -> Result<P::Output> {
-    if !problem.check(aba) {
+    problem.check(aba)?;
-        return Err(Error::ProblemCheckFailed);
-    }
     let mut map = Mapper::new();
     let mut sat: Solver = Solver::default();
     let mut iteration = 0;

src/args.rs

@@ -29,6 +29,11 @@ pub enum Problems {
         #[arg(long, short = 's', required = true)]
         set: Vec<u32>,
     },
+    #[clap(visible_alias = "dc-ad")]
+    DecideCredulousAdmissibility {
+        #[arg(long, short = 'a', required = true)]
+        query: u32,
+    },
     #[clap(visible_alias = "ee-ad")]
     EnumerateAdmissibility,
     /// Will only return the empty extension if no other is found

src/error.rs

@@ -10,8 +10,8 @@ pub enum Error {
     OpeningAbaFile(::std::io::Error),
     #[error("sat call interrupted")]
     SatCallInterrupted,
-    #[error("problem internal check failed")]
+    #[error("problem internal check failed: {_0}")]
-    ProblemCheckFailed,
+    ProblemCheckFailed(String),
     #[error("formatting: {_0}")]
     Format(#[from] std::fmt::Error),
     #[error("outputting: {_0}")]

src/main.rs

@@ -5,7 +5,8 @@
 use std::{collections::HashSet, fmt::Write as WriteFmt, fs::read_to_string, io::Write as WriteIo};
 
 use aba::problems::admissibility::{
-    EnumerateAdmissibleExtensions, SampleAdmissibleExtension, VerifyAdmissibleExtension,
+    DecideCredulousAdmissibility, EnumerateAdmissibleExtensions, SampleAdmissibleExtension,
+    VerifyAdmissibleExtension,
 };
 use clap::Parser;
 
@@ -59,6 +60,10 @@ fn __main() -> Result {
         args::Problems::SampleAdmissibility => {
             aba::problems::solve(SampleAdmissibleExtension, &aba)?.fmt_iccma()
         }
+        args::Problems::DecideCredulousAdmissibility { query } => {
+            aba::problems::solve(DecideCredulousAdmissibility { assumption: query }, &aba)?
+                .fmt_iccma()
+        }
     }?;
     let mut stdout = std::io::stdout().lock();
     match writeln!(stdout, "{}", result) {