feat: return error when assumption is eliminated

resolves #64

glucose/src/lib.rs

@@ -12,7 +12,10 @@
 //! The version of Glucose in this crate is Version 4.2.1.
 //! The used C++ source repository can be found [here](https://github.com/chrjabs/glucose4).
 
-use rustsat::{solvers::SolverState, types::Lit};
+use rustsat::{
+    solvers::SolverState,
+    types::{Lit, Var},
+};
 use std::{ffi::c_int, fmt};
 use thiserror::Error;
 
@@ -26,6 +29,10 @@ pub struct InvalidApiReturn {
     value: c_int,
 }
 
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("assumption variable {0} has been eliminated by glucose simplification")]
+pub struct AssumpEliminated(Var);
+
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
     #[default]

glucose/src/simp.rs

@@ -5,7 +5,7 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, InvalidApiReturn, Limit};
+use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::Glucose4Handle;
 use rustsat::{
@@ -176,6 +176,11 @@ impl SolveIncremental for Glucose {
     fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with glucose backend
+        for a in assumps {
+            if self.var_eliminated(a.var()) {
+                return Err(AssumpEliminated(a.var()).into());
+            }
+        }
         for a in assumps {
             unsafe { ffi::cglucosesimp4_assume(self.handle, a.to_ipasir()) }
         }

minisat/src/lib.rs

@@ -12,7 +12,10 @@
 //! The version of minisat in this crate is Version 2.2.0.
 //! The used C++ source repository can be found [here](https://github.com/chrjabs/minisat).
 
-use rustsat::{solvers::SolverState, types::Lit};
+use rustsat::{
+    solvers::SolverState,
+    types::{Lit, Var},
+};
 use std::{ffi::c_int, fmt};
 use thiserror::Error;
 
@@ -26,6 +29,10 @@ pub struct InvalidApiReturn {
     value: c_int,
 }
 
+#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)]
+#[error("assumption variable {0} has been eliminated by minisat simplification")]
+pub struct AssumpEliminated(Var);
+
 #[derive(Debug, PartialEq, Eq, Default)]
 enum InternalSolverState {
     #[default]

minisat/src/simp.rs

@@ -5,7 +5,7 @@
 
 use core::ffi::{c_int, CStr};
 
-use super::{InternalSolverState, InvalidApiReturn, Limit};
+use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit};
 use cpu_time::ProcessTime;
 use ffi::MinisatHandle;
 use rustsat::{
@@ -176,6 +176,11 @@ impl SolveIncremental for Minisat {
     fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result<SolverResult> {
         let start = ProcessTime::now();
         // Solve with minisat backend
+        for a in assumps {
+            if self.var_eliminated(a.var()) {
+                return Err(AssumpEliminated(a.var()).into());
+            }
+        }
         for a in assumps {
             unsafe { ffi::cminisatsimp_assume(self.handle, a.to_ipasir()) }
         }