update

src/transys/builder.rs

@@ -6,7 +6,9 @@ use logic_form::{DagCnf, Lit, LitMap, LitVec, Var, VarMap};
 #[derive(Default, Debug)]
 pub struct TransysBuilder {
     pub input: Vec<Var>,
-    pub latch: GHashMap<Var, (Option<bool>, Lit)>,
+    pub latch: Vec<Var>,
+    pub next: GHashMap<Var, Lit>,
+    pub init: GHashMap<Var, bool>,
     pub bad: Lit,
     pub constraint: LitVec,
     pub rel: DagCnf,
@@ -21,15 +23,24 @@ impl TransysBuilder {
     pub fn from_aig(aig: &Aig, rst: &GHashMap<Var, Var>) -> Self {
         let input: Vec<Var> = aig.inputs.iter().map(|x| Var::new(*x)).collect();
         let constraint: LitVec = aig.constraints.iter().map(|c| c.to_lit()).collect();
-        let mut latch = GHashMap::new();
+        let mut latch = Vec::new();
+        let mut next = GHashMap::new();
+        let mut init = GHashMap::new();
         for l in aig.latchs.iter() {
-            latch.insert(Var::from(l.input), (l.init, l.next.to_lit()));
+            let lv = Var::from(l.input);
+            latch.push(lv);
+            next.insert(lv, l.next.to_lit());
+            if let Some(i) = l.init {
+                init.insert(lv, i);
+            }
         }
         let bad = aig.bads[0].to_lit();
         let rel = aig.get_cnf();
         Self {
             input,
             latch,
+            next,
+            init,
             bad,
             constraint,
             rel,
@@ -38,25 +49,23 @@ impl TransysBuilder {
     }
 
     pub fn build(mut self) -> Transys {
-        let mut latchs: Vec<_> = self.latch.keys().cloned().collect();
-        latchs.sort();
-        let primes: Vec<Lit> = latchs
+        self.latch.sort();
+        let primes: Vec<Lit> = self
+            .latch
             .iter()
-            .map(|l| {
-                let next = self.latch.get(l).unwrap().1;
-                self.rel.new_var().lit().not_if(!next.polarity())
-            })
+            .map(|l| self.rel.new_var().lit().not_if(!self.next[l].polarity()))
             .collect();
         let max_var = self.rel.max_var();
-        let max_latch = *latchs.iter().max().unwrap_or(&Var::CONST);
+        let max_latch = *self.latch.iter().max().unwrap_or(&Var::CONST);
         let mut init_map = VarMap::new_with(max_latch);
         let mut is_latch = VarMap::new_with(max_var);
         let mut init = LitVec::new();
         let mut next_map = LitMap::new_with(max_latch);
         let mut prev_map = LitMap::new_with(max_var);
-        for (v, p) in latchs.iter().cloned().zip(primes.iter().cloned()) {
+        for (v, p) in self.latch.iter().cloned().zip(primes.iter().cloned()) {
             let l = v.lit();
-            let (i, n) = *self.latch.get(&v).unwrap();
+            let i = self.init.get(&v).cloned();
+            let n = self.next[&v];
             self.rel.add_assign_rel(p, n);
             if let Some(i) = i {
                 init_map[v] = Some(i);
@@ -68,16 +77,16 @@ impl TransysBuilder {
             prev_map[!p] = !l;
             is_latch[v] = true;
         }
-        for (l, p) in latchs.iter().zip(primes.iter()) {
-            let n = self.latch[l].1;
+        for (l, p) in self.latch.iter().zip(primes.iter()) {
+            let n = self.next[l];
             assert!(p.polarity() == n.polarity());
             if let Some(r) = self.rst.get(&n.var()).cloned() {
                 self.rst.insert(p.var(), r);
             }
         }
         Transys {
             inputs: self.input,
-            latchs,
+            latchs: self.latch,
             init,
             bad: self.bad,
             init_map,

src/transys/simplify.rs

@@ -16,9 +16,9 @@ impl TransysBuilder {
         }
         let mut frozens = vec![Var::CONST, self.bad.var()];
         frozens.extend_from_slice(&self.input);
-        for (&l, (_, n)) in self.latch.iter() {
-            frozens.push(l);
-            frozens.push(n.var());
+        for l in self.latch.iter() {
+            frozens.push(*l);
+            frozens.push(self.next[l].var());
         }
         for c in self.constraint.iter() {
             if assert_constrain {
@@ -39,10 +39,12 @@ impl TransysBuilder {
         let domain_map = self.rel.arrange(frozens.into_iter());
         let map_lit = |l: &Lit| Lit::new(domain_map[&l.var()], l.polarity());
         self.input = self.input.iter().map(|v| domain_map[v]).collect();
-        self.latch = self
-            .latch
+        self.latch = self.latch.iter().map(|v| domain_map[v]).collect();
+        self.init = self.init.iter().map(|(v, i)| (domain_map[v], *i)).collect();
+        self.next = self
+            .next
             .iter()
-            .map(|(l, (i, n))| (domain_map[l], (*i, map_lit(n))))
+            .map(|(v, n)| (domain_map[v], map_lit(n)))
             .collect();
         self.bad = map_lit(&self.bad);
         self.constraint = if assert_constrain {