diff --git a/lib/import/import-glucose.mk b/lib/import/import-glucose.mk new file mode 100644 index 0000000..fe7d571 --- /dev/null +++ b/lib/import/import-glucose.mk @@ -0,0 +1,2 @@ +INC_DIR += $(call select_from_ports,glucose)/include/glucose +INC_DIR += $(call select_from_ports,glucose)/include/ diff --git a/lib/mk/glucose.mk b/lib/mk/glucose.mk new file mode 100644 index 0000000..6cd602f --- /dev/null +++ b/lib/mk/glucose.mk @@ -0,0 +1,13 @@ +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 diff --git a/ports/glucose.hash b/ports/glucose.hash new file mode 100644 index 0000000..22abbd2 --- /dev/null +++ b/ports/glucose.hash @@ -0,0 +1 @@ +0a138c29411f0e7802764c5e4ce0451bd8e4be56 diff --git a/ports/glucose.port b/ports/glucose.port new file mode 100644 index 0000000..dd5fc71 --- /dev/null +++ b/ports/glucose.port @@ -0,0 +1,15 @@ +LICENSE := MiniSat +VERSION := 3.0 +DOWNLOADS := glucose.archive + +URL(glucose) := http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-$(VERSION).tgz +SHA(glucose) := 3c4598e1ee911b4dfaedc0ce296d5eb8a9a2796e +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) + +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 new file mode 100644 index 0000000..449ed50 --- /dev/null +++ b/run/glucose.run @@ -0,0 +1,90 @@ +build "core init test/glucose drivers/timer" + +create_boot_directory + +set fd [open "bin/Test.cnf" w] +puts $fd { +p cnf 15 20 +-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 + +set filesize [exec stat -c "%s" bin/Test.cnf] + +append config { + + + + + + + + + + + + + + + + + + + + + + + +} + +append config " + + + + + + + + + + + +" + +install_config $config + +build_boot_image { + core init test-glucose timer + ld.lib.so libc.lib.so + libm.lib.so + stdcxx.lib.so + zlib.lib.so + Test.cnf +} + +append qemu_args " -nographic -m 64 " + +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 new file mode 100644 index 0000000..88365eb --- /dev/null +++ b/src/lib/glucose/buffer_size.patch @@ -0,0 +1,10 @@ ++++ 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 new file mode 100644 index 0000000..15cd4b7 --- /dev/null +++ b/src/lib/glucose/c++11.patch @@ -0,0 +1,20 @@ ++++ 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 new file mode 100644 index 0000000..6594ded --- /dev/null +++ b/src/lib/glucose/copy_constructor.patch @@ -0,0 +1,35 @@ ++++ 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 new file mode 100644 index 0000000..4719488 --- /dev/null +++ b/src/lib/glucose/cputime.patch @@ -0,0 +1,21 @@ ++++ 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 new file mode 100644 index 0000000..f905852 --- /dev/null +++ b/src/lib/glucose/map.patch @@ -0,0 +1,24 @@ ++++ 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/pow.patch b/src/lib/glucose/pow.patch new file mode 100644 index 0000000..8bf41a8 --- /dev/null +++ b/src/lib/glucose/pow.patch @@ -0,0 +1,10 @@ ++++ 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 new file mode 100644 index 0000000..a4f6005 --- /dev/null +++ b/src/test/glucose/main.cc @@ -0,0 +1,103 @@ +#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 : %d (%.1f µs)\n", 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: %d (%.1f µs) |\n", 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 */ + + PINF("Okay"); + } + else { + PERR("Unable to open file \"Test.cnf\""); + return 1; + } + + return 0; +} diff --git a/src/test/glucose/target.mk b/src/test/glucose/target.mk new file mode 100644 index 0000000..525e212 --- /dev/null +++ b/src/test/glucose/target.mk @@ -0,0 +1,5 @@ +TARGET = test-glucose +LIBS = base stdcxx zlib glucose +SRC_CC = main.cc + +CC_OPT += -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS