From f23baaa0e1953a5d3d68c0e32f3bfb3793780083 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Tue, 8 Oct 2024 11:51:37 +1100
Subject: [PATCH] Fix handling of empty clauses

---
 crates/pindakaas-derive/src/lib.rs     | 12 +++++++-----
 crates/pindakaas/src/lib.rs            |  8 +++++---
 crates/pindakaas/src/solver/cadical.rs |  9 ++++++++-
 3 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs
index 1b97195fc..1edf467eb 100644
--- 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
index 0e0535a51..a7915ce73 100755
--- 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
index 3f374c9fb..57462da2a 100644
--- 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() {