Fix handling of empty clauses

pindakaashq · Oct 8, 2024 · f23baaa · f23baaa
1 parent 4a16611
commit f23baaa
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 9 deletions.
diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs
@@ -406,15 +406,17 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 				&mut self,
 				clause: I,
 			) -> crate::Result {
-				let mut added = false;
+				let mut empty = true;
 				for lit in clause.into_iter() {
 					unsafe { #krate::ipasir_add( #ptr , lit.into()) };
-					added = true;
+					empty = false;
 				}
-				if added {
-					unsafe { #krate::ipasir_add( #ptr , 0) };
+				unsafe { #krate::ipasir_add( #ptr , 0) };
+				if empty {
+					Err(crate::Unsatisfiable)
+				} else {
+					Ok(())
 				}
-				Ok(())
 			}
 
 			type CondDB = Self;

diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs
@@ -687,10 +687,12 @@ impl ClauseDatabase for Cnf {
 		let size = self.lits.len();
 		self.lits.extend(cl);
 		let len = self.lits.len() - size;
-		if len > 0 {
-			self.size.push(len);
+		self.size.push(len);
+		if len == 0 {
+			Err(Unsatisfiable)
+		} else {
+			Ok(())
 		}
-		Ok(())
 	}
 
 	type CondDB = Self;

diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs
@@ -113,7 +113,7 @@ mod tests {
 	use crate::{
 		linear::LimitComp,
 		solver::{cadical::Cadical, SolveResult, Solver},
-		CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, Valuation,
+		CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder, Unsatisfiable, Valuation,
 	};
 
 	#[test]
@@ -152,6 +152,13 @@ mod tests {
 		);
 	}
 
+	#[test]
+	fn test_cadical_empty_clause() {
+		let mut slv = Cadical::default();
+		assert_eq!(slv.add_clause([]), Err(Unsatisfiable));
+		assert_eq!(slv.solve(|_| unreachable!()), SolveResult::Unsat);
+	}
+
 	#[cfg(feature = "ipasir-up")]
 	#[test]
 	fn test_ipasir_up() {