Release 0.5

fatemender · Jul 5, 2024 · 4c4ec1b · 4c4ec1b
1 parent 1c338f4
commit 4c4ec1b
Show file tree

Hide file tree

Showing 8 changed files with 809 additions and 1,041 deletions.
diff --git a/Cargo.toml b/Cargo.toml
@@ -4,21 +4,21 @@ build                                   = "build.rs"
 categories                              = ["external-ffi-bindings"]
 description                             = "Low-level bindings for the Bitwuzla SMT solver"
 documentation                           = "https://docs.rs/bitwuzla-sys"
-edition                                 = "2018"
+edition                                 = "2021"
 homepage                                = "https://github.com/fatemender/bitwuzla-sys"
 keywords                                = ["ffi", "smt"]
 license                                 = "MIT"
 links                                   = "bitwuzla"
 name                                    = "bitwuzla-sys"
 readme                                  = "README.md"
 repository                              = "https://github.com/fatemender/bitwuzla-sys"
-version                                 = "0.2.0"
+version                                 = "0.5.0"
 
 [features]
 vendor-cadical                          = ["copy_dir"]
 
 [dependencies]
-libc                                    = "0.2.73"
+libc                                    = "0.2"
 
 [build-dependencies]
-copy_dir                                = { version = "0.1.2", optional = true }
+copy_dir                                = { version = "0.1", optional = true }
diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2021 Mikhail Solovev
+Copyright (c) 2021, 2024 Mikhail Solovev
 Copyright (c) 2022 Mrmaxmeier <https://github.com/Mrmaxmeier>
 
 Permission is hereby granted, free of charge, to any person obtaining a copy

diff --git a/README.md b/README.md
@@ -3,7 +3,8 @@
 
 # bitwuzla-sys
 
-This Rust crate provides low-level bindings for the [Bitwuzla] SMT solver.
+This Rust crate provides low-level bindings for the [Bitwuzla] SMT solver,
+version 0.5.0.
 
 [Bitwuzla]: https://bitwuzla.github.io/
 
@@ -16,7 +17,7 @@ to your `Cargo.toml`:
 
 ```toml
 [dependencies]
-bitwuzla-sys = "0.2"
+bitwuzla-sys = "0.5"
 ```
 
 ### Using vendored static `bitwuzla` library
@@ -26,15 +27,15 @@ with the `vendor-cadical` feature enabled:
 
 ```toml
 [dependencies]
-bitwuzla-sys = { version = "0.2", features = ["vendor-cadical"] }
+bitwuzla-sys = { version = "0.5", features = ["vendor-cadical"] }
 ```
 
 Enabling `vendor-cadical` will automatically build a static `bitwuzla` library
 and link against it.  Currently this uses the CaDiCaL SAT solver.
 
 In order for the build to succeed, you'll need to install some tools on your
-build host; for a Debian-based distribution `build-essential`, `cmake`, `curl`,
-and `git` should be sufficient.
+build host; for a Debian-based distribution `build-essential`, `git`, `m4`,
+and `meson` should be sufficient.
 
 ## License
 

diff --git a/bitwuzla b/bitwuzla
diff --git a/build-vendor.rs b/build-vendor.rs
@@ -22,62 +22,38 @@ impl BitwuzlaBuild {
             copy_dir(&self.src_dir, &self.out_dir).expect("failed to copy Bitwuzla sources to `OUT_DIR`");
         }
 
-        if !self.out_dir.join("deps/install/lib/libcadical.a").exists() {
-            self.run_command(
-                "Download and build CaDiCaL",
-                Command::new("/usr/bin/env")
-                    .arg("bash")
-                    .arg(self.out_dir.join("contrib/setup-cadical.sh"))
-                    .current_dir(&self.out_dir),
-            );
-        }
-
-        if !self.out_dir.join("deps/install/lib/libbtor2parser.a").exists() {
-            self.run_command(
-                "Download and build BTOR2Tools",
-                Command::new("/usr/bin/env")
-                    .arg("bash")
-                    .arg(self.out_dir.join("contrib/setup-btor2tools.sh"))
-                    .current_dir(&self.out_dir),
-            );
-        }
-
-        if !self.out_dir.join("deps/symfpu").exists() {
-            self.run_command(
-                "Download and build SymFPU",
-                Command::new("/usr/bin/env")
-                    .arg("bash")
-                    .arg(self.out_dir.join("contrib/setup-symfpu.sh"))
-                    .current_dir(&self.out_dir),
-            );
-        }
-
-        println!("cargo:rustc-link-search=native={}", self.out_dir.join("deps/install/lib").display());
-        println!("cargo:rustc-link-lib=static=cadical");
-        println!("cargo:rustc-link-lib=static=btor2parser");
-
         self
     }
 
     pub fn build(self) -> Self {
         self.run_command(
             "Configure Bitwuzla",
-            Command::new("/bin/sh")
-                .arg(self.out_dir.join("configure.sh"))
+            Command::new("/usr/bin/env")
+                .arg("python3")
+                .arg(self.out_dir.join("configure.py"))
                 .current_dir(&self.out_dir),
         );
 
         self.run_command(
             "Build Bitwuzla",
-            Command::new("make")
-                .arg("-j")
+            Command::new("meson")
+                .arg("compile")
                 .current_dir(self.out_dir.join("build")),
         );
 
-        println!("cargo:rustc-link-search=native={}", self.out_dir.join("build/lib").display());
-        println!("cargo:rustc-link-lib=static=bitwuzla");
-        println!("cargo:rustc-link-lib=stdc++");
-        println!("cargo:rustc-link-lib=gmp");
+        println!("cargo:rustc-link-search=native={}", self.out_dir.join("build/src").display());
+        println!("cargo:rustc-link-search=native={}", self.out_dir.join("build/src/lib").display());
+        println!("cargo:rustc-link-search=native={}", self.out_dir.join("build/subprojects/gmp-6.3.0/build/.libs").display());
+        println!("cargo:rustc-link-arg=-Wl,-Bstatic");
+        println!("cargo:rustc-link-arg=-Wl,--start-group");
+        println!("cargo:rustc-link-arg=-lbitwuzla");
+        println!("cargo:rustc-link-arg=-lbitwuzlabb");
+        println!("cargo:rustc-link-arg=-lbitwuzlabv");
+        println!("cargo:rustc-link-arg=-lbitwuzlals");
+        println!("cargo:rustc-link-arg=-Wl,--end-group");
+        println!("cargo:rustc-link-arg=-Wl,-Bdynamic");
+        println!("cargo:rustc-link-arg=-Wl,-lstdc++");
+        println!("cargo:rustc-link-arg=-Wl,-lgmp");
 
         self
     }