diff --git a/src/transys/mod.rs b/src/transys/mod.rs
index f6c02de..51124b8 100644
--- a/src/transys/mod.rs
+++ b/src/transys/mod.rs
@@ -1,5 +1,3 @@
-pub mod others;
-pub mod sec;
 pub mod simplify;
 pub mod simulate;
 pub mod unroll;
@@ -260,23 +258,4 @@ impl Transys {
         println!("trans size: {}", self.trans.len());
         println!("num constraint: {}", self.constraints.len());
     }
-
-    // pub fn simplify_eq_latchs(&mut self, eqs: &[(Lit, Lit)], keep_dep: bool) {
-    //     let mut marks = HashSet::new();
-    //     let mut map = HashMap::new();
-    //     for (x, y) in eqs.iter() {
-    //         assert!(marks.insert(x.var()));
-    //         assert!(marks.insert(y.var()));
-    //         map.insert(*y, *x);
-    //         map.insert(!*y, !*x);
-    //     }
-    //     for cls in self.trans.iter_mut() {
-    //         for l in cls.iter_mut() {
-    //             if let Some(r) = map.get(l) {
-    //                 *l = *r;
-    //             }
-    //         }
-    //     }
-    //     self.simplify(&[], keep_dep, true)
-    // }
 }
diff --git a/src/transys/others.rs b/src/transys/others.rs
deleted file mode 100644
index c094ca3..0000000
--- a/src/transys/others.rs
+++ /dev/null
@@ -1,65 +0,0 @@
-use super::Transys;
-
-impl Transys {
-    pub fn encode_bad_to_latch(&mut self) {
-        todo!();
-        // assert!(self.bad.len() == 1);
-        // let bad = self.bad[0];
-        // let bad_latch = self.new_var().lit();
-        // let bad_next = self.new_var().lit();
-        // let trans = vec![
-        //     Clause::from([bad_next, !bad]),
-        //     Clause::from([!bad_next, bad]),
-        // ];
-        // self.latchs.push(bad_latch.var());
-        // self.init_map[bad_latch.var()] = Some(false);
-        // self.init.push(!bad_latch);
-        // self.is_latch[bad_latch.var()] = true;
-        // self.next_map[bad_latch] = bad_next;
-        // self.next_map[!bad_latch] = !bad_next;
-        // self.prev_map[bad_next] = bad_latch;
-        // self.prev_map[!bad_next] = !bad_latch;
-        // self.max_latch = self.max_latch.max(bad_latch.var());
-        // self.dependence[bad_next.var()] = vec![bad.var()];
-        // for t in trans {
-        //     self.trans.push(t);
-        // }
-        // self.bad = Cube::from([bad_next]);
-    }
-
-    pub fn reverse(&self) -> Self {
-        // let mut res = self.clone();
-        // res.encode_bad_to_latch();
-        // let latchs: Vec<Var> = res
-        //     .latchs
-        //     .iter()
-        //     .map(|v| res.lit_next(v.lit()).var())
-        //     .collect();
-        // let bad = res.bad[0];
-        // let mut init_map = VarMap::new();
-        // init_map.reserve(res.max_var);
-        // init_map[bad.var()] = Some(bad.polarity());
-        // let mut is_latch = VarMap::new();
-        // is_latch.reserve(res.max_var);
-        // for l in latchs.iter() {
-        //     is_latch[*l] = true;
-        // }
-        // let max_latch = *latchs.iter().max().unwrap();
-        // Self {
-        //     inputs: res.inputs,
-        //     latchs,
-        //     init: res.bad,
-        //     bad: res.init,
-        //     init_map,
-        //     constraints: res.constraints,
-        //     trans: res.trans,
-        //     max_var: res.max_var,
-        //     is_latch,
-        //     next_map: res.prev_map,
-        //     prev_map: res.next_map,
-        //     dependence: res.dependence,
-        //     max_latch,
-        // }
-        todo!()
-    }
-}
diff --git a/src/transys/sec.rs b/src/transys/sec.rs
deleted file mode 100644
index 946f3ca..0000000
--- a/src/transys/sec.rs
+++ /dev/null
@@ -1,77 +0,0 @@
-use super::unroll::TransysUnroll;
-use crate::transys::Transys;
-use logic_form::{Clause, Lit, Var};
-use satif::Satif;
-use std::collections::{HashMap, HashSet};
-
-impl Transys {
-    fn sec_with_bound(
-        uts: &TransysUnroll,
-        simulations: &HashMap<Var, u64>,
-        avoid: &mut HashSet<Var>,
-        eqs: &mut Vec<(Lit, Lit)>,
-    ) {
-        let mut solver = satif_cadical::Solver::new();
-        for k in 0..=uts.num_unroll {
-            uts.load_trans(&mut solver, k, true);
-            for (x, y) in eqs.iter() {
-                solver.add_clause(&uts.lits_next(&Clause::from([*x, !*y]), k));
-                solver.add_clause(&uts.lits_next(&Clause::from([!*x, *y]), k));
-            }
-        }
-        for i in 0..uts.ts.latchs.len() {
-            let x = uts.ts.latchs[i];
-            if avoid.contains(&x) {
-                continue;
-            }
-            for j in i + 1..uts.ts.latchs.len() {
-                let y = uts.ts.latchs[j];
-                if avoid.contains(&y) {
-                    continue;
-                }
-                if uts.ts.init_map[x].is_some()
-                    && uts.ts.init_map[x] == uts.ts.init_map[y]
-                    && simulations[&x] == simulations[&y]
-                {
-                    let act = solver.new_var().lit();
-                    let xl = x.lit();
-                    let yl = y.lit();
-                    for k in 0..=uts.num_unroll {
-                        let kxl = uts.lit_next(xl, k);
-                        let kyl = uts.lit_next(yl, k);
-                        solver.add_clause(&[!act, kxl, !kyl]);
-                        solver.add_clause(&[!act, !kxl, kyl]);
-                    }
-                    let nxl = uts.lit_next(xl, uts.num_unroll + 1);
-                    let nyl = uts.lit_next(yl, uts.num_unroll + 1);
-                    if !solver.solve(&[act, nxl, !nyl]) && !solver.solve(&[act, !nxl, nyl]) {
-                        eqs.push((xl, yl));
-                        avoid.insert(x);
-                        avoid.insert(y);
-                        dbg!(x, y);
-                        solver.add_clause(&[act]);
-                        break;
-                    } else {
-                        solver.add_clause(&[!act]);
-                    }
-                }
-            }
-        }
-    }
-
-    pub fn sec(&self) -> Vec<(Lit, Lit)> {
-        let mut eqs = Vec::new();
-        let mut avoid = HashSet::new();
-        let simulations = self.simulations();
-        let Some(simulations) = self.simulation_bv(simulations) else {
-            return eqs;
-        };
-        let mut uts = TransysUnroll::new(self);
-        Self::sec_with_bound(&uts, &simulations, &mut avoid, &mut eqs);
-        dbg!(eqs.len());
-        uts.unroll();
-        // Self::sec_with_bound(&uts, &simulations, &mut avoid, &mut eqs);
-        // dbg!(eqs.len());
-        eqs
-    }
-}
diff --git a/src/transys/unroll.rs b/src/transys/unroll.rs
index b2bbad9..3918b0f 100644
--- a/src/transys/unroll.rs
+++ b/src/transys/unroll.rs
@@ -155,50 +155,6 @@ impl TransysUnroll {
         }
     }
 
-    // pub fn primed_constrains(&self) -> Transys {
-    //     assert!(self.num_unroll == 1);
-    //     let mut trans = Cnf::new();
-    //     for u in 0..=1 {
-    //         for c in self.ts.trans.iter() {
-    //             let c: Clause = c.iter().map(|l| self.lit_next(*l, u)).collect();
-    //             trans.push(c);
-    //         }
-    //     }
-    //     let mut dependence = self.ts.dependence.clone();
-    //     dependence.reserve(Var::new(self.num_var));
-    //     let mut next_map = self.ts.next_map.clone();
-    //     next_map.reserve(Var::new(self.num_var));
-    //     for i in 0..self.ts.num_var {
-    //         let l = Var::new(i).lit();
-    //         next_map[l] = self.lit_next(l, 1);
-    //         next_map[!l] = self.lit_next(!l, 1);
-    //     }
-    //     for i in 0..self.ts.num_var {
-    //         let v = Var::new(i);
-    //         let n = self.lit_next(v.lit(), 1).var();
-    //         if dependence[n].is_empty() {
-    //             dependence[n] = dependence[v]
-    //                 .iter()
-    //                 .map(|l| self.lit_next(l.lit(), 1).var())
-    //                 .collect()
-    //         }
-    //     }
-    //     Transys {
-    //         inputs: self.ts.inputs.clone(),
-    //         latchs: self.ts.latchs.clone(),
-    //         init: self.ts.init.clone(),
-    //         bad: self.ts.bad.clone(),
-    //         init_map: self.ts.init_map.clone(),
-    //         constraints: self.ts.constraints.clone(),
-    //         trans,
-    //         num_var: self.num_var,
-    //         next_map,
-    //         dependence,
-    //         max_latch: self.ts.max_latch,
-    //         latch_group: self.ts.latch_group.clone(),
-    //     }
-    // }
-
     pub fn interal_signals(&self) -> Transys {
         let mut trans = self.ts.trans.clone();
         for c in self.ts.trans.iter() {