update

Cargo.toml

@@ -10,7 +10,7 @@ repository = "https://github.com/gipsyh/rIC3"
 [dependencies]
 aig = { path = "./deps/aig-rs", version = "0.2.1" }
 satif-minisat = { path = "./deps/minisat-rs", version = "0.2.1" }
-cadical = { path = "./deps/cadical-rs", version = "0.1.0" }
+satif-cadical = { path = "./deps/cadical-rs", version = "0.1.0" }
 satif-kissat = { path = "./deps/kissat-rs", version = "0.4.0" }
 logic-form = { path = "./deps/logic-form", version = "0.2.0" }
 clap = { version = "4.5.16", features = ["derive"] }

src/bmc.rs

@@ -21,7 +21,7 @@ impl BMC {
         let mut solver: Box<dyn Satif> = if options.bmc.bmc_kissat {
             Box::new(satif_kissat::Solver::new())
         } else {
-            Box::new(cadical::Solver::new())
+            Box::new(satif_cadical::Solver::new())
         };
         ts.load_init(solver.as_mut());
         Self {
@@ -35,7 +35,7 @@ impl BMC {
         self.solver = if self.options.bmc.bmc_kissat {
             Box::new(satif_kissat::Solver::new())
         } else {
-            Box::new(cadical::Solver::new())
+            Box::new(satif_cadical::Solver::new())
         };
         self.uts.ts.load_init(self.solver.as_mut());
     }

src/kind.rs

@@ -20,7 +20,7 @@ impl Kind {
         let solver: Box<dyn Satif> = if options.kind.kind_kissat {
             Box::new(satif_kissat::Solver::new())
         } else {
-            Box::new(cadical::Solver::new())
+            Box::new(satif_cadical::Solver::new())
         };
         Self {
             uts,
@@ -56,7 +56,7 @@ impl Kind {
         self.solver = if self.options.kind.kind_kissat {
             Box::new(satif_kissat::Solver::new())
         } else {
-            Box::new(cadical::Solver::new())
+            Box::new(satif_cadical::Solver::new())
         };
     }
 }

src/transys/sec.rs

@@ -11,7 +11,7 @@ impl Transys {
         avoid: &mut HashSet<Var>,
         eqs: &mut Vec<(Lit, Lit)>,
     ) {
-        let mut solver = cadical::Solver::new();
+        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() {

src/transys/simplify.rs

@@ -51,7 +51,7 @@ impl Transys {
         let mut simp_solver: Box<dyn Satif> = if keep_dep {
             Box::new(SimpSolver::new())
         } else {
-            Box::new(cadical::Solver::new())
+            Box::new(satif_cadical::Solver::new())
         };
         let false_lit: Lit = simp_solver.new_var().into();
         simp_solver.add_clause(&[!false_lit]);

src/transys/simulate.rs

@@ -1,7 +1,7 @@
 use crate::{transys::unroll::TransysUnroll, Transys};
-use cadical::Solver;
 use logic_form::{Cube, Var};
 use satif::Satif;
+use satif_cadical::Solver;
 use std::collections::HashMap;
 
 impl Transys {

src/verify.rs

@@ -103,7 +103,7 @@ impl IC3 {
     pub fn check_witness_by_bmc(&mut self, b: ProofObligation) -> Option<Cube> {
         let mut uts = TransysUnroll::new(&self.ts);
         uts.unroll_to(b.depth);
-        let mut solver: Box<dyn satif::Satif> = Box::new(cadical::Solver::new());
+        let mut solver: Box<dyn satif::Satif> = Box::new(satif_cadical::Solver::new());
         for k in 0..=b.depth {
             uts.load_trans(solver.as_mut(), k, false);
         }