refactor: solver build system

- include minisat and glucose as submodules
- specify linked libraries in code rather than in the build script

.github/workflows/docs.yml

@@ -16,6 +16,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

.github/workflows/glucose.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

.github/workflows/minisat.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

.github/workflows/rustsat.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

.github/workflows/tools.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

@@ -0,0 +1,6 @@
+[submodule "minisat/cppsrc"]
+	path = minisat/cppsrc
+	url = git@github.com:chrjabs/minisat.git
+[submodule "glucose/cppsrc"]
+	path = glucose/cppsrc
+	url = git@github.com:chrjabs/glucose4.git

cadical/build.rs

@@ -76,6 +76,12 @@ fn main() {
 
     let out_dir = env::var("OUT_DIR").unwrap();
 
+    #[cfg(target_os = "macos")]
+    println!("cargo:rustc-flags=-l dylib=c++");
+
+    #[cfg(not(target_os = "macos"))]
+    println!("cargo:rustc-flags=-l dylib=stdc++");
+
     // Built solver is in out_dir
     println!("cargo:rustc-link-search={}", out_dir);
     println!("cargo:rustc-link-search={}/lib", out_dir);
@@ -149,14 +155,6 @@ fn build(repo: &str, branch: &str, reference: &str, patch: &str) {
             .files(src_files)
             .compile("cadical");
     };
-
-    println!("cargo:rustc-link-lib=static=cadical");
-
-    #[cfg(target_os = "macos")]
-    println!("cargo:rustc-flags=-l dylib=c++");
-
-    #[cfg(not(target_os = "macos"))]
-    println!("cargo:rustc-flags=-l dylib=stdc++");
 }
 
 /// Returns true if there were changes, false if not

cadical/src/lib.rs

@@ -873,6 +873,7 @@ mod ffi {
         _private: [u8; 0],
     }
 
+    #[link(name = "cadical", kind = "static")]
     extern "C" {
         // Redefinitions of CaDiCaL C API
         pub fn ccadical_signature() -> *const c_char;
@@ -941,6 +942,7 @@ mod ffi {
             not(feature = "v1-5-0")
         )
     ))]
+    #[link(name = "cadical", kind = "static")]
     extern "C" {
         pub fn ccadical_flip(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;
         pub fn ccadical_flippable(solver: *mut CaDiCaLHandle, lit: c_int) -> bool;

glucose/build.rs

@@ -1,4 +1,4 @@
-use std::{env, fs, path::Path, str};
+use std::{env, path::Path};
 
 fn main() {
     if std::env::var("DOCS_RS").is_ok() {
@@ -8,99 +8,34 @@ fn main() {
 
     // Build C++ library
     // Full commit hash needs to be provided
-    build(
-        "https://github.com/chrjabs/glucose4.git",
-        "main",
-        "a244a12a3f34da6c93377a6196291494fddf491e",
-    );
+    build();
 
     let out_dir = env::var("OUT_DIR").unwrap();
 
-    // Built solver is in out_dir
-    println!("cargo:rustc-link-search={}", out_dir);
-    println!("cargo:rustc-link-search={}/lib", out_dir);
-}
-
-fn build(repo: &str, branch: &str, commit: &str) {
-    let out_dir = env::var("OUT_DIR").unwrap();
-    let mut glucose_dir_str = out_dir.clone();
-    glucose_dir_str.push_str("/glucose");
-    let glucose_dir = Path::new(&glucose_dir_str);
-    if update_repo(glucose_dir, repo, branch, commit)
-        || !Path::new(&out_dir)
-            .join("lib")
-            .join("libglucose4.a")
-            .exists()
-    {
-        let mut conf = cmake::Config::new(glucose_dir);
-        conf.define("BUILD_SYRUP", "OFF")
-            .define("BUILD_EXECUTABLES", "OFF");
-        #[cfg(feature = "quiet")]
-        conf.define("QUIET", "ON");
-        #[cfg(not(feature = "debug"))]
-        conf.profile("Release");
-        conf.build();
-    };
-
-    println!("cargo:rustc-link-lib=static=glucose4");
+    println!("cargo:rerun-if-changed=cppsrc/");
 
     #[cfg(target_os = "macos")]
     println!("cargo:rustc-flags=-l dylib=c++");
 
     #[cfg(not(any(target_os = "macos", target_os = "windows")))]
     println!("cargo:rustc-flags=-l dylib=stdc++");
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
 }
 
-/// Returns true if there were changes, false if not
-fn update_repo(path: &Path, url: &str, branch: &str, commit: &str) -> bool {
-    let mut changed = false;
-    let target_oid = git2::Oid::from_str(commit)
-        .unwrap_or_else(|e| panic!("Invalid commit hash {}: {}", commit, e));
-    let repo = match git2::Repository::open(path) {
-        Ok(repo) => {
-            // Check if already at correct commit
-            if let Some(oid) = repo.head().unwrap().target_peel() {
-                if oid == target_oid {
-                    return changed;
-                }
-            };
-            // Check if commit needs to be fetched
-            if repo.find_commit(target_oid).is_err() {
-                // Fetch repo
-                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
-                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
-                });
-                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
-                    panic!(
-                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
-                        branch, path, e
-                    )
-                });
-                drop(remote);
-            }
-            repo
-        }
-        Err(_) => {
-            if path.exists() {
-                fs::remove_dir_all(path).unwrap_or_else(|e| {
-                    panic!(
-                        "Could not delete directory {}: {}",
-                        path.to_str().unwrap(),
-                        e
-                    )
-                });
-            };
-            changed = true;
-            git2::Repository::clone(url, path)
-                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
-        }
-    };
-    let target_commit = repo
-        .find_commit(target_oid)
-        .unwrap_or_else(|e| panic!("Could not find commit {}: {}", commit, e));
-    repo.checkout_tree(target_commit.as_object(), None)
-        .unwrap_or_else(|e| panic!("Could not checkout commit {}: {}", commit, e));
-    repo.set_head_detached(target_oid)
-        .unwrap_or_else(|e| panic!("Could not detach head at {}: {}", commit, e));
-    changed
+fn build() {
+    let crate_dir = env::var("CARGO_MANIFEST_DIR").unwrap();
+    let mut glucose_dir_str = crate_dir.clone();
+    glucose_dir_str.push_str("/cppsrc");
+    let glucose_dir = Path::new(&glucose_dir_str);
+    let mut conf = cmake::Config::new(glucose_dir);
+    conf.define("BUILD_SYRUP", "OFF")
+        .define("BUILD_EXECUTABLES", "OFF");
+    #[cfg(feature = "quiet")]
+    conf.define("QUIET", "ON");
+    #[cfg(not(feature = "debug"))]
+    conf.profile("Release");
+    conf.build();
 }

glucose/src/core.rs

@@ -359,6 +359,7 @@ mod ffi {
         _private: [u8; 0],
     }
 
+    #[link(name = "glucose4", kind = "static")]
     extern "C" {
         // Redefinitions of Glucose C API
         pub fn cglucose4_signature() -> *const c_char;

glucose/src/simp.rs

@@ -389,6 +389,7 @@ mod ffi {
         _private: [u8; 0],
     }
 
+    #[link(name = "glucose4", kind = "static")]
     extern "C" {
         // Redefinitions of Glucose C API
         pub fn cglucose4_signature() -> *const c_char;

kissat/build.rs

@@ -110,8 +110,6 @@ fn build(repo: &str, branch: &str, reference: &str) {
             .files(src_files)
             .compile("kissat");
     };
-
-    println!("cargo:rustc-link-lib=static=kissat");
 }
 
 /// Returns true if there were changes, false if not

kissat/src/lib.rs

@@ -475,6 +475,7 @@ mod ffi {
         _private: [u8; 0],
     }
 
+    #[link(name = "kissat", kind = "static")]
     extern "C" {
         // Redefinitions of Kissat API
         pub fn kissat_signature() -> *const c_char;

minisat/build.rs

@@ -1,4 +1,4 @@
-use std::{env, fs, path::Path, str};
+use std::{env, path::Path};
 
 fn main() {
     if std::env::var("DOCS_RS").is_ok() {
@@ -8,98 +8,33 @@ fn main() {
 
     // Build C++ library
     // Full commit hash needs to be provided
-    build(
-        "https://github.com/chrjabs/minisat.git",
-        "master",
-        "e168f6e72600f4b04769b0f3bbb7f89b1a200a67",
-    );
+    build();
 
     let out_dir = env::var("OUT_DIR").unwrap();
 
-    // Built solver is in out_dir
-    println!("cargo:rustc-link-search={}", out_dir);
-    println!("cargo:rustc-link-search={}/lib", out_dir);
-}
-
-fn build(repo: &str, branch: &str, commit: &str) {
-    let out_dir = env::var("OUT_DIR").unwrap();
-    let mut minisat_dir_str = out_dir.clone();
-    minisat_dir_str.push_str("/minisat");
-    let minisat_dir = Path::new(&minisat_dir_str);
-    if update_repo(minisat_dir, repo, branch, commit)
-        || !Path::new(&out_dir)
-            .join("lib")
-            .join("libminisat.a")
-            .exists()
-    {
-        let mut conf = cmake::Config::new(minisat_dir);
-        conf.define("BUILD_BINARIES", "OFF");
-        #[cfg(feature = "quiet")]
-        conf.define("QUIET", "ON");
-        #[cfg(not(feature = "debug"))]
-        conf.profile("Release");
-        conf.build();
-    };
-
-    println!("cargo:rustc-link-lib=static=minisat");
+    println!("cargo:rerun-if-changed=cppsrc/");
 
     #[cfg(target_os = "macos")]
     println!("cargo:rustc-flags=-l dylib=c++");
 
     #[cfg(not(any(target_os = "macos", target_os = "windows")))]
     println!("cargo:rustc-flags=-l dylib=stdc++");
+
+    // Built solver is in out_dir
+    println!("cargo:rustc-link-search={}", out_dir);
+    println!("cargo:rustc-link-search={}/lib", out_dir);
 }
 
-/// Returns true if there were changes, false if not
-fn update_repo(path: &Path, url: &str, branch: &str, commit: &str) -> bool {
-    let mut changed = false;
-    let target_oid = git2::Oid::from_str(commit)
-        .unwrap_or_else(|e| panic!("Invalid commit hash {}: {}", commit, e));
-    let repo = match git2::Repository::open(path) {
-        Ok(repo) => {
-            // Check if already at correct commit
-            if let Some(oid) = repo.head().unwrap().target_peel() {
-                if oid == target_oid {
-                    return changed;
-                }
-            };
-            // Check if commit needs to be fetched
-            if repo.find_commit(target_oid).is_err() {
-                // Fetch repo
-                let mut remote = repo.find_remote("origin").unwrap_or_else(|e| {
-                    panic!("Expected remote \"origin\" in git repo {:?}: {}", path, e)
-                });
-                remote.fetch(&[branch], None, None).unwrap_or_else(|e| {
-                    panic!(
-                        "Could not fetch \"origin/{}\" for git repo {:?}: {}",
-                        branch, path, e
-                    )
-                });
-                drop(remote);
-            }
-            repo
-        }
-        Err(_) => {
-            if path.exists() {
-                fs::remove_dir_all(path).unwrap_or_else(|e| {
-                    panic!(
-                        "Could not delete directory {}: {}",
-                        path.to_str().unwrap(),
-                        e
-                    )
-                });
-            };
-            changed = true;
-            git2::Repository::clone(url, path)
-                .unwrap_or_else(|e| panic!("Could not clone repository {}: {}", url, e))
-        }
-    };
-    let target_commit = repo
-        .find_commit(target_oid)
-        .unwrap_or_else(|e| panic!("Could not find commit {}: {}", commit, e));
-    repo.checkout_tree(target_commit.as_object(), None)
-        .unwrap_or_else(|e| panic!("Could not checkout commit {}: {}", commit, e));
-    repo.set_head_detached(target_oid)
-        .unwrap_or_else(|e| panic!("Could not detach head at {}: {}", commit, e));
-    changed
+fn build() {
+    let crate_dir = env::var("CARGO_MANIFEST_DIR").unwrap();
+    let mut minisat_dir_str = crate_dir.clone();
+    minisat_dir_str.push_str("/cppsrc");
+    let minisat_dir = Path::new(&minisat_dir_str);
+    let mut conf = cmake::Config::new(minisat_dir);
+    conf.define("BUILD_BINARIES", "OFF");
+    #[cfg(feature = "quiet")]
+    conf.define("QUIET", "ON");
+    #[cfg(not(feature = "debug"))]
+    conf.profile("Release");
+    conf.build();
 }

minisat/src/core.rs

@@ -358,7 +358,7 @@ mod ffi {
     pub struct MinisatHandle {
         _private: [u8; 0],
     }
-
+    #[link(name = "minisat", kind = "static")]
     extern "C" {
         // Redefinitions of Minisat C API
         pub fn cminisat_signature() -> *const c_char;

minisat/src/simp.rs

@@ -390,6 +390,7 @@ mod ffi {
         _private: [u8; 0],
     }
 
+    #[link(name = "minisat", kind = "static")]
     extern "C" {
         // Redefinitions of Minisat C API
         pub fn cminisat_signature() -> *const c_char;