update

Cargo.toml

@@ -12,12 +12,12 @@ rust-version = "1.85"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-aig = { path = "./deps/aig-rs", version = "~0.2.4" }
+aig = { path = "./deps/aig-rs", version = "0.2.4" }
 satif-minisat = { path = "./deps/minisat-rs", version = "0.2" }
 satif-cadical = { path = "./deps/cadical-rs", version = "0.1" }
 satif-kissat = { path = "./deps/kissat-rs", version = "0.4" }
 logic-form = { path = "./deps/logic-form", version = "0.2" }
-giputils = { path = "./deps/giputils", version = "0.2" }
+giputils = { path = "./deps/giputils", version = "0.2.3" }
 satif = { path = "./deps/satif", version = "0.1" }
 abc-rs = { path = "./deps/abc-rs", version = "0.2" }
 btor = { path = "./deps/btor-rs", version = "0.1" }

src/gipsat/domain.rs

@@ -1,10 +1,10 @@
 use super::{search::Value, Solver};
 use crate::transys::Transys;
+use giputils::grc::Grc;
 use logic_form::{Var, VarSet};
 use std::{
     collections::HashSet,
     ops::{Deref, DerefMut},
-    rc::Rc,
 };
 
 pub struct Domain {
@@ -24,7 +24,7 @@ impl Domain {
         self.domain.reserve(var);
     }
 
-    pub fn calculate_constrain(&mut self, ts: &Rc<Transys>, value: &Value) {
+    pub fn calculate_constrain(&mut self, ts: &Grc<Transys>, value: &Value) {
         let mut marked = HashSet::new();
         let mut queue = Vec::new();
         for c in ts.constraints.iter() {
@@ -62,7 +62,7 @@ impl Domain {
     pub fn enable_local(
         &mut self,
         domain: impl Iterator<Item = Var>,
-        ts: &Rc<Transys>,
+        ts: &Grc<Transys>,
         _value: &Value,
     ) {
         self.reset();

src/gipsat/mod.rs

@@ -14,14 +14,13 @@ use analyze::Analyze;
 pub use cdb::ClauseKind;
 use cdb::{CRef, ClauseDB, CREF_NONE};
 use domain::Domain;
-use giputils::gvec::Gvec;
+use giputils::{grc::Grc, gvec::Gvec};
 use logic_form::{Clause, Cube, Lemma, Lit, LitSet, Var, VarMap};
 use propagate::Watchers;
 use rand::{rngs::StdRng, SeedableRng};
 use search::Value;
 use simplify::Simplify;
 use statistic::SolverStatistic;
-use std::rc::Rc;
 use utils::Lbool;
 use vsids::Vsids;
 
@@ -45,7 +44,7 @@ pub struct Solver {
     prepared_vsids: bool,
     constrain_act: Var,
 
-    ts: Rc<Transys>,
+    ts: Grc<Transys>,
 
     pub assump: Cube,
     pub constrain: Vec<Clause>,
@@ -59,7 +58,7 @@ pub struct Solver {
 }
 
 impl Solver {
-    pub fn new(options: Options, id: Option<usize>, ts: &Rc<Transys>) -> Self {
+    pub fn new(options: Options, id: Option<usize>, ts: &Grc<Transys>) -> Self {
         let mut solver = Self {
             id,
             ts: ts.clone(),

src/ic3/frame.rs

@@ -1,10 +1,10 @@
 use super::{proofoblig::ProofObligation, IC3};
 use crate::transys::Transys;
+use giputils::grc::Grc;
 use logic_form::{Cube, Lemma, Lit, LitSet};
 use std::{
     collections::HashSet,
     ops::{Deref, DerefMut},
-    rc::Rc,
 };
 
 #[derive(Clone)]
@@ -67,21 +67,20 @@ impl DerefMut for Frame {
     }
 }
 
-#[derive(Clone)]
 pub struct Frames {
-    frames: Rc<Vec<Frame>>,
+    frames: Vec<Frame>,
     pub early: usize,
-    pub tmp_lit_set: Rc<LitSet>,
+    pub tmp_lit_set: LitSet,
 }
 
 impl Frames {
-    pub fn new(ts: &Rc<Transys>) -> Self {
+    pub fn new(ts: &Grc<Transys>) -> Self {
         let mut tmp_lit_set = LitSet::new();
         tmp_lit_set.reserve(ts.max_latch);
         Self {
             frames: Default::default(),
             early: 1,
-            tmp_lit_set: Rc::new(tmp_lit_set),
+            tmp_lit_set,
         }
     }
 
@@ -91,20 +90,18 @@ impl Frames {
         frame: usize,
         lemma: &Lemma,
     ) -> Option<(usize, &'a mut Option<ProofObligation>)> {
-        let tmp_lit_set = unsafe { Rc::get_mut_unchecked(&mut self.tmp_lit_set) };
-        let frames = unsafe { Rc::get_mut_unchecked(&mut self.frames) };
         for l in lemma.iter() {
-            tmp_lit_set.insert(*l);
+            self.tmp_lit_set.insert(*l);
         }
-        for (i, fi) in frames.iter_mut().enumerate().skip(frame) {
+        for (i, fi) in self.frames.iter_mut().enumerate().skip(frame) {
             for j in 0..fi.len() {
-                if fi[j].lemma.subsume_set(lemma, tmp_lit_set) {
-                    tmp_lit_set.clear();
+                if fi[j].lemma.subsume_set(lemma, &self.tmp_lit_set) {
+                    self.tmp_lit_set.clear();
                     return Some((i, &mut fi[j].po));
                 }
             }
         }
-        tmp_lit_set.clear();
+        self.tmp_lit_set.clear();
         None
     }
 
@@ -198,7 +195,7 @@ impl DerefMut for Frames {
 impl Frames {
     #[inline]
     pub fn get_mut(&mut self) -> &mut Vec<Frame> {
-        unsafe { Rc::get_mut_unchecked(&mut self.frames) }
+        &mut self.frames
     }
 }
 

src/ic3/mod.rs

@@ -7,11 +7,12 @@ use crate::{
 use activity::Activity;
 use aig::{Aig, AigEdge};
 use frame::{Frame, Frames};
+use giputils::grc::Grc;
 use logic_form::{Clause, Cube, Lemma, Lit, Var};
 use mic::{DropVarParameter, MicType};
 use proofoblig::{ProofObligation, ProofObligationQueue};
 use statistic::Statistic;
-use std::{collections::HashMap, rc::Rc, time::Instant};
+use std::{collections::HashMap, time::Instant};
 
 mod activity;
 mod frame;
@@ -23,7 +24,7 @@ mod verify;
 
 pub struct IC3 {
     options: Options,
-    ts: Rc<Transys>,
+    ts: Grc<Transys>,
     frame: Frames,
     solvers: Vec<Solver>,
     lift: Solver,
@@ -64,9 +65,8 @@ impl IC3 {
                     }
                 }
             }
-            let ts = unsafe { Rc::get_mut_unchecked(&mut self.ts) };
             for i in init {
-                ts.add_init(i.var(), Some(i.polarity()));
+                self.ts.add_init(i.var(), Some(i.polarity()));
             }
         } else if self.level() == 1 {
             for cls in self.pre_lemmas.clone().iter() {
@@ -321,7 +321,7 @@ impl IC3 {
             ts = uts.interal_signals();
             ts = ts.simplify(&[], true, false);
         }
-        let ts = Rc::new(ts);
+        let ts = Grc::new(ts);
         let statistic = Statistic::new(&options.model);
         let activity = Activity::new(&ts);
         let frame = Frames::new(&ts);

src/ic3/proofoblig.rs

@@ -1,10 +1,10 @@
 use super::IC3;
+use giputils::grc::Grc;
 use logic_form::{Cube, Lemma};
 use std::cmp::Ordering;
 use std::collections::{btree_set, BTreeSet};
 use std::fmt::{self, Debug};
 use std::ops::{Deref, DerefMut};
-use std::rc::Rc;
 
 #[derive(Default)]
 pub struct ProofObligationInner {
@@ -65,13 +65,13 @@ impl Debug for ProofObligationInner {
 
 #[derive(Clone, Default)]
 pub struct ProofObligation {
-    inner: Rc<ProofObligationInner>,
+    inner: Grc<ProofObligationInner>,
 }
 
 impl ProofObligation {
     pub fn new(frame: usize, lemma: Lemma, input: Cube, depth: usize, next: Option<Self>) -> Self {
         Self {
-            inner: Rc::new(ProofObligationInner {
+            inner: Grc::new(ProofObligationInner {
                 frame,
                 input,
                 lemma,
@@ -112,7 +112,7 @@ impl Deref for ProofObligation {
 impl DerefMut for ProofObligation {
     #[inline]
     fn deref_mut(&mut self) -> &mut Self::Target {
-        unsafe { Rc::get_mut_unchecked(&mut self.inner) }
+        &mut self.inner
     }
 }
 

src/ic3/solver.rs

@@ -2,7 +2,7 @@ use super::IC3;
 use crate::gipsat::ClauseKind;
 use logic_form::{Clause, Cube, Lemma, Lit, Var};
 use rand::seq::SliceRandom;
-use std::{collections::HashSet, rc::Rc, time::Instant};
+use std::{collections::HashSet, time::Instant};
 
 impl IC3 {
     pub fn get_bad(&mut self) -> Option<(Cube, Cube)> {
@@ -118,8 +118,7 @@ impl IC3 {
     }
 
     pub fn new_var(&mut self) -> Var {
-        let ts = unsafe { Rc::get_mut_unchecked(&mut self.ts) };
-        let var = ts.new_var();
+        let var = self.ts.new_var();
         for s in self.solvers.iter_mut() {
             assert!(var == s.new_var());
         }
@@ -146,10 +145,10 @@ impl IC3 {
             }
             trans.push(nt);
         }
-        let ts = unsafe { Rc::get_mut_unchecked(&mut self.ts) };
-        ts.add_latch(state, next, init, trans.clone(), dep.clone());
-        let tmp_lit_set = unsafe { Rc::get_mut_unchecked(&mut self.frame.tmp_lit_set) };
-        tmp_lit_set.reserve(ts.max_latch);
+        self.ts
+            .add_latch(state, next, init, trans.clone(), dep.clone());
+        let tmp_lit_set = &mut self.frame.tmp_lit_set;
+        tmp_lit_set.reserve(self.ts.max_latch);
         for s in self.solvers.iter_mut().chain(Some(&mut self.lift)) {
             s.reset();
             for cls in trans.iter() {
@@ -159,18 +158,18 @@ impl IC3 {
         }
         if !self.solvers[0].value.v(state.lit()).is_none() {
             if self.solvers[0].value.v(state.lit()).is_true() {
-                ts.init.push(state.lit());
-                ts.init_map[state] = Some(true);
+                self.ts.init.push(state.lit());
+                self.ts.init_map[state] = Some(true);
             } else {
-                ts.init.push(!state.lit());
-                ts.init_map[state] = Some(false);
+                self.ts.init.push(!state.lit());
+                self.ts.init_map[state] = Some(false);
             }
         } else if !self.solvers[0].solve_with_domain(&[state.lit()], vec![], true) {
-            ts.init.push(!state.lit());
-            ts.init_map[state] = Some(false);
+            self.ts.init.push(!state.lit());
+            self.ts.init_map[state] = Some(false);
         } else if !self.solvers[0].solve_with_domain(&[!state.lit()], vec![], true) {
-            ts.init.push(state.lit());
-            ts.init_map[state] = Some(true);
+            self.ts.init.push(state.lit());
+            self.ts.init_map[state] = Some(true);
         }
         self.activity.reserve(state);
         self.auxiliary_var.push(state);