PicoSAT (https://fmv.jku.at/picosat/) is the SAT solver used in this
project. It is used as a dynamically loaded library. This commit contains a
script that installs PicoSAT as a library on the host system, a source file
that provides a function for loading a subset of functions from the
library, and a header file that declares these functions.

Signed-off-by: Patrick Franz <deltaone@debian.org>
Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>
Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
---
 scripts/kconfig/picosat_functions.c | 74 +++++++++++++++++++++++++++++
 scripts/kconfig/picosat_functions.h | 35 ++++++++++++++
 2 files changed, 109 insertions(+)
 create mode 100644 scripts/kconfig/picosat_functions.c
 create mode 100644 scripts/kconfig/picosat_functions.h

diff --git a/scripts/kconfig/picosat_functions.c b/scripts/kconfig/picosat_functions.c
new file mode 100644
index 000000000000..ada42abbc22b
--- /dev/null
+++ b/scripts/kconfig/picosat_functions.c
@@ -0,0 +1,74 @@
+// SPDX-License-Identifier: GPL-2.0
+
+#include <dlfcn.h>
+#include <unistd.h>
+
+#include "array_size.h"
+
+#include "cf_defs.h"
+#include "picosat_functions.h"
+
+const char *picosat_lib_names[] = { "libpicosat-trace.so",
+				    "libpicosat-trace.so.0",
+				    "libpicosat-trace.so.1" };
+
+PicoSAT *(*picosat_init)(void);
+int (*picosat_add)(PicoSAT *pico, int lit);
+int (*picosat_deref)(PicoSAT *pico, int lit);
+void (*picosat_assume)(PicoSAT *pico, int lit);
+int (*picosat_sat)(PicoSAT *pico, int decision_limit);
+const int *(*picosat_failed_assumptions)(PicoSAT *pico);
+int (*picosat_added_original_clauses)(PicoSAT *pico);
+int (*picosat_enable_trace_generation)(PicoSAT *pico);
+void (*picosat_print)(PicoSAT *pico, FILE *file);
+
+#define PICOSAT_FUNCTION_LIST             \
+	X(picosat_init)                   \
+	X(picosat_add)                    \
+	X(picosat_deref)                  \
+	X(picosat_assume)                 \
+	X(picosat_sat)                    \
+	X(picosat_failed_assumptions)     \
+	X(picosat_added_original_clauses) \
+	X(picosat_enable_trace_generation)\
+	X(picosat_print)
+
+static void load_function(const char *name, void **ptr, void *handle, bool *failed)
+{
+	if (*failed)
+		return;
+
+	*ptr = dlsym(handle, name);
+	if (!*ptr) {
+		printd("While loading %s: %s\n", name, dlerror());
+		*failed = true;
+	}
+}
+
+bool load_picosat(void)
+{
+	void *handle = NULL;
+	bool failed = false;
+
+	/*
+	 * Try different names for the .so library. This is necessary since
+	 * all packages don't use the same versioning.
+	 */
+	for (int i = 0; i < ARRAY_SIZE(picosat_lib_names) && !handle; ++i)
+		handle = dlopen(picosat_lib_names[i], RTLD_LAZY);
+	if (!handle) {
+		printd("%s\n", dlerror());
+		return false;
+	}
+
+#define X(name) load_function(#name, (void **) &name, handle, &failed);
+
+	PICOSAT_FUNCTION_LIST
+#undef X
+
+	if (failed) {
+		dlclose(handle);
+		return false;
+	} else
+		return true;
+}
diff --git a/scripts/kconfig/picosat_functions.h b/scripts/kconfig/picosat_functions.h
new file mode 100644
index 000000000000..5d8524afa844
--- /dev/null
+++ b/scripts/kconfig/picosat_functions.h
@@ -0,0 +1,35 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+
+#ifndef PICOSAT_FUNCTIONS_H
+#define PICOSAT_FUNCTIONS_H
+
+#include <stdbool.h>
+#include <stdio.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#define PICOSAT_UNKNOWN         0
+#define PICOSAT_SATISFIABLE     10
+#define PICOSAT_UNSATISFIABLE   20
+
+typedef struct PicoSAT PicoSAT;
+
+extern PicoSAT *(*picosat_init)(void);
+extern int (*picosat_add)(PicoSAT *pico, int lit);
+extern int (*picosat_deref)(PicoSAT *pico, int lit);
+extern void (*picosat_assume)(PicoSAT *pico, int lit);
+extern int (*picosat_sat)(PicoSAT *pico, int decision_limit);
+extern const int *(*picosat_failed_assumptions)(PicoSAT *pico);
+extern int (*picosat_added_original_clauses)(PicoSAT *pico);
+extern int (*picosat_enable_trace_generation)(PicoSAT *pico);
+extern void (*picosat_print)(PicoSAT *pico, FILE *file);
+
+bool load_picosat(void);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // PICOSAT_FUNCTIONS_H
-- 
2.39.5