Include kissat source code

.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

.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

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.
+
 <!-- cargo-rdme end -->

kissat/build.rs

@@ -10,60 +10,126 @@ 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}");
     println!("cargo:rustc-link-search={out_dir}/lib");
     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