Add nodeedge files

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
new file mode 100644 (file)
index 0000000..e5c50b0
--- /dev/null
+++ b/src/Backend/nodeedge.c
@@ -0,0 +1,145 @@
+#include "nodeedge.h"
+#include <string.h>
+
+CNF * createCNF() {
+       CNF * cnf=ourmalloc(sizeof(CNF));
+       cnf->varcount=1;
+       cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
+       cnf->mask=cnf->capacity-1;
+       cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
+       cnf->size=0;
+       cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
+       return cnf;
+}
+
+void deleteCNF(CNF * cnf) {
+       ourfree(cnf);
+}
+
+void resizeCNF(CNF *cnf, uint newCapacity) {
+       Node **old_array=cnf->node_array;
+       Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
+       uint oldCapacity=cnf->capacity;
+       uint newMask=newCapacity-1;
+       for(uint i=0;i<oldCapacity;i++) {
+               Node *n=old_array[i];
+               uint hashCode=n->hashCode;
+               uint newindex=hashCode & newMask;
+               for(;;newindex=(newindex+1) & newMask) {
+                       if (new_array[newindex] == NULL) {
+                               new_array[newindex]=n;
+                               break;
+                       }
+               }
+       }
+       ourfree(old_array);
+       cnf->node_array=new_array;
+       cnf->capacity=newCapacity;
+       cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
+       cnf->mask=newMask;
+}
+
+Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
+       Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
+       memcpy(n->edges, edges, sizeof(Edge)*numEdges);
+       n->numEdges=numEdges;
+       n->flags.type=type;
+       n->hashCode=hashcode;
+       return n;
+}
+
+Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
+       if (cnf->size > cnf->maxsize) {
+               resizeCNF(cnf, cnf->capacity << 1);
+       }
+       uint hashvalue=hashNode(type, numEdges, edges);
+       uint mask=cnf->mask;
+       uint index=hashvalue & mask;
+       Node **n_ptr;
+       for(;;index=(index+1)&mask) {
+               n_ptr=&cnf->node_array[index];
+               if (*n_ptr!=NULL) {
+                       if ((*n_ptr)->hashCode==hashvalue) {
+                               if (compareNodes(*n_ptr, type, numEdges, edges)) {
+                                       Edge e={*n_ptr};
+                                       return e;
+                               }
+                       }
+               } else {
+                       break;
+               }
+       }
+       *n_ptr=allocNode(type, numEdges, edges, hashvalue);
+       Edge e={*n_ptr};
+       return e;
+}
+
+uint hashNode(NodeType type, uint numEdges, Edge * edges) {
+       uint hashvalue=type ^ numEdges;
+       for(uint i=0;i<numEdges;i++) {
+               hashvalue ^= (uint) edges[i].node_ptr;
+               hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
+       }
+       return (uint) hashvalue;
+}
+
+bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
+       if (node->flags.type!=type || node->numEdges != numEdges)
+               return false;
+       Edge *nodeedges=node->edges;
+       for(uint i=0;i<numEdges;i++) {
+               if (nodeedges[i].node_ptr!=edges[i].node_ptr)
+                       return false;
+       }
+       return true;
+}
+
+Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
+       Edge edgearray[numEdges];
+       
+       for(uint i=0; i<numEdges; i++) {
+               edgearray[i]=constraintNegate(edges[i]);
+       }
+       Edge eand=constraintAND(cnf, numEdges, edgearray);
+       return constraintNegate(eand);
+}
+
+Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
+       Edge lneg=constraintNegate(left);
+       Edge rneg=constraintNegate(right);
+       Edge eand=constraintAND2(cnf, left, right);
+       return constraintNegate(eand);
+}
+
+Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
+       return createNode(cnf, NodeType_AND, numEdges, edges);
+}
+
+Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
+       Edge edges[2]={left, right};
+       return createNode(cnf, NodeType_AND, 2, edges);
+}
+
+Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
+       Edge array[2];
+       array[0]=left;
+       array[1]=constraintNegate(right);
+       Edge eand=constraintAND(cnf, 2, array);
+       return constraintNegate(eand);
+}
+
+Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
+       Edge edges[]={left, right};
+       return createNode(cnf, NodeType_IFF, 2, edges);
+}
+
+Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
+       Edge edges[]={cond, thenedge, elseedge};
+       return createNode(cnf, NodeType_ITE, 3, edges);
+}
+
+Edge constraintNewVar(CNF *cnf) {
+       uint varnum=cnf->varcount++;
+       Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
+       return e;
+}

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
new file mode 100644 (file)
index 0000000..4a4f6d3
--- /dev/null
+++ b/src/Backend/nodeedge.h
@@ -0,0 +1,74 @@
+#ifndef NODEEDGE_H
+#define NODEEDGE_H
+#include "classlist.h"
+
+#define NEGATE_EDGE 1
+#define EDGE_IS_VAR_CONSTANT 2
+#define VAR_SHIFT 2
+
+struct Edge;
+typedef struct Edge Edge;
+
+struct Node;
+typedef struct Node Node;
+
+struct Edge {
+       Node * node_ptr;
+};
+
+enum NodeType {
+       NodeType_AND,
+       NodeType_ITE,
+       NodeType_IFF
+};
+
+typedef enum NodeType NodeType;
+
+struct NodeFlags {
+       NodeType type:2;
+};
+
+typedef struct NodeFlags NodeFlags;
+
+struct Node {
+       NodeFlags flags;
+       uint numEdges;
+       uint hashCode;
+       Edge edges[];
+};
+
+#define DEFAULT_CNF_ARRAY_SIZE 256
+#define LOAD_FACTOR 0.25
+
+struct CNF {
+       uint varcount;
+       uint capacity;
+       uint size;
+       uint mask;
+       uint maxsize;
+       Node ** node_array;
+};
+
+typedef struct CNF CNF;
+
+static inline Edge constraintNegate(Edge e) {
+       Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+       return enew;
+}
+
+uint hashNode(NodeType type, uint numEdges, Edge * edges);
+Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
+bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
+Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
+Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
+Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
+Edge constraintOR2(CNF * cnf, Edge left, Edge right);
+Edge constraintAND2(CNF * cnf, Edge left, Edge right);
+Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
+Edge constraintIFF(CNF * cnf, Edge left, Edge right);
+Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
+Edge constraintNewVar(CNF *cnf);
+
+Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
+Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
+#endif