diff --git a/.github/workflows/kissat.yml b/.github/workflows/kissat.yml index 4d52e60b..bbd201a6 100644 --- a/.github/workflows/kissat.yml +++ b/.github/workflows/kissat.yml @@ -19,6 +19,8 @@ jobs: steps: - name: Checkout sources uses: actions/checkout@v4 + with: + submodules: "recursive" - name: Install stable toolchain uses: dtolnay/rust-toolchain@stable - uses: Swatinem/rust-cache@v2 diff --git a/.gitmodules b/.gitmodules index 7ce0f13d..17774e45 100644 --- a/.gitmodules +++ b/.gitmodules @@ -4,3 +4,6 @@ [submodule "glucose/cppsrc"] path = glucose/cppsrc url = git@github.com:chrjabs/glucose4.git +[submodule "kissat/csrc"] + path = kissat/csrc + url = git@github.com:arminbiere/kissat.git diff --git a/kissat/README.md b/kissat/README.md index beedd70c..6bcf8484 100644 --- a/kissat/README.md +++ b/kissat/README.md @@ -32,4 +32,10 @@ The following Kissat versions are available: Without any features selected, the newest version will be used. If conflicting Kissat versions are requested, the newest requested version will be selected. +## Customization + +In order to build a custom version of Kissat, this crate supports the `KISSAT_SRC_DIR` +environment variable. +If this is set, Kissat will be built from the path specified there. + diff --git a/kissat/build.rs b/kissat/build.rs index 6388f768..1c278ab5 100644 --- a/kissat/build.rs +++ b/kissat/build.rs @@ -10,41 +10,81 @@ use std::{ str, }; -fn main() { - let out_dir = env::var("OUT_DIR").unwrap(); +#[derive(Default, Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +enum Version { + // Note: derived order makes top < bottom + Sc2022Bulky, + Sc2022Hyper, + Sc2022Light, + V300, + V310, + V311, + V400, + #[default] + V401, +} + +/// Checks if the version was set manually via a feature +macro_rules! version_set_manually { + () => { + cfg!(any( + feature = "v4-0-1", + feature = "v4-0-0", + feature = "v3-1-1", + feature = "v3-1-0", + feature = "v3-0-0", + feature = "sc2022-light", + feature = "sc2022-hyper", + feature = "sc2022-bulky", + )) + }; +} - if std::env::var("DOCS_RS").is_ok() { - // don't build c library on docs.rs due to network restrictions - // instead, only generate bindings from included header file - generate_bindings("csrc/dummy-kissat.h", "csrc/dummy-error.h", &out_dir); - return; +impl Version { + fn determine() -> Self { + if cfg!(feature = "v4-0-1") { + Version::V401 + } else if cfg!(feature = "v4-0-0") { + Version::V400 + } else if cfg!(feature = "v3-1-1") { + Version::V311 + } else if cfg!(feature = "v3-1-0") { + Version::V310 + } else if cfg!(feature = "v3-0-0") { + Version::V300 + } else if cfg!(feature = "sc2022-light") { + Version::Sc2022Light + } else if cfg!(feature = "sc2022-hyper") { + Version::Sc2022Hyper + } else if cfg!(feature = "sc2022-bulky") { + Version::Sc2022Bulky + } else { + // default to newest version + Version::default() + } } - // Select commit based on features. If conflict, always choose newest release - let tag = if cfg!(feature = "v4-0-1") { - "refs/tags/rel-4.0.1" - } else if cfg!(feature = "v4-0-0") { - "refs/tags/rel-4.0.0" - } else if cfg!(feature = "v3-1-1") { - "refs/tags/rel-3.1.1" - } else if cfg!(feature = "v3-1-0") { - "refs/tags/rel-3.1.0" - } else if cfg!(feature = "v3-0-0") { - "refs/tags/rel-3.0.0" - } else if cfg!(feature = "sc2022-light") { - "refs/tags/sc2022-light" - } else if cfg!(feature = "sc2022-hyper") { - "refs/tags/sc2022-hyper" - } else if cfg!(feature = "sc2022-bulky") { - "refs/tags/sc2022-bulky" - } else { - // default to newest version - "refs/tags/rel-4.0.1" - }; + fn reference(self) -> &'static str { + match self { + Version::Sc2022Bulky => "refs/tags/sc2022-bulky", + Version::Sc2022Hyper => "refs/tags/sc2022-hyper", + Version::Sc2022Light => "refs/tags/sc2022-light", + Version::V300 => "refs/tags/rel-3.0.0", + Version::V310 => "refs/tags/rel-3.1.0", + Version::V311 => "refs/tags/rel-3.1.1", + Version::V400 => "refs/tags/rel-4.0.0", + Version::V401 => "refs/tags/rel-4.0.1", + } + } +} + +fn main() { + let out_dir = env::var("OUT_DIR").unwrap(); + + let version = Version::determine(); // Build C library - // Full commit hash needs to be provided - build("https://github.com/arminbiere/kissat.git", "master", tag); + let kissat_src_dir = build(version); // Built solver is in out_dir println!("cargo:rustc-link-search={out_dir}"); @@ -52,18 +92,44 @@ fn main() { println!("cargo:rustc-link-lib=static=kissat"); // Generate Rust FFI bindings - generate_bindings( - &format!("{out_dir}/kissat/src/kissat.h"), - &format!("{out_dir}/kissat/src/error.h"), - &out_dir, + generate_bindings(&kissat_src_dir, &out_dir); +} + +fn get_kissat_src(version: Version) -> PathBuf { + if let Ok(src_dir) = std::env::var("KISSAT_SRC_DIR") { + if version_set_manually!() { + println!("cargo:warning=Both version feature and KISSAT_SRC_DIR. Will ignore version feature"); + } + return PathBuf::from(src_dir); + } + + if version == Version::default() { + // the sources for the default version are included with the crate and do not need to be + // cloned + return PathBuf::from("csrc"); + } + let mut kissat_src_dir = PathBuf::from(env::var("OUT_DIR").unwrap()); + kissat_src_dir.push("kissat"); + update_repo( + &kissat_src_dir, + "https://github.com/arminbiere/kissat.git", + "master", + version.reference(), ); + kissat_src_dir } /// Generates Rust FFI bindings -fn generate_bindings(main_header_path: &str, error_header_path: &str, out_dir: &str) { +fn generate_bindings(kissat_src_dir: &Path, out_dir: &str) { let bindings = bindgen::Builder::default() - .header(main_header_path) - .header(error_header_path) + .header( + kissat_src_dir + .join("src") + .join("kissat.h") + .to_str() + .unwrap(), + ) + .header(kissat_src_dir.join("src").join("error.h").to_str().unwrap()) .blocklist_function("kissat_copyright") .blocklist_function("kissat_build") .blocklist_function("kissat_banner") @@ -79,74 +145,71 @@ fn generate_bindings(main_header_path: &str, error_header_path: &str, out_dir: & .expect("Could not write ffi bindings"); } -fn build(repo: &str, branch: &str, reference: &str) { - let out_dir = env::var("OUT_DIR").unwrap(); - let mut kissat_dir_str = out_dir.clone(); - kissat_dir_str.push_str("/kissat"); - let kissat_dir = Path::new(&kissat_dir_str); - if update_repo(kissat_dir, repo, branch, reference) - || !Path::new(&out_dir).join("libkissat.a").exists() - { - // Repo changed, rebuild - // We specify the build manually here instead of calling make for better portability - let src_files = glob(&format!("{kissat_dir_str}/src/*.c")) - .unwrap() - .filter_map(|res| { - if let Ok(p) = res { - if let Some(name) = p.file_name() { - if name == "main.c" - || name == "application.c" - || name == "handle.c" - || name == "parse.c" - || name == "witness.c" - { - return None; // Filter out application files - } - }; - Some(p) - } else { - None - } - }); - // Setup build configuration - let mut kissat_build = cc::Build::new(); - if cfg!(feature = "debug") && env::var("PROFILE").unwrap() == "debug" { - kissat_build - .opt_level(0) - .define("DEBUG", None) - .warnings(true) - .debug(true); - } else { - kissat_build - .opt_level(3) - .define("NDEBUG", None) - .warnings(false); - } - #[cfg(feature = "safe")] - kissat_build.define("SAFE", None); // --safe - #[cfg(feature = "quiet")] - kissat_build.define("QUIET", None); // --quiet - - // Generate build header - let mut build_header = File::create(kissat_dir.join("src").join("build.h")) - .expect("Could not create kissat build header"); - let mut kissat_version = - fs::read_to_string(kissat_dir.join("VERSION")).expect("Cannot read kissat version"); - kissat_version.retain(|c| c != '\n'); - let (compiler_desc, compiler_flags) = - get_compiler_description(&kissat_build.get_compiler()); - write!( +fn build(version: Version) -> PathBuf { + let kissat_src_dir = get_kissat_src(version); + let kissat_dir_str = kissat_src_dir.to_str().unwrap(); + + // We specify the build manually here instead of calling make for better portability + let src_files = glob(&format!("{kissat_dir_str}/src/*.c")) + .unwrap() + .filter_map(|res| { + if let Ok(p) = res { + if let Some(name) = p.file_name() { + if name == "main.c" + || name == "application.c" + || name == "handle.c" + || name == "parse.c" + || name == "witness.c" + { + return None; // Filter out application files + } + }; + Some(p) + } else { + None + } + }); + // Setup build configuration + let mut kissat_build = cc::Build::new(); + if cfg!(feature = "debug") && env::var("PROFILE").unwrap() == "debug" { + kissat_build + .opt_level(0) + .define("DEBUG", None) + .warnings(true) + .debug(true); + } else { + kissat_build + .opt_level(3) + .define("NDEBUG", None) + .warnings(false); + } + #[cfg(feature = "safe")] + kissat_build.define("SAFE", None); // --safe + #[cfg(feature = "quiet")] + kissat_build.define("QUIET", None); // --quiet + + // Generate build header + let out_dir = PathBuf::from(env::var("OUT_DIR").unwrap()); + let mut build_header = + File::create(out_dir.join("build.h")).expect("Could not create kissat build header"); + let mut kissat_version = + fs::read_to_string(kissat_src_dir.join("VERSION")).expect("Cannot read kissat version"); + kissat_version.retain(|c| c != '\n'); + let (compiler_desc, compiler_flags) = get_compiler_description(&kissat_build.get_compiler()); + write!( build_header, "#define VERSION \"{}\"\n#define COMPILER \"{} {}\"\n#define ID \"{}\"\n#define BUILD \"{}\"\n#define DIR \"{}\"", - kissat_version, compiler_desc, compiler_flags, reference, chrono::Utc::now(), kissat_dir.as_os_str().to_str().unwrap() + kissat_version, compiler_desc, compiler_flags, version.reference(), chrono::Utc::now(), kissat_dir_str ).expect("Failed to write kissat build.h"); - // Build Kissat - kissat_build - .include(kissat_dir.join("src")) - .warnings(false) - .files(src_files) - .compile("kissat"); - }; + // Build Kissat + kissat_build + .include(kissat_src_dir.join("src")) + .include(out_dir) + .warnings(false) + .files(src_files) + .compile("kissat"); + + kissat_src_dir } /// Returns true if there were changes, false if not diff --git a/kissat/csrc b/kissat/csrc new file mode 160000 index 00000000..43f02cf3 --- /dev/null +++ b/kissat/csrc @@ -0,0 +1 @@ +Subproject commit 43f02cf3e992cb44653b35e5cb26f93281552ae0 diff --git a/kissat/csrc/dummy-error.h b/kissat/csrc/dummy-error.h deleted file mode 100644 index a6f58a3e..00000000 --- a/kissat/csrc/dummy-error.h +++ /dev/null @@ -1,20 +0,0 @@ -// This is a copy of the `error.h` file of Kissat, included to enable -// building the crate without network access, mainly on docs.rs -#ifndef _error_h_INCLUDED -#define _error_h_INCLUDED - -#include "attribute.h" - -// clang-format off - -void kissat_error (const char *fmt, ...) ATTRIBUTE_FORMAT (1, 2); -void kissat_fatal (const char *fmt, ...) ATTRIBUTE_FORMAT (1, 2); - -void kissat_fatal_message_start (void); - -void kissat_call_function_instead_of_abort (void (*)(void)); -void kissat_abort (void); - -// clang-format on - -#endif diff --git a/kissat/csrc/dummy-kissat.h b/kissat/csrc/dummy-kissat.h deleted file mode 100644 index 3d979cf1..00000000 --- a/kissat/csrc/dummy-kissat.h +++ /dev/null @@ -1,44 +0,0 @@ -// This is a copy of the `kissat.h` file of Kissat, included to enable -// building the crate without network access, mainly on docs.rs -#ifndef _kissat_h_INCLUDED -#define _kissat_h_INCLUDED - -typedef struct kissat kissat; - -// Default (partial) IPASIR interface. - -const char *kissat_signature(void); -kissat *kissat_init(void); -void kissat_add(kissat *solver, int lit); -int kissat_solve(kissat *solver); -int kissat_value(kissat *solver, int lit); -void kissat_release(kissat *solver); - -void kissat_set_terminate(kissat *solver, void *state, - int (*terminate)(void *state)); - -// Additional API functions. - -void kissat_terminate(kissat *solver); -void kissat_reserve(kissat *solver, int max_var); - -const char *kissat_id(void); -const char *kissat_version(void); -const char *kissat_compiler(void); - -const char **kissat_copyright(void); -void kissat_build(const char *line_prefix); -void kissat_banner(const char *line_prefix, const char *name_of_app); - -int kissat_get_option(kissat *solver, const char *name); -int kissat_set_option(kissat *solver, const char *name, int new_value); - -int kissat_has_configuration(const char *name); -int kissat_set_configuration(kissat *solver, const char *name); - -void kissat_set_conflict_limit(kissat *solver, unsigned); -void kissat_set_decision_limit(kissat *solver, unsigned); - -void kissat_print_statistics(kissat *solver); - -#endif diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs index 3f748f24..0f6aa36b 100644 --- a/kissat/src/lib.rs +++ b/kissat/src/lib.rs @@ -24,6 +24,12 @@ //! //! Without any features selected, the newest version will be used. //! If conflicting Kissat versions are requested, the newest requested version will be selected. +//! +//! ## Customization +//! +//! In order to build a custom version of Kissat, this crate supports the `KISSAT_SRC_DIR` +//! environment variable. +//! If this is set, Kissat will be built from the path specified there. #![warn(clippy::pedantic)] #![warn(missing_docs)]