Resolve issues when linking two IPASIR libraries

crates/pindakaas-build-macros/Cargo.toml

@@ -4,3 +4,5 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
+cc = "1.0"
+paste = "1.0"

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

@@ -1,26 +1,87 @@
-#[macro_export]
+use cc::Build;
+pub use paste::paste;
+
+#[macro_export(local_inner_macros)]
 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(
+	($prefix:ident) => {
+		paste! {
+			extern "C" {
+				pub fn [<$prefix _signature>]() -> *const std::ffi::c_char;
+				pub fn [<$prefix _init>]() -> *mut std::ffi::c_void;
+				pub fn [<$prefix _release>](slv: *mut std::ffi::c_void);
+				pub fn [<$prefix _add>](slv: *mut std::ffi::c_void, lit: i32);
+				pub fn [<$prefix _assume>](slv: *mut std::ffi::c_void, lit: i32);
+				pub fn [<$prefix _solve>](slv: *mut std::ffi::c_void) -> std::ffi::c_int;
+				pub fn [<$prefix _val>](slv: *mut std::ffi::c_void, lit: i32) -> i32;
+				pub fn [<$prefix _failed>](slv: *mut std::ffi::c_void, lit: i32) -> std::ffi::c_int;
+				pub fn [<$prefix _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 [<$prefix _set_learn>](
+					slv: *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)>,
+				);
+			}
+			pub unsafe fn ipasir_signature() -> *const std::ffi::c_char {
+				[<$prefix _signature>]()
+			}
+			pub unsafe fn ipasir_init() -> *mut std::ffi::c_void {
+				[<$prefix _init>]()
+			}
+			pub unsafe fn ipasir_release(slv: *mut std::ffi::c_void) {
+				[<$prefix _release>](slv)
+			}
+			pub unsafe fn ipasir_add(slv: *mut std::ffi::c_void, lit: i32) {
+				[<$prefix _add>](slv, lit)
+			}
+			pub unsafe fn ipasir_assume(slv: *mut std::ffi::c_void, lit: i32) {
+				[<$prefix _assume>](slv, lit)
+			}
+			pub unsafe fn ipasir_solve(slv: *mut std::ffi::c_void) -> std::ffi::c_int {
+				[<$prefix _solve>](slv)
+			}
+			pub unsafe fn ipasir_val(slv: *mut std::ffi::c_void, lit: i32) -> i32 {
+				[<$prefix _val>](slv, lit)
+			}
+			pub unsafe fn ipasir_failed(slv: *mut std::ffi::c_void, lit: i32) -> std::ffi::c_int {
+				[<$prefix _failed>](slv, lit)
+			}
+			pub unsafe 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,
+			) {
+				[<$prefix _set_terminate>](slv, data, cb)
+			}
+			pub unsafe fn ipasir_set_learn(
+				slv: *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)>,
-			);
+			){
+				[<$prefix _set_learn>](slv, data, max_len, cb)
+			}
 		}
 	};
 }
+
+pub fn change_ipasir_prefix(build: &mut Build, prefix: &str) {
+	build
+		.define("ipasir_signature", format!("{prefix}_signature").as_ref())
+		.define("ipasir_init", format!("{prefix}_init").as_ref())
+		.define("ipasir_release", format!("{prefix}_release").as_ref())
+		.define("ipasir_add", format!("{prefix}_add").as_ref())
+		.define("ipasir_assume", format!("{prefix}_assume").as_ref())
+		.define("ipasir_solve", format!("{prefix}_solve").as_ref())
+		.define("ipasir_val", format!("{prefix}_val").as_ref())
+		.define("ipasir_failed", format!("{prefix}_failed").as_ref())
+		.define(
+			"ipasir_set_terminate",
+			format!("{prefix}_set_terminate").as_ref(),
+		)
+		.define("ipasir_set_learn", format!("{prefix}_set_learn").as_ref());
+}

crates/pindakaas-cadical/build.rs

@@ -33,7 +33,6 @@ fn main() {
 		"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",
@@ -87,6 +86,11 @@ fn main() {
 		.define("NTRACING", None)
 		.define("QUIET", None);
 
+	assert_eq!(
+		env!("CARGO_PKG_VERSION"),
+		include_str!("vendor/cadical/VERSION").trim()
+	);
+
 	build.files(src);
 
 	build.compile("cadical");

crates/pindakaas-cadical/src/lib.rs

@@ -3,7 +3,7 @@ use std::ffi::{c_char, c_int, c_void};
 use pindakaas_build_macros::ipasir_definitions;
 
 // Standard IPASIR definitions
-ipasir_definitions!();
+ipasir_definitions!(ccadical);
 
 // Additional C-API functions in CaDiCaL
 extern "C" {

crates/pindakaas-intel-sat/Cargo.toml

@@ -8,6 +8,7 @@ exclude = ["vendor/intel_sat"]
 include = ["vendor/intel_sat/*.cc"]
 
 [build-dependencies]
+pindakaas-build-macros = { path = "../pindakaas-build-macros" }
 cc = { version = "1.0", features = ["parallel"] }
 
 [dependencies]

crates/pindakaas-intel-sat/build.rs

@@ -1,3 +1,5 @@
+use pindakaas_build_macros::change_ipasir_prefix;
+
 fn main() {
 	let src = [
 		"vendor/intel_sat/Topi.cc",
@@ -17,8 +19,7 @@ fn main() {
 
 	let mut builder = cc::Build::new();
 	let build = builder.cpp(true).flag_if_supported("-std=c++20");
+	change_ipasir_prefix(build, "intel_sat");
 
-	build.files(src);
-
-	build.compile("intel_sat");
+	build.files(src).compile("intel_sat");
 }

crates/pindakaas-intel-sat/src/lib.rs

@@ -1,3 +1,3 @@
 use pindakaas_build_macros::ipasir_definitions;
 
-ipasir_definitions!();
+ipasir_definitions!(intel_sat);

crates/pindakaas/src/solver.rs

@@ -181,13 +181,14 @@ macro_rules! ipasir_solver {
 					10 => {
 						// 10 -> Sat
 						let val_fn = |lit: crate::Lit| {
-							let lit: i32 = lit.into();
-							let val = unsafe { $loc::ipasir_val(self.ptr, lit) };
-							match val {
-								_ if val == lit => Some(true),
-								_ if val == -lit => Some(false),
+							let var: i32 = lit.var().into();
+							// WARN: Always ask about variable (positive) literal, otherwise solvers sometimes seem incorrect
+							let ret = unsafe { $loc::ipasir_val(self.ptr, var) };
+							match ret {
+								_ if ret == var => Some(!lit.is_negated()),
+								_ if ret == -var => Some(lit.is_negated()),
 								_ => {
-									debug_assert_eq!(val, 0); // zero according to spec, both value are valid
+									debug_assert_eq!(ret, 0); // zero according to spec, both value are valid
 									None
 								}
 							}

crates/pindakaas/src/solver/cadical.rs

@@ -17,6 +17,8 @@ mod tests {
 	#[test]
 	fn test_cadical() {
 		let mut slv = Cadical::default();
+		assert!(slv.signature().starts_with("cadical"));
+
 		let a = slv.new_var();
 		let b = slv.new_var();
 		PairwiseEncoder::default()

crates/pindakaas/src/solver/intel_sat.rs

@@ -17,6 +17,7 @@ mod tests {
 	#[test]
 	fn test_intel_sat() {
 		let mut slv = IntelSat::default();
+		assert!(slv.signature().starts_with("IntelSat"));
 		let a = slv.new_var();
 		let b = slv.new_var();
 		PairwiseEncoder::default()