From 5d3812b998119beab7d4ff29041dac951be8b06e Mon Sep 17 00:00:00 2001
From: gothictomato <gothictomato@pm.me>
Date: Mon, 18 Jul 2022 02:19:32 -0400
Subject: [PATCH] Added more comments to cnf.c

---
 cnf.c | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/cnf.c b/cnf.c
index 9ae5009..b5c6710 100644
--- a/cnf.c
+++ b/cnf.c
@@ -171,9 +171,6 @@ const u64 RSIZE = 1LU << RBITS;
 const u64 RLVLS = (63LU / RBITS) + 1;
 const u64 RMASK = RSIZE - 1;
 
-// Currently sorting array of program pointers by the score of the programs
-// I need to sort by lastvar, within that sort by clause
-
 void sortlastnum(cnf* c, u64 N) {
     // Radix sort on the literals themselves based on their clause's
     bool v = false;
@@ -190,6 +187,7 @@ void sortlastnum(cnf* c, u64 N) {
         u64 shift = pass * RBITS;
 
         for (u64 i = 0; i < N; ++i) {
+            // U32MAX - because we want to sort highest to lowest, not lowest to highest
             u32 val = UINT32_MAX - c->lastvars[c->clauses[i]];
             u64 ind = (val >> shift) & RMASK;
             qe[pass * RSIZE + ind]++;
@@ -216,6 +214,7 @@ void sortlastnum(cnf* c, u64 N) {
             __builtin_prefetch(d3 + qb[pass * RSIZE + ind] + 1);
         }
 
+        // Every iteration we swap pointers to avoid doing a memcpy
         u32* tptr = c->variables;
         c->variables = d;
         d = tptr;
@@ -228,6 +227,8 @@ void sortlastnum(cnf* c, u64 N) {
         v = !v;
     }
 
+    // If the pointers are still swapped at the end, we swap them to their original locations and
+    // copy over the result
     if (v) {
         u32* tptr = c->variables;
         c->variables = d;
@@ -246,11 +247,13 @@ void sortlastnum(cnf* c, u64 N) {
     free(d2);
     free(d3);
 
+    // Initialize an array with all the clause indices in their current order
     u32* swaparr = malloc(sizeof(u32) * c->clausecnt);
     for (u32 i = 0; i < c->clausecnt; ++i) {
         swaparr[i] = i;
     }
 
+    // Perform another radix sort!
     v = false;
     d = malloc(sizeof(u32) * c->clausecnt);
 
@@ -261,6 +264,8 @@ void sortlastnum(cnf* c, u64 N) {
         u64 shift = pass * RBITS;
 
         for (u64 i = 0; i < c->clausecnt; ++i) {
+            // Sort highest to lowest by lastvar again, but this time sorting the indices in swaparr
+            // instead of sorting literals
             u32 val = UINT32_MAX - c->lastvars[swaparr[i]];
             u64 ind = (val >> shift) & RMASK;
             qe[pass * RSIZE + ind]++;
@@ -297,18 +302,25 @@ void sortlastnum(cnf* c, u64 N) {
     }
     //free(d);
 
+    // Swaparr now has each clause index value at the correct index for where
+    // it appears in the CNF now that it has been sorted
+    // We'll now invert the permutation in swaparr
     for (uint i = 0; i < c->clausecnt; ++i) {
         d[swaparr[i]] = i;
     }
 
+    // giving us a lookup table from oldindex to newindex
+    // Which we then correct in all the literals
     for (uint i = 0; i < c->litcnt; ++i) {
         c->clauses[i] = d[c->clauses[i]];
     }
 
+    // and then finally reorder the lastvars
     for (uint i = 0; i < c->clausecnt; ++i) {
         swaparr[d[i]] = c->lastvars[i];
     }
 
+    // Copy the lastvars back into the correct array, clean up, and we're done!
     memcpy(c->lastvars, swaparr, sizeof(u32) * c->clausecnt);
     free(swaparr);
     free(d);