Add initial Kissat interface

.gitmodules

@@ -4,3 +4,6 @@
 [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
+[submodule "crates/pindakaas-kissat/vendor/kissat"]
+	path = crates/pindakaas-kissat/vendor/kissat
+	url = https://github.com/arminbiere/kissat.git

crates/pindakaas-kissat/Cargo.toml

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

crates/pindakaas-kissat/build.rs

@@ -0,0 +1,148 @@
+use std::process::Command;
+
+fn main() {
+	let src = [
+		"vendor/kissat/src/allocate.c",
+		"vendor/kissat/src/analyze.c",
+		"vendor/kissat/src/ands.c",
+		"vendor/kissat/src/application.c",
+		"vendor/kissat/src/arena.c",
+		"vendor/kissat/src/assign.c",
+		"vendor/kissat/src/averages.c",
+		"vendor/kissat/src/backbone.c",
+		"vendor/kissat/src/backtrack.c",
+		"vendor/kissat/src/build.c",
+		"vendor/kissat/src/bump.c",
+		"vendor/kissat/src/check.c",
+		"vendor/kissat/src/clause.c",
+		"vendor/kissat/src/collect.c",
+		"vendor/kissat/src/colors.c",
+		"vendor/kissat/src/compact.c",
+		"vendor/kissat/src/config.c",
+		"vendor/kissat/src/decide.c",
+		"vendor/kissat/src/deduce.c",
+		"vendor/kissat/src/definition.c",
+		"vendor/kissat/src/dense.c",
+		"vendor/kissat/src/dump.c",
+		"vendor/kissat/src/eliminate.c",
+		"vendor/kissat/src/equivalences.c",
+		"vendor/kissat/src/error.c",
+		"vendor/kissat/src/extend.c",
+		"vendor/kissat/src/file.c",
+		"vendor/kissat/src/flags.c",
+		"vendor/kissat/src/format.c",
+		"vendor/kissat/src/forward.c",
+		"vendor/kissat/src/gates.c",
+		"vendor/kissat/src/handle.c",
+		"vendor/kissat/src/heap.c",
+		"vendor/kissat/src/ifthenelse.c",
+		"vendor/kissat/src/import.c",
+		"vendor/kissat/src/internal.c",
+		"vendor/kissat/src/kimits.c",
+		"vendor/kissat/src/kitten.c",
+		"vendor/kissat/src/learn.c",
+		"vendor/kissat/src/logging.c",
+		"vendor/kissat/src/minimize.c",
+		"vendor/kissat/src/mode.c",
+		"vendor/kissat/src/options.c",
+		"vendor/kissat/src/parse.c",
+		"vendor/kissat/src/phases.c",
+		"vendor/kissat/src/print.c",
+		"vendor/kissat/src/probe.c",
+		"vendor/kissat/src/profile.c",
+		"vendor/kissat/src/promote.c",
+		"vendor/kissat/src/proof.c",
+		"vendor/kissat/src/propbeyond.c",
+		"vendor/kissat/src/propdense.c",
+		"vendor/kissat/src/proprobe.c",
+		"vendor/kissat/src/propsearch.c",
+		"vendor/kissat/src/queue.c",
+		"vendor/kissat/src/reduce.c",
+		"vendor/kissat/src/reluctant.c",
+		"vendor/kissat/src/rephase.c",
+		"vendor/kissat/src/report.c",
+		"vendor/kissat/src/resize.c",
+		"vendor/kissat/src/resolve.c",
+		"vendor/kissat/src/resources.c",
+		"vendor/kissat/src/restart.c",
+		"vendor/kissat/src/search.c",
+		"vendor/kissat/src/shrink.c",
+		"vendor/kissat/src/smooth.c",
+		"vendor/kissat/src/sort.c",
+		"vendor/kissat/src/stack.c",
+		"vendor/kissat/src/statistics.c",
+		"vendor/kissat/src/strengthen.c",
+		"vendor/kissat/src/substitute.c",
+		"vendor/kissat/src/sweep.c",
+		"vendor/kissat/src/terminate.c",
+		"vendor/kissat/src/trail.c",
+		"vendor/kissat/src/transitive.c",
+		"vendor/kissat/src/utilities.c",
+		"vendor/kissat/src/vector.c",
+		"vendor/kissat/src/vivify.c",
+		"vendor/kissat/src/walk.c",
+		"vendor/kissat/src/warmup.c",
+		"vendor/kissat/src/watch.c",
+		"vendor/kissat/src/weaken.c",
+		"vendor/kissat/src/witness.c",
+		"src/ipasir.c",
+	];
+
+	let mut builder = cc::Build::new();
+
+	let compiler = builder.try_get_compiler().unwrap();
+	let version = include_str!("vendor/kissat/VERSION").trim();
+	let git_id = String::from_utf8(
+		Command::new("git")
+			.current_dir("vendor/kissat")
+			.args(&["rev-parse", "HEAD"])
+			.output()
+			.unwrap()
+			.stdout,
+	)
+	.unwrap();
+	let date = String::from_utf8(
+		Command::new("date")
+			.env("LC_LANG", "en_US")
+			.output()
+			.unwrap()
+			.stdout,
+	)
+	.unwrap();
+	let uname = String::from_utf8(
+		Command::new("uname")
+			.args(&["-srmn"])
+			.output()
+			.unwrap()
+			.stdout,
+	)
+	.unwrap();
+
+	assert_eq!(env!("CARGO_PKG_VERSION"), version);
+
+	let build = builder
+		.include("./src")
+		.define("VERSION", format!("\"{version}\"").as_str())
+		.define(
+			"COMPILER",
+			format!(
+				"{:?}",
+				format!(
+					"{} {}",
+					compiler.path().to_str().unwrap(),
+					compiler.args().join(" ".as_ref()).to_str().unwrap()
+				)
+			)
+			.as_ref(),
+		)
+		.define("ID", format!("\"{}\"", git_id.trim()).as_ref())
+		.define(
+			"BUILD",
+			format!("\"{} {}\"", date.trim(), uname.trim()).as_ref(),
+		)
+		.define("QUIET", None);
+
+	build.files(src);
+
+	build.compile("kissat");
+}

crates/pindakaas-kissat/src/build.h

@@ -0,0 +1 @@
+// Empty file, defines are set in build.rs

crates/pindakaas-kissat/src/ipasir.c

@@ -0,0 +1,19 @@
+#include "../vendor/kissat/src/kissat.h"
+#include <assert.h>
+#include <stdint.h>
+
+/// Empty function to complete IPASIR default interface
+void kissar_set_learn(void *solver, void *state, int max_length,
+                      void (*learn)(void *state, int *clause)) {
+  assert(0);
+}
+
+int32_t kissat_val(void *solver, int32_t lit) {
+  return kissat_value(solver, lit);
+}
+
+int kissat_failed(void *solver, int32_t lit) {
+  assert(0);
+  return 0;
+}
+void kissat_assume(void *solver, int32_t lit) { assert(0); }

crates/pindakaas-kissat/src/lib.rs

@@ -0,0 +1,29 @@
+use std::ffi::{c_char, c_int, c_uint, c_void};
+
+use pindakaas_build_macros::ipasir_definitions;
+
+ipasir_definitions!(kissat);
+
+extern "C" {
+	pub fn kissat_terminate(slv: *mut c_void);
+	pub fn kissat_reserve(slv: *mut c_void, max_var: c_int);
+
+	pub fn kissat_id() -> *const c_char;
+	pub fn kissat_version() -> *const c_char;
+	pub fn kissat_compiler() -> *const c_char;
+
+	pub fn kissat_copyright() -> *const *const c_char;
+	pub fn kissat_build(line_prefix: *const c_char);
+	pub fn kissat_banner(line_prefix: *const c_char, name_of_app: *const c_char);
+
+	pub fn kissat_get_option(slv: *mut c_void, name: *const c_char) -> c_int;
+	pub fn kissat_set_option(slv: *mut c_void, name: *const c_char, new_value: c_int) -> c_int;
+
+	pub fn kissat_has_configuration(name: *const c_char) -> c_int;
+	pub fn kissat_set_configuration(slv: *mut c_void, name: *const c_char) -> c_int;
+
+	pub fn kissat_set_conflict_limit(slv: *mut c_void, limit: c_uint);
+	pub fn kissat_set_decision_limit(slv: *mut c_void, limit: c_uint);
+
+	pub fn kissat_print_statistics(slv: *mut c_void);
+}

crates/pindakaas/Cargo.toml

@@ -24,14 +24,16 @@ tracing = { version = "0.1", optional = true }
 # Optional Solver Interfaces
 pindakaas-cadical = { path = "../pindakaas-cadical", optional = true }
 pindakaas-intel-sat = { path = "../pindakaas-intel-sat", optional = true }
+pindakaas-kissat = { path = "../pindakaas-kissat", optional = true }
 splr = { version = "0.17", optional = true }
 
 [dev-dependencies]
 splr = { version = "0.17", features = ["incremental_solver"] }
 traced_test = { path = "../traced_test" }
 
 [features]
-trace = ["tracing"]
 cadical = ["pindakaas-cadical"]
 intel-sat = ["pindakaas-intel-sat"]
-default = []
+kissat = ["pindakaas-kissat"]
+trace = ["tracing"]
+default = ["cadical", "intel-sat", "kissat"]