src/Backend/nodeedge.c

   1 #include "nodeedge.h"
   2 #include <string.h>
   3
   4 CNF * createCNF() {
   5         CNF * cnf=ourmalloc(sizeof(CNF));
   6         cnf->varcount=1;
   7         cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
   8         cnf->mask=cnf->capacity-1;
   9         cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
  10         cnf->size=0;
  11         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  12         return cnf;
  13 }
  14
  15 void deleteCNF(CNF * cnf) {
  16         ourfree(cnf);
  17 }
  18
  19 void resizeCNF(CNF *cnf, uint newCapacity) {
  20         Node **old_array=cnf->node_array;
  21         Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
  22         uint oldCapacity=cnf->capacity;
  23         uint newMask=newCapacity-1;
  24         for(uint i=0;i<oldCapacity;i++) {
  25                 Node *n=old_array[i];
  26                 uint hashCode=n->hashCode;
  27                 uint newindex=hashCode & newMask;
  28                 for(;;newindex=(newindex+1) & newMask) {
  29                         if (new_array[newindex] == NULL) {
  30                                 new_array[newindex]=n;
  31                                 break;
  32                         }
  33                 }
  34         }
  35         ourfree(old_array);
  36         cnf->node_array=new_array;
  37         cnf->capacity=newCapacity;
  38         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  39         cnf->mask=newMask;
  40 }
  41
  42 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
  43         Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
  44         memcpy(n->edges, edges, sizeof(Edge)*numEdges);
  45         n->numEdges=numEdges;
  46         n->flags.type=type;
  47         n->hashCode=hashcode;
  48         return n;
  49 }
  50
  51 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
  52         if (cnf->size > cnf->maxsize) {
  53                 resizeCNF(cnf, cnf->capacity << 1);
  54         }
  55         uint hashvalue=hashNode(type, numEdges, edges);
  56         uint mask=cnf->mask;
  57         uint index=hashvalue & mask;
  58         Node **n_ptr;
  59         for(;;index=(index+1)&mask) {
  60                 n_ptr=&cnf->node_array[index];
  61                 if (*n_ptr!=NULL) {
  62                         if ((*n_ptr)->hashCode==hashvalue) {
  63                                 if (compareNodes(*n_ptr, type, numEdges, edges)) {
  64                                         Edge e={*n_ptr};
  65                                         return e;
  66                                 }
  67                         }
  68                 } else {
  69                         break;
  70                 }
  71         }
  72         *n_ptr=allocNode(type, numEdges, edges, hashvalue);
  73         Edge e={*n_ptr};
  74         return e;
  75 }
  76
  77 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
  78         uint hashvalue=type ^ numEdges;
  79         for(uint i=0;i<numEdges;i++) {
  80                 hashvalue ^= (uint) edges[i].node_ptr;
  81                 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
  82         }
  83         return (uint) hashvalue;
  84 }
  85
  86 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
  87         if (node->flags.type!=type || node->numEdges != numEdges)
  88                 return false;
  89         Edge *nodeedges=node->edges;
  90         for(uint i=0;i<numEdges;i++) {
  91                 if (nodeedges[i].node_ptr!=edges[i].node_ptr)
  92                         return false;
  93         }
  94         return true;
  95 }
  96
  97 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
  98         Edge edgearray[numEdges];
  99
 100         for(uint i=0; i<numEdges; i++) {
 101                 edgearray[i]=constraintNegate(edges[i]);
 102         }
 103         Edge eand=constraintAND(cnf, numEdges, edgearray);
 104         return constraintNegate(eand);
 105 }
 106
 107 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
 108         Edge lneg=constraintNegate(left);
 109         Edge rneg=constraintNegate(right);
 110         Edge eand=constraintAND2(cnf, left, right);
 111         return constraintNegate(eand);
 112 }
 113
 114 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 115         return createNode(cnf, NodeType_AND, numEdges, edges);
 116 }
 117
 118 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
 119         Edge edges[2]={left, right};
 120         return createNode(cnf, NodeType_AND, 2, edges);
 121 }
 122
 123 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 124         Edge array[2];
 125         array[0]=left;
 126         array[1]=constraintNegate(right);
 127         Edge eand=constraintAND(cnf, 2, array);
 128         return constraintNegate(eand);
 129 }
 130
 131 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
 132         Edge edges[]={left, right};
 133         return createNode(cnf, NodeType_IFF, 2, edges);
 134 }
 135
 136 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 137         Edge edges[]={cond, thenedge, elseedge};
 138         return createNode(cnf, NodeType_ITE, 3, edges);
 139 }
 140
 141 Edge constraintNewVar(CNF *cnf) {
 142         uint varnum=cnf->varcount++;
 143         Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 144         return e;
 145 }