compatability to 0.5.1 and solvertests implemented

chrjabs · Jun 26, 2024 · 4649148 · 4649148
1 parent ed21c4f
commit 4649148
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 127 deletions.
diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "rustsat-batsat"
-version = "0.2.4"
+version = "0.1.0"
 edition = "2021"
 authors = ["Noah Bruns <nbruns@efs.at>"]
 license = "MIT"
@@ -15,8 +15,10 @@ readme = "README.md"
 debug = []
 
 [dependencies]
-batsat = "0.5.0" # when changing this version, do not forget to update signature
-rustsat = { version = "0.4.3", path = "../rustsat", default-features = false, features = [
-] }
+batsat = "0.5.0"                                                               # when changing this version, do not forget to update signature
+rustsat = { version = "0.5.1", path = "../rustsat", default-features = false }
 anyhow = { version = "1.0.80" }
 thiserror = { version = "1.0.57" }
+
+[dev-dependencies]
+rustsat-solvertests = { path = "../solvertests" }
diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs
@@ -30,6 +30,15 @@ impl Extend<Clause> for BatsatBasicSolver {
     }
 }
 
+impl<'a> Extend<&'a Clause> for BatsatBasicSolver {
+    fn extend<T: IntoIterator<Item = &'a Clause>>(&mut self, iter: T) {
+        iter.into_iter().for_each(|cl| {
+            self.add_clause_ref(cl)
+                .expect("Error adding clause in extend")
+        })
+    }
+}
+
 impl Solve for BatsatBasicSolver {
     fn signature(&self) -> &'static str {
         "BatSat 0.5.0"
@@ -68,6 +77,17 @@ impl Solve for BatsatBasicSolver {
 
         Ok(())
     }
+
+    fn add_clause_ref(&mut self, clause: &Clause) -> anyhow::Result<()> {
+        let mut c: Vec<batsat::Lit> = clause
+            .iter()
+            .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos()))
+            .collect::<Vec<batsat::Lit>>();
+
+        self.0.add_clause_reuse(&mut c);
+
+        Ok(())
+    }
 }
 
 impl SolveIncremental for BatsatBasicSolver {

diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs
@@ -1,86 +1 @@
-use rustsat::{
-    instances::{BasicVarManager, SatInstance},
-    lit,
-    solvers::{SolveIncremental, SolverResult},
-};
-use rustsat_batsat::BatsatBasicSolver;
-
-fn test_assumption_sequence<S: SolveIncremental>(mut solver: S) {
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/small.cnf").unwrap();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let res = solver.solve_assumps(&[!lit![0], !lit![1]]).unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], lit![1], lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], lit![1], lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], lit![1], !lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], lit![1], !lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let res = solver
-        .solve_assumps(&[lit![0], !lit![1], lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], !lit![1], lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let res = solver
-        .solve_assumps(&[lit![0], !lit![1], !lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[lit![0], !lit![1], !lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], lit![1], lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], lit![1], lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], lit![1], !lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let res = solver
-        .solve_assumps(&[!lit![0], lit![1], !lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Sat);
-    let res = solver
-        .solve_assumps(&[!lit![0], !lit![1], lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], !lit![1], lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], !lit![1], !lit![2], lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-    let res = solver
-        .solve_assumps(&[!lit![0], !lit![1], !lit![2], !lit![3]])
-        .unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-}
-
-#[test]
-fn assumption_sequence() {
-    let solver = BatsatBasicSolver::default();
-    test_assumption_sequence(solver);
-}
+rustsat_solvertests::incremental_tests!(rustsat_batsat::BatsatBasicSolver);
diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs
@@ -1,38 +1,3 @@
-use rustsat::{
-    instances::{BasicVarManager, SatInstance},
-    solvers::{Solve, SolverResult},
-};
-use rustsat_batsat::BatsatBasicSolver;
-
-#[test]
-fn ms_segfault() {
-    let mut solver = BatsatBasicSolver::default();
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Unsat);
-}
-
-#[test]
-fn small_sat() {
-    let mut solver = BatsatBasicSolver::default();
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Sat);
-}
-
-// Note: this instance seems too hard for batsat to solve
-#[test]
-#[ignore]
-fn small_unsat() {
-    let mut solver = BatsatBasicSolver::default();
-    let inst: SatInstance<BasicVarManager> =
-        SatInstance::from_dimacs_path("./data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf")
-            .unwrap();
-    solver.add_cnf(inst.as_cnf().0).unwrap();
-    let res = solver.solve().unwrap();
-    assert_eq!(res, SolverResult::Unsat);
+mod base {
+    rustsat_solvertests::base_tests!(rustsat_batsat::BatsatBasicSolver, false, true);
 }