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/install-picosat.sh | 29 +++++++++++
scripts/kconfig/picosat_functions.c | 74 +++++++++++++++++++++++++++++
scripts/kconfig/picosat_functions.h | 35 ++++++++++++++
3 files changed, 138 insertions(+)
create mode 100755 scripts/kconfig/install-picosat.sh
create mode 100644 scripts/kconfig/picosat_functions.c
create mode 100644 scripts/kconfig/picosat_functions.h
diff --git a/scripts/kconfig/install-picosat.sh b/scripts/kconfig/install-picosat.sh
new file mode 100755
index 000000000000..aadfa9582ecb
--- /dev/null
+++ b/scripts/kconfig/install-picosat.sh
@@ -0,0 +1,29 @@
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+
+psinstdir=$(mktemp -d)
+if [ $? -ne 0 ]; then
+ echo "mktemp failed"
+ exit 1
+fi
+cd $psinstdir
+wget "https://fmv.jku.at/picosat/picosat-965.tar.gz"
+tar -xf picosat-965.tar.gz
+cd picosat-965
+cp makefile.in makefile.in2
+# change soname to conform with packages for Debian and Fedora
+sed -e "s,-soname -Xlinker libpicosat.so,-soname -Xlinker \
+ libpicosat-trace.so.0," makefile.in2 > makefile.in
+./configure.sh -O -t --shared
+make libpicosat.so
+install -m 0755 -p libpicosat.so /usr/local/lib/libpicosat-trace.so.0.0.965 \
+&& ln -s -f libpicosat-trace.so.0.0.965 /usr/local/lib/libpicosat-trace.so.0 \
+&& ln -s -f libpicosat-trace.so.0 /usr/local/lib/libpicosat-trace.so \
+&& ldconfig
+echo
+if [ $? -ne 0 ]; then
+ echo "Installation of PicoSAT failed, make sure you are running with root privileges."
+ exit 1
+else
+ echo "Installation of PicoSAT succeeded."
+fi
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.2