From a0e1d4f5b4339f0d8f389606a79cc077f812f378 Mon Sep 17 00:00:00 2001
From: gothictomato <gothictomato@pm.me>
Date: Sun, 24 Jul 2022 17:47:31 -0400
Subject: [PATCH] Added new CNF format

Signed-off-by: gothictomato <gothictomato@pm.me>
---
 main.c    |   2 +-
 ncnf.c    | 133 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 ncnf.h    |   1 +
 subtree.c |  20 ++------
 4 files changed, 138 insertions(+), 18 deletions(-)

diff --git a/main.c b/main.c
index 354797a..0acc02c 100644
--- a/main.c
+++ b/main.c
@@ -11,7 +11,7 @@ int main() {
 
     printf("\n\n\n\n");
     nprintcnf2(c2);
-    nsortlastnum(c2);
+    nsort(c2);
     printf("\n\n\n\n");
     nprintcnf2(c2);
     printf("the balcony is to your left\n");
diff --git a/ncnf.c b/ncnf.c
index c99f21f..0cf969b 100644
--- a/ncnf.c
+++ b/ncnf.c
@@ -301,4 +301,137 @@ void nsortlastnum(ncnf* c) {
     free(d3);
 
 
+}
+
+
+void nsort(ncnf* c) {
+    bool v = false;
+    u32 dlen = c->clens[0];
+    u32* d = malloc(sizeof(u32) * dlen);
+    u8* dpar = malloc(sizeof(u8) * dlen);
+
+    u32 qb[RLVLS2 * RSIZE2];
+    u32 qe[RLVLS2 * RSIZE2];
+
+    for (u32 k = 0; k < c->clausecnt; ++k) {
+        if (c->clens[k] > dlen) {
+            d = realloc(d, sizeof(u32) * c->clens[k]);
+            dpar = realloc(dpar, sizeof(u8) * c->clens[k]);
+            if (d == NULL || dpar == NULL) {
+                printf("I'm giving up\n");
+            }
+            dlen = c->clens[k];
+        }
+
+        memset(qb, 0, sizeof(u32) * RLVLS2 * RSIZE2);
+        memset(qe, 0, sizeof(u32) * RLVLS2 * RSIZE2);
+
+        for (u32 pass = 0; pass < RLVLS2; ++pass) {
+            u32 shift = pass * RBITS2;
+
+            for (u32 i = 0; i < c->clens[k]; ++i) {
+                u32 val = c->varbak[c->cptrs[k] + i];
+                u32 ind = (val >> shift) & RMASK2;
+                qe[pass * RSIZE2 + ind]++;
+            }
+
+            u32 uc = 0;
+            for (u32 i = 0; i < RSIZE2; ++i) uc += (qe[pass * RSIZE2 + i] != 0);
+            if (uc == 1) continue;
+
+            qb[pass * RSIZE2] = 0;
+            for (u32 i = 1; i < RSIZE2; ++i) {
+                qb[pass * RSIZE2 + i] = qb[pass * RSIZE2 + i - 1] + qe[pass * RSIZE2 + i - 1];
+            }
+
+            for (u32 i = 0; i < c->clens[k]; ++i) {
+                u32 val = c->varbak[c->cptrs[k] + i];
+                u32 ind = (val >> shift) & RMASK2;
+                d[qb[pass * RSIZE2 + ind]] = c->varbak[c->cptrs[k] + i];
+                dpar[qb[pass * RSIZE2 + ind]] = c->parbak[c->cptrs[k] + i];
+                qb[pass * RSIZE2 + ind]++;
+                __builtin_prefetch(d + qb[pass * RSIZE2 + ind] + 1);
+                __builtin_prefetch(dpar + qb[pass * RSIZE2 + ind] + 1);
+            }
+
+            memcpy(c->varbak + c->cptrs[k], d, sizeof(u32) * c->clens[k]);
+            memcpy(c->parbak + c->cptrs[k], dpar, sizeof(u8) * c->clens[k]);
+        }
+    }
+
+    free(dpar);
+    /*
+    if (c->clausecnt > dlen) {
+        d = realloc(d, sizeof(u32) * c->clausecnt);
+        if (d == NULL) {
+            printf("I'm giving up x2\n");
+        }
+        dlen = c->clausecnt;
+    }
+    u32* d2 = malloc(sizeof(u32) * c->clausecnt);
+    u32* d3 = malloc(sizeof(u32) * c->clausecnt);
+
+    memset(qb, 0, sizeof(u32) * RLVLS2 * RSIZE2);
+    memset(qe, 0, sizeof(u32) * RLVLS2 * RSIZE2);
+
+    for (u32 pass = 0; pass < RLVLS2; ++pass) {
+        u32 shift = pass * RBITS2;
+
+        for (u32 i = 0; i < c->clausecnt; ++i) {
+            u32 val = c->varbak[c->cptrs[i]];
+            u32 ind = (val >> shift) & RMASK2;
+            qe[pass * RSIZE2 + ind]++;
+        }
+
+        u32 uc = 0;
+        for (u32 i = 0; i < RSIZE2; ++i) uc += (qe[pass * RSIZE2 + i] != 0);
+        if (uc == 1) continue;
+
+        qb[pass * RSIZE2] = 0;
+        for (u32 i = 1; i < RSIZE2; ++i) {
+            qb[pass * RSIZE2 + i] = qb[pass * RSIZE2 + i - 1] + qe[pass * RSIZE2 + i - 1];
+        }
+
+        for (u32 i = 0; i < c->clausecnt; ++i) {
+            u32 val =  c->varbak[c->cptrs[i]];
+            u32 ind = (val >> shift) & RMASK2;
+            d[qb[pass * RSIZE2 + ind]] = c->cptrs[i];
+            d2[qb[pass * RSIZE2 + ind]] = c->clens[i];
+            d3[qb[pass * RSIZE2 + ind]] = c->lvars[i];
+            qb[pass * RSIZE2 + ind]++;
+            __builtin_prefetch(d2 + qb[pass * RSIZE2 + ind] + 1);
+            __builtin_prefetch(d + qb[pass * RSIZE2 + ind] + 1);
+        }
+
+        u32* tptr = c->cptrs;
+        c->cptrs = d;
+        d = tptr;
+        tptr = c->clens;
+        c->clens = d2;
+        d2 = tptr;
+        tptr = c->lvars;
+        c->lvars = d3;
+        d3 = tptr;
+        v = !v;
+    }
+
+    if (v) {
+        u32* tptr = c->cptrs;
+        c->cptrs = d;
+        d = tptr;
+        tptr = c->clens;
+        c->clens = d2;
+        d2 = tptr;
+        tptr = c->lvars;
+        c->lvars = d3;
+        d3 = tptr;
+        v = !v;
+        memcpy(c->cptrs, d, c->clausecnt * sizeof(u32));
+        memcpy(c->clens, d2, c->clausecnt * sizeof(u32));
+        memcpy(c->lvars, d3, c->clausecnt * sizeof(u32));
+    }
+     */
+    free(d);
+    //free(d2);
+    // free(d3);
 }
\ No newline at end of file
diff --git a/ncnf.h b/ncnf.h
index 03b26fc..6c300c9 100644
--- a/ncnf.h
+++ b/ncnf.h
@@ -18,5 +18,6 @@ void nprintcnf(ncnf* c);
 void nprintcnf2(ncnf* c);
 
 void nsortlastnum(ncnf* c);
+void nsort(ncnf* c);
 
 void nfreecnf(ncnf* c);
\ No newline at end of file
diff --git a/subtree.c b/subtree.c
index 0c509b9..faf0f93 100644
--- a/subtree.c
+++ b/subtree.c
@@ -1,20 +1,6 @@
 #include "subtree.h"
+#include "ncnf.h"
 
+void brzozowski(ncnf* c) {
 
-
-void gendfa() {
-    u32 varcnt = 4;
-    char* clauses[4] = {
-            "0121",
-            "0122",
-            "2122",
-            "2222"
-    };
-
-    // Order the clauses
-    // Make nodes for each clause
-    // Combine 2 nodes into 1 if their next prefix is identical
-    // If their next prefix is 1, create 2 combinations
-
-
-}
\ No newline at end of file
+}