Simple C API for embedding caqe

[rndmcnlly]

I'm interested in using QBF solvers in interactive applications. When I've needed SAT or 2QBF solving in an interactive setting before, it has been convenient that there was both a Python (for prototyping) and JavaScript (for public deployment on the web) interface to the clasp answer-set solver. Rather than suggesting that the caqe project maintain multiple systems of bindings for high-level languages and weird compilation targets, I have a simpler solution.

Add a single new file, caqe/src/bin/libcaqe.rs (or whatever) that exports a single C function with the following signature (and update Cargo.toml to build an associated dylib):

const char* run_caqe(const char* args, const char* input);

It might go something like this. I've only been using Rust for like 3 days, but this advice looks relevant.

use std::ffi::CStr;
use std::os::raw::c_char;

#[no_mangle]
pub extern fn run_caqe(args: *const c_char, input: *const c_char) *const c_char {
    // args is whatever you'd have found from main's argv entries, joined by spaces
    // input is whatever you'd have read from the input file
    // return value is pointer to whatever you would have written to stdout
    ... // caller assumes ownership of memory referred to by returned pointer
}

Goals:

• caqe can be run from inside a host process without spawning a new OS process
• filesystem is not touched during execution

Non-goals:

• incremental construction of problems
• structured data API (the embedding code can parse strings just as if it were reading interacting with the solver via stdio)
• be like the inverse of https://github.com/Storyyeller/cryptominisat-rs/blob/master/src/lib.rs (although that would be nice to have in the future)

How does this enable Python usage? Plain Python code can use the builtin ctypes library to dynamically link and call C functions from the native executable. The string-to-string API design here makes the glue code simple while implying some extra overhead for encoding/decoding to strings. Until we've got some example integrations, we don't know if trying to avoid this overhead is relevant. The point is that the language-specific glue code lives outside of the caqe project.

How does this enable JavaScript usage? By compiling Rust to WebAssembly, a browser-compatible library can be built with minimal changes to the codebase. Existing guidance for calling exported C functions will allow calling the one exported function above from plain JavaScript code. The fact that caqe internally uses C++-based CryptoMiniSat somewhat complicates the compile-to-WASM pipeline, but I think the relevant fixes only involve build scripts and not any Rust or C++ changes. Regardless, these build scripts and associated glue logic again live outside the caqe project.

People actually want a QBF solver in JavaScript??? Yes! The core mechanics of the browser-based game Proofdoku involves solving a 2-QBF problem during each main gameplay step. See the discussion of argument.lp in this paper. The game was made before WebAssembly emerged and the C++-to-JavaScript pipeline of the time didn't yield acceptable performance in mobile browsers. In 2021 (and now the solver maintainers provide pre-compiled WASM binaries), I'd happily have run the solver right inside of the browser in the same way I'd like to try using caqe. The problem instances that arise in interactive settings are usually very small, so making sure the solver can run on strange devices (phones, watches, refrigerators, etc.) and without the need to run a central solving service is usually more important than performance in this setting.

[ltentrup]

I like the idea of extending CAQE to a QBF solver library. There is a lot to unpack in this issue, so maybe it is a good idea to split it into smaller, more actionable items? I am not sure that this single function would suffice in your use case: don't you need the solver result, i.e., assignments? It is pretty easy to create Python bindings from Rust using https://crates.io/crates/pyo3. For WASM, I don't know because I have never tried it before.

[rndmcnlly]

Digging into it more, I agree; there's more to unpack. Some notes so far:

• I was following this example of creating a separate C ffi crate for an existing crate, but I ran into trouble with wanting access to private fields from caqe. Caqe's public Rust API doesn't expose enough to build the C API as a separate crate. One resolution is to expose more from caqe (low maintenance in the long term), the other is to have the C api code supported in the caqe project (fewest lines of code overall).

• Having a string output is a little messy. It's easy to return the integer solve result, but this isn't enough to access the assignment. If a pointer to a string result is returned, the API needs to make sure to expose a corresponding free function to make sure the right allocator frees the memory. If a buffer (and size value) is passed in, we'd need documentation for what should happen when the result doesn't fit.

I figure out the basics of a C API in https://github.com/rndmcnlly/caqe (takes a borrowed string as input; returns an integer; no rich output or configuration of solver).

I'll close the issue in a few days if I can't figure out something more satisfying overall.

[rndmcnlly]

Given that I only proposed the C API as a means to two unrelated ends, I'll close the issue now.

Final notes:

• Python: Python programs can already use the caqe command line tool via a subprocess and pipes. So, if there was going to be a more direct API, it should be a well designed one rather than something that duplicates the text data flowing over the pipes. I'll save proposing one until I've got a proposal with specific details motivated by what is awkward to do with pipes.
• JavaScript/browsers: Regardless of whether caqe had a C API, it looks like there might be some work needed to get caqe to compile with rust's WebAssembly wasm32 targets. The wasm32-wasi target would seem to allow the code to read/write files from a pre-specified virtual filesystem. This would mostly obviate the need for a C API because I think it would allow caqe to be run in the browser much like a command line tool. A few upstream crates (notably CryptoMiniSat) have build scripts that aren't yet compatible with this build target. It sure would be nice if there were a competitive pure-Rust SAT solver to replace CMS inside of caqe. This solver is less mature, but it looks promising: https://crates.io/crates/varisat