Add initial Intel SAT interface

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "crates/pindakaas-cadical/vendor/cadical"]
 	path = crates/pindakaas-cadical/vendor/cadical
 	url = https://github.com/arminbiere/cadical.git
+[submodule "crates/pindakaas-intel-sat/vendor/intel_sat"]
+	path = crates/pindakaas-intel-sat/vendor/intel_sat
+	url = https://github.com/alexander-nadel/intel_sat_solver.git

crates/pindakaas-cadical/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "pindakaas-cadical"
-version = "0.1.0"
+version = "1.8.0"
 edition = "2021"
 build = "build.rs"
 links = "cadical"

crates/pindakaas-intel-sat/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "pindakaas-intel-sat"
+version = "0.1.0"
+edition = "2021"
+build = "build.rs"
+links = "intel_sat"
+exclude = ["vendor/intel_sat"]
+include = ["vendor/intel_sat/*.cc"]
+
+[build-dependencies]
+cc = { version = "1.0", features = ["parallel"] }
+
+[dependencies]
+pindakaas-build-macros = { path = "../pindakaas-build-macros" }

crates/pindakaas-intel-sat/build.rs

@@ -0,0 +1,24 @@
+fn main() {
+	let src = [
+		"vendor/intel_sat/Topi.cc",
+		"vendor/intel_sat/TopiAsg.cc",
+		"vendor/intel_sat/TopiBacktrack.cc",
+		"vendor/intel_sat/TopiBcp.cc",
+		"vendor/intel_sat/TopiBitCompression.cc",
+		"vendor/intel_sat/TopiCompression.cc",
+		"vendor/intel_sat/TopiConflictAnalysis.cc",
+		"vendor/intel_sat/TopiDebugPrinting.cc",
+		"vendor/intel_sat/TopiDecision.cc",
+		"vendor/intel_sat/TopiRestart.cc",
+		"vendor/intel_sat/TopiWL.cc",
+		"vendor/intel_sat/Topor.cc",
+		"vendor/intel_sat/ToporIpasir.cc",
+	];
+
+	let mut builder = cc::Build::new();
+	let build = builder.cpp(true).flag_if_supported("-std=c++20");
+
+	build.files(src);
+
+	build.compile("intel_sat");
+}

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

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

crates/pindakaas/Cargo.toml

@@ -22,8 +22,9 @@ libloading = "0.8"
 tracing = { version = "0.1", optional = true }
 
 # Optional Solver Interfaces
-splr = { version = "0.17", optional = true }
 pindakaas-cadical = { path = "../pindakaas-cadical", optional = true }
+pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true }
+splr = { version = "0.17", optional = true }
 
 [dev-dependencies]
 splr = { version = "0.17", features = ["incremental_solver"] }
@@ -32,4 +33,5 @@ traced_test = { path = "../traced_test" }
 [features]
 trace = ["tracing"]
 cadical = ["pindakaas-cadical"]
+intel-sat = ["pindakaas-intel-sat"]
 default = []

crates/pindakaas/src/solver.rs

@@ -4,11 +4,12 @@ use crate::{ClauseDatabase, Lit, Valuation, Var};
 
 pub mod libloading;
 
-#[cfg(feature = "splr")]
-pub mod splr;
-
 #[cfg(feature = "cadical")]
 pub mod cadical;
+#[cfg(feature = "intel-sat")]
+pub mod intel_sat;
+#[cfg(feature = "splr")]
+pub mod splr;
 
 pub trait Solver: ClauseDatabase {
 	/// Return the name and the version of SAT solving library.

crates/pindakaas/src/solver/cadical.rs

@@ -1,3 +1,42 @@
 use super::ipasir_solver;
 
 ipasir_solver!(pindakaas_cadical, Cadical);
+
+#[cfg(test)]
+mod tests {
+	#[cfg(feature = "trace")]
+	use traced_test::test;
+
+	use super::*;
+	use crate::{
+		linear::LimitComp,
+		solver::{SolveResult, Solver},
+		CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder,
+	};
+
+	#[test]
+	fn test_cadical() {
+		let mut slv = Cadical::default();
+		let a = slv.new_var();
+		let b = slv.new_var();
+		PairwiseEncoder::default()
+			.encode(
+				&mut slv,
+				&CardinalityOne {
+					lits: vec![a, b],
+					cmp: LimitComp::Equal,
+				},
+			)
+			.unwrap();
+		let res = slv.solve(
+			|value| {
+				assert!(
+					(value(!a).unwrap() && value(b).unwrap())
+						|| (value(a).unwrap() && value(!b).unwrap()),
+				)
+			},
+			|_| {},
+		);
+		assert_eq!(res, SolveResult::Sat);
+	}
+}

crates/pindakaas/src/solver/intel_sat.rs

@@ -0,0 +1,42 @@
+use super::ipasir_solver;
+
+ipasir_solver!(pindakaas_intel_sat, IntelSat);
+
+#[cfg(test)]
+mod tests {
+	#[cfg(feature = "trace")]
+	use traced_test::test;
+
+	use super::*;
+	use crate::{
+		linear::LimitComp,
+		solver::{SolveResult, Solver},
+		CardinalityOne, ClauseDatabase, Encoder, PairwiseEncoder,
+	};
+
+	#[test]
+	fn test_intel_sat() {
+		let mut slv = IntelSat::default();
+		let a = slv.new_var();
+		let b = slv.new_var();
+		PairwiseEncoder::default()
+			.encode(
+				&mut slv,
+				&CardinalityOne {
+					lits: vec![a, b],
+					cmp: LimitComp::Equal,
+				},
+			)
+			.unwrap();
+		let res = slv.solve(
+			|value| {
+				assert!(
+					(value(!a).unwrap() && value(b).unwrap())
+						|| (value(a).unwrap() && value(!b).unwrap()),
+				)
+			},
+			|_| {},
+		);
+		assert_eq!(res, SolveResult::Sat);
+	}
+}