refactor: use bindgen to generate solver bindings

Cargo.toml

@@ -20,6 +20,7 @@ edition = "2021"
 [workspace.dependencies]
 anyhow = "1.0.86"
 atty = "0.2.14"
+bindgen = "0.69.4"
 bzip2 = "0.4.4"
 cc = { version = "1.0.104", features = ["parallel"] }
 chrono = "0.4.38"

cadical/Cargo.toml

@@ -47,6 +47,7 @@ thiserror.workspace = true
 rustsat.workspace = true
 
 [build-dependencies]
+bindgen.workspace = true
 cc.workspace = true
 git2.workspace = true
 glob.workspace = true

cadical/build.rs

@@ -149,30 +149,63 @@ fn main() {
     #[cfg(all(feature = "quiet", feature = "logging"))]
     compile_error!("cannot combine cadical features quiet and logging");
 
+    let version = Version::determine();
+
     // Build C++ library
     build(
         "https://github.com/arminbiere/cadical.git",
         "master",
-        Version::determine(),
+        version,
     );
 
     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={out_dir}/lib");
+    println!("cargo:rustc-link-lib=cadical");
+
+    // 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++");
 
     for ext in ["h", "cpp"] {
         for file in glob(&format!("cppsrc/*.{ext}")).unwrap() {
             println!("cargo::rerun-if-changed={:?}", file.unwrap());
         }
     }
+
+    // Generate Rust FFI bindings
+    let bindings = bindgen::Builder::default()
+        .clang_arg("-Icppsrc")
+        .header(format!("{out_dir}/cadical/src/ccadical.h"))
+        .allowlist_file(format!("{out_dir}/cadical/src/ccadical.h"))
+        .allowlist_file("cppsrc/ccadical_extension.h")
+        .blocklist_item("FILE")
+        .blocklist_function("ccadical_add")
+        .blocklist_function("ccadical_assume")
+        .blocklist_function("ccadical_solve")
+        .blocklist_function("ccadical_constrain")
+        .blocklist_function("ccadical_set_option")
+        .blocklist_function("ccadical_limit")
+        .blocklist_function("ccadical_trace_proof")
+        .blocklist_function("ccadical_close_proof")
+        .blocklist_function("ccadical_conclude")
+        .blocklist_function("ccadical_simplify");
+    let bindings = if version.has_flip() {
+        bindings.clang_arg("-DFLIP")
+    } else {
+        bindings
+    };
+    let bindings = bindings
+        .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(repo: &str, branch: &str, version: Version) {

cadical/cppsrc/ccadical_extension.cpp

@@ -3,8 +3,6 @@
 
 extern "C" {
 
-const int OUT_OF_MEM = 50;
-
 int ccadical_add_mem(CCaDiCaL *wrapper, int lit) {
   try {
     ((Wrapper *)wrapper)->solver->add(lit);

cadical/cppsrc/ccadical_extension.h

@@ -0,0 +1,27 @@
+// CaDiCaL C API Extension (Christoph Jabs)
+// To be included at the bottom of `ccadical.h`
+
+#include <stdbool.h>
+
+const int OUT_OF_MEM = 50;
+
+int ccadical_add_mem(CCaDiCaL *wrapper, int lit);
+int ccadical_assume_mem(CCaDiCaL *wrapper, int lit);
+int ccadical_constrain_mem(CCaDiCaL *wrapper, int lit);
+int ccadical_solve_mem(CCaDiCaL *wrapper);
+bool ccadical_configure(CCaDiCaL *ptr, const char *name);
+void ccadical_phase(CCaDiCaL *ptr, int lit);
+void ccadical_unphase(CCaDiCaL *ptr, int lit);
+int ccadical_vars(CCaDiCaL *ptr);
+bool ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val);
+bool ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val);
+int64_t ccadical_redundant(CCaDiCaL *wrapper);
+int ccadical_simplify_rounds(CCaDiCaL *wrapper, int rounds);
+int ccadical_reserve(CCaDiCaL *wrapper, int min_max_var);
+int64_t ccadical_propagations(CCaDiCaL *wrapper);
+int64_t ccadical_decisions(CCaDiCaL *wrapper);
+int64_t ccadical_conflicts(CCaDiCaL *wrapper);
+#ifdef FLIP
+bool ccadical_flip(CCaDiCaL *wrapper, int lit);
+bool ccadical_flippable(CCaDiCaL *wrapper, int lit);
+#endif

cadical/patches/v150.patch

@@ -1,13 +1,14 @@
-From 61d7d681eff0bffa21ceb06d7bdf26510943d5de Mon Sep 17 00:00:00 2001
+From 28cbfbe8533c4ee828236292567c62b2ea40ceef Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:51:07 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 3 ++-
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+), 1 deletion(-)
+ 4 files changed, 8 insertions(+), 1 deletion(-)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index cbe476d..5837547 100644
@@ -34,6 +35,19 @@ index e6e7d28..8bc4838 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 332f842..01c75e5 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 31b1610..b502623 100644
 --- a/src/solver.cpp

cadical/patches/v154.patch

@@ -1,13 +1,14 @@
-From e61e938ca8436e99acac25e7c8d60c598eb6d356 Mon Sep 17 00:00:00 2001
+From 796ee16856ba4ed2759192e0b7e5127ad6560d08 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:55:22 +0300
+Date: Thu, 11 Jul 2024 15:51:07 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 3 ++-
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+), 1 deletion(-)
+ 4 files changed, 8 insertions(+), 1 deletion(-)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 066c94b..5ee73d9 100644
@@ -34,6 +35,19 @@ index e6e7d28..8bc4838 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 332f842..01c75e5 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 5648101..7dcd418 100644
 --- a/src/solver.cpp

cadical/patches/v156.patch

@@ -1,13 +1,14 @@
-From c077ccc600cf19918bf6adf19156babe78aa2daa Mon Sep 17 00:00:00 2001
+From 0259e107798a2131a994f20ebe46a688b95bc30b Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:52:35 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+)
+ 4 files changed, 8 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 49310c7..079587e 100644
@@ -32,6 +33,19 @@ index ac11e44..8747cbf 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..f782606 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 63293ad..0e31a37 100644
 --- a/src/solver.cpp

cadical/patches/v160.patch

@@ -1,13 +1,14 @@
-From 78e9c894413a254b0e30508e136fa1415208d657 Mon Sep 17 00:00:00 2001
+From 56abcd5286937d8931a3f2815d82040890e9e6af Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:52:35 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+)
+ 4 files changed, 8 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 26cb9ca..fdb5e21 100644
@@ -32,6 +33,19 @@ index ac11e44..8747cbf 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..f782606 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 9ac3887..e0a2989 100644
 --- a/src/solver.cpp

cadical/patches/v170.patch

@@ -1,13 +1,14 @@
-From 81cabcda6f18f9d4c76458cc997c6e2a796ca118 Mon Sep 17 00:00:00 2001
+From 0dfb9d10f79608876fd7dec0efa29e630a52210e Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:52:35 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+)
+ 4 files changed, 8 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 26cb9ca..fdb5e21 100644
@@ -32,6 +33,19 @@ index ac11e44..8747cbf 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..f782606 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 3887a97..9e5dd6b 100644
 --- a/src/solver.cpp

cadical/patches/v171.patch

@@ -1,13 +1,14 @@
-From a7ed359532daf2a9d483321d6268bef9e2352942 Mon Sep 17 00:00:00 2001
+From 7ed9976cf1074ccea1897d4202de46adc8b36279 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:52:35 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+)
+ 4 files changed, 8 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 0991695..74563f3 100644
@@ -32,6 +33,19 @@ index ac11e44..8747cbf 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..f782606 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 5a5733c..f8933b0 100644
 --- a/src/solver.cpp

cadical/patches/v180.patch

@@ -1,13 +1,14 @@
-From cbef0528491c3baa7d07c30800c6d1de7cda30b4 Mon Sep 17 00:00:00 2001
+From d87e6795eb7c13dedf16b1965102199a3a4d6c93 Mon Sep 17 00:00:00 2001
 From: Christoph Jabs <christoph.jabs@helsinki.fi>
-Date: Tue, 2 Jul 2024 14:23:50 +0300
+Date: Thu, 11 Jul 2024 15:52:35 +0300
 Subject: [PATCH] extend C api
 
 ---
  src/cadical.hpp  | 2 ++
  src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
  src/solver.cpp   | 2 ++
- 3 files changed, 6 insertions(+)
+ 4 files changed, 8 insertions(+)
 
 diff --git a/src/cadical.hpp b/src/cadical.hpp
 index 0ce3e82..6794af6 100644
@@ -32,6 +33,19 @@ index ac11e44..8747cbf 100644
  }
 +
 +#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 30a79b3..f782606 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -56,6 +56,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
 diff --git a/src/solver.cpp b/src/solver.cpp
 index 520664d..1306c76 100644
 --- a/src/solver.cpp