update

Cargo.toml

@@ -16,7 +16,7 @@ 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" }
+logic-form = { path = "./deps/logic-form", version = "0.2.6" }
 giputils = { path = "./deps/giputils", version = "0.2.3" }
 satif = { path = "./deps/satif", version = "0.1" }
 abc-rs = { path = "./deps/abc-rs", version = "0.2" }

src/bmc.rs

@@ -54,7 +54,7 @@ impl Engine for BMC {
             for s in last_bound..=k {
                 self.uts.load_trans(self.solver.as_mut(), s, true);
             }
-            let mut assump = self.uts.lits_next(&self.uts.ts.bad, k);
+            let mut assump = self.uts.lits_next(&self.uts.ts.bad.cube(), k);
             if self.options.bmc.bmc_kissat {
                 for b in assump.iter() {
                     self.solver.add_clause(&[*b]);

src/ic3/mod.rs

@@ -450,7 +450,7 @@ impl Engine for IC3 {
         let mut assump = if let Some(next) = b.next.clone() {
             self.ts.cube_next(&next.lemma)
         } else {
-            self.ts.bad.clone()
+            self.ts.bad.cube()
         };
         assump.extend_from_slice(&b.input);
         assert!(self.solvers[0].solve_with_domain(&assump, vec![], false));

src/ic3/solver.rs

@@ -9,9 +9,9 @@ impl IC3 {
         self.statistic.num_get_bad += 1;
         let start = Instant::now();
         let solver = self.solvers.last_mut().unwrap();
-        solver.assump = self.ts.bad.clone();
+        solver.assump = self.ts.bad.cube();
         solver.constrain = Default::default();
-        let res = solver.solve_with_domain(&self.ts.bad, vec![], false);
+        let res = solver.solve_with_domain(&self.ts.bad.cube(), vec![], false);
         self.statistic.block_get_bad_time += start.elapsed();
         if res {
             let frame = self.solvers.len();

src/ic3/verify.rs

@@ -17,12 +17,12 @@ pub fn verify_invariant(ts: &Transys, invariants: &[Lemma]) -> bool {
     for c in ts.constraints.iter() {
         solver.add_clause(&Clause::from([*c]));
     }
-    if solver.solve(&ts.bad) {
+    if solver.solve(&ts.bad.cube()) {
         return false;
     }
     for lemma in invariants {
         let mut assump = ts.constraints.clone();
-        assump.extend_from_slice(&ts.bad);
+        assump.push(ts.bad);
         if solver.solve(&ts.cube_next(lemma)) {
             return false;
         }
@@ -53,7 +53,7 @@ impl IC3 {
             let imply = if let Some(next) = bad.next.clone() {
                 self.ts.cube_next(&next.lemma)
             } else {
-                self.ts.bad.clone()
+                self.ts.bad.cube()
             };
             let mut assump = bad.lemma.deref().clone();
             assump.extend_from_slice(&bad.input);
@@ -86,7 +86,7 @@ impl IC3 {
         for k in 0..=uts.num_unroll {
             assumps.extend_from_slice(&uts.lits_next(constrain, k));
         }
-        assumps.extend_from_slice(&uts.lits_next(&uts.ts.bad, uts.num_unroll));
+        assumps.push(uts.lit_next(uts.ts.bad, uts.num_unroll));
         solver.solve(&assumps)
     }
 

src/kind.rs

@@ -75,7 +75,7 @@ impl Engine for Kind {
                 if bmc_k >= step {
                     for i in 0..=bmc_k - step {
                         self.solver
-                            .add_clause(&!self.uts.lits_next(&self.uts.ts.bad, i));
+                            .add_clause(&!self.uts.lits_next(&self.uts.ts.bad.cube(), i));
                     }
                 }
             }
@@ -85,7 +85,7 @@ impl Engine for Kind {
             }
             if !self.options.kind.no_bmc {
                 let mut assump = self.uts.ts.init.clone();
-                assump.extend_from_slice(&self.uts.lits_next(&self.uts.ts.bad, bmc_k));
+                assump.extend_from_slice(&self.uts.lits_next(&self.uts.ts.bad.cube(), bmc_k));
                 if self.options.verbose > 0 {
                     println!("kind bmc depth: {bmc_k}");
                 }
@@ -98,20 +98,21 @@ impl Engine for Kind {
             }
             for i in bmc_k + 1 - step..=bmc_k {
                 self.solver
-                    .add_clause(&!self.uts.lits_next(&self.uts.ts.bad, i));
+                    .add_clause(&!self.uts.lits_next(&self.uts.ts.bad.cube(), i));
             }
             self.uts.unroll_to(k);
             self.uts.load_trans(self.solver.as_mut(), k, true);
             if self.options.verbose > 0 {
                 println!("kind depth: {k}");
             }
             let res = if self.options.kind.kind_kissat {
-                for l in self.uts.lits_next(&self.uts.ts.bad, k) {
+                for l in self.uts.lits_next(&self.uts.ts.bad.cube(), k) {
                     self.solver.add_clause(&[l]);
                 }
                 self.solver.solve(&[])
             } else {
-                self.solver.solve(&self.uts.lits_next(&self.uts.ts.bad, k))
+                self.solver
+                    .solve(&self.uts.lits_next(&self.uts.ts.bad.cube(), k))
             };
             if !res {
                 println!("k-induction proofed in depth {k}");

src/transys/mod.rs

@@ -14,7 +14,7 @@ pub struct Transys {
     pub inputs: Vec<Var>,
     pub latchs: Vec<Var>,
     pub init: Cube,
-    pub bad: Cube,
+    pub bad: Lit,
     pub init_map: VarMap<Option<bool>>,
     pub constraints: Cube,
     pub trans: Vec<Clause>,
@@ -106,7 +106,7 @@ impl Transys {
             inputs,
             latchs,
             init,
-            bad: Cube::from([bad]),
+            bad,
             init_map,
             constraints,
             trans,

src/transys/simplify.rs

@@ -67,9 +67,7 @@ impl Transys {
             frozens.push(*l);
             frozens.push(self.var_next(*l))
         }
-        for b in self.bad.iter() {
-            frozens.push(b.var());
-        }
+        frozens.push(self.bad.var());
         for c in self.constraints.iter() {
             if assert_constrain {
                 simp_solver.add_clause(&[*c]);
@@ -108,7 +106,7 @@ impl Transys {
         let inputs = self.inputs.iter().map(|v| domain_map[v]).collect();
         let latchs: Vec<Var> = self.latchs.iter().map(|v| domain_map[v]).collect();
         let init = self.init.iter().map(map_lit).collect();
-        let bad = self.bad.iter().map(map_lit).collect();
+        let bad = map_lit(&self.bad);
         let max_latch = domain_map[&self.max_latch];
         let mut init_map: VarMap<Option<bool>> = VarMap::new_with(max_latch);
         for l in self.latchs.iter() {

src/transys/unroll.rs

@@ -141,7 +141,7 @@ impl TransysUnroll {
             inputs,
             latchs: self.ts.latchs.clone(),
             init: self.ts.init.clone(),
-            bad: self.lits_next(&self.ts.bad, 1),
+            bad: self.lit_next(self.ts.bad, 1),
             init_map: self.ts.init_map.clone(),
             constraints,
             trans,
@@ -236,10 +236,8 @@ impl TransysUnroll {
         for l in self.ts.latchs.iter() {
             keep.insert(self.ts.var_next(*l));
         }
-        for l in self.ts.bad.iter() {
-            if !self.ts.is_latch(l.var()) {
-                keep.insert(l.var());
-            }
+        if !self.ts.is_latch(self.ts.bad.var()) {
+            keep.insert(self.ts.bad.var());
         }
         let mut latchs = Vec::new();
         for v in Var::new(1)..=self.ts.max_var {
@@ -275,7 +273,7 @@ impl TransysUnroll {
             inputs: self.ts.inputs.clone(),
             latchs,
             init,
-            bad: self.ts.bad.clone(),
+            bad: self.ts.bad,
             init_map,
             constraints: self.ts.constraints.clone(),
             trans,