From 2d9b6c7c4d800dc8f4c8e4c4ba6fabf2857fa110 Mon Sep 17 00:00:00 2001 From: Chris Matrakidis
Date: Sun, 8 Jan 2017 22:13:26 +0200 Subject: [PATCH 1/3] less restrictive minisat 64-bit portability check diff --git a/src/api/minisat1.c b/src/api/minisat1.c index cb4148d..2244493 100644 --- a/src/api/minisat1.c +++ b/src/api/minisat1.c @@ -50,9 +50,9 @@ int glp_minisat1(glp_prob *P) goto done; } #if 1 /* 07/XI-2015 */ - if (sizeof(void *) != sizeof(int)) + if (sizeof(void *) != sizeof(size_t)) { xprintf("glp_minisat1: sorry, MiniSat solver is not supported " - "on 64-bit platforms\n"); + "on this platform\n"); ret = GLP_EFAIL; goto done; } diff --git a/src/minisat/minisat.c b/src/minisat/minisat.c index f242d83..47cf920 100644 --- a/src/minisat/minisat.c +++ b/src/minisat/minisat.c @@ -143,13 +143,13 @@ struct clause_t /* Encode literals in clause pointers: */ #define clause_from_lit(l) \ - (clause*)((unsigned long)(l) + (unsigned long)(l) + 1) + (clause*)((size_t)(l) + (size_t)(l) + 1) #define clause_is_lit(c) \ - ((unsigned long)(c) & 1) + ((size_t)(c) & 1) #define clause_read_lit(c) \ - (lit)((unsigned long)(c) >> 1) + (lit)((size_t)(c) >> 1) /*====================================================================*/ /* Simple helpers: */ @@ -332,8 +332,11 @@ static clause* clause_new(solver* s, lit* begin, lit* end, int learnt) c = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float)); c->size_learnt = (size << 1) | learnt; -#if 0 /* by mao; meaningless non-portable check */ - assert(((unsigned int)c & 1) == 0); +#if 1 /* by mao & cmatraki; non-portable check that is a fundamental + * assumption of minisat code: bit 0 is used as a flag (zero + * for pointer, one for shifted int) so allocated memory should + * be at least 16-bit aligned */ + assert(((size_t)c & 1) == 0); #endif for (i = 0; i < size; i++) -- 2.7.4