update

Cargo.toml

@@ -5,7 +5,7 @@ edition = "2021"
 authors = ["Yuheng Su <gipsyh.icu@gmail.com>"]
 repository = "https://github.com/gipsyh/rIC3"
 description = "rIC3: An efficient hardware model checker"
-keywords = ["model-checking", "formal-verification", "IC3", "SAT"]
+keywords = ["formal-verification", "model-checking", "IC3"]
 license = "GPL-3.0"
 rust-version = "1.85"
 
@@ -37,6 +37,9 @@ shadow-rs = "0.37.0"
 default = ["no_bound_check"]
 no_bound_check = ["logic-form/no_bound_check", "giputils/no_bound_check"]
 
+[profile.dev]
+opt-level = 3
+
 [profile.release]
 lto = true
 panic = "abort"

src/gipsat/analyze.rs

@@ -67,7 +67,7 @@ impl DerefMut for Analyze {
 
 impl Solver {
     fn lit_redundant(&mut self, lit: Lit) -> bool {
-        assert!(matches!(self.analyze[lit], Mark::Unseen | Mark::Seen));
+        debug_assert!(matches!(self.analyze[lit], Mark::Unseen | Mark::Seen));
         if self.reason[lit] == CREF_NONE {
             return false;
         }

src/gipsat/cdb.rs

@@ -79,13 +79,13 @@ impl Clause {
 
     #[inline]
     fn get_act(&self) -> f32 {
-        assert!(self.is_learnt());
+        debug_assert!(self.is_learnt());
         unsafe { (*self.data.add(self.len() + 1)).act }
     }
 
     #[inline]
     fn get_mut_act(&mut self) -> &mut f32 {
-        assert!(self.is_learnt());
+        debug_assert!(self.is_learnt());
         unsafe { &mut (*self.data.add(self.len() + 1)).act }
     }
 
@@ -165,7 +165,7 @@ impl Allocator {
 
     #[inline]
     fn alloc(&mut self, clause: &[Lit], trans: bool, learnt: bool) -> CRef {
-        assert!(!(trans && learnt));
+        debug_assert!(!(trans && learnt));
         let cid = self.data.len();
         let mut additional = clause.len() + 1;
         if learnt {
@@ -336,7 +336,7 @@ impl Solver {
     }
 
     pub fn attach_clause(&mut self, clause: &[Lit], kind: ClauseKind) -> CRef {
-        assert!(clause.len() > 1);
+        debug_assert!(clause.len() > 1);
         let id = self.cdb.alloc(clause, kind);
         self.watchers.attach(id, self.cdb.get(id));
         id
@@ -392,7 +392,7 @@ impl Solver {
     #[inline]
     pub fn strengthen_clause(&mut self, cref: CRef, lit: Lit) {
         let mut cls = self.cdb.get(cref);
-        assert!(cls.len() > 2);
+        debug_assert!(cls.len() > 2);
         let pos = cls.slice().iter().position(|l| l.eq(&lit)).unwrap();
         self.watchers.detach(cref, self.cdb.get(cref));
         cls.swap_remove(pos);
@@ -429,7 +429,6 @@ impl Solver {
                 self.cdb.lemmas.push(cref);
             }
         }
-        // assert!(lazy_remove_map.is_empty());
     }
 
     pub fn garbage_collect(&mut self) {

src/gipsat/propagate.rs

@@ -175,7 +175,7 @@ impl Solver {
             if cref[0] == l {
                 cref.swap(0, 1);
             }
-            assert!(cref[1] == l);
+            debug_assert!(cref[1] == l);
             let new_watcher = Watcher::new(cid, cref[0]);
             let v = self.value.v(cref[0]);
             if v == Lbool::TRUE || (v != Lbool::FALSE && !self.domain.has(cref[0].var())) {

src/gipsat/search.rs

@@ -112,7 +112,7 @@ impl Solver {
                 let (learnt, btl) = self.analyze(conflict);
                 self.backtrack(btl, true);
                 if learnt.len() == 1 {
-                    assert!(btl == 0);
+                    debug_assert!(btl == 0);
                     if !self.assign_full(learnt[0], CREF_NONE) {
                         self.unsat_core.clear();
                         return Some(false);