Add initial CaDiCaL interface

.github/workflows/rust.yml

@@ -36,7 +36,9 @@ jobs:
   test:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
       - name: Install Rust toolchain
         run: |
           rustup toolchain install --profile minimal --no-self-update ${{ env.RUST_CHANNEL }}
@@ -48,7 +50,9 @@ jobs:
   clippy:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
       - name: Install Rust toolchain
         run: |
           rustup toolchain install --profile minimal --component clippy --no-self-update ${{ env.RUST_CHANNEL }}
@@ -60,7 +64,9 @@ jobs:
   format:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
       - name: Install Rust toolchain
         run: |
           rustup toolchain install --profile minimal --component rustfmt --no-self-update ${{ env.RUST_FMT_CHANNEL }}
@@ -70,7 +76,9 @@ jobs:
   semver:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
       - name: Check semver
         uses: obi1kenobi/cargo-semver-checks-action@v2
         with:

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "crates/pindakaas-cadical/vendor/cadical"]
+	path = crates/pindakaas-cadical/vendor/cadical
+	url = https://github.com/arminbiere/cadical.git

crates/pindakaas-build-macros/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "pindakaas-build-macros"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

crates/pindakaas-build-macros/src/lib.rs

@@ -0,0 +1,26 @@
+#[macro_export]
+macro_rules! ipasir_definitions {
+	() => {
+		extern "C" {
+			pub fn ipasir_signature() -> *const std::ffi::c_char;
+			pub fn ipasir_init() -> *mut std::ffi::c_void;
+			pub fn ipasir_release(slv: *mut std::ffi::c_void);
+			pub fn ipasir_add(slv: *mut std::ffi::c_void, lit: i32);
+			pub fn ipasir_assume(slv: *mut std::ffi::c_void, lit: i32);
+			pub fn ipasir_solve(slv: *mut std::ffi::c_void) -> std::ffi::c_int;
+			pub fn ipasir_val(slv: *mut std::ffi::c_void, lit: i32) -> i32;
+			pub fn ipasir_failed(slv: *mut std::ffi::c_void, lit: i32) -> std::ffi::c_int;
+			pub fn ipasir_set_terminate(
+				slv: *mut std::ffi::c_void,
+				data: *mut std::ffi::c_void,
+				cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void) -> std::ffi::c_int>,
+			);
+			pub fn ipasir_set_learn(
+				ptr: *mut std::ffi::c_void,
+				data: *mut std::ffi::c_void,
+				max_len: std::ffi::c_int,
+				cb: Option<unsafe extern "C" fn(*mut std::ffi::c_void, *const i32)>,
+			);
+		}
+	};
+}

crates/pindakaas-cadical/Cargo.toml

@@ -0,0 +1,16 @@
+[package]
+name = "pindakaas-cadical"
+version = "0.1.0"
+edition = "2021"
+build = "build.rs"
+links = "cadical"
+exclude = ["vendor/cadical"]
+include = ["vendor/cadical/src/*.cpp"]
+
+publish = false
+
+[build-dependencies]
+cc = { version = "1.0", features = ["parallel"] }
+
+[dependencies]
+pindakaas-build-macros = { path = "../pindakaas-build-macros" }

crates/pindakaas-cadical/build.rs

@@ -0,0 +1,96 @@
+fn main() {
+	let src = [
+		"vendor/cadical/src/analyze.cpp",
+		"vendor/cadical/src/arena.cpp",
+		"vendor/cadical/src/assume.cpp",
+		"vendor/cadical/src/averages.cpp",
+		"vendor/cadical/src/backtrack.cpp",
+		"vendor/cadical/src/backward.cpp",
+		"vendor/cadical/src/bins.cpp",
+		"vendor/cadical/src/block.cpp",
+		"vendor/cadical/src/cadical.cpp",
+		"vendor/cadical/src/ccadical.cpp",
+		"vendor/cadical/src/checker.cpp",
+		"vendor/cadical/src/clause.cpp",
+		"vendor/cadical/src/collect.cpp",
+		"vendor/cadical/src/compact.cpp",
+		"vendor/cadical/src/condition.cpp",
+		"vendor/cadical/src/config.cpp",
+		"vendor/cadical/src/constrain.cpp",
+		"vendor/cadical/src/contract.cpp",
+		"vendor/cadical/src/cover.cpp",
+		"vendor/cadical/src/cover.hpp",
+		"vendor/cadical/src/decide.cpp",
+		"vendor/cadical/src/decompose.cpp",
+		"vendor/cadical/src/deduplicate.cpp",
+		"vendor/cadical/src/elim.cpp",
+		"vendor/cadical/src/ema.cpp",
+		"vendor/cadical/src/extend.cpp",
+		"vendor/cadical/src/external.cpp",
+		"vendor/cadical/src/external_propagate.cpp",
+		"vendor/cadical/src/file.cpp",
+		"vendor/cadical/src/flags.cpp",
+		"vendor/cadical/src/flip.cpp",
+		"vendor/cadical/src/format.cpp",
+		"vendor/cadical/src/gates.cpp",
+		"vendor/cadical/src/instantiate.cpp",
+		"vendor/cadical/src/internal.cpp",
+		"vendor/cadical/src/ipasir.cpp",
+		"vendor/cadical/src/limit.cpp",
+		"vendor/cadical/src/logging.cpp",
+		"vendor/cadical/src/lookahead.cpp",
+		"vendor/cadical/src/lratbuilder.cpp",
+		"vendor/cadical/src/lratchecker.cpp",
+		"vendor/cadical/src/lucky.cpp",
+		"vendor/cadical/src/message.cpp",
+		"vendor/cadical/src/minimize.cpp",
+		"vendor/cadical/src/mobical.cpp",
+		"vendor/cadical/src/occs.cpp",
+		"vendor/cadical/src/options.cpp",
+		"vendor/cadical/src/parse.cpp",
+		"vendor/cadical/src/phases.cpp",
+		"vendor/cadical/src/probe.cpp",
+		"vendor/cadical/src/profile.cpp",
+		"vendor/cadical/src/proof.cpp",
+		"vendor/cadical/src/propagate.cpp",
+		"vendor/cadical/src/queue.cpp",
+		"vendor/cadical/src/random.cpp",
+		"vendor/cadical/src/reap.cpp",
+		"vendor/cadical/src/reduce.cpp",
+		"vendor/cadical/src/rephase.cpp",
+		"vendor/cadical/src/report.cpp",
+		"vendor/cadical/src/resources.cpp",
+		"vendor/cadical/src/restart.cpp",
+		"vendor/cadical/src/restore.cpp",
+		"vendor/cadical/src/score.cpp",
+		"vendor/cadical/src/shrink.cpp",
+		"vendor/cadical/src/signal.cpp",
+		"vendor/cadical/src/solution.cpp",
+		"vendor/cadical/src/solver.cpp",
+		"vendor/cadical/src/stats.cpp",
+		"vendor/cadical/src/subsume.cpp",
+		"vendor/cadical/src/terminal.cpp",
+		"vendor/cadical/src/ternary.cpp",
+		"vendor/cadical/src/tracer.cpp",
+		"vendor/cadical/src/transred.cpp",
+		"vendor/cadical/src/util.cpp",
+		"vendor/cadical/src/var.cpp",
+		"vendor/cadical/src/version.cpp",
+		"vendor/cadical/src/vivify.cpp",
+		"vendor/cadical/src/walk.cpp",
+		"vendor/cadical/src/watch.cpp",
+	];
+
+	let mut builder = cc::Build::new();
+	let build = builder
+		.cpp(true)
+		.flag_if_supported("-std=c++11")
+		.define("NBUILD", None)
+		.define("NUNLOCKED", None)
+		.define("NTRACING", None)
+		.define("QUIET", None);
+
+	build.files(src);
+
+	build.compile("cadical");
+}

crates/pindakaas-cadical/src/lib.rs

@@ -0,0 +1,24 @@
+use std::ffi::{c_char, c_int, c_void};
+
+use pindakaas_build_macros::ipasir_definitions;
+
+// Standard IPASIR definitions
+ipasir_definitions!();
+
+// Additional C-API functions in CaDiCaL
+extern "C" {
+	pub fn ccadical_constrain(slv: *mut c_void, lit: i32);
+	pub fn ccadical_constraint_failed(slv: *mut c_void) -> c_int;
+	pub fn ccadical_set_option(slv: *mut c_void, name: *const c_char, val: c_int);
+	pub fn ccadical_limit(slv: *mut c_void, name: *const c_char, limit: c_int);
+	pub fn ccadical_get_option(slv: *mut c_void, name: *const c_char) -> c_int;
+	pub fn ccadical_print_statistics(slv: *mut c_void);
+	pub fn ccadical_active(slv: *mut c_void) -> i64;
+	pub fn ccadical_irredundant(slv: *mut c_void) -> i64;
+	pub fn ccadical_fixed(slv: *mut c_void, lit: i32) -> c_int;
+	pub fn ccadical_terminate(slv: *mut c_void);
+	pub fn ccadical_freeze(slv: *mut c_void, lit: i32);
+	pub fn ccadical_frozen(slv: *mut c_void, lit: i32) -> c_int;
+	pub fn ccadical_melt(slv: *mut c_void, lit: i32);
+	pub fn ccadical_simplify(slv: *mut c_void) -> c_int;
+}

crates/pindakaas/Cargo.toml

@@ -15,20 +15,21 @@ cached = "0.46"
 iset = "0.2"
 itertools = "0.11"
 rustc-hash = "1.1"
+# Dynamically load solver libraries (through IPASIR interfaces)
+libloading = "0.8"
 
 # Optional encoding tracing capabilities
 tracing = { version = "0.1", optional = true }
 
-# Optional library to dynamically load solver libraries (through IPASIR interfaces)
-libloading = { version = "0.8", optional = true }
-
 # Optional Solver Interfaces
 splr = { version = "0.17", optional = true }
+pindakaas-cadical = { path = "../pindakaas-cadical", optional = true }
 
 [dev-dependencies]
 splr = { version = "0.17", features = ["incremental_solver"] }
 traced_test = { path = "../traced_test" }
 
 [features]
 trace = ["tracing"]
+cadical = ["pindakaas-cadical"]
 default = []

crates/pindakaas/src/helpers.rs

@@ -7,6 +7,7 @@ use crate::{
 	Encoder, LinExp, Lit, Result, Unsatisfiable, Valuation,
 };
 
+#[allow(unused_macros)]
 macro_rules! maybe_std_concat {
 	($e:literal) => {
 		concat!($e)
@@ -15,8 +16,10 @@ macro_rules! maybe_std_concat {
 		$e
 	};
 }
+#[allow(unused_imports)]
 pub(crate) use maybe_std_concat;
 
+#[allow(unused_macros)]
 macro_rules! concat_slices {
     ([$init:expr; $T:ty]: $($s:expr),+ $(,)?) => {{
         $(
@@ -44,9 +47,10 @@ macro_rules! concat_slices {
         $crate::helpers::concat_slices!([0; $T]: $($s),+)
     };
 }
+#[allow(unused_imports)]
 pub(crate) use concat_slices;
 
-#[doc(hidden)]
+#[allow(unused_macros)]
 macro_rules! const_concat {
 	() => { "" };
 
@@ -62,6 +66,7 @@ macro_rules! const_concat {
 			unsafe { std::str::from_utf8_unchecked(slice) }
 	}};
 }
+#[allow(unused_imports)]
 pub(crate) use const_concat;
 
 /// Given coefficients are powers of two multiplied by some value (1*c, 2*c, 4*c, 8*c, ..)

crates/pindakaas/src/lib.rs

@@ -21,13 +21,14 @@ use std::{
 };
 
 use itertools::{Itertools, Position};
+use solver::VarFactory;
 
 mod cardinality;
 mod cardinality_one;
 pub(crate) mod helpers;
 mod int;
 mod linear;
-mod solver;
+pub mod solver;
 mod sorted;
 pub mod trace;
 
@@ -39,11 +40,6 @@ pub use crate::{
 		AdderEncoder, BddEncoder, Comparator, LimitComp, LinExp, LinVariant, Linear,
 		LinearAggregator, LinearConstraint, LinearEncoder, SwcEncoder, TotalizerEncoder,
 	},
-	solver::{
-		libloading::{IpasirLibrary, IpasirSolver},
-		splr::SplrSolver,
-		Solver, VarFactory,
-	},
 	sorted::{SortedEncoder, SortedStrategy},
 };