From f23baaa0e1953a5d3d68c0e32f3bfb3793780083 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 8 Oct 2024 11:51:37 +1100 Subject: [PATCH 1/2] 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 1b97195fcb..1edf467ebb 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 0e0535a51d..a7915ce73e 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 3f374c9fb6..57462da2a2 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() { From e9a239abdf7724740b0303616c1bb7a3094f3d04 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 8 Oct 2024 11:55:00 +1100 Subject: [PATCH 2/2] Change DIMACS parser to use const generic --- crates/pindakaas/src/lib.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/crates/pindakaas/src/lib.rs b/crates/pindakaas/src/lib.rs index a7915ce73e..4ce02e7736 100755 --- a/crates/pindakaas/src/lib.rs +++ b/crates/pindakaas/src/lib.rs @@ -564,7 +564,7 @@ enum Dimacs { Wcnf(Wcnf), } -fn parse_dimacs_file(path: &Path, expect_wcnf: bool) -> Result { +fn parse_dimacs_file(path: &Path) -> Result { let file = File::open(path)?; let mut had_header = false; @@ -579,7 +579,7 @@ fn parse_dimacs_file(path: &Path, expect_wcnf: bool) -> Result (), Ok(line) if had_header => { for seg in line.split(' ') { - if expect_wcnf { + if WEIGHTED { if let Ok(weight) = seg.parse::() { wcnf.weights.push(match weight.cmp(&top.unwrap()) { Ordering::Less => Some(weight), @@ -607,12 +607,12 @@ fn parse_dimacs_file(path: &Path, expect_wcnf: bool) -> Result { let vec: Vec<&str> = line.split_whitespace().collect(); // check "p" and "cnf" keyword - if !expect_wcnf && (vec.len() != 4 || vec[0..2] != ["p", "cnf"]) { + if !WEIGHTED && (vec.len() != 4 || vec[0..2] != ["p", "cnf"]) { return Err(io::Error::new( io::ErrorKind::InvalidInput, "expected DIMACS CNF header formatted \"p cnf {variables} {clauses}\"", )); - } else if expect_wcnf && (vec.len() != 4 || vec[0..2] != ["p", "wcnf"]) { + } else if WEIGHTED && (vec.len() != 4 || vec[0..2] != ["p", "wcnf"]) { return Err(io::Error::new( io::ErrorKind::InvalidInput, "expected DIMACS WCNF header formatted \"p wcnf {variables} {clauses} {top}\"", @@ -638,7 +638,7 @@ fn parse_dimacs_file(path: &Path, expect_wcnf: bool) -> Result Result Result Result { - match parse_dimacs_file(path, false)? { + match parse_dimacs_file::(path)? { Dimacs::Cnf(cnf) => Ok(cnf), _ => unreachable!(), } @@ -671,7 +671,7 @@ impl Cnf { impl Wcnf { /// Read a WCNF formula from a file formatted in the (W)DIMACS WCNF format pub fn from_file(path: &Path) -> Result { - match parse_dimacs_file(path, true)? { + match parse_dimacs_file::(path)? { Dimacs::Wcnf(wcnf) => Ok(wcnf), _ => unreachable!(), }