update

gipsyh · Dec 22, 2024 · e6523f0 · e6523f0
1 parent 001197e
commit e6523f0
Showing 1 changed file with 12 additions and 12 deletions.
diff --git a/src/ic3/mic.rs b/src/ic3/mic.rs
@@ -136,18 +136,19 @@ impl IC3 {
             if self.blocked_with_ordered(frame, &cube, false, true) {
                 return Some(self.solvers[frame - 1].inductive_core());
             }
-            // for lit in cube.iter() {
-            //     if keep.contains(lit) && !self.solvers[frame - 1].sat_value(*lit).is_some_and(|v| v)
-            //     {
-            //         return None;
-            //     }
-            // }
+            for lit in cube.iter() {
+                if keep.contains(lit) && !self.solvers[frame - 1].sat_value(*lit).is_some_and(|v| v)
+                {
+                    return None;
+                }
+            }
             let (model, _) = self.get_pred(frame, false);
-            // for lit in cube.iter() {
-            //     if keep.contains(lit) && !cex_set.contains(lit) {
-            //         return None;
-            //     }
-            // }
+            let cex_set: HashSet<Lit> = HashSet::from_iter(model.iter().cloned());
+            for lit in cube.iter() {
+                if keep.contains(lit) && !cex_set.contains(lit) {
+                    return None;
+                }
+            }
             if ctg < parameter.max
                 && frame > 1
                 && !self.ts.cube_subsume_init(&model)
@@ -162,7 +163,6 @@ impl IC3 {
                 continue;
             }
             ctg = 0;
-            let cex_set: HashSet<Lit> = HashSet::from_iter(model.iter().cloned());
             let mut cube_new = Cube::new();
             for lit in cube {
                 if cex_set.contains(&lit) {