CryptoMiniSat interface

.config/names.dic

@@ -1,4 +1,4 @@
-58
+59
 Argelich
 Armin
 Audemard
@@ -12,6 +12,7 @@ Boufkhad
 bzip2
 CaDiCaL
 CaDiCaL's
+CryptoMiniSat
 Eén
 Fazekas
 Fleury

Cargo.toml

@@ -10,6 +10,7 @@ members = [
   "capi",
   "pyapi",
   "batsat",
+  "cryptominisat",
 ]
 resolver = "2"
 

clippy.toml

@@ -1,6 +1,7 @@
 doc-valid-idents = [
   "RustSAT",
   "CaDiCaL",
+  "CryptoMiniSat",
   "MaxSAT",
   "BatSat",
   "AllDifferent",

cryptominisat/CHANGELOG.md

@@ -0,0 +1,133 @@
+# Changelog
+
+All notable changes to this project will be documented in this file.
+
+## [0.4.4] - 2025-02-18
+
+### Miscellaneous Tasks
+
+- Update Cargo.toml dependencies
+
+<!-- generated by git-cliff -->
+## [0.4.3] - 2024-12-20
+
+### Miscellaneous Tasks
+
+- Exclude unnecessary files from release
+
+<!-- generated by git-cliff -->
+## [0.4.2] - 2024-12-13
+
+### Documentation
+
+- Spellchecking
+
+<!-- generated by git-cliff -->
+## [0.4.1] - 2024-10-16
+
+### Documentation
+
+- Fix docsrs build
+
+<!-- generated by git-cliff -->
+## [0.4.0] - 2024-10-16
+
+### Features
+
+- `Propagate` trait
+
+### Miscellaneous Tasks
+
+- Pedantic clippy
+
+### Refactor
+
+- [**breaking**] Make reading functions take reader by reference
+- Use bindgen to generate solver bindings
+
+<!-- generated by git-cliff -->
+## [0.3.1] - 2024-06-12
+
+### Miscellaneous Tasks
+
+- Updated the following local packages: rustsat
+
+<!-- generated by git-cliff -->
+## [0.3.0] - 2024-04-30
+
+The corresponding RustSAT release contains breaking changes. For detailed
+instructions on how to handle migration, please refer to the [migration
+guide](https://github.com/chrjabs/rustsat/blob/main/docs/0-5-0-migration-guide.md).
+
+### Bug Fixes
+
+- Variable freezing and return value for `var_eliminated`
+- Segfault in minisat
+
+### Documentation
+
+- Add missing documentation
+
+### Features
+
+- `quiet` feature to disable stdout printing
+- Migrate error handling to `anyhow` create
+- `FreezeVar` trait
+- Return error when assumption is eliminated
+- Add `add_clause_ref` method to `Solve` trait
+- `Extend<&Clause>` for solvers
+- Catch memory out in solvers
+- Catch memory outs in clause collector
+
+### Refactor
+
+- Clean up control flow in solver methods
+- Factor out solver integration tests
+- Factor out solver unit tests
+- Solver build system
+
+### Testing
+
+- Minisat segfault tests
+
+### Example
+
+- `minisat-cli` tool
+
+<!-- generated by git-cliff -->
+## [0.2.4] - 2024-02-22
+
+### Bug Fixes
+
+- Remove zlib dependency from minisat and glucose
+
+<!-- generated by git-cliff -->
+<!-- generated by git-cliff -->
+## [0.2.3] - 2024-01-11
+
+### Documentation
+
+- Fix [docs.rs](https://docs.rs/rustsat-minisat) build
+
+## [0.2.2] - 2024-01-11
+
+### Bug Fixes
+
+- Build on non-linux
+
+### Documentation
+
+- Add shields to READMEs
+
+### Features
+
+- Debug feature
+
+<!-- generated by git-cliff -->
+## [0.2.1] - 2023-12-18
+
+### Miscellaneous Tasks
+
+- Updated the following local packages: rustsat
+
+<!-- generated by git-cliff -->

cryptominisat/Cargo.toml

@@ -0,0 +1,45 @@
+[package]
+name = "rustsat-cryptominisat"
+version = "0.1.0"
+edition.workspace = true
+authors = ["Christoph Jabs <[email protected]>"]
+license.workspace = true
+description = "Interface to the SAT solver CryptoMiniSat for the RustSAT library."
+keywords = ["sat-solver", "rustsat"]
+repository = "https://github.com/chrjabs/rustsat"
+readme = "README.md"
+include = [
+  "build.rs",
+  "CHANGELOG.md",
+  "README.md",
+  "/src/",
+  "/examples/",
+  "/cppsrc/src/",
+  "/cppsrc/README.markdown",
+  "/cppsrc/LICENSE.txt",
+  "/cppsrc/AUTHORS",
+  "/cppsrc/CMakeLists.txt",
+  "/cppsrc/cryptominisat5Config.cmake.in",
+]
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[features]
+debug = []
+
+[dependencies]
+anyhow.workspace = true
+cpu-time.workspace = true
+thiserror.workspace = true
+rustsat.workspace = true
+
+[build-dependencies]
+bindgen.workspace = true
+cmake.workspace = true
+
+[dev-dependencies]
+clap.workspace = true
+signal-hook.workspace = true
+rustsat-solvertests.workspace = true

cryptominisat/README.md

@@ -0,0 +1,22 @@
+[![Check & Test](https://github.com/chrjabs/rustsat/actions/workflows/minisat.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/minisat.yml)
+[![crates.io](https://img.shields.io/crates/v/rustsat-minisat)](https://crates.io/crates/rustsat-minisat)
+[![docs.rs](https://img.shields.io/docsrs/rustsat-minisat)](https://docs.rs/rustsat-minisat)
+[![License](https://img.shields.io/crates/l/rustsat-minisat)](../LICENSE)
+
+<!-- cargo-rdme start -->
+
+# rustsat-minisat - Interface to the Minisat SAT Solver for RustSAT
+
+The Minisat SAT solver to be used with the [RustSAT](https://github.com/chrjabs/rustsat) library.
+
+## Features
+
+- `debug`: if this feature is enables, the Cpp library will be built with debug and check functionality if the Rust project is built in debug mode
+- `quiet`: disable all glucose-internal printing to `stdout` during solving (on by default)
+
+## Minisat Version
+
+The version of Minisat in this crate is Version 2.2.0.
+The used Cpp source repository can be found [here](https://github.com/chrjabs/minisat).
+
+<!-- cargo-rdme end -->

cryptominisat/build.rs

@@ -0,0 +1,64 @@
+#![warn(clippy::pedantic)]
+
+use std::{
+    env,
+    path::{Path, PathBuf},
+};
+
+fn main() {
+    // Build C++ library
+    build();
+
+    let out_dir = env::var("OUT_DIR").unwrap();
+
+    println!("cargo:rerun-if-changed=cppsrc/");
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={out_dir}/build/lib");
+    println!("cargo:rustc-link-lib=static=cryptominisat5");
+
+    // Link c++ std lib
+    // Note: this should be _after_ linking the solver itself so that it is actually pulled in
+    #[cfg(target_os = "macos")]
+    println!("cargo:rustc-link-lib=dylib=c++");
+    #[cfg(not(any(target_os = "macos", target_os = "windows")))]
+    println!("cargo:rustc-link-lib=dylib=stdc++");
+
+    // Generate Rust FFI bindings
+    let bindings = bindgen::Builder::default()
+        .rust_target("1.66.1".parse().unwrap()) // Set MSRV of RustSAT
+        .header("cppsrc/src/cryptominisat_c.h")
+        .allowlist_file("cppsrc/src/cryptominisat_c.h")
+        .blocklist_function("cmsat_print_stats")
+        .blocklist_function("cmsat_set_up_for_scalmc")
+        .blocklist_function("set_up_for_arjun")
+        .blocklist_function("cmsat_set_yes_comphandler")
+        .blocklist_function("cmsat_simplify")
+        .blocklist_function("cmsat_set_polarity_auto")
+        .parse_callbacks(Box::new(bindgen::CargoCallbacks::new()))
+        .generate()
+        .expect("Unable to generate ffi bindings");
+    bindings
+        .write_to_file(PathBuf::from(out_dir).join("bindings.rs"))
+        .expect("Could not write ffi bindings");
+}
+
+fn build() {
+    let crate_dir = env::var("CARGO_MANIFEST_DIR").unwrap();
+    let mut cms_dir_str = crate_dir.clone();
+    cms_dir_str.push_str("/cppsrc");
+    let cms_dir = Path::new(&cms_dir_str);
+    let mut conf = cmake::Config::new(cms_dir);
+    conf.build_target("cryptominisat5")
+        .define("STATICCOMPILE", "ON")
+        .define("ENABLE_PYTHON_INTERFACE", "OFF")
+        .define("ONLY_SIMPLE", "ON")
+        .define("NOZLIB", "ON")
+        .define("NOM4RI", "ON")
+        .define("STATS", "OFF")
+        .define("NOVALGRIND", "ON")
+        .define("ENABLE_TESTING", "OFF");
+    #[cfg(not(feature = "debug"))]
+    conf.profile("Release");
+    conf.build();
+}