[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-Id: <20250208163959.3973163-2-ole0811sch@gmail.com>
Date: Sat, 8 Feb 2025 17:39:49 +0100
From: Ole Schuerks <ole0811sch@...il.com>
To: linux-kbuild@...r.kernel.org
Cc: ole0811sch@...il.com,
jude.gyimah@....de,
thorsten.berger@....de,
deltaone@...ian.org,
jan.sollmann@....de,
mcgrof@...nel.org,
masahiroy@...nel.org,
linux-kernel@...r.kernel.org,
nathan@...nel.org,
nicolas@...sle.eu
Subject: [PATCH v7 01/11] kconfig: Add PicoSAT interface
PicoSAT [0] is the SAT solver used in this project. It is used as a
dynamically loaded library. Add PicoSAT dynamic library support to
kconfig, which will be used in the subsequent patches.
Link: https://fmv.jku.at/picosat/ # [0]
Signed-off-by: Patrick Franz <deltaone@...ian.org>
Signed-off-by: Ibrahim Fayaz <phayax@...il.com>
Signed-off-by: Thorsten Berger <thorsten.berger@....de>
Signed-off-by: Ole Schuerks <ole0811sch@...il.com>
---
scripts/kconfig/picosat_functions.c | 79 +++++++++++++++++++++++++++++
scripts/kconfig/picosat_functions.h | 35 +++++++++++++
2 files changed, 114 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..dcfc80d418c2
--- /dev/null
+++ b/scripts/kconfig/picosat_functions.c
@@ -0,0 +1,79 @@
+// 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)
+{
+ const char *error_str;
+
+ if (*failed)
+ return;
+
+ dlerror(); // clear error
+ *ptr = dlsym(handle, name);
+ error_str = dlerror();
+ if (error_str) {
+ printd("While loading %s: %s\n", name, error_str);
+ *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
Powered by blists - more mailing lists