From 4bbf867656bf86ab70bab4c7a8ba4e9ae1effa8c Mon Sep 17 00:00:00 2001
From: Christoph Jabs <christoph.jabs@helsinki.fi>
Date: Wed, 27 Mar 2024 10:50:05 +0200
Subject: [PATCH] fix: dpw edge cases with < 2 inputs

---
 rustsat/src/encodings/pb/dpw.rs | 47 ++++++++++++++++++++++++++++++---
 1 file changed, 44 insertions(+), 3 deletions(-)

diff --git a/rustsat/src/encodings/pb/dpw.rs b/rustsat/src/encodings/pb/dpw.rs
index 3205445e..14e70099 100644
--- a/rustsat/src/encodings/pb/dpw.rs
+++ b/rustsat/src/encodings/pb/dpw.rs
@@ -129,7 +129,18 @@ impl BoundUpper for DynamicPolyWatchdog {
     fn enforce_ub(&self, ub: usize) -> Result<Vec<Lit>, Error> {
         match &self.structure {
             Some(structure) => enforce_ub(structure, ub, &self.db),
-            None => Ok(vec![]),
+            None => {
+                if self.weight_sum() <= ub {
+                    return Ok(vec![]);
+                }
+                if self.in_lits.len() > 1 {
+                    return Err(Error::NotEncoded);
+                }
+                debug_assert_eq!(self.in_lits.len(), 1);
+                let (l, w) = self.in_lits.iter().next().unwrap();
+                debug_assert!(*w > ub);
+                Ok(vec![-(*l)])
+            }
         }
     }
 
@@ -161,7 +172,7 @@ impl BoundUpperIncremental for DynamicPolyWatchdog {
         R: RangeBounds<usize>,
     {
         let range = super::prepare_ub_range(self, range);
-        if range.is_empty() {
+        if range.is_empty() || self.in_lits.len() <= 1 {
             return;
         }
         let n_vars_before = var_manager.n_used();
@@ -659,6 +670,7 @@ mod tests {
         instances::{BasicVarManager, Cnf},
         lit,
         types::RsHashMap,
+        types::Var,
     };
 
     use super::DynamicPolyWatchdog;
@@ -671,13 +683,42 @@ mod tests {
         lits.insert(lit![2], 2);
         lits.insert(lit![3], 2);
         let mut dpw = DynamicPolyWatchdog::from(lits);
-        let mut var_manager = BasicVarManager::default();
+        let mut var_manager = BasicVarManager::from_next_free(Var::new(4));
         let mut cnf = Cnf::new();
         dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
         assert_eq!(dpw.n_vars(), 9);
         assert_eq!(cnf.len(), 13);
     }
 
+    #[test]
+    fn single_lit() {
+        let mut lits = RsHashMap::default();
+        lits.insert(lit![0], 4);
+        let mut dpw = DynamicPolyWatchdog::from(lits);
+        let mut var_manager = BasicVarManager::from_next_free(Var::new(1));
+        let mut cnf = Cnf::new();
+        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
+        assert_eq!(dpw.n_vars(), 0);
+        assert_eq!(cnf.len(), 0);
+        debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
+        let assumps = dpw.enforce_ub(2).unwrap();
+        debug_assert_eq!(assumps.len(), 1);
+        debug_assert_eq!(assumps[0], -lit![0]);
+    }
+
+    #[test]
+    fn no_lit() {
+        let lits = RsHashMap::default();
+        let mut dpw = DynamicPolyWatchdog::from(lits);
+        let mut var_manager = BasicVarManager::default();
+        let mut cnf = Cnf::new();
+        dpw.encode_ub(0..=6, &mut cnf, &mut var_manager);
+        assert_eq!(dpw.n_vars(), 0);
+        assert_eq!(cnf.len(), 0);
+        debug_assert!(dpw.enforce_ub(4).unwrap().is_empty());
+        debug_assert!(dpw.enforce_ub(0).unwrap().is_empty());
+    }
+
     #[test]
     fn coarse_convergence() {
         let mut lits = RsHashMap::default();