diff --git a/lib/import/import-glucose.mk b/lib/import/import-glucose.mk deleted file mode 100644 index 52909e3..0000000 --- a/lib/import/import-glucose.mk +++ /dev/null @@ -1,4 +0,0 @@ -INC_DIR += $(call select_from_ports,glucose)/include/glucose -INC_DIR += $(call select_from_ports,glucose)/include/ - -CC_CXX_WARN_STRICT = diff --git a/lib/mk/glucose.mk b/lib/mk/glucose.mk deleted file mode 100644 index 15262c1..0000000 --- a/lib/mk/glucose.mk +++ /dev/null @@ -1,15 +0,0 @@ -GLUCOSE_DIR = $(call select_from_ports,glucose)/src/lib/glucose/ -LIBS += stdcxx zlib libc libm -INC_DIR += $(GLUCOSE_DIR) -SRC_CC = Solver.cc - -CC_OPT += -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS - -CC_WARN = - -vpath %.cc $(GLUCOSE_DIR)/core -vpath %.cc $(GLUCOSE_DIR)/utils - -#SHARED_LIB = yes - -CC_CXX_WARN_STRICT = diff --git a/ports/glucose.hash b/ports/glucose.hash deleted file mode 100644 index 9c9b396..0000000 --- a/ports/glucose.hash +++ /dev/null @@ -1 +0,0 @@ -41c79967122ef8dc145eb592c6c518f06af8ef6b diff --git a/ports/glucose.port b/ports/glucose.port deleted file mode 100644 index 766c016..0000000 --- a/ports/glucose.port +++ /dev/null @@ -1,15 +0,0 @@ -LICENSE := MiniSat -VERSION := 3.0 -DOWNLOADS := glucose.archive - -URL(glucose) := http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-$(VERSION).tgz -SHA(glucose) := e721005535f8ca96d58c0c7e3923924e948a231fb305960b1bf4af49cbc936a6 -DIR(glucose) := src/lib/glucose - -PATCHES := $(addprefix src/lib/glucose/,c++11.patch pow.patch map.patch buffer_size.patch copy_constructor.patch cputime.patch parse.patch) - -DIRS := include/glucose/core include/glucose/mtl include/glucose/utils - -DIR_CONTENT(include/glucose/core) := src/lib/glucose/core/*.h -DIR_CONTENT(include/glucose/mtl) := src/lib/glucose/mtl/*.h -DIR_CONTENT(include/glucose/utils) := src/lib/glucose/utils/*.h diff --git a/run/glucose.run b/run/glucose.run deleted file mode 100644 index 903166f..0000000 --- a/run/glucose.run +++ /dev/null @@ -1,85 +0,0 @@ -build "core init test/glucose timer" - -create_boot_directory - -set fd [open "bin/Test.cnf" w] -puts $fd { -p cnf 15 22 --1 10 11 8 9 0 --2 10 11 8 9 0 --2 4 0 --2 5 6 0 --3 4 5 0 --6 7 0 --8 -9 0 -8 9 0 --10 8 9 0 --11 8 9 0 -1 -12 0 -8 -12 0 -2 -13 0 -8 -13 0 -1 -14 0 -9 -14 0 -2 -15 0 -9 -15 0 --1 12 14 0 --2 13 15 0 -10 11 -12 -13 0 -10 11 -14 -15 0 -} -close $fd - -append config { - - - - - - - - - - - - - - - - - - - - - - - - -} - -append config " - - - - - - - - - - -" - -install_config $config - -build_boot_image { - core init test-glucose timer - ld.lib.so libc.lib.so vfs.lib.so posix.lib.so libm.lib.so stdcxx.lib.so zlib.lib.so - Test.cnf -} - -append qemu_args " -nographic " - -run_genode_until {.*Okay.*} 20 - -exec rm bin/Test.cnf diff --git a/src/lib/glucose/buffer_size.patch b/src/lib/glucose/buffer_size.patch deleted file mode 100644 index 88365eb..0000000 --- a/src/lib/glucose/buffer_size.patch +++ /dev/null @@ -1,10 +0,0 @@ -+++ src/lib/glucose/utils/ParseUtils.h 2014-10-31 10:40:41.409180338 +0100 -@@ -32,7 +32,7 @@ namespace Glucose { - //------------------------------------------------------------------------------------------------- - // A simple buffered character stream class: - --static const int buffer_size = 1048576; -+static const int buffer_size = 1024*4; - - - class StreamBuffer { diff --git a/src/lib/glucose/c++11.patch b/src/lib/glucose/c++11.patch deleted file mode 100644 index 15cd4b7..0000000 --- a/src/lib/glucose/c++11.patch +++ /dev/null @@ -1,20 +0,0 @@ -+++ src/lib/glucose/utils/Options.h 2014-04-25 15:02:14.077028723 +0200 -@@ -282,15 +282,15 @@ class Int64Option : public Option - if (range.begin == INT64_MIN) - fprintf(stderr, "imin"); - else -- fprintf(stderr, "%4"PRIi64, range.begin); -+ fprintf(stderr, "%4" PRIi64, range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT64_MAX) - fprintf(stderr, "imax"); - else -- fprintf(stderr, "%4"PRIi64, range.end); -+ fprintf(stderr, "%4" PRIi64, range.end); - -- fprintf(stderr, "] (default: %"PRIi64")\n", value); -+ fprintf(stderr, "] (default: %" PRIi64")\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); diff --git a/src/lib/glucose/copy_constructor.patch b/src/lib/glucose/copy_constructor.patch deleted file mode 100644 index 6594ded..0000000 --- a/src/lib/glucose/copy_constructor.patch +++ /dev/null @@ -1,35 +0,0 @@ -+++ src/lib/glucose/core/Solver.cc 2015-08-28 17:42:26.782504938 +0200 -@@ -164,6 +164,23 @@ Solver::~Solver() - { - } - -+void Solver::copyFrom(Solver &s) -+{ -+ /* "copy" variables from s */ -+ for (int i=0; i < s.nVars(); i++) { -+ newVar(); -+ } -+ -+ /* TODO copy clauses from s */ -+ for (int i=0; i < s.nClauses(); i++) { -+ Clause &old_clause = s.ca[s.clauses[i]]; -+ vec lits; -+ for (int j=0; j < old_clause.size(); j++) { -+ lits.push(old_clause[j]); -+ } -+ addClause(lits); -+ } -+} - - /**************************************************************** - Set the incremental mode -+++ src/lib/glucose/core/Solver.h 2015-08-28 17:35:27.393544963 +0200 -@@ -51,6 +51,8 @@ public: - Solver(); - virtual ~Solver(); - -+ void copyFrom(Solver &s); -+ - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. diff --git a/src/lib/glucose/cputime.patch b/src/lib/glucose/cputime.patch deleted file mode 100644 index 4719488..0000000 --- a/src/lib/glucose/cputime.patch +++ /dev/null @@ -1,21 +0,0 @@ -+++ src/lib/glucose/utils/System.h 2016-03-10 13:09:39.945805425 +0100 -@@ -21,6 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR - #ifndef Glucose_System_h - #define Glucose_System_h - -+#define _NO_RUSAGE -+ - #if defined(__linux__) - #include - #endif -@@ -45,6 +47,10 @@ extern double memUsedPeak(); // P - - static inline double Glucose::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } - -+#elif defined(_NO_RUSAGE) -+ -+static inline double Glucose::cpuTime(void) { return 0; } -+ - #else - #include - #include diff --git a/src/lib/glucose/map.patch b/src/lib/glucose/map.patch deleted file mode 100644 index f905852..0000000 --- a/src/lib/glucose/map.patch +++ /dev/null @@ -1,24 +0,0 @@ -+++ src/lib/glucose/mtl/Map.h 2014-04-25 16:31:15.008872872 +0200 -@@ -29,17 +29,17 @@ - // Default hash/equals functions - // - -+static inline uint32_t hash(uint32_t x){ return x; } -+static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } -+static inline uint32_t hash(int32_t x) { return (uint32_t)x; } -+static inline uint32_t hash(int64_t x) { return (uint32_t)x; } -+ - template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; - template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; - - template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; - template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; - --static inline uint32_t hash(uint32_t x){ return x; } --static inline uint32_t hash(uint64_t x){ return (uint32_t)x; } --static inline uint32_t hash(int32_t x) { return (uint32_t)x; } --static inline uint32_t hash(int64_t x) { return (uint32_t)x; } -- - - //================================================================================================= - // Some primes diff --git a/src/lib/glucose/parse.patch b/src/lib/glucose/parse.patch deleted file mode 100644 index 93ead1b..0000000 --- a/src/lib/glucose/parse.patch +++ /dev/null @@ -1,10 +0,0 @@ -+++ src/lib/glucose/core/Dimacs.h 2018-06-13 13:12:39.770427200 +0200 -@@ -52,7 +52,7 @@ - int cnt = 0; - for (;;){ - skipWhitespace(in); -- if (*in == EOF) break; -+ if (*in == EOF or *in == 0) break; - else if (*in == 'p'){ - if (eagerMatch(in, "p cnf")){ - vars = parseInt(in); diff --git a/src/lib/glucose/pow.patch b/src/lib/glucose/pow.patch deleted file mode 100644 index 8bf41a8..0000000 --- a/src/lib/glucose/pow.patch +++ /dev/null @@ -1,10 +0,0 @@ -+++ src/lib/glucose/utils/ParseUtils.h 2014-04-25 16:28:25.714627116 +0200 -@@ -103,7 +103,7 @@ - if (*in != 'e') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3); - ++in; // skip dot - exponent = parseInt(in); // read exponent -- accu *= pow(10,exponent); -+ accu *= pow(10.0,exponent); - return neg ? -accu:accu; - } - diff --git a/src/test/glucose/main.cc b/src/test/glucose/main.cc deleted file mode 100644 index 3986648..0000000 --- a/src/test/glucose/main.cc +++ /dev/null @@ -1,104 +0,0 @@ -#include - -#include -#include - -#include - -#include - -// this value is for the Raspberry Pi -#define TICKS_PER_USEC (700.0/64.0) - -using namespace Glucose; - -inline double cpuTime() -{ - static Timer::Connection _timer; - return _timer.elapsed_ms(); -} - -void printStats(Solver& solver, double initial_time, Genode::Trace::Timestamp start_ts) -{ - Genode::Trace::Timestamp ts_ticks = Genode::Trace::timestamp() - start_ts; - double cpu_time = cpuTime() - initial_time; - double mem_used = 0;//memUsedPeak(); - printf("c restarts : %lld (%lld conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); - printf("c blocked restarts : %lld (multiple: %lld) \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); - printf("c last block at restart : %lld\n",solver.lastblockatrestart); - printf("c nb ReduceDB : %lld\n", solver.nbReduceDB); - printf("c nb removed Clauses : %lld\n",solver.nbRemovedClauses); - printf("c nb learnts DL2 : %lld\n", solver.nbDL2); - printf("c nb learnts size 2 : %lld\n", solver.nbBin); - printf("c nb learnts size 1 : %lld\n", solver.nbUn); - - printf("c conflicts : %-12lld (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("c decisions : %-12lld (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("c propagations : %-12lld (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("c conflict literals : %-12lld (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); - printf("c nb reduced Clauses : %lld\n",solver.nbReducedClauses); - - if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); - printf("c CPU time : %.2f ms\n", cpu_time); - printf("c TS ticks : %u (%.1f µs)\n", (unsigned)ts_ticks, (double)ts_ticks/TICKS_PER_USEC); -} - -int main() -{ - Solver S; - - gzFile gzfile_components = gzopen("Test.cnf", "rb"); - if (gzfile_components != NULL) { - double initial_time = cpuTime(); - - Genode::Trace::Timestamp start_ts = Genode::Trace::timestamp(); -// Genode::Trace::Timestamp start_ts = 0; - parse_DIMACS(gzfile_components, S); - gzclose(gzfile_components); - - double parsed_time = cpuTime(); - Genode::Trace::Timestamp parse_ticks = Genode::Trace::timestamp(); - - /* run solver */ - printf("c | Number of variables: %12d |\n", S.nVars()); - printf("c | Number of clauses: %12d |\n", S.nClauses()); - - printf("c | Parse time: %12.2f ms |\n", parsed_time - initial_time); - printf("c | Parse ticks: %u (%.1f µs) |\n", (unsigned)parse_ticks - start_ts, (double)(parse_ticks-start_ts)/TICKS_PER_USEC); - printf("c | |\n"); - - if (!S.simplify()){ - printf("c =========================================================================================================\n"); - printf("Solved by unit propagation\n"); - printStats(S, initial_time, start_ts); - printf("\n"); - printf("s UNSATISFIABLE\n"); - exit(20); - } - - vec dummy; - lbool ret = S.solveLimited(dummy); - printStats(S, initial_time, start_ts); - printf("\n"); - - printf(ret == l_True ? "s SATISFIABLE\n" : ret == l_False ? "s UNSATISFIABLE\n" : "s INDETERMINATE\n"); - if(ret==l_True) { - printf("v "); - for (int i = 0; i < S.nVars(); i++) - if (S.model[i] != l_Undef) - - printf("%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1); - printf(" 0\n"); - } - - /* solver finished */ - - Genode::log("Okay"); - } - else { - Genode::error("Unable to open file \"Test.cnf\""); - return 1; - } - - return 0; -} diff --git a/src/test/glucose/target.mk b/src/test/glucose/target.mk deleted file mode 100644 index 8336f20..0000000 --- a/src/test/glucose/target.mk +++ /dev/null @@ -1,7 +0,0 @@ -TARGET = test-glucose -LIBS = posix stdcxx zlib glucose -SRC_CC = main.cc - -CC_OPT += -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS - -CC_CXX_WARN_STRICT =