@@ -25,6 +25,7 @@ along with this program. If not, see <https://www.gnu.org/licenses/>.
2525#include " function.cuh"
2626#include " ifthenelse.cuh"
2727#include " equivalence.cuh"
28+ #include " shared.cuh"
2829
2930namespace ParaFROST {
3031
@@ -65,8 +66,6 @@ namespace ParaFROST {
6566
6667 // ==========================================//
6768
68- __device__ int lastEliminatedID;
69-
7069 #define ADD_RESOLVENT \
7170 { \
7271 int rsize; \
@@ -262,21 +261,7 @@ namespace ParaFROST {
262261 // =========================================================//
263262 // kernels
264263 // =========================================================//
265-
266- __global__ void reset_id () { lastEliminatedID = -1 ; }
267-
268- __global__ void print_id () { printf (" c lastEliminatedID = %d\n " , lastEliminatedID); }
269264
270- __global__ void mapfrozen_k (const uint32* __restrict__ frozen, uint32* __restrict__ varcore, const uint32 size)
271- {
272- grid_t tid = global_tx;
273- while (tid < size) {
274- assert (frozen[tid] && frozen[tid] < NOVAR );
275- varcore[frozen[tid]] = tid;
276- tid += stride_x;
277- }
278- }
279-
280265 // Macros for checking applicability of variable elimination
281266 #define MEMORY_SAFE_DBG \
282267 if ((addedPos + nAddedCls) > cnf->refs ().capacity()) { \
@@ -491,6 +476,19 @@ namespace ParaFROST {
491476 }
492477 }
493478
479+ _PFROST_IN_D_ uint32 laneId () {
480+ uint32 id;
481+ asm (" mov.u32 %0, %%laneid;" : " =r" (id));
482+ return id;
483+ }
484+
485+ template <class T , class R >
486+ _PFROST_IN_D_ void atomicAggMax (T* counter, const R ref) {
487+ const uint32 mask = __activemask (), max_id = (32 - __clz (mask)) - 1 ;
488+ if (laneId () == max_id)
489+ atomicMax (counter, ref);
490+ }
491+
494492 __global__ void ve_k_2 (
495493 CNF * __restrict__ cnf,
496494 OT * __restrict__ ot,
@@ -551,32 +549,6 @@ namespace ParaFROST {
551549 }
552550 }
553551
554- __global__ void resizeCNF_k (CNF * cnf,
555- const uint32* __restrict__ type,
556- const uint32* __restrict__ rpos,
557- const S_REF * __restrict__ rref,
558- const int verbose)
559- {
560- if (lastEliminatedID >= 0 ) {
561- const uint32 lastAdded = type[lastEliminatedID];
562- const uint32 lastAddedPos = rpos[lastEliminatedID];
563- const S_REF lastAddedRef = rref[lastEliminatedID];
564- assert (lastAdded < NOVAR );
565- assert (lastAddedPos < NOVAR );
566- assert (lastAddedRef < GNOREF );
567- assert (RECOVERTYPE (lastAdded) < TYPE_MASK );
568- const uint32 lastAddedCls = RECOVERADDEDCLS (lastAdded);
569- const uint32 lastAddedLits = RECOVERADDEDLITS (lastAdded);
570- assert (lastAddedCls && lastAddedCls <= ADDEDCLS_MAX );
571- assert (lastAddedLits && lastAddedLits <= ADDEDLITS_MAX );
572- const S_REF lastAddedBuckets = lastAddedLits + DC_NBUCKETS * lastAddedCls;
573- const S_REF data_size = lastAddedBuckets + lastAddedRef;
574- const uint32 cs_size = lastAddedCls + lastAddedPos;
575- cnf->resize (data_size, cs_size);
576- if (verbose > 1 ) printf (" c resized CNF to %d clauses and %lld data for a last ID %d\n " , cs_size, data_size, lastEliminatedID);
577- }
578- }
579-
580552}
581553
582554
0 commit comments