refactor: factor out C-API

factor out C-API into separate crate and tooling around that

.github/workflows/capi.yml

@@ -0,0 +1,54 @@
+name: C-API
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build-test:
+    name: Build and test
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest, windows-latest]
+    runs-on: ${{ matrix.os }}
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+      - name: Install stable toolchain
+        uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+        with:
+          shared-key: "build-test"
+      - name: Cargo build
+        run: cargo build -p rustsat-capi --verbose
+        env:
+          CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
+      - name: Cargo test
+        run: cargo test -p rustsat --verbose --features=all
+        env:
+          CMAKE_BUILD_PARALLEL_LEVEL: ${{ fromJSON('["", "4"]')[matrix.os == 'macos-latest'] }}
+
+  version:
+    name: Ensure C-API crate version is in sync
+    runs-on: ubuntu-latest
+    steps:
+      - name: Check
+        run: [ "$(grep '^version = ' rustsat/Cargo.toml)" = "$(grep '^version = ' capi/Cargo.toml)" ]
+
+  cbindgen:
+    name: Test generated C header
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+      - name: Install stable toolchain
+        uses: dtolnay/rust-toolchain@stable
+      - name: Check C header
+        run: |
+          cargo install cbindgen
+          cbindgen -c capi/cbindgen.toml --crate rustsat-capi -o capi/rustsat.h --verify

.github/workflows/rustsat.yml

@@ -48,16 +48,3 @@ jobs:
         run: maturin build -m rustsat/Cargo.toml && pip install --no-index --find-links target/wheels/ rustsat
       - name: Test stubs
         run: stubtest --mypy-config-file rustsat/pyproject.toml --allowlist rustsat/stubtest-allowlist.txt rustsat
-
-  cbindgen:
-    name: Test generated C header
-    runs-on: ubuntu-latest
-    steps:
-      - name: Checkout sources
-        uses: actions/checkout@v4
-      - name: Install stable toolchain
-        uses: dtolnay/rust-toolchain@stable
-      - name: Check C header
-        run: |
-          cargo install cbindgen
-          cbindgen -c rustsat/cbindgen.toml --crate rustsat -o rustsat/rustsat.h --verify

Cargo.toml

@@ -8,6 +8,7 @@ members = [
   "minisat",
   "ipasir",
   "solvertests",
+  "capi",
 ]
 resolver = "2"
 

README.md

@@ -69,9 +69,6 @@ crate](https://crates.io/crates/rustsat_tools) at `tools/src/bin`. For a bigger
 example you can look at this [multi-objective optimization
 solver](https://github.com/chrjabs/scuttle).
 
-For an example of how to use the C-API, see `rustsat/examples/capi*.cpp`.
-Similarly, for an example of using the Python API, see `rustsat/examples/pyapi*.py`.
-
 <!-- cargo-rdme end -->
 
 ## Python Bindings

capi/Cargo.toml

@@ -0,0 +1,26 @@
+[package]
+name = "rustsat-capi"
+version = "0.4.3"
+edition = "2021"
+authors = ["Christoph Jabs <christoph.jabs@helsinki.fi>"]
+license = "MIT"
+description = "C-API for the RustSAT library"
+keywords = ["sat", "satisfiability", "encodings"]
+
+build = "build.rs"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+rustsat = { version = "0.4.3", path = "../rustsat", default-features = false, features = [
+  "internals",
+] }
+
+[build-dependencies]
+cbindgen = "0.26.0"
+
+[dev-dependencies]
+inline-c = "0.1.7"
+
+[lib]
+crate-type = ["staticlib"]

capi/README.md

@@ -0,0 +1,17 @@
+[![Build & Test](https://github.com/chrjabs/rustsat/actions/workflows/capi.yml/badge.svg)](https://github.com/chrjabs/rustsat/actions/workflows/capi.yml)
+[![License](https://img.shields.io/crates/l/rustsat)](./LICENSE)
+
+<!-- cargo-rdme start -->
+
+# C-API For RustSAT
+
+In the C-API, literals are represented as IPASIR literals.
+
+This is the C-API for RustSAT. Currently this API is very minimal and not
+the focus of this project. For now, only the API of certain encodings is
+available.
+
+For the API itself, see `rustsat.h`. To use RustSAT from an external project,
+build this crate and link against `librustsat.a`
+
+<!-- cargo-rdme end -->

rustsat/build.rs → capi/build.rs

@@ -8,20 +8,6 @@ fn main() {
         return;
     }
 
-    #[cfg(feature = "ipasir")]
-    {
-        // Link to custom IPASIR solver
-        // Uncomment and modify this for linking to your static library
-        // The name of the library should be _without_ the prefix 'lib' and the suffix '.a'
-        //println!("cargo:rustc-link-lib=static=<path-to-your-static-lib>");
-        //println!("cargo:rustc-link-search=<name-of-your-static-lib>");
-        // If your IPASIR solver links to the C++ stdlib, uncomment the next four lines
-        //#[cfg(target_os = "macos")]
-        //println!("cargo:rustc-flags=-l dylib=c++");
-        //#[cfg(not(target_os = "macos"))]
-        //println!("cargo:rustc-flags=-l dylib=stdc++");
-    }
-
     let crate_dir = env::var("CARGO_MANIFEST_DIR").unwrap();
 
     // Generate C-API header
@@ -44,21 +30,17 @@ fn main() {
     #[cfg(feature = "pyapi")]
     let python_lib = pyo3_build_config::get().lib_name.as_ref().unwrap();
 
-    let cflags = format!("cargo:rustc-env=INLINE_C_RS_CFLAGS=-I{I} -L{L} -lrustsat -D_DEBUG -D_CRT_SECURE_NO_WARNINGS", I=include_dir, L=ld_dir.to_string_lossy());
+    let cflags = format!("cargo:rustc-env=INLINE_C_RS_CFLAGS=-I{I} -L{L} -lrustsat_capi -D_DEBUG -D_CRT_SECURE_NO_WARNINGS", I=include_dir, L=ld_dir.to_string_lossy());
     #[cfg(feature = "compression")]
     let cflags = format!("{} -llzma -lbz2", cflags);
-    #[cfg(feature = "pyapi")]
-    let cflags = format!("{} -l{}", cflags, python_lib);
     println!("{}", cflags);
 
     let ldflags = format!(
-        "cargo:rustc-env=INLINE_C_RS_LDFLAGS={L}/librustsat.a",
+        "cargo:rustc-env=INLINE_C_RS_LDFLAGS={L}/librustsat_capi.a",
         L = ld_dir.to_string_lossy()
     );
     #[cfg(feature = "compression")]
     let ldflags = format!("{} -llzma -lbz2", ldflags);
-    #[cfg(feature = "pyapi")]
-    let ldflags = format!("{} -l{}", ldflags, python_lib);
     println!("{}", ldflags);
 }
 

rustsat/cbindgen.toml → capi/cbindgen.toml

@@ -5,19 +5,17 @@
 # for detailed documentation of every option here.
 
 
-
 language = "C"
 
 
-
 ############## Options for Wrapping the Contents of the Header #################
 
 # header = "/* Text to put at the beginning of the generated file. Probably a license. */"
 # trailer = "/* Text to put at the end of the generated file */"
 include_guard = "rustsat_h"
 # pragma_once = true
 # autogen_warning = "/* Warning, this file is autogenerated by cbindgen. Don't modify this manually. */"
-include_version = true
+include_version = false
 namespace = "RustSAT"
 namespaces = []
 using_namespaces = []
@@ -27,8 +25,6 @@ no_includes = false
 after_includes = ""
 
 
-
-
 ############################ Code Style Options ################################
 
 braces = "SameLine"
@@ -37,39 +33,33 @@ tab_width = 2
 documentation = true
 documentation_style = "auto"
 documentation_length = "full"
-line_endings = "LF" # also "CR", "CRLF", "Native"
-
-
+line_endings = "LF"           # also "CR", "CRLF", "Native"
 
 
 ############################# Codegen Options ##################################
 
 style = "both"
-sort_by = "Name" # default for `fn.sort_by` and `const.sort_by`
+sort_by = "Name"       # default for `fn.sort_by` and `const.sort_by`
 usize_is_size_t = true
 cpp_compat = true
 
 
-
 [defines]
 # "target_os = freebsd" = "DEFINE_FREEBSD"
 # "feature = serde" = "DEFINE_SERDE"
 
 
-
 [export]
-include = []
+include = ["DbTotalizer", "DynamicPolyWatchdog"]
 exclude = []
 # prefix = "CAPI_"
 item_types = []
 renaming_overrides_prefixing = false
 
 
-
 [export.rename]
 
 
-
 [export.body]
 
 
@@ -88,8 +78,6 @@ args = "auto"
 sort_by = "Name"
 
 
-
-
 [struct]
 rename_fields = "None"
 # must_use = "MUST_USE_STRUCT"
@@ -104,8 +92,6 @@ derive_gt = false
 derive_gte = false
 
 
-
-
 [enum]
 rename_variants = "None"
 # must_use = "MUST_USE_ENUM"
@@ -123,35 +109,26 @@ enum_class = true
 private_default_tagged_enum_constructor = false
 
 
-
-
 [const]
 allow_static_const = true
 allow_constexpr = false
 sort_by = "Name"
 
 
-
-
 [macro_expansion]
 bitflags = false
 
 
-
-
-
-
 ############## Options for How Your Rust library Should Be Parsed ##############
 
 [parse]
-parse_deps = false
-# include = []
+parse_deps = true
+include = ["rustsat"]
 exclude = []
 clean = false
 extra_bindings = []
 
 
-
 [parse.expand]
 crates = []
 all_features = false

rustsat/rustsat.h → capi/rustsat.h

@@ -1,8 +1,6 @@
 #ifndef rustsat_h
 #define rustsat_h
 
-/* Generated with cbindgen:0.26.0 */
-
 #include <stdarg.h>
 #include <stdbool.h>
 #include <stddef.h>

rustsat/src/capi.rs → capi/src/lib.rs

@@ -2,16 +2,18 @@
 //!
 //! In the C-API, literals are represented as IPASIR literals.
 //!
-//! This is the C-API for RustSAT. Currently this API is very minimal and not
-//! the focus of this project. For now, only the API of certain encodings is
-//! available.
+//! This is the C-API for RustSAT. Currently this API is very minimal and not the focus of this
+//! project. For now, only the API of certain encodings is available.
+//!
+//! For the API itself, see `rustsat.h`. To use RustSAT from an external project, build this crate
+//! and link against `librustsat.a` (produced by `cargo` in `target/release`).
 
 pub mod encodings {
     //! # C-API For Encodings
 
     use std::ffi::{c_int, c_void};
 
-    use crate::{
+    use rustsat::{
         encodings::{self, CollectClauses},
         instances::ManageVars,
         types::{Clause, Var},
@@ -129,7 +131,7 @@ pub mod encodings {
 
         use std::ffi::{c_int, c_void};
 
-        use crate::{
+        use rustsat::{
             encodings::card::{BoundUpper, BoundUpperIncremental, DbTotalizer},
             types::Lit,
         };
@@ -286,7 +288,7 @@ pub mod encodings {
 
         use std::ffi::{c_int, c_void};
 
-        use crate::{
+        use rustsat::{
             encodings::pb::{BoundUpper, BoundUpperIncremental, DynamicPolyWatchdog},
             types::Lit,
         };
@@ -314,16 +316,16 @@ pub mod encodings {
             weight: usize,
         ) -> MaybeError {
             let mut boxed = unsafe { Box::from_raw(dpw) };
-            if boxed.structure.is_some() {
-                return MaybeError::InvalidState;
-            }
-            boxed.in_lits.insert(
+            let res = boxed.add_input(
                 Lit::from_ipasir(lit).expect("invalid IPASIR literal"),
                 weight,
             );
-            boxed.weight_sum += weight;
             Box::into_raw(boxed);
-            MaybeError::Ok
+            if res.is_ok() {
+                MaybeError::Ok
+            } else {
+                MaybeError::InvalidState
+            }
         }
 
         /// Lazily builds the _change in_ pseudo-boolean encoding to enable

release-plz.toml

@@ -35,3 +35,8 @@ git_release_enable = false
 name = "rustsat-solvertests"
 release = false
 git_release_enable = false
+
+[[package]]
+name = "rustsat-capi"
+release = false
+git_release_enable = false