From 63810804fbf54a4cdf58ed0a72782d2979169407 Mon Sep 17 00:00:00 2001
From: gothictomato <gothictomato@pm.me>
Date: Mon, 18 Jul 2022 02:05:22 -0400
Subject: [PATCH] Added some comments, fixed what I think is a bug in the
 clause sorting.

---
 cnf.c | 28 ++++++++++++++++++++++++----
 1 file changed, 24 insertions(+), 4 deletions(-)

diff --git a/cnf.c b/cnf.c
index cdd7059..9ae5009 100644
--- a/cnf.c
+++ b/cnf.c
@@ -13,15 +13,19 @@ cnf* readDIMACS(char* path) {
 
     CHECK(fgets(buf, sizeof(char) * bufsize, f), "Failed to read file\n");
 
+    // 'c' marks the beginning of a comment line in DIMACs. Skip this line
     while (buf[0] == 'c') {
         CHECK(fgets(buf, sizeof(char) * bufsize, f), "Failed to read file\n");
     }
 
+    // The first non-comment line is the header, should have format 'p cnf [varcnt] [clausecnt]
+    // We skip the first bit by iterating and skipping any character that's p, c, n, f, or space
     char* temp = buf;
     while (*temp == ' ' || *temp == 'p' || *temp == 'c' || *temp == 'n' || *temp == 'f') {
         temp++;
     }
 
+    // Char by char we read in the number of variables
     c->varcnt = 0;
     while (((u8) (*temp - '0')) < 10) {
         c->varcnt *= 10;
@@ -29,8 +33,10 @@ cnf* readDIMACS(char* path) {
         temp++;
     }
 
+    // Skip any trailing whitespace
     while (*temp == ' ') temp++;
 
+    // Read in clausecnt
     c->clausecnt = 0;
     while (((u8) (*temp - '0')) < 10) {
         c->clausecnt *= 10;
@@ -38,6 +44,9 @@ cnf* readDIMACS(char* path) {
         temp++;
     }
 
+    // Resize line buffer: the maximum clause size is varcnt, the maximum size of a u32 in decimal
+    // is 10, and conservatively given 2 extra characters for the - symbol and space delimiting,
+    // resizing the buffer to this should mean we never encounter a clause we fail to read.
     u32 nsize = sizeof(char) * (c->varcnt * 12LU) + 10;
     char* nbuf = realloc(buf, nsize);
     CHECK(nbuf, "Failed to realloc read buffer\n");
@@ -47,6 +56,9 @@ cnf* readDIMACS(char* path) {
     u32 cnt = 0;
     u32 cap = 32;
 
+    // We store separate arrays: literal i of the CNF has a parity at index i in one array
+    // the variable it corresponds to at the same index in another
+    // And the clause it's a member of in a third
     c->variables = calloc( cap, sizeof(u32));
     CHECK(c->variables, "Failed to allocate literal variables\n");
     c->clauses = calloc( cap, sizeof(u32));
@@ -60,15 +72,15 @@ cnf* readDIMACS(char* path) {
     for (u32 i = 0; i < c->clausecnt; ++i) {
         CHECK(fgets(buf, nsize, f), "Failed to read clause\n");
 
-
-
         temp = buf;
         while (*temp == ' ') temp++;
 
+        // Iterate through char by char
         bool empty = true;
         bool tr = true;
         while (*temp != '\n') {
             if (cnt == cap) {
+                // Out of space to add more literals, realloc arrays
                 u32 ncap = cap << 1U;
                 c->variables = realloc(c->variables, sizeof(u32) * ncap);
                 memset(c->variables + cap, 0, sizeof(u32) * cap);
@@ -83,11 +95,15 @@ cnf* readDIMACS(char* path) {
             }
 
             if (*temp == '-') {
+                // Mark that the literal currently being read is negated
                 tr = false;
             } else if (((u8) (*temp - '0'))  < 10) {
+                // Read in the literal's digits
                 c->variables[cnt] *= 10;
                 c->variables[cnt] += (*temp - '0');
             } else {
+                // Skip any whitespace and pack the read value into the arrays, along with
+                // any additional data
                 while (temp[1] == ' ') temp++;
                 c->pars[cnt] = tr;
                 c->clauses[cnt] = i;
@@ -109,6 +125,8 @@ cnf* readDIMACS(char* path) {
         }
     }
 
+    // Lastvars is set to the index of the last variable of each clause. However, because in the
+    // counter, the last variable has the lsb position, we flip the value of lastvars
     for (u32 i = 0; i < c->clausecnt; ++i) {
         c->lastvars[i] += 1U;
         c->lastvars[i] = c->varcnt - c->lastvars[i];
@@ -116,6 +134,7 @@ cnf* readDIMACS(char* path) {
 
     c->litcnt = cnt;
 
+    // Realloc the arrays to exactly match the number of literals
     c->variables = realloc(c->variables, sizeof(u32) * c->litcnt);
     c->clauses = realloc(c->clauses, sizeof(u32) * c->litcnt);
     c->pars = realloc(c->pars, sizeof(u8) * c->litcnt);
@@ -156,6 +175,7 @@ const u64 RMASK = RSIZE - 1;
 // 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;
     u32* d = malloc(sizeof(u32) * c->litcnt);
     u32* d2 = malloc(sizeof(u32) * c->litcnt);
@@ -170,7 +190,7 @@ void sortlastnum(cnf* c, u64 N) {
         u64 shift = pass * RBITS;
 
         for (u64 i = 0; i < N; ++i) {
-            u32 val = UINT32_MAX - c->lastvars[(c->clausecnt - 1) - c->clauses[i]];
+            u32 val = UINT32_MAX - c->lastvars[c->clauses[i]];
             u64 ind = (val >> shift) & RMASK;
             qe[pass * RSIZE + ind]++;
         }
@@ -185,7 +205,7 @@ void sortlastnum(cnf* c, u64 N) {
         }
 
         for (u64 i = 0; i < N; ++i) {
-            u32 val = UINT32_MAX - c->lastvars[(c->clausecnt - 1) - c->clauses[i]];
+            u32 val = UINT32_MAX - c->lastvars[c->clauses[i]];
             u64 ind = (val >> shift) & RMASK;
             d[qb[pass * RSIZE + ind]] = c->variables[i];
             d2[qb[pass * RSIZE + ind]] = c->clauses[i];