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@xxxxxxxxxx> Signed-off-by: Ibrahim Fayaz <phayax@xxxxxxxxx> Signed-off-by: Thorsten Berger <thorsten.berger@xxxxxx> Signed-off-by: Ole Schuerks <ole0811sch@xxxxxxxxx> --- 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
