From 3809783f384552725b95d9568a2bfe63649039da Mon Sep 17 00:00:00 2001 From: Christoph Jabs Date: Thu, 11 Jul 2024 15:55:42 +0300 Subject: [PATCH] refactor: use bindgen to generate solver bindings --- Cargo.toml | 1 + cadical/Cargo.toml | 1 + cadical/build.rs | 47 +++++++++-- cadical/cppsrc/ccadical_extension.cpp | 2 - cadical/cppsrc/ccadical_extension.h | 27 +++++++ cadical/patches/v150.patch | 20 ++++- cadical/patches/v154.patch | 20 ++++- cadical/patches/v156.patch | 20 ++++- cadical/patches/v160.patch | 20 ++++- cadical/patches/v170.patch | 20 ++++- cadical/patches/v171.patch | 20 ++++- cadical/patches/v180.patch | 20 ++++- cadical/patches/v190.patch | 20 ++++- cadical/patches/v192.patch | 20 ++++- cadical/patches/v200.patch | 20 ++++- cadical/src/lib.rs | 109 +++++--------------------- cadical/tests/flipping.rs | 7 ++ glucose/Cargo.toml | 1 + glucose/build.rs | 30 +++++-- glucose/cppsrc | 2 +- glucose/src/core.rs | 45 +---------- glucose/src/lib.rs | 11 ++- glucose/src/simp.rs | 48 +----------- kissat/Cargo.toml | 1 + kissat/build.rs | 21 ++++- kissat/src/lib.rs | 63 ++++----------- minisat/Cargo.toml | 1 + minisat/build.rs | 30 +++++-- minisat/cppsrc | 2 +- minisat/src/core.rs | 42 +--------- minisat/src/lib.rs | 11 ++- minisat/src/simp.rs | 46 +---------- 32 files changed, 385 insertions(+), 363 deletions(-) create mode 100644 cadical/cppsrc/ccadical_extension.h diff --git a/Cargo.toml b/Cargo.toml index 296a8def..8526457d 100644 --- a/Cargo.toml +++ b/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" diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml index 8216f976..2877c0b5 100644 --- a/cadical/Cargo.toml +++ b/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 diff --git a/cadical/build.rs b/cadical/build.rs index b0b80921..2a5fe03c 100644 --- a/cadical/build.rs +++ b/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) { diff --git a/cadical/cppsrc/ccadical_extension.cpp b/cadical/cppsrc/ccadical_extension.cpp index 49a8daef..57877481 100644 --- a/cadical/cppsrc/ccadical_extension.cpp +++ b/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); diff --git a/cadical/cppsrc/ccadical_extension.h b/cadical/cppsrc/ccadical_extension.h new file mode 100644 index 00000000..e85a1e44 --- /dev/null +++ b/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 + +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 diff --git a/cadical/patches/v150.patch b/cadical/patches/v150.patch index 2c5c8e7a..9118753b 100644 --- a/cadical/patches/v150.patch +++ b/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 -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 diff --git a/cadical/patches/v154.patch b/cadical/patches/v154.patch index 346be64c..991f6c25 100644 --- a/cadical/patches/v154.patch +++ b/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 -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 diff --git a/cadical/patches/v156.patch b/cadical/patches/v156.patch index 14315f25..396305f7 100644 --- a/cadical/patches/v156.patch +++ b/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 -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 diff --git a/cadical/patches/v160.patch b/cadical/patches/v160.patch index 2cc98d2d..fc0e5fce 100644 --- a/cadical/patches/v160.patch +++ b/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 -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 diff --git a/cadical/patches/v170.patch b/cadical/patches/v170.patch index dd6bb5f0..cdd6a362 100644 --- a/cadical/patches/v170.patch +++ b/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 -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 diff --git a/cadical/patches/v171.patch b/cadical/patches/v171.patch index 62d59959..15e2da73 100644 --- a/cadical/patches/v171.patch +++ b/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 -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 diff --git a/cadical/patches/v180.patch b/cadical/patches/v180.patch index 102f9e3d..4d1ee837 100644 --- a/cadical/patches/v180.patch +++ b/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 -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 diff --git a/cadical/patches/v190.patch b/cadical/patches/v190.patch index 8da527b6..cc64a056 100644 --- a/cadical/patches/v190.patch +++ b/cadical/patches/v190.patch @@ -1,13 +1,14 @@ -From e432e84d526e98c528ed82086182a6e9e19c5420 Mon Sep 17 00:00:00 2001 +From 584cf4ea826b87e5a2fb4b09572494fdf63e16b6 Mon Sep 17 00:00:00 2001 From: Christoph Jabs -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 3270592..b25099b 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 590d3f1..687e193 100644 --- a/src/solver.cpp diff --git a/cadical/patches/v192.patch b/cadical/patches/v192.patch index d3b6bb7c..973cfc4d 100644 --- a/cadical/patches/v192.patch +++ b/cadical/patches/v192.patch @@ -1,13 +1,14 @@ -From 359f0852cf10730bcb3a6fa11e5e73494e97ddf8 Mon Sep 17 00:00:00 2001 +From 473256132d6259492e33055979086d61862ff4f3 Mon Sep 17 00:00:00 2001 From: Christoph Jabs -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 a803292..2301c40 100644 @@ -32,6 +33,19 @@ index 88ab164..8186054 100644 } + +#include "ccadical_extension.cpp" +diff --git a/src/ccadical.h b/src/ccadical.h +index 6d1b3ff..a8f1b48 100644 +--- a/src/ccadical.h ++++ b/src/ccadical.h +@@ -60,6 +60,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 a2505ee..54ba611 100644 --- a/src/solver.cpp diff --git a/cadical/patches/v200.patch b/cadical/patches/v200.patch index 92ce6e59..bcdc19b2 100644 --- a/cadical/patches/v200.patch +++ b/cadical/patches/v200.patch @@ -1,13 +1,14 @@ -From 4bd4976c8539ea4121d234dde135e7723f60a7d1 Mon Sep 17 00:00:00 2001 +From 42d92c89a5a5b52ed86f7549fd8a5d9392fb525e Mon Sep 17 00:00:00 2001 From: Christoph Jabs -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 a803292..2301c40 100644 @@ -32,6 +33,19 @@ index 88ab164..8186054 100644 } + +#include "ccadical_extension.cpp" +diff --git a/src/ccadical.h b/src/ccadical.h +index 6d1b3ff..a8f1b48 100644 +--- a/src/ccadical.h ++++ b/src/ccadical.h +@@ -60,6 +60,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 e917b3c..34535c1 100644 --- a/src/solver.cpp diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs index 145bde28..4d3ebe12 100644 --- a/cadical/src/lib.rs +++ b/cadical/src/lib.rs @@ -27,7 +27,6 @@ use core::ffi::{c_int, c_void, CStr}; use std::{cmp::Ordering, ffi::CString, fmt}; use cpu_time::ProcessTime; -use ffi::CaDiCaLHandle; use rustsat::solvers::{ ControlSignal, FreezeVar, GetInternalStats, Interrupt, InterruptSolver, Learn, LimitConflicts, LimitDecisions, PhaseLit, Solve, SolveIncremental, SolveStats, SolverResult, SolverState, @@ -36,12 +35,10 @@ use rustsat::solvers::{ use rustsat::types::{Clause, Lit, TernaryVal, Var}; use thiserror::Error; -const OUT_OF_MEM: c_int = 50; - macro_rules! handle_oom { ($val:expr) => {{ let val = $val; - if val == crate::OUT_OF_MEM { + if val == $crate::ffi::OUT_OF_MEM { return anyhow::Context::context( Err(rustsat::OutOfMemory::ExternalApi), "cadical out of memory", @@ -51,7 +48,7 @@ macro_rules! handle_oom { }}; ($val:expr, noanyhow) => {{ let val = $val; - if val == crate::OUT_OF_MEM { + if val == $crate::ffi::OUT_OF_MEM { return Err(rustsat::OutOfMemory::ExternalApi); } val @@ -96,7 +93,7 @@ type OptLearnCallbackStore<'a> = Option>>; /// The CaDiCaL solver type pub struct CaDiCaL<'term, 'learn> { - handle: *mut CaDiCaLHandle, + handle: *mut ffi::CCaDiCaL, state: InternalSolverState, terminate_cb: OptTermCallbackStore<'term>, learner_cb: OptLearnCallbackStore<'learn>, @@ -632,7 +629,7 @@ impl<'term> Terminate<'term> for CaDiCaL<'term, '_> { { self.terminate_cb = Some(Box::new(Box::new(cb))); let cb_ptr = - std::ptr::from_ref(self.terminate_cb.as_mut().unwrap().as_mut()).cast::(); + std::ptr::from_mut(self.terminate_cb.as_mut().unwrap().as_mut()).cast::(); unsafe { ffi::ccadical_set_terminate(self.handle, cb_ptr, Some(ffi::ccadical_terminate_cb)); } @@ -640,7 +637,7 @@ impl<'term> Terminate<'term> for CaDiCaL<'term, '_> { fn detach_terminator(&mut self) { self.terminate_cb = None; - unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null(), None) } + unsafe { ffi::ccadical_set_terminate(self.handle, std::ptr::null_mut(), None) } } } @@ -676,7 +673,7 @@ impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn> { { self.learner_cb = Some(Box::new(Box::new(cb))); let cb_ptr = - std::ptr::from_ref(self.learner_cb.as_mut().unwrap().as_mut()).cast::(); + std::ptr::from_mut(self.learner_cb.as_mut().unwrap().as_mut()).cast::(); unsafe { ffi::ccadical_set_learn( self.handle, @@ -689,7 +686,7 @@ impl<'learn> Learn<'learn> for CaDiCaL<'_, 'learn> { fn detach_learner(&mut self) { self.terminate_cb = None; - unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null(), 0, None) } + unsafe { ffi::ccadical_set_learn(self.handle, std::ptr::null_mut(), 0, None) } } } @@ -705,7 +702,7 @@ impl Interrupt for CaDiCaL<'_, '_> { /// An Interrupter for the CaDiCaL solver pub struct Interrupter { /// The C API handle - handle: *mut CaDiCaLHandle, + handle: *mut ffi::CCaDiCaL, } unsafe impl Send for Interrupter {} @@ -1009,96 +1006,30 @@ mod test { } mod ffi { - use core::ffi::{c_char, c_int, c_void}; - use rustsat::{solvers::ControlSignal, types::Lit}; - use std::slice; + #![allow(non_upper_case_globals)] + #![allow(non_camel_case_types)] + #![allow(non_snake_case)] - use super::{LearnCallbackPtr, TermCallbackPtr}; + use core::ffi::{c_int, c_void}; + use std::slice; - #[repr(C)] - pub struct CaDiCaLHandle { - _private: [u8; 0], - } + use rustsat::{solvers::ControlSignal, types::Lit}; - #[link(name = "cadical", kind = "static")] - extern "C" { - // Redefinitions of CaDiCaL C API - pub fn ccadical_signature() -> *const c_char; - pub fn ccadical_init() -> *mut CaDiCaLHandle; - pub fn ccadical_release(solver: *mut CaDiCaLHandle); - pub fn ccadical_add_mem(solver: *mut CaDiCaLHandle, lit_or_zero: c_int) -> c_int; - pub fn ccadical_assume_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_solve_mem(solver: *mut CaDiCaLHandle) -> c_int; - pub fn ccadical_val(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_failed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_set_terminate( - solver: *mut CaDiCaLHandle, - state: *const c_void, - terminate: Option c_int>, - ); - pub fn ccadical_set_learn( - solver: *mut CaDiCaLHandle, - state: *const c_void, - max_length: c_int, - learn: Option, - ); - pub fn ccadical_constrain_mem(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_constraint_failed(solver: *mut CaDiCaLHandle) -> c_int; - pub fn ccadical_set_option_ret( - solver: *mut CaDiCaLHandle, - name: *const c_char, - val: c_int, - ) -> bool; - pub fn ccadical_get_option(solver: *mut CaDiCaLHandle, name: *const c_char) -> c_int; - pub fn ccadical_limit_ret( - solver: *mut CaDiCaLHandle, - name: *const c_char, - limit: c_int, - ) -> bool; - pub fn ccadical_print_statistics(solver: *mut CaDiCaLHandle); - pub fn ccadical_active(solver: *mut CaDiCaLHandle) -> i64; - pub fn ccadical_irredundant(solver: *mut CaDiCaLHandle) -> i64; - pub fn ccadical_redundant(solver: *mut CaDiCaLHandle) -> i64; - pub fn ccadical_fixed(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_terminate(solver: *mut CaDiCaLHandle); - pub fn ccadical_freeze(solver: *mut CaDiCaLHandle, lit: c_int); - pub fn ccadical_frozen(solver: *mut CaDiCaLHandle, lit: c_int) -> c_int; - pub fn ccadical_melt(solver: *mut CaDiCaLHandle, lit: c_int); - pub fn ccadical_simplify_rounds(solver: *mut CaDiCaLHandle, rounds: c_int) -> c_int; - pub fn ccadical_configure(solver: *mut CaDiCaLHandle, name: *const c_char) -> bool; - pub fn ccadical_phase(solver: *mut CaDiCaLHandle, lit: c_int); - pub fn ccadical_unphase(solver: *mut CaDiCaLHandle, lit: c_int); - pub fn ccadical_vars(solver: *mut CaDiCaLHandle) -> c_int; - pub fn ccadical_reserve(solver: *mut CaDiCaLHandle, min_max_var: c_int) -> c_int; - pub fn ccadical_propagations(solver: *mut CaDiCaLHandle) -> i64; - pub fn ccadical_decisions(solver: *mut CaDiCaLHandle) -> i64; - pub fn ccadical_conflicts(solver: *mut CaDiCaLHandle) -> i64; - } + use super::{LearnCallbackPtr, TermCallbackPtr}; - // >= v1.5.4 - #[cfg(all( - not(feature = "v1-5-3"), - not(feature = "v1-5-2"), - not(feature = "v1-5-1"), - 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; - } + include!(concat!(env!("OUT_DIR"), "/bindings.rs")); // Raw callbacks forwarding to user callbacks - pub extern "C" fn ccadical_terminate_cb(ptr: *const c_void) -> c_int { - let cb = unsafe { &mut *(ptr as *mut TermCallbackPtr<'_>) }; + pub extern "C" fn ccadical_terminate_cb(ptr: *mut c_void) -> c_int { + let cb = unsafe { &mut *ptr.cast::>() }; match cb() { ControlSignal::Continue => 0, ControlSignal::Terminate => 1, } } - pub extern "C" fn ccadical_learn_cb(ptr: *const c_void, clause: *const c_int) { - let cb = unsafe { &mut *(ptr as *mut LearnCallbackPtr<'_>) }; + pub extern "C" fn ccadical_learn_cb(ptr: *mut c_void, clause: *mut c_int) { + let cb = unsafe { &mut *ptr.cast::>() }; let mut cnt = 0; for n in 0.. { diff --git a/cadical/tests/flipping.rs b/cadical/tests/flipping.rs index c83e4f70..7a6ddafd 100644 --- a/cadical/tests/flipping.rs +++ b/cadical/tests/flipping.rs @@ -1 +1,8 @@ +// >= v1.5.4 +#![cfg(all( + not(feature = "v1-5-3"), + not(feature = "v1-5-2"), + not(feature = "v1-5-1"), + not(feature = "v1-5-0") +))] rustsat_solvertests::flipping_tests!(rustsat_cadical::CaDiCaL); diff --git a/glucose/Cargo.toml b/glucose/Cargo.toml index 3fa190da..596b68cd 100644 --- a/glucose/Cargo.toml +++ b/glucose/Cargo.toml @@ -25,6 +25,7 @@ thiserror.workspace = true rustsat.workspace = true [build-dependencies] +bindgen.workspace = true cmake.workspace = true [dev-dependencies] diff --git a/glucose/build.rs b/glucose/build.rs index 8411de12..f88f8a19 100644 --- a/glucose/build.rs +++ b/glucose/build.rs @@ -1,6 +1,9 @@ #![warn(clippy::pedantic)] -use std::{env, path::Path}; +use std::{ + env, + path::{Path, PathBuf}, +}; fn main() { if std::env::var("DOCS_RS").is_ok() { @@ -16,15 +19,28 @@ fn main() { 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={out_dir}/lib"); + println!("cargo:rustc-link-lib=glucose4"); + + // 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++"); + + // Generate Rust FFI bindings + let bindings = bindgen::Builder::default() + .header("cppsrc/cglucose4.h") + .allowlist_file("cppsrc/cglucose4.h") + .parse_callbacks(Box::new(bindgen::CargoCallbacks::new())) + .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() { diff --git a/glucose/cppsrc b/glucose/cppsrc index f8dc4e9e..7defb730 160000 --- a/glucose/cppsrc +++ b/glucose/cppsrc @@ -1 +1 @@ -Subproject commit f8dc4e9ee77be9fc8b79cf7fcc2bc6d6d3a96dd1 +Subproject commit 7defb730f96d867081972151548d69c8237ae362 diff --git a/glucose/src/core.rs b/glucose/src/core.rs index c80e671a..020506f6 100644 --- a/glucose/src/core.rs +++ b/glucose/src/core.rs @@ -5,11 +5,7 @@ use core::ffi::{c_int, CStr}; -use crate::handle_oom; - -use super::{InternalSolverState, InvalidApiReturn, Limit}; use cpu_time::ProcessTime; -use ffi::Glucose4Handle; use rustsat::{ solvers::{ GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit, @@ -18,9 +14,11 @@ use rustsat::{ types::{Clause, Lit, TernaryVal, Var}, }; +use super::{ffi, handle_oom, InternalSolverState, InvalidApiReturn, Limit}; + /// The Glucose 4 solver type without preprocessing pub struct Glucose { - handle: *mut Glucose4Handle, + handle: *mut ffi::CGlucose4, state: InternalSolverState, stats: SolverStats, } @@ -247,7 +245,7 @@ impl Interrupt for Glucose { /// An Interrupter for the Glucose 4 Core solver pub struct Interrupter { /// The C API handle - handle: *mut Glucose4Handle, + handle: *mut ffi::CGlucose4, } unsafe impl Send for Interrupter {} @@ -378,38 +376,3 @@ mod test { assert_eq!(solver.max_var(), Some(var![9])); } } - -mod ffi { - use core::ffi::{c_char, c_int}; - - #[repr(C)] - pub struct Glucose4Handle { - _private: [u8; 0], - } - - #[link(name = "glucose4", kind = "static")] - extern "C" { - // Redefinitions of Glucose C API - pub fn cglucose4_signature() -> *const c_char; - pub fn cglucose4_init() -> *mut Glucose4Handle; - pub fn cglucose4_release(solver: *mut Glucose4Handle); - pub fn cglucose4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int) -> c_int; - pub fn cglucose4_assume(solver: *mut Glucose4Handle, lit: c_int); - pub fn cglucose4_solve(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucose4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucose4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucose4_phase(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucose4_unphase(solver: *mut Glucose4Handle, lit: c_int); - pub fn cglucose4_n_assigns(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucose4_n_clauses(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucose4_n_learnts(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucose4_n_vars(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucose4_set_conf_limit(solver: *mut Glucose4Handle, limit: i64); - pub fn cglucose4_set_prop_limit(solver: *mut Glucose4Handle, limit: i64); - pub fn cglucose4_set_no_limit(solver: *mut Glucose4Handle); - pub fn cglucose4_interrupt(solver: *mut Glucose4Handle); - pub fn cglucose4_propagations(solver: *mut Glucose4Handle) -> u64; - pub fn cglucose4_decisions(solver: *mut Glucose4Handle) -> u64; - pub fn cglucose4_conflicts(solver: *mut Glucose4Handle) -> u64; - } -} diff --git a/glucose/src/lib.rs b/glucose/src/lib.rs index 34a8e15f..df5baf4b 100644 --- a/glucose/src/lib.rs +++ b/glucose/src/lib.rs @@ -25,8 +25,6 @@ use thiserror::Error; pub mod core; pub mod simp; -const OUT_OF_MEM: c_int = 50; - /// Fatal error returned if the Glucose API returns an invalid value #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] #[error("glucose c-api returned an invalid value: {api_call} -> {value}")] @@ -87,7 +85,7 @@ impl fmt::Display for Limit { macro_rules! handle_oom { ($val:expr) => {{ let val = $val; - if val == crate::OUT_OF_MEM { + if val == $crate::ffi::OUT_OF_MEM { return anyhow::Context::context( Err(rustsat::OutOfMemory::ExternalApi), "glucose out of memory", @@ -97,3 +95,10 @@ macro_rules! handle_oom { }}; } pub(crate) use handle_oom; + +pub(crate) mod ffi { + #![allow(non_upper_case_globals)] + #![allow(non_camel_case_types)] + #![allow(non_snake_case)] + include!(concat!(env!("OUT_DIR"), "/bindings.rs")); +} diff --git a/glucose/src/simp.rs b/glucose/src/simp.rs index 177aafba..a5b98da7 100644 --- a/glucose/src/simp.rs +++ b/glucose/src/simp.rs @@ -5,11 +5,7 @@ use core::ffi::{c_int, CStr}; -use crate::handle_oom; - -use super::{AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit}; use cpu_time::ProcessTime; -use ffi::Glucose4Handle; use rustsat::{ solvers::{ FreezeVar, GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, @@ -19,9 +15,11 @@ use rustsat::{ types::{Clause, Lit, TernaryVal, Var}, }; +use super::{ffi, handle_oom, AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit}; + /// The Glucose 4 solver type with preprocessing pub struct Glucose { - handle: *mut Glucose4Handle, + handle: *mut ffi::CGlucoseSimp4, state: InternalSolverState, stats: SolverStats, } @@ -259,7 +257,7 @@ impl Interrupt for Glucose { /// An Interrupter for the Glucose 4 Simp solver pub struct Interrupter { /// The C API handle - handle: *mut Glucose4Handle, + handle: *mut ffi::CGlucoseSimp4, } unsafe impl Send for Interrupter {} @@ -407,41 +405,3 @@ mod test { assert_eq!(solver.max_var(), Some(var![9])); } } - -mod ffi { - use core::ffi::{c_char, c_int}; - - #[repr(C)] - pub struct Glucose4Handle { - _private: [u8; 0], - } - - #[link(name = "glucose4", kind = "static")] - extern "C" { - // Redefinitions of Glucose C API - pub fn cglucose4_signature() -> *const c_char; - pub fn cglucosesimp4_init() -> *mut Glucose4Handle; - pub fn cglucosesimp4_release(solver: *mut Glucose4Handle); - pub fn cglucosesimp4_add(solver: *mut Glucose4Handle, lit_or_zero: c_int) -> c_int; - pub fn cglucosesimp4_assume(solver: *mut Glucose4Handle, lit: c_int); - pub fn cglucosesimp4_solve(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucosesimp4_val(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucosesimp4_failed(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucosesimp4_phase(solver: *mut Glucose4Handle, lit: c_int) -> c_int; - pub fn cglucosesimp4_unphase(solver: *mut Glucose4Handle, lit: c_int); - pub fn cglucosesimp4_n_assigns(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucosesimp4_n_clauses(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucosesimp4_n_learnts(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucosesimp4_n_vars(solver: *mut Glucose4Handle) -> c_int; - pub fn cglucosesimp4_set_conf_limit(solver: *mut Glucose4Handle, limit: i64); - pub fn cglucosesimp4_set_prop_limit(solver: *mut Glucose4Handle, limit: i64); - pub fn cglucosesimp4_set_no_limit(solver: *mut Glucose4Handle); - pub fn cglucosesimp4_interrupt(solver: *mut Glucose4Handle); - pub fn cglucosesimp4_set_frozen(solver: *mut Glucose4Handle, var: c_int, frozen: bool); - pub fn cglucosesimp4_is_frozen(solver: *mut Glucose4Handle, var: c_int) -> c_int; - pub fn cglucosesimp4_is_eliminated(solver: *mut Glucose4Handle, var: c_int) -> c_int; - pub fn cglucosesimp4_propagations(solver: *mut Glucose4Handle) -> u64; - pub fn cglucosesimp4_decisions(solver: *mut Glucose4Handle) -> u64; - pub fn cglucosesimp4_conflicts(solver: *mut Glucose4Handle) -> u64; - } -} diff --git a/kissat/Cargo.toml b/kissat/Cargo.toml index 4b1707e3..9246222b 100644 --- a/kissat/Cargo.toml +++ b/kissat/Cargo.toml @@ -31,6 +31,7 @@ thiserror.workspace = true rustsat.workspace = true [build-dependencies] +bindgen.workspace = true cc.workspace = true chrono.workspace = true git2.workspace = true diff --git a/kissat/build.rs b/kissat/build.rs index f226b1fa..9b63c231 100644 --- a/kissat/build.rs +++ b/kissat/build.rs @@ -5,7 +5,7 @@ use std::{ env, fs::{self, File}, io::Write, - path::Path, + path::{Path, PathBuf}, process::Command, str, }; @@ -43,6 +43,25 @@ fn main() { // 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=kissat"); + + // Generate Rust FFI bindings + let bindings = bindgen::Builder::default() + .header(format!("{out_dir}/kissat/src/kissat.h")) + .header(format!("{out_dir}/kissat/src/error.h")) + .blocklist_function("kissat_copyright") + .blocklist_function("kissat_build") + .blocklist_function("kissat_banner") + .blocklist_function("kissat_has_configuration") + .blocklist_function("kissat_error") + .blocklist_function("kissat_fatal") + .blocklist_function("kissat_fatal_message_start") + .blocklist_function("kissat_abort") + .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, reference: &str) { diff --git a/kissat/src/lib.rs b/kissat/src/lib.rs index 77124f41..223281ac 100644 --- a/kissat/src/lib.rs +++ b/kissat/src/lib.rs @@ -30,7 +30,6 @@ use core::ffi::{c_int, c_uint, c_void, CStr}; use std::{ffi::CString, fmt}; use cpu_time::ProcessTime; -use ffi::KissatHandle; use rustsat::{ solvers::{ ControlSignal, Interrupt, InterruptSolver, Solve, SolveStats, SolverResult, SolverState, @@ -74,7 +73,7 @@ type OptTermCallbackStore<'a> = Option>>; /// The Kissat solver type pub struct Kissat<'term> { - handle: *mut KissatHandle, + handle: *mut ffi::kissat, state: InternalSolverState, terminate_cb: OptTermCallbackStore<'term>, stats: SolverStats, @@ -375,13 +374,13 @@ impl<'term> Terminate<'term> for Kissat<'term> { { self.terminate_cb = Some(Box::new(Box::new(cb))); let cb_ptr = - std::ptr::from_ref(self.terminate_cb.as_mut().unwrap().as_mut()).cast::(); + std::ptr::from_mut(self.terminate_cb.as_mut().unwrap().as_mut()).cast::(); unsafe { ffi::kissat_set_terminate(self.handle, cb_ptr, Some(ffi::kissat_terminate_cb)) } } fn detach_terminator(&mut self) { self.terminate_cb = None; - unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null(), None) } + unsafe { ffi::kissat_set_terminate(self.handle, std::ptr::null_mut(), None) } } } @@ -398,7 +397,7 @@ impl Interrupt for Kissat<'_> { /// An Interrupter for the Kissat solver pub struct Interrupter { /// The C API handle - handle: *mut KissatHandle, + handle: *mut ffi::kissat, } unsafe impl Send for Interrupter {} @@ -495,7 +494,7 @@ pub fn panic_intead_of_abort() { } /// Changes Kissat's abort behaviour to call the given function instead -pub fn call_instead_of_abort(abort: Option) { +pub fn call_instead_of_abort(abort: Option) { unsafe { ffi::kissat_call_function_instead_of_abort(abort) }; } @@ -543,51 +542,21 @@ mod test { } mod ffi { - use super::TermCallbackPtr; - use core::ffi::{c_char, c_int, c_uint, c_void}; + #![allow(non_upper_case_globals)] + #![allow(non_camel_case_types)] + #![allow(non_snake_case)] + + use core::ffi::{c_int, c_void}; + use rustsat::solvers::ControlSignal; - #[repr(C)] - pub struct KissatHandle { - _private: [u8; 0], - } - - #[link(name = "kissat", kind = "static")] - extern "C" { - // Redefinitions of Kissat API - pub fn kissat_signature() -> *const c_char; - pub fn kissat_init() -> *mut KissatHandle; - pub fn kissat_release(solver: *mut KissatHandle); - pub fn kissat_add(solver: *mut KissatHandle, lit_or_zero: c_int); - pub fn kissat_solve(solver: *mut KissatHandle) -> c_int; - pub fn kissat_value(solver: *mut KissatHandle, lit: c_int) -> c_int; - pub fn kissat_set_terminate( - solver: *mut KissatHandle, - state: *const c_void, - terminate: Option c_int>, - ); - pub fn kissat_terminate(solver: *mut KissatHandle); - pub fn kissat_reserve(solver: *mut KissatHandle, max_var: c_int); - pub fn kissat_id() -> *const c_char; - pub fn kissat_version() -> *const c_char; - pub fn kissat_compiler() -> *const c_char; - pub fn kissat_set_option( - solver: *mut KissatHandle, - name: *const c_char, - val: c_int, - ) -> c_int; - pub fn kissat_get_option(solver: *mut KissatHandle, name: *const c_char) -> c_int; - pub fn kissat_set_configuration(solver: *mut KissatHandle, name: *const c_char) -> c_int; - pub fn kissat_set_conflict_limit(solver: *mut KissatHandle, limit: c_uint); - pub fn kissat_set_decision_limit(solver: *mut KissatHandle, limit: c_uint); - pub fn kissat_print_statistics(solver: *mut KissatHandle); - // This is from `error.h` - pub fn kissat_call_function_instead_of_abort(abort: Option); - } + use super::TermCallbackPtr; + + include!(concat!(env!("OUT_DIR"), "/bindings.rs")); // Raw callbacks forwarding to user callbacks - pub extern "C" fn kissat_terminate_cb(ptr: *const c_void) -> c_int { - let cb = unsafe { &mut *(ptr as *mut TermCallbackPtr) }; + pub extern "C" fn kissat_terminate_cb(ptr: *mut c_void) -> c_int { + let cb = unsafe { &mut *ptr.cast::() }; match cb() { ControlSignal::Continue => 0, ControlSignal::Terminate => 1, diff --git a/minisat/Cargo.toml b/minisat/Cargo.toml index 516bee6e..e279c8e6 100644 --- a/minisat/Cargo.toml +++ b/minisat/Cargo.toml @@ -25,6 +25,7 @@ thiserror.workspace = true rustsat.workspace = true [build-dependencies] +bindgen.workspace = true cmake.workspace = true [dev-dependencies] diff --git a/minisat/build.rs b/minisat/build.rs index 4f082204..3e20eb05 100644 --- a/minisat/build.rs +++ b/minisat/build.rs @@ -1,6 +1,9 @@ #![warn(clippy::pedantic)] -use std::{env, path::Path}; +use std::{ + env, + path::{Path, PathBuf}, +}; fn main() { if std::env::var("DOCS_RS").is_ok() { @@ -16,15 +19,28 @@ fn main() { 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={out_dir}/lib"); + println!("cargo:rustc-link-lib=minisat"); + + // 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++"); + + // Generate Rust FFI bindings + let bindings = bindgen::Builder::default() + .header("cppsrc/minisat/cminisat.h") + .allowlist_file("cppsrc/minisat/cminisat.h") + .parse_callbacks(Box::new(bindgen::CargoCallbacks::new())) + .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() { diff --git a/minisat/cppsrc b/minisat/cppsrc index c17b905d..bc79344a 160000 --- a/minisat/cppsrc +++ b/minisat/cppsrc @@ -1 +1 @@ -Subproject commit c17b905d3654cdfffe5837cf275402e4f40c3435 +Subproject commit bc79344a27a9e4b8f0709d6890d6c2efeb6cbc36 diff --git a/minisat/src/core.rs b/minisat/src/core.rs index fbe7ec29..73f94ae5 100644 --- a/minisat/src/core.rs +++ b/minisat/src/core.rs @@ -5,9 +5,7 @@ use core::ffi::{c_int, CStr}; -use super::{handle_oom, InternalSolverState, InvalidApiReturn, Limit}; use cpu_time::ProcessTime; -use ffi::MinisatHandle; use rustsat::{ solvers::{ GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, PhaseLit, @@ -16,9 +14,11 @@ use rustsat::{ types::{Clause, Lit, TernaryVal, Var}, }; +use super::{ffi, handle_oom, InternalSolverState, InvalidApiReturn, Limit}; + /// The Minisat solver type without preprocessing pub struct Minisat { - handle: *mut MinisatHandle, + handle: *mut ffi::CMinisat, state: InternalSolverState, stats: SolverStats, } @@ -245,7 +245,7 @@ impl Interrupt for Minisat { /// An Interrupter for the Minisat Core solver pub struct Interrupter { /// The C API handle - handle: *mut MinisatHandle, + handle: *mut ffi::CMinisat, } unsafe impl Send for Interrupter {} @@ -376,37 +376,3 @@ mod test { assert_eq!(solver.max_var(), Some(var![9])); } } - -mod ffi { - use core::ffi::{c_char, c_int}; - - #[repr(C)] - 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; - pub fn cminisat_init() -> *mut MinisatHandle; - pub fn cminisat_release(solver: *mut MinisatHandle); - pub fn cminisat_add(solver: *mut MinisatHandle, lit_or_zero: c_int) -> c_int; - pub fn cminisat_assume(solver: *mut MinisatHandle, lit: c_int); - pub fn cminisat_solve(solver: *mut MinisatHandle) -> c_int; - pub fn cminisat_val(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisat_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisat_phase(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisat_unphase(solver: *mut MinisatHandle, lit: c_int); - pub fn cminisat_n_assigns(solver: *mut MinisatHandle) -> c_int; - pub fn cminisat_n_clauses(solver: *mut MinisatHandle) -> c_int; - pub fn cminisat_n_learnts(solver: *mut MinisatHandle) -> c_int; - pub fn cminisat_n_vars(solver: *mut MinisatHandle) -> c_int; - pub fn cminisat_set_conf_limit(solver: *mut MinisatHandle, limit: i64); - pub fn cminisat_set_prop_limit(solver: *mut MinisatHandle, limit: i64); - pub fn cminisat_set_no_limit(solver: *mut MinisatHandle); - pub fn cminisat_interrupt(solver: *mut MinisatHandle); - pub fn cminisat_propagations(solver: *mut MinisatHandle) -> u64; - pub fn cminisat_decisions(solver: *mut MinisatHandle) -> u64; - pub fn cminisat_conflicts(solver: *mut MinisatHandle) -> u64; - } -} diff --git a/minisat/src/lib.rs b/minisat/src/lib.rs index 905627a2..4d0f0c8c 100644 --- a/minisat/src/lib.rs +++ b/minisat/src/lib.rs @@ -25,8 +25,6 @@ use thiserror::Error; pub mod core; pub mod simp; -const OUT_OF_MEM: c_int = 50; - /// Fatal error returned if the Minisat API returns an invalid value #[derive(Error, Clone, Copy, PartialEq, Eq, Debug)] #[error("minisat c-api returned an invalid value: {api_call} -> {value}")] @@ -87,7 +85,7 @@ impl fmt::Display for Limit { macro_rules! handle_oom { ($val:expr) => {{ let val = $val; - if val == crate::OUT_OF_MEM { + if val == $crate::ffi::OUT_OF_MEM { return anyhow::Context::context( Err(rustsat::OutOfMemory::ExternalApi), "minisat out of memory", @@ -97,3 +95,10 @@ macro_rules! handle_oom { }}; } pub(crate) use handle_oom; + +pub(crate) mod ffi { + #![allow(non_upper_case_globals)] + #![allow(non_camel_case_types)] + #![allow(non_snake_case)] + include!(concat!(env!("OUT_DIR"), "/bindings.rs")); +} diff --git a/minisat/src/simp.rs b/minisat/src/simp.rs index 245295ba..3967ec5c 100644 --- a/minisat/src/simp.rs +++ b/minisat/src/simp.rs @@ -5,9 +5,7 @@ use core::ffi::{c_int, CStr}; -use super::{handle_oom, AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit}; use cpu_time::ProcessTime; -use ffi::MinisatHandle; use rustsat::{ solvers::{ FreezeVar, GetInternalStats, Interrupt, InterruptSolver, LimitConflicts, LimitPropagations, @@ -17,9 +15,11 @@ use rustsat::{ types::{Clause, Lit, TernaryVal, Var}, }; +use super::{ffi, handle_oom, AssumpEliminated, InternalSolverState, InvalidApiReturn, Limit}; + /// The Minisat solver type with preprocessing pub struct Minisat { - handle: *mut MinisatHandle, + handle: *mut ffi::CMinisatSimp, state: InternalSolverState, stats: SolverStats, } @@ -258,7 +258,7 @@ impl Interrupt for Minisat { /// An Interrupter for the Minisat Simp solver pub struct Interrupter { /// The C API handle - handle: *mut MinisatHandle, + handle: *mut ffi::CMinisatSimp, } unsafe impl Send for Interrupter {} @@ -407,41 +407,3 @@ mod test { assert_eq!(solver.max_var(), Some(var![9])); } } - -mod ffi { - use core::ffi::{c_char, c_int}; - - #[repr(C)] - 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; - pub fn cminisatsimp_init() -> *mut MinisatHandle; - pub fn cminisatsimp_release(solver: *mut MinisatHandle); - pub fn cminisatsimp_add(solver: *mut MinisatHandle, lit_or_zero: c_int) -> c_int; - pub fn cminisatsimp_assume(solver: *mut MinisatHandle, lit: c_int); - pub fn cminisatsimp_solve(solver: *mut MinisatHandle) -> c_int; - pub fn cminisatsimp_val(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisatsimp_failed(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisatsimp_phase(solver: *mut MinisatHandle, lit: c_int) -> c_int; - pub fn cminisatsimp_unphase(solver: *mut MinisatHandle, lit: c_int); - pub fn cminisatsimp_n_assigns(solver: *mut MinisatHandle) -> c_int; - pub fn cminisatsimp_n_clauses(solver: *mut MinisatHandle) -> c_int; - pub fn cminisatsimp_n_learnts(solver: *mut MinisatHandle) -> c_int; - pub fn cminisatsimp_n_vars(solver: *mut MinisatHandle) -> c_int; - pub fn cminisatsimp_set_conf_limit(solver: *mut MinisatHandle, limit: i64); - pub fn cminisatsimp_set_prop_limit(solver: *mut MinisatHandle, limit: i64); - pub fn cminisatsimp_set_no_limit(solver: *mut MinisatHandle); - pub fn cminisatsimp_interrupt(solver: *mut MinisatHandle); - pub fn cminisatsimp_set_frozen(solver: *mut MinisatHandle, var: c_int, frozen: bool); - pub fn cminisatsimp_is_frozen(solver: *mut MinisatHandle, var: c_int) -> c_int; - pub fn cminisatsimp_is_eliminated(solver: *mut MinisatHandle, var: c_int) -> c_int; - pub fn cminisatsimp_propagations(solver: *mut MinisatHandle) -> u64; - pub fn cminisatsimp_decisions(solver: *mut MinisatHandle) -> u64; - pub fn cminisatsimp_conflicts(solver: *mut MinisatHandle) -> u64; - } -}