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@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/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
