alex/genode-world
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove stale port of glucose

Browse Source 
Fixes #178
This commit is contained in:
Norman Feske
2020-04-22 15:41:54 +02:00
parent dbdc441258
commit c548f19c34
14 changed files with 0 additions and 361 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
lib/import/import-glucose.mk
View File

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

15
lib/mk/glucose.mk
View File

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

1
ports/glucose.hash
View File

@@ -1 +0,0 @@
41c79967122ef8dc145eb592c6c518f06af8ef6b

15
ports/glucose.port
View File

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

85
run/glucose.run
View File

@@ -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 {
<config>
<parent-provides>
<service name="ROM"/>
<service name="RAM"/>
<service name="IRQ"/>
<service name="IO_MEM"/>
<service name="IO_PORT"/>
<service name="CAP"/>
<service name="PD"/>
<service name="RM"/>
<service name="CPU"/>
<service name="LOG"/>
<service name="SIGNAL"/>
</parent-provides>
<default-route>
<any-service> <parent/> <any-child/> </any-service>
</default-route>
<default caps="100" />
<start name="timer">
<resource name="RAM" quantum="1M"/>
<provides>
<service name="Timer"/>
</provides>
</start>
}
append config "
<start name=\"test-glucose\">
<resource name=\"RAM\" quantum=\"32M\"/>
<config>
<libc stdin=\"/dev/null\" stdout=\"/dev/log\" stderr=\"/dev/log\" />
<vfs>
<dir name=\"dev\"> <log/> <null/> </dir>
<rom name=\"Test.cnf\" />
</vfs>
</config>
</start>
</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

10
src/lib/glucose/buffer_size.patch
View File

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

20
src/lib/glucose/c++11.patch
View File

@@ -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");

35
src/lib/glucose/copy_constructor.patch
View File

@@ -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<Lit> 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.

21
src/lib/glucose/cputime.patch
View File

@@ -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 <fpu_control.h>
#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 <sys/time.h>
#include <sys/resource.h>

24
src/lib/glucose/map.patch
View File

@@ -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<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
template<class K> 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

10
src/lib/glucose/parse.patch
View File

@@ -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);

10
src/lib/glucose/pow.patch
View File

@@ -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;
}

104
src/test/glucose/main.cc
View File

@@ -1,104 +0,0 @@
#include <timer_session/connection.h>
#include <glucose/core/Solver.h>
#include <glucose/core/Dimacs.h>
#include <trace/timestamp.h>
#include <stdio.h>
// 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<Lit> 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;
}

7
src/test/glucose/target.mk
View File

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