From 5b78bd22cb25cb8adb1763064fdb81637cf192e1 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 10 Apr 2024 15:17:41 +0200 Subject: [PATCH 01/25] feat:implemented batsat api --- Cargo.toml | 1 + batsat/Cargo.toml | 22 ++++++++ batsat/data | 1 + batsat/src/lib.rs | 107 ++++++++++++++++++++++++++++++++++++ batsat/tests/incremental.rs | 89 ++++++++++++++++++++++++++++++ batsat/tests/small.rs | 38 +++++++++++++ 6 files changed, 258 insertions(+) create mode 100644 batsat/Cargo.toml create mode 120000 batsat/data create mode 100644 batsat/src/lib.rs create mode 100644 batsat/tests/incremental.rs create mode 100644 batsat/tests/small.rs diff --git a/Cargo.toml b/Cargo.toml index cc31a465..3af1375c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,6 +7,7 @@ members = [ "glucose", "minisat", "ipasir", + "batsat", ] resolver = "2" diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml new file mode 100644 index 00000000..0ebf7b28 --- /dev/null +++ b/batsat/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "rustsat-batsat" +version = "0.2.4" +edition = "2021" +authors = ["Noah Bruns "] +license = "MIT" +description = "Interface to the SAT solver BatSat for the RustSAT library. BatSat is fully implemented in Rust" +keywords = ["sat-solver", "rustsat", "batsat"] +repository = "https://github.com/chrjabs/rustsat" +readme = "README.md" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[features] +debug = [] + +[dependencies] +batsat = "0.5.0" +rustsat = { version = "0.4.3", path = "../rustsat", default-features = false, features = [ +] } +anyhow = { version = "1.0.80" } +thiserror = { version = "1.0.57" } diff --git a/batsat/data b/batsat/data new file mode 120000 index 00000000..4909e06e --- /dev/null +++ b/batsat/data @@ -0,0 +1 @@ +../data \ No newline at end of file diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs new file mode 100644 index 00000000..76904587 --- /dev/null +++ b/batsat/src/lib.rs @@ -0,0 +1,107 @@ +//! # Minisat Solver Interface Without Preprocessing (Core) +//! +//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental +//! SAT solver. + +use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; +use rustsat::{ + solvers::{Solve, SolveIncremental, SolverResult}, + types::{Clause, Lit, TernaryVal}, +}; +use thiserror::Error; + +#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] +#[error("BatSat returned an invalid value: {error}")] +pub struct InvalidApiReturn { + error: &'static str, +} + +pub struct BatsatBasicSolver(BasicSolver); + +impl Default for BatsatBasicSolver { + fn default() -> BatsatBasicSolver { + BatsatBasicSolver(BasicSolver::default()) + } +} + +impl Extend for BatsatBasicSolver { + fn extend>(&mut self, iter: T) { + iter.into_iter() + .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend")) + } +} + +impl Solve for BatsatBasicSolver { + fn signature(&self) -> &'static str { + "BatSat 0.5.0" + } + + fn solve(&mut self) -> anyhow::Result { + match self.0.solve_limited(&[]) { + x if x == lbool::TRUE => Ok(SolverResult::Sat), + x if x == lbool::FALSE => Ok(SolverResult::Unsat), + x if x == lbool::UNDEF => Err(InvalidApiReturn { + error: "BatSat Solver is in an UNSAT state".into(), + } + .into()), + + _ => unreachable!(), + } + } + + fn lit_val(&self, lit: Lit) -> anyhow::Result { + let l = batsat::Lit::new(batsat::Var::from_index(lit.vidx() + 1), lit.is_pos()); + + match self.0.value_lit(l) { + x if x == lbool::TRUE => Ok(TernaryVal::True), + x if x == lbool::FALSE => Ok(TernaryVal::False), + x if x == lbool::UNDEF => Ok(TernaryVal::DontCare), + _ => unreachable!(), + } + } + + fn add_clause(&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::>(); + + match self.0.add_clause_reuse(&mut c) { + true => Ok(()), + false => Ok(()), //Err(SolverError::Api("Currently in an UNSAT state".into())), + } + } +} + +impl SolveIncremental for BatsatBasicSolver { + fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result { + let a = assumps + .iter() + .map(|l| { + batsat::Lit::new( + self.0.var_of_int((l.vidx32() + 1).try_into().unwrap()), + l.is_pos(), + ) + }) + .collect::>(); + + match self.0.solve_limited(&a) { + x if x == lbool::TRUE => Ok(SolverResult::Sat), + x if x == lbool::FALSE => Ok(SolverResult::Unsat), + x if x == lbool::UNDEF => Err(InvalidApiReturn { + error: "BatSat Solver is in an UNSAT state".into(), + } + .into()), + _ => unreachable!(), + } + } + + fn core(&mut self) -> anyhow::Result> { + Ok(self + .0 + .unsat_core() + .iter() + .map(|l| Lit::new(l.var().idx() - 1, !l.sign())) + .collect::>()) + } +} diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs new file mode 100644 index 00000000..712645c7 --- /dev/null +++ b/batsat/tests/incremental.rs @@ -0,0 +1,89 @@ +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); +} + +// Note: Cannot test prepro version of minisat with this small example because +// the variable are eliminated by preprocessing diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs new file mode 100644 index 00000000..c72dd409 --- /dev/null +++ b/batsat/tests/small.rs @@ -0,0 +1,38 @@ +use rustsat::{ + instances::{BasicVarManager, SatInstance}, + solvers::{Solve, SolverResult}, +}; +use rustsat_batsat::BatsatBasicSolver; + +#[test] +fn core_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 simp_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 minisat to solve +#[test] +#[ignore] +fn simp_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); +} From b8326bea437248ab8f622519fd8cc5d56fa8a412 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 10 Apr 2024 15:55:25 +0200 Subject: [PATCH 02/25] docs: changelog and readme added --- batsat/.gitignore | 2 ++ batsat/CHANGELOG.md | 11 +++++++++++ batsat/README.md | 18 ++++++++++++++++++ batsat/src/lib.rs | 4 ++-- 4 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 batsat/.gitignore create mode 100644 batsat/CHANGELOG.md create mode 100644 batsat/README.md diff --git a/batsat/.gitignore b/batsat/.gitignore new file mode 100644 index 00000000..2ebc5ea0 --- /dev/null +++ b/batsat/.gitignore @@ -0,0 +1,2 @@ +/target +/Cargo.lock \ No newline at end of file diff --git a/batsat/CHANGELOG.md b/batsat/CHANGELOG.md new file mode 100644 index 00000000..ef16d198 --- /dev/null +++ b/batsat/CHANGELOG.md @@ -0,0 +1,11 @@ +# Changelog + +All notable changes to this project will be documented in this file. + +## [0.2.4] - 2024-04-10 + +### 🚀 Features + +- Implemented batsat api + + diff --git a/batsat/README.md b/batsat/README.md new file mode 100644 index 00000000..846af6d9 --- /dev/null +++ b/batsat/README.md @@ -0,0 +1,18 @@ +[![Check & Test](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml) +[![crates.io](https://img.shields.io/crates/v/rustsat-batsat)](https://crates.io/crates/rustsat-batsat) +[![docs.rs](https://img.shields.io/docsrs/rustsat-batsat)](https://docs.rs/rustsat-batsat) +[![License](https://img.shields.io/crates/l/rustsat-batsat)](../LICENSE) + + + +# rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT + +The BatSat solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. + +## Features + +## BatSat Version + +The version of BatSat in this crate is Version 0.5.0. + + diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 76904587..b4a8b4a6 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,6 +1,6 @@ -//! # Minisat Solver Interface Without Preprocessing (Core) +//! # BatSat Solver Interface //! -//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental +//! Interface to the [Minisat](https://github.com/c-cube/batsat) incremental //! SAT solver. use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; From ae01e17faee9988cea6f5d18ee3612a8df7edbd4 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 10 Apr 2024 15:56:36 +0200 Subject: [PATCH 03/25] ci: running github workflows --- .github/workflows/batsat.yml | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 .github/workflows/batsat.yml diff --git a/.github/workflows/batsat.yml b/.github/workflows/batsat.yml new file mode 100644 index 00000000..8eb0e5dd --- /dev/null +++ b/.github/workflows/batsat.yml @@ -0,0 +1,34 @@ +name: BatSat + +on: + push: + branches: [ "main" ] + pull_request: + branches: [ "main" ] + +env: + CARGO_TERM_COLOR: always + +jobs: + build-test: + name: Build and test + strategy: + matrix: + os: [ubuntu-latest, macos-latest, windows-latest] + runs-on: ${{ matrix.os }} + steps: + - name: Checkout sources + uses: actions/checkout@v4 + - name: Install stable toolchain + uses: dtolnay/rust-toolchain@stable + - uses: Swatinem/rust-cache@v2 + with: + shared-key: "build-test" + - name: Cargo build + run: cargo build -p rustsat-batsat --verbose + env: + CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} + - name: Cargo test + run: cargo test -p rustsat-batsat --verbose + env: + CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} From 4b58cc80477944fd9188f02cf4b5dd02138974da Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed, 10 Apr 2024 17:08:58 +0200 Subject: [PATCH 04/25] docs: fixed comments --- batsat/Cargo.toml | 2 +- batsat/src/lib.rs | 3 +-- batsat/tests/incremental.rs | 3 --- batsat/tests/small.rs | 2 +- 4 files changed, 3 insertions(+), 7 deletions(-) diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml index 0ebf7b28..dc406b1a 100644 --- a/batsat/Cargo.toml +++ b/batsat/Cargo.toml @@ -15,7 +15,7 @@ readme = "README.md" debug = [] [dependencies] -batsat = "0.5.0" +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 = [ ] } anyhow = { version = "1.0.80" } diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index b4a8b4a6..8562666b 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,7 +1,6 @@ //! # BatSat Solver Interface //! -//! Interface to the [Minisat](https://github.com/c-cube/batsat) incremental -//! SAT solver. +//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; use rustsat::{ diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs index 712645c7..a8b355f1 100644 --- a/batsat/tests/incremental.rs +++ b/batsat/tests/incremental.rs @@ -84,6 +84,3 @@ fn assumption_sequence() { let solver = BatsatBasicSolver::default(); test_assumption_sequence(solver); } - -// Note: Cannot test prepro version of minisat with this small example because -// the variable are eliminated by preprocessing diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs index c72dd409..fa445d9b 100644 --- a/batsat/tests/small.rs +++ b/batsat/tests/small.rs @@ -24,7 +24,7 @@ fn simp_small_sat() { assert_eq!(res, SolverResult::Sat); } -// Note: this instance seems too hard for minisat to solve +// Note: this instance seems too hard for batsat to solve #[test] #[ignore] fn simp_small_unsat() { From 46b2c2724d41cd91fa029abb9fdf184d4a803bd8 Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed, 10 Apr 2024 17:10:03 +0200 Subject: [PATCH 05/25] fix: return of ok if clause not added --- batsat/src/lib.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 8562666b..77bdb4fa 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -43,7 +43,6 @@ impl Solve for BatsatBasicSolver { error: "BatSat Solver is in an UNSAT state".into(), } .into()), - _ => unreachable!(), } } @@ -65,10 +64,9 @@ impl Solve for BatsatBasicSolver { .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) .collect::>(); - match self.0.add_clause_reuse(&mut c) { - true => Ok(()), - false => Ok(()), //Err(SolverError::Api("Currently in an UNSAT state".into())), - } + self.0.add_clause_reuse(&mut c); + + Ok(()) } } From 31d7e1c623f4682f2b65417f81882503c7121077 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 10 Apr 2024 16:25:51 +0200 Subject: [PATCH 06/25] test: cleanup and renaming --- batsat/tests/small.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs index fa445d9b..90414ee8 100644 --- a/batsat/tests/small.rs +++ b/batsat/tests/small.rs @@ -5,7 +5,7 @@ use rustsat::{ use rustsat_batsat::BatsatBasicSolver; #[test] -fn core_ms_segfault() { +fn ms_segfault() { let mut solver = BatsatBasicSolver::default(); let inst: SatInstance = SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); @@ -15,7 +15,7 @@ fn core_ms_segfault() { } #[test] -fn simp_small_sat() { +fn small_sat() { let mut solver = BatsatBasicSolver::default(); let inst: SatInstance = SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); @@ -27,7 +27,7 @@ fn simp_small_sat() { // Note: this instance seems too hard for batsat to solve #[test] #[ignore] -fn simp_small_unsat() { +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") From 1e6aa6b2fb2a52a18d87c3509bb658cfebb48c69 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Fri, 14 Jun 2024 17:21:51 +0200 Subject: [PATCH 07/25] 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); } From 9f59fdd724d660d54073df2985f7b41524114a38 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 08/25] feat:implemented batsat api --- Cargo.toml | 1 + batsat/Cargo.toml | 22 ++++++++ batsat/data | 1 + batsat/src/lib.rs | 107 ++++++++++++++++++++++++++++++++++++ batsat/tests/incremental.rs | 89 ++++++++++++++++++++++++++++++ batsat/tests/small.rs | 38 +++++++++++++ 6 files changed, 258 insertions(+) create mode 100644 batsat/Cargo.toml create mode 120000 batsat/data create mode 100644 batsat/src/lib.rs create mode 100644 batsat/tests/incremental.rs create mode 100644 batsat/tests/small.rs diff --git a/Cargo.toml b/Cargo.toml index 8714c4b4..386f0b2d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -9,6 +9,7 @@ members = [ "solvertests", "capi", "pyapi", + "batsat", ] resolver = "2" diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml new file mode 100644 index 00000000..0ebf7b28 --- /dev/null +++ b/batsat/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "rustsat-batsat" +version = "0.2.4" +edition = "2021" +authors = ["Noah Bruns "] +license = "MIT" +description = "Interface to the SAT solver BatSat for the RustSAT library. BatSat is fully implemented in Rust" +keywords = ["sat-solver", "rustsat", "batsat"] +repository = "https://github.com/chrjabs/rustsat" +readme = "README.md" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[features] +debug = [] + +[dependencies] +batsat = "0.5.0" +rustsat = { version = "0.4.3", path = "../rustsat", default-features = false, features = [ +] } +anyhow = { version = "1.0.80" } +thiserror = { version = "1.0.57" } diff --git a/batsat/data b/batsat/data new file mode 120000 index 00000000..4909e06e --- /dev/null +++ b/batsat/data @@ -0,0 +1 @@ +../data \ No newline at end of file diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs new file mode 100644 index 00000000..76904587 --- /dev/null +++ b/batsat/src/lib.rs @@ -0,0 +1,107 @@ +//! # Minisat Solver Interface Without Preprocessing (Core) +//! +//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental +//! SAT solver. + +use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; +use rustsat::{ + solvers::{Solve, SolveIncremental, SolverResult}, + types::{Clause, Lit, TernaryVal}, +}; +use thiserror::Error; + +#[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] +#[error("BatSat returned an invalid value: {error}")] +pub struct InvalidApiReturn { + error: &'static str, +} + +pub struct BatsatBasicSolver(BasicSolver); + +impl Default for BatsatBasicSolver { + fn default() -> BatsatBasicSolver { + BatsatBasicSolver(BasicSolver::default()) + } +} + +impl Extend for BatsatBasicSolver { + fn extend>(&mut self, iter: T) { + iter.into_iter() + .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend")) + } +} + +impl Solve for BatsatBasicSolver { + fn signature(&self) -> &'static str { + "BatSat 0.5.0" + } + + fn solve(&mut self) -> anyhow::Result { + match self.0.solve_limited(&[]) { + x if x == lbool::TRUE => Ok(SolverResult::Sat), + x if x == lbool::FALSE => Ok(SolverResult::Unsat), + x if x == lbool::UNDEF => Err(InvalidApiReturn { + error: "BatSat Solver is in an UNSAT state".into(), + } + .into()), + + _ => unreachable!(), + } + } + + fn lit_val(&self, lit: Lit) -> anyhow::Result { + let l = batsat::Lit::new(batsat::Var::from_index(lit.vidx() + 1), lit.is_pos()); + + match self.0.value_lit(l) { + x if x == lbool::TRUE => Ok(TernaryVal::True), + x if x == lbool::FALSE => Ok(TernaryVal::False), + x if x == lbool::UNDEF => Ok(TernaryVal::DontCare), + _ => unreachable!(), + } + } + + fn add_clause(&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::>(); + + match self.0.add_clause_reuse(&mut c) { + true => Ok(()), + false => Ok(()), //Err(SolverError::Api("Currently in an UNSAT state".into())), + } + } +} + +impl SolveIncremental for BatsatBasicSolver { + fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result { + let a = assumps + .iter() + .map(|l| { + batsat::Lit::new( + self.0.var_of_int((l.vidx32() + 1).try_into().unwrap()), + l.is_pos(), + ) + }) + .collect::>(); + + match self.0.solve_limited(&a) { + x if x == lbool::TRUE => Ok(SolverResult::Sat), + x if x == lbool::FALSE => Ok(SolverResult::Unsat), + x if x == lbool::UNDEF => Err(InvalidApiReturn { + error: "BatSat Solver is in an UNSAT state".into(), + } + .into()), + _ => unreachable!(), + } + } + + fn core(&mut self) -> anyhow::Result> { + Ok(self + .0 + .unsat_core() + .iter() + .map(|l| Lit::new(l.var().idx() - 1, !l.sign())) + .collect::>()) + } +} diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs new file mode 100644 index 00000000..712645c7 --- /dev/null +++ b/batsat/tests/incremental.rs @@ -0,0 +1,89 @@ +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); +} + +// Note: Cannot test prepro version of minisat with this small example because +// the variable are eliminated by preprocessing diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs new file mode 100644 index 00000000..c72dd409 --- /dev/null +++ b/batsat/tests/small.rs @@ -0,0 +1,38 @@ +use rustsat::{ + instances::{BasicVarManager, SatInstance}, + solvers::{Solve, SolverResult}, +}; +use rustsat_batsat::BatsatBasicSolver; + +#[test] +fn core_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 simp_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 minisat to solve +#[test] +#[ignore] +fn simp_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); +} From 2ccc905540fe14f0189caf89691f4036b60f71c2 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 09/25] docs: changelog and readme added --- batsat/.gitignore | 2 ++ batsat/CHANGELOG.md | 11 +++++++++++ batsat/README.md | 18 ++++++++++++++++++ batsat/src/lib.rs | 4 ++-- 4 files changed, 33 insertions(+), 2 deletions(-) create mode 100644 batsat/.gitignore create mode 100644 batsat/CHANGELOG.md create mode 100644 batsat/README.md diff --git a/batsat/.gitignore b/batsat/.gitignore new file mode 100644 index 00000000..2ebc5ea0 --- /dev/null +++ b/batsat/.gitignore @@ -0,0 +1,2 @@ +/target +/Cargo.lock \ No newline at end of file diff --git a/batsat/CHANGELOG.md b/batsat/CHANGELOG.md new file mode 100644 index 00000000..ef16d198 --- /dev/null +++ b/batsat/CHANGELOG.md @@ -0,0 +1,11 @@ +# Changelog + +All notable changes to this project will be documented in this file. + +## [0.2.4] - 2024-04-10 + +### 🚀 Features + +- Implemented batsat api + + diff --git a/batsat/README.md b/batsat/README.md new file mode 100644 index 00000000..846af6d9 --- /dev/null +++ b/batsat/README.md @@ -0,0 +1,18 @@ +[![Check & Test](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/batsat.yml) +[![crates.io](https://img.shields.io/crates/v/rustsat-batsat)](https://crates.io/crates/rustsat-batsat) +[![docs.rs](https://img.shields.io/docsrs/rustsat-batsat)](https://docs.rs/rustsat-batsat) +[![License](https://img.shields.io/crates/l/rustsat-batsat)](../LICENSE) + + + +# rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT + +The BatSat solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. + +## Features + +## BatSat Version + +The version of BatSat in this crate is Version 0.5.0. + + diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 76904587..b4a8b4a6 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,6 +1,6 @@ -//! # Minisat Solver Interface Without Preprocessing (Core) +//! # BatSat Solver Interface //! -//! Interface to the [Minisat](https://github.com/niklasso/minisat) incremental +//! Interface to the [Minisat](https://github.com/c-cube/batsat) incremental //! SAT solver. use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; From 4acddcd783dcfe9f6511e3744b700fed26a920af Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 10/25] ci: running github workflows --- .github/workflows/batsat.yml | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 .github/workflows/batsat.yml diff --git a/.github/workflows/batsat.yml b/.github/workflows/batsat.yml new file mode 100644 index 00000000..8eb0e5dd --- /dev/null +++ b/.github/workflows/batsat.yml @@ -0,0 +1,34 @@ +name: BatSat + +on: + push: + branches: [ "main" ] + pull_request: + branches: [ "main" ] + +env: + CARGO_TERM_COLOR: always + +jobs: + build-test: + name: Build and test + strategy: + matrix: + os: [ubuntu-latest, macos-latest, windows-latest] + runs-on: ${{ matrix.os }} + steps: + - name: Checkout sources + uses: actions/checkout@v4 + - name: Install stable toolchain + uses: dtolnay/rust-toolchain@stable + - uses: Swatinem/rust-cache@v2 + with: + shared-key: "build-test" + - name: Cargo build + run: cargo build -p rustsat-batsat --verbose + env: + CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} + - name: Cargo test + run: cargo test -p rustsat-batsat --verbose + env: + CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} From a0e84a1d286b8b31742bc2b65ba2ced2218bee82 Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 11/25] docs: fixed comments --- batsat/Cargo.toml | 2 +- batsat/src/lib.rs | 3 +-- batsat/tests/incremental.rs | 3 --- batsat/tests/small.rs | 2 +- 4 files changed, 3 insertions(+), 7 deletions(-) diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml index 0ebf7b28..dc406b1a 100644 --- a/batsat/Cargo.toml +++ b/batsat/Cargo.toml @@ -15,7 +15,7 @@ readme = "README.md" debug = [] [dependencies] -batsat = "0.5.0" +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 = [ ] } anyhow = { version = "1.0.80" } diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index b4a8b4a6..8562666b 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,7 +1,6 @@ //! # BatSat Solver Interface //! -//! Interface to the [Minisat](https://github.com/c-cube/batsat) incremental -//! SAT solver. +//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; use rustsat::{ diff --git a/batsat/tests/incremental.rs b/batsat/tests/incremental.rs index 712645c7..a8b355f1 100644 --- a/batsat/tests/incremental.rs +++ b/batsat/tests/incremental.rs @@ -84,6 +84,3 @@ fn assumption_sequence() { let solver = BatsatBasicSolver::default(); test_assumption_sequence(solver); } - -// Note: Cannot test prepro version of minisat with this small example because -// the variable are eliminated by preprocessing diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs index c72dd409..fa445d9b 100644 --- a/batsat/tests/small.rs +++ b/batsat/tests/small.rs @@ -24,7 +24,7 @@ fn simp_small_sat() { assert_eq!(res, SolverResult::Sat); } -// Note: this instance seems too hard for minisat to solve +// Note: this instance seems too hard for batsat to solve #[test] #[ignore] fn simp_small_unsat() { From 8ecd6ad406d6de7feade94bac6e85025709dcbe8 Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 12/25] fix: return of ok if clause not added --- batsat/src/lib.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 8562666b..77bdb4fa 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -43,7 +43,6 @@ impl Solve for BatsatBasicSolver { error: "BatSat Solver is in an UNSAT state".into(), } .into()), - _ => unreachable!(), } } @@ -65,10 +64,9 @@ impl Solve for BatsatBasicSolver { .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) .collect::>(); - match self.0.add_clause_reuse(&mut c) { - true => Ok(()), - false => Ok(()), //Err(SolverError::Api("Currently in an UNSAT state".into())), - } + self.0.add_clause_reuse(&mut c); + + Ok(()) } } From ed21c4f61c2d054ebe2e2f63c8780904a86a3e99 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 13/25] test: cleanup and renaming --- batsat/tests/small.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/batsat/tests/small.rs b/batsat/tests/small.rs index fa445d9b..90414ee8 100644 --- a/batsat/tests/small.rs +++ b/batsat/tests/small.rs @@ -5,7 +5,7 @@ use rustsat::{ use rustsat_batsat::BatsatBasicSolver; #[test] -fn core_ms_segfault() { +fn ms_segfault() { let mut solver = BatsatBasicSolver::default(); let inst: SatInstance = SatInstance::from_dimacs_path("./data/minisat-segfault.cnf").unwrap(); @@ -15,7 +15,7 @@ fn core_ms_segfault() { } #[test] -fn simp_small_sat() { +fn small_sat() { let mut solver = BatsatBasicSolver::default(); let inst: SatInstance = SatInstance::from_dimacs_path("./data/AProVE11-12.cnf").unwrap(); @@ -27,7 +27,7 @@ fn simp_small_sat() { // Note: this instance seems too hard for batsat to solve #[test] #[ignore] -fn simp_small_unsat() { +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") From 464914895972d85863d582ff3fde8194142a9661 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:08:40 +0200 Subject: [PATCH 14/25] 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); } From 727e42c06b56159f9daad899a0c3cb914852514a Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Fri, 21 Jun 2024 19:19:21 +0200 Subject: [PATCH 15/25] fix: use workspace dependencies --- batsat/Cargo.toml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml index 94ad690a..aa0a33a0 100644 --- a/batsat/Cargo.toml +++ b/batsat/Cargo.toml @@ -15,10 +15,10 @@ readme = "README.md" debug = [] [dependencies] -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" } +batsat = "0.5.0" # when changing this version, do not forget to update signature +anyhow.workspace = true +thiserror.workspace = true +rustsat.workspace = true [dev-dependencies] rustsat-solvertests = { path = "../solvertests" } From 15449807c3923b9dd02ae09a958d7378011b142b Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 26 Jun 2024 11:17:22 +0200 Subject: [PATCH 16/25] fix: clippy linting issues addressed --- batsat/src/lib.rs | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 806d76c0..2e9d74de 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -15,14 +15,9 @@ pub struct InvalidApiReturn { error: &'static str, } +#[derive(Default)] pub struct BatsatBasicSolver(BasicSolver); -impl Default for BatsatBasicSolver { - fn default() -> BatsatBasicSolver { - BatsatBasicSolver(BasicSolver::default()) - } -} - impl Extend for BatsatBasicSolver { fn extend>(&mut self, iter: T) { iter.into_iter() @@ -49,7 +44,7 @@ impl Solve for BatsatBasicSolver { x if x == lbool::TRUE => Ok(SolverResult::Sat), x if x == lbool::FALSE => Ok(SolverResult::Unsat), x if x == lbool::UNDEF => Err(InvalidApiReturn { - error: "BatSat Solver is in an UNSAT state".into(), + error: "BatSat Solver is in an UNSAT state", } .into()), _ => unreachable!(), @@ -94,19 +89,14 @@ impl SolveIncremental for BatsatBasicSolver { fn solve_assumps(&mut self, assumps: &[Lit]) -> anyhow::Result { let a = assumps .iter() - .map(|l| { - batsat::Lit::new( - self.0.var_of_int((l.vidx32() + 1).try_into().unwrap()), - l.is_pos(), - ) - }) + .map(|l| batsat::Lit::new(self.0.var_of_int(l.vidx32() + 1), l.is_pos())) .collect::>(); match self.0.solve_limited(&a) { x if x == lbool::TRUE => Ok(SolverResult::Sat), x if x == lbool::FALSE => Ok(SolverResult::Unsat), x if x == lbool::UNDEF => Err(InvalidApiReturn { - error: "BatSat Solver is in an UNSAT state".into(), + error: "BatSat Solver is in an UNSAT state", } .into()), _ => unreachable!(), From fcfa9dffed93f914dfa92181fe672c0c5a1e479f Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Mon, 1 Jul 2024 17:32:42 +0200 Subject: [PATCH 17/25] PR: implemented suggestions and applied reviews --- .github/workflows/batsat.yml | 8 ++------ .github/workflows/docs.yml | 2 +- .github/workflows/semver-checks.yml | 4 ++++ Cargo.toml | 1 - batsat/CHANGELOG.md | 6 ++---- batsat/Cargo.toml | 3 --- batsat/src/lib.rs | 11 +++++++++-- release-plz.toml | 5 +++++ 8 files changed, 23 insertions(+), 17 deletions(-) diff --git a/.github/workflows/batsat.yml b/.github/workflows/batsat.yml index 8eb0e5dd..cd5ef4df 100644 --- a/.github/workflows/batsat.yml +++ b/.github/workflows/batsat.yml @@ -2,9 +2,9 @@ name: BatSat on: push: - branches: [ "main" ] + branches: [ "main", "next-major" ] pull_request: - branches: [ "main" ] + branches: [ "main", "next-major" ] env: CARGO_TERM_COLOR: always @@ -26,9 +26,5 @@ jobs: shared-key: "build-test" - name: Cargo build run: cargo build -p rustsat-batsat --verbose - env: - CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} - name: Cargo test run: cargo test -p rustsat-batsat --verbose - env: - CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }} diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 82831b8e..9a954b6c 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -32,7 +32,7 @@ jobs: echo "failed for main crate" return=false fi - for dir in tools cadical kissat minisat glucose ipasir capi pyapi; do + for dir in tools cadical kissat minisat glucose batsat ipasir capi pyapi; do cd ${dir} if ! cargo rdme --check; then echo "failed for ${dir}" diff --git a/.github/workflows/semver-checks.yml b/.github/workflows/semver-checks.yml index d756f6eb..3b073590 100644 --- a/.github/workflows/semver-checks.yml +++ b/.github/workflows/semver-checks.yml @@ -43,3 +43,7 @@ jobs: uses: obi1kenobi/cargo-semver-checks-action@v2 with: package: rustsat-ipasir + - name: BatSat + uses: obi1kenobi/cargo-semver-checks-action@v2 + with: + package: rustsat-batsat \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 1c97d27d..386f0b2d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,7 +6,6 @@ members = [ "glucose", "minisat", "ipasir", - "batsat", "solvertests", "capi", "pyapi", diff --git a/batsat/CHANGELOG.md b/batsat/CHANGELOG.md index ef16d198..c582dab2 100644 --- a/batsat/CHANGELOG.md +++ b/batsat/CHANGELOG.md @@ -2,10 +2,8 @@ All notable changes to this project will be documented in this file. -## [0.2.4] - 2024-04-10 +## [0.1.0] - -### 🚀 Features - -- Implemented batsat api +Initial Release diff --git a/batsat/Cargo.toml b/batsat/Cargo.toml index aa0a33a0..d23d95bb 100644 --- a/batsat/Cargo.toml +++ b/batsat/Cargo.toml @@ -11,9 +11,6 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html -[features] -debug = [] - [dependencies] batsat = "0.5.0" # when changing this version, do not forget to update signature anyhow.workspace = true diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 2e9d74de..462acfc4 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,6 +1,13 @@ -//! # BatSat Solver Interface +//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT //! -//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver +//! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. +//! +//! # BatSat Version +//! +//! The version of BatSat in this crate is Version 0.5.0. + +#![warn(clippy::pedantic)] +#![warn(missing_docs)] use batsat::{intmap::AsIndex, lbool, BasicSolver, SolverInterface}; use rustsat::{ diff --git a/release-plz.toml b/release-plz.toml index fe2e31a4..28ca80fb 100644 --- a/release-plz.toml +++ b/release-plz.toml @@ -40,3 +40,8 @@ git_release_enable = false name = "rustsat-pyapi" release = false git_release_enable = false + +[[package]] +name = "rustsat-batsat" +release = false +git_release_enable = false From a1e44980b557544e72c2a7b205a61855811997ff Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Mon, 1 Jul 2024 17:48:15 +0200 Subject: [PATCH 18/25] lint: clippy fixes and docu --- batsat/src/lib.rs | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 462acfc4..3c80b396 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,10 +1,10 @@ -//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT +//! # rustsat-batsat - Interface to the `BatSat` SAT Solver for `RustSAT` //! //! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. //! -//! # BatSat Version +//! # `BatSat` Version //! -//! The version of BatSat in this crate is Version 0.5.0. +//! The version of `BatSat` in this crate is Version 0.5.0. #![warn(clippy::pedantic)] #![warn(missing_docs)] @@ -16,19 +16,21 @@ use rustsat::{ }; use thiserror::Error; +/// API Error from the `BatSat` library (for example if the solver is in an UNSAT state) #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] #[error("BatSat returned an invalid value: {error}")] pub struct InvalidApiReturn { error: &'static str, } +/// RustSAT Interface to the `BatSat` Solver which is fully implemented in Rust [BatSat](https://github.com/c-cube/batsat) #[derive(Default)] pub struct BatsatBasicSolver(BasicSolver); impl Extend for BatsatBasicSolver { fn extend>(&mut self, iter: T) { iter.into_iter() - .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend")) + .for_each(|cl| self.add_clause(cl).expect("Error adding clause in extend")); } } @@ -36,8 +38,8 @@ 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") - }) + .expect("Error adding clause in extend"); + }); } } From a549dda76b99558347aaca5dde0dde2beb741aa2 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Mon, 1 Jul 2024 17:51:42 +0200 Subject: [PATCH 19/25] docu: cargo rdme run --- batsat/README.md | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/batsat/README.md b/batsat/README.md index 846af6d9..1bb4e6b7 100644 --- a/batsat/README.md +++ b/batsat/README.md @@ -5,14 +5,12 @@ -# rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT +# rustsat-batsat - Interface to the `BatSat` SAT Solver for `RustSAT` -The BatSat solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. +Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. -## Features +# `BatSat` Version -## BatSat Version - -The version of BatSat in this crate is Version 0.5.0. +The version of `BatSat` in this crate is Version 0.5.0. From 0aeac456fc5371417008d102953a88f109f00bcb Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Mon, 1 Jul 2024 18:09:57 +0200 Subject: [PATCH 20/25] docu: more comments and restructuring --- batsat/src/lib.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index 3c80b396..b5c4c8af 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -2,6 +2,8 @@ //! //! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. //! +//! `BatSat` is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. +//! //! # `BatSat` Version //! //! The version of `BatSat` in this crate is Version 0.5.0. @@ -23,7 +25,7 @@ pub struct InvalidApiReturn { error: &'static str, } -/// RustSAT Interface to the `BatSat` Solver which is fully implemented in Rust [BatSat](https://github.com/c-cube/batsat) +/// RustSAT wrapper for the `BasicSolver` Solver from `BatSat` #[derive(Default)] pub struct BatsatBasicSolver(BasicSolver); From e0a9cd2c04b7248800f4cba8f610826576df6b2b Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Wed, 3 Jul 2024 11:03:56 +0200 Subject: [PATCH 21/25] ci: run cargo rdme after comments changed --- batsat/README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/batsat/README.md b/batsat/README.md index 1bb4e6b7..b358c048 100644 --- a/batsat/README.md +++ b/batsat/README.md @@ -9,6 +9,8 @@ Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. +`BatSat` is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. + # `BatSat` Version The version of `BatSat` in this crate is Version 0.5.0. From 3a3bd46ebf5fcc9bfec98d6409ad87629606e0c4 Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Thu, 4 Jul 2024 09:41:02 +0200 Subject: [PATCH 22/25] docu: remove code blocks for names Co-authored-by: Christoph Jabs <98587286+chrjabs@users.noreply.github.com> --- batsat/src/lib.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/batsat/src/lib.rs b/batsat/src/lib.rs index b5c4c8af..5937ffd9 100644 --- a/batsat/src/lib.rs +++ b/batsat/src/lib.rs @@ -1,12 +1,12 @@ -//! # rustsat-batsat - Interface to the `BatSat` SAT Solver for `RustSAT` +//! # rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT //! //! Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. //! -//! `BatSat` is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. +//! BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. //! -//! # `BatSat` Version +//! # BatSat Version //! -//! The version of `BatSat` in this crate is Version 0.5.0. +//! The version of BatSat in this crate is Version 0.5.0. #![warn(clippy::pedantic)] #![warn(missing_docs)] @@ -18,14 +18,14 @@ use rustsat::{ }; use thiserror::Error; -/// API Error from the `BatSat` library (for example if the solver is in an UNSAT state) +/// API Error from the BatSat library (for example if the solver is in an UNSAT state) #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] #[error("BatSat returned an invalid value: {error}")] pub struct InvalidApiReturn { error: &'static str, } -/// RustSAT wrapper for the `BasicSolver` Solver from `BatSat` +/// RustSAT wrapper for the [`BasicSolver`] Solver from BatSat #[derive(Default)] pub struct BatsatBasicSolver(BasicSolver); From 80db5aab3e76beefdc2076393228735ca0c0c2ab Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Thu, 4 Jul 2024 09:42:01 +0200 Subject: [PATCH 23/25] ci: run cargo rdme --- batsat/README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/batsat/README.md b/batsat/README.md index b358c048..218809a9 100644 --- a/batsat/README.md +++ b/batsat/README.md @@ -5,14 +5,14 @@ -# rustsat-batsat - Interface to the `BatSat` SAT Solver for `RustSAT` +# rustsat-batsat - Interface to the BatSat SAT Solver for RustSAT Interface to the [BatSat](https://github.com/c-cube/batsat) incremental SAT-Solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library. -`BatSat` is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. +BatSat is fully implemented in Rust which has advantages in restricted compilation scenarios like WebAssembly. -# `BatSat` Version +# BatSat Version -The version of `BatSat` in this crate is Version 0.5.0. +The version of BatSat in this crate is Version 0.5.0. From adbe43efc18187df93c036003836f0f39e834d80 Mon Sep 17 00:00:00 2001 From: Noah Bruns Date: Thu, 4 Jul 2024 12:03:33 +0200 Subject: [PATCH 24/25] lint: Batsat added as valid ident --- clippy.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clippy.toml b/clippy.toml index eff43ef7..98e9d828 100644 --- a/clippy.toml +++ b/clippy.toml @@ -1,2 +1,2 @@ -doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", ".."] +doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", "..", "BatSat"] avoid-breaking-exported-api = false From 25bea4d13862e0d02e39861b467f1830529b58a1 Mon Sep 17 00:00:00 2001 From: Noah Bruns <51422579+nfbruns@users.noreply.github.com> Date: Thu, 4 Jul 2024 16:01:43 +0200 Subject: [PATCH 25/25] refactor: reorder clippy valid idents list Co-authored-by: Christoph Jabs <98587286+chrjabs@users.noreply.github.com> --- clippy.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clippy.toml b/clippy.toml index 98e9d828..a9773d0a 100644 --- a/clippy.toml +++ b/clippy.toml @@ -1,2 +1,2 @@ -doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", "..", "BatSat"] +doc-valid-idents = ["RustSAT", "CaDiCaL", "MaxSAT", "BatSat", ".."] avoid-breaking-exported-api = false