From 464914895972d85863d582ff3fde8194142a9661 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH] compatability to 0.5.1 and solvertests implemented --- batsat/Cargo.toml | 10 +++-- batsat/src/lib.rs | 20 +++++++++ batsat/tests/incremental.rs | 87 +------------------------------------ batsat/tests/small.rs | 39 +---------------- 4 files changed, 29 insertions(+), 127 deletions(-) diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml index dc406b1a..94ad690a 100644 --- 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 "] 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 index 77bdb4fa..806d76c0 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -30,6 +30,15 @@ impl Extend for BatsatBasicSolver { } } +impl<'a> Extend<&'a Clause> for BatsatBasicSolver { + fn extend>(&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 = clause + .iter() + .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) + .collect::>(); + + self.0.add_clause_reuse(&mut c); + + Ok(()) + } } impl SolveIncremental for BatsatBasicSolver { diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs index a8b355f1..f76eb878 100644 --- 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(mut solver: S) { - let inst: SatInstance = - 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 index 90414ee8..a6f444c0 100644 --- 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 = - 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 = - 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 = - 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); }