Add integer-based interface supporting SCM work

.gitattributes

@@ -0,0 +1 @@
+crates/pindakaas/src/int/res/scm_db.rs -diff

.gitignore

@@ -1,2 +1,7 @@
 /target
 Cargo.lock
+crates/pindakaas/res/scm
+!crates/pindakaas/res/scm.tar.gz
+crates/pindakaas/src/int/scm_db.rs
+crates/pindakaas/tmp
+

crates/pindakaas-cadical/build.rs

@@ -1,4 +1,6 @@
 fn main() {
+	// TODO [?] something like this needs to be added to all build.rs files? Even better, pinpointing the specific files which could change?
+	println!("cargo:rerun-if-changed=vendor");
 	let src = [
 		"vendor/cadical/src/analyze.cpp",
 		"vendor/cadical/src/arena.cpp",

crates/pindakaas/Cargo.toml

@@ -12,8 +12,10 @@ edition = "2021"
 
 [dependencies]
 cached = "0.46"
-iset = "0.2"
+bzip2 = "0.4"
+flate2 = "1.0"
 itertools = "0.12.0"
+rand = "0.8.5"
 rustc-hash = "1.1"
 # Dynamically load solver libraries (through IPASIR interfaces)
 libloading = "0.8"
@@ -27,6 +29,13 @@ pindakaas-derive = { path = "../pindakaas-derive", optional = true }
 pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true }
 pindakaas-kissat = { path = "../pindakaas-kissat", optional = true }
 splr = { version = "0.17", optional = true }
+iset = "0.2.2"
+# assert_ok = "1.0.2"
+
+[build-dependencies]
+itertools = "0.11"
+tar = "0.4"
+flate2 = "1.0"
 
 [dev-dependencies]
 splr = { version = "0.17", features = ["incremental_solver"] }
@@ -37,7 +46,6 @@ cadical = ["pindakaas-cadical", "pindakaas-derive"]
 intel-sat = ["pindakaas-intel-sat", "pindakaas-derive"]
 kissat = ["pindakaas-kissat", "pindakaas-derive"]
 trace = ["tracing"]
-default = ["cadical"]
 ipasir-up = ["cadical"]
 
 [lints]

crates/pindakaas/build.rs

@@ -0,0 +1,107 @@
+use std::{fs, path::Path};
+
+use flate2::read::GzDecoder;
+use itertools::Itertools;
+use tar::Archive;
+
+// TODO [!] once recipes added, to be moved from build.rs to a rust script type thing: scm_db_res.rs
+fn scm() -> Result<Vec<(usize, u32, Vec<ScmNode>)>, std::io::Error> {
+	if Path::new("./res/scm").exists() {
+		fs::remove_dir_all("./res/scm")?;
+		fs::create_dir("./res/scm")?;
+	} else {
+		fs::create_dir("./res/scm")?;
+	}
+
+	let db = Path::new("./res/scm.tar.gz");
+	assert!(db.exists());
+
+	Archive::new(GzDecoder::new(fs::File::open(db)?))
+		.unpack("./res/")
+		.unwrap();
+
+	Ok(fs::read_dir("./res/scm")?
+		.map(|f| {
+			let path = f.unwrap().path();
+			let scm = fs::read_to_string(&path)
+				.unwrap()
+				.lines()
+				.filter(|line| !(line.is_empty() || line.starts_with('#')))
+				.map(|line| match line.split(',').collect::<Vec<_>>()[..] {
+					[i, i1, sh1, add, i2, sh2] => ScmNode {
+						i: i.parse().unwrap(),
+						i1: i1.parse().unwrap(),
+						sh1: sh1.parse().unwrap(),
+						add: match add {
+							"+" => true,
+							"-" => false,
+							_ => unreachable!(),
+						},
+						i2: i2.parse().unwrap(),
+						sh2: sh2.parse().unwrap(),
+					},
+					_ => panic!("Unexpected line {line}"),
+				})
+				.collect();
+			let (bits, v) = path
+				.file_stem()
+				.unwrap()
+				.to_str()
+				.unwrap()
+				.split('_')
+				.collect::<Vec<_>>()
+				.into_iter()
+				.collect_tuple()
+				.unwrap();
+			(bits.parse().unwrap(), v.parse().unwrap(), scm)
+		})
+		.sorted_by_key(|(b, c, _)| (*b, *c))
+		.collect())
+}
+
+#[allow(dead_code)]
+#[derive(Debug)]
+pub(crate) struct ScmNode {
+	i: u32,
+	i1: u32,
+	sh1: u32,
+	add: bool,
+	i2: u32,
+	sh2: u32,
+}
+
+pub fn main() {
+	println!("cargo:rerun-if-changed=res/scm.tar.gz");
+	println!("cargo:rerun-if-changed=res/ecm.tar.gz");
+	println!("cargo:rerun-if-changed=build.rs");
+
+	let scm = scm().unwrap();
+
+	let scm_node_def = r"use crate::Coeff;
+#[derive(Debug, Clone)]
+pub(crate) struct ScmNode {
+pub(crate) i: usize,
+pub(crate) i1: usize,
+pub(crate) sh1: u32,
+pub(crate) add: bool,
+pub(crate) i2: usize,
+pub(crate) sh2: u32,
+}";
+	// TODO make HashMap (but this is not easy using static/const)
+	let o = format!(
+		"{scm_node_def}
+        pub(crate) static SCM: [(u32, Coeff, &[ScmNode]); {}] = [\n{}\n];",
+		scm.len(),
+		scm.iter()
+			.map(|(x, c, scm)| format!("\t({}, {}, &{:?})", x, c, scm))
+			.join(",\n")
+	);
+	fs::write("./src/int/res/scm_db.rs", o).unwrap();
+
+	let db = Path::new("./res/ecm.tar.gz");
+	assert!(db.exists());
+
+	Archive::new(GzDecoder::new(fs::File::open(db).unwrap()))
+		.unpack("./res/")
+		.unwrap();
+}

crates/pindakaas/src/cardinality.rs

@@ -3,9 +3,6 @@ use crate::{
 	CardinalityOne, CheckError, Checker, ClauseDatabase, Encoder, Lit, Valuation,
 };
 
-mod sorting_network;
-pub use sorting_network::SortingNetworkEncoder;
-
 #[derive(Clone, Debug)]
 pub struct Cardinality {
 	pub(crate) lits: Vec<Lit>,
@@ -56,7 +53,6 @@ impl<DB: ClauseDatabase, Enc: Encoder<DB, Cardinality> + CardMarker> Encoder<DB,
 // local marker trait, to ensure the previous definition only applies within this crate
 pub(crate) trait CardMarker {}
 impl<T: LinMarker> CardMarker for T {}
-impl CardMarker for SortingNetworkEncoder {}
 
 #[cfg(test)]
 pub(crate) mod tests {