src/Backend/nodeedge.c

   1 #include "nodeedge.h"
   2 #include <string.h>
   3 #include <stdlib.h>
   4
   5 CNF * createCNF() {
   6         CNF * cnf=ourmalloc(sizeof(CNF));
   7         cnf->varcount=1;
   8         cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
   9         cnf->mask=cnf->capacity-1;
  10         cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
  11         cnf->size=0;
  12         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  13         return cnf;
  14 }
  15
  16 void deleteCNF(CNF * cnf) {
  17         for(uint i=0;i<cnf->capacity;i++) {
  18                 Node *n=cnf->node_array[i];
  19                 if (n!=NULL)
  20                         ourfree(n);
  21         }
  22         ourfree(cnf->node_array);
  23         ourfree(cnf);
  24 }
  25
  26 void resizeCNF(CNF *cnf, uint newCapacity) {
  27         Node **old_array=cnf->node_array;
  28         Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
  29         uint oldCapacity=cnf->capacity;
  30         uint newMask=newCapacity-1;
  31         for(uint i=0;i<oldCapacity;i++) {
  32                 Node *n=old_array[i];
  33                 uint hashCode=n->hashCode;
  34                 uint newindex=hashCode & newMask;
  35                 for(;;newindex=(newindex+1) & newMask) {
  36                         if (new_array[newindex] == NULL) {
  37                                 new_array[newindex]=n;
  38                                 break;
  39                         }
  40                 }
  41         }
  42         ourfree(old_array);
  43         cnf->node_array=new_array;
  44         cnf->capacity=newCapacity;
  45         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  46         cnf->mask=newMask;
  47 }
  48
  49 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
  50         Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
  51         memcpy(n->edges, edges, sizeof(Edge)*numEdges);
  52         n->numEdges=numEdges;
  53         n->flags.type=type;
  54         n->hashCode=hashcode;
  55         return n;
  56 }
  57
  58 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
  59         if (cnf->size > cnf->maxsize) {
  60                 resizeCNF(cnf, cnf->capacity << 1);
  61         }
  62         uint hashvalue=hashNode(type, numEdges, edges);
  63         uint mask=cnf->mask;
  64         uint index=hashvalue & mask;
  65         Node **n_ptr;
  66         for(;;index=(index+1)&mask) {
  67                 n_ptr=&cnf->node_array[index];
  68                 if (*n_ptr!=NULL) {
  69                         if ((*n_ptr)->hashCode==hashvalue) {
  70                                 if (compareNodes(*n_ptr, type, numEdges, edges)) {
  71                                         Edge e={*n_ptr};
  72                                         return e;
  73                                 }
  74                         }
  75                 } else {
  76                         break;
  77                 }
  78         }
  79         *n_ptr=allocNode(type, numEdges, edges, hashvalue);
  80         Edge e={*n_ptr};
  81         return e;
  82 }
  83
  84 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
  85         uint hashvalue=type ^ numEdges;
  86         for(uint i=0;i<numEdges;i++) {
  87                 hashvalue ^= (uint) edges[i].node_ptr;
  88                 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
  89         }
  90         return (uint) hashvalue;
  91 }
  92
  93 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
  94         if (node->flags.type!=type || node->numEdges != numEdges)
  95                 return false;
  96         Edge *nodeedges=node->edges;
  97         for(uint i=0;i<numEdges;i++) {
  98                 if (!equalsEdge(nodeedges[i], edges[i]))
  99                         return false;
 100         }
 101         return true;
 102 }
 103
 104 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
 105         Edge edgearray[numEdges];
 106
 107         for(uint i=0; i<numEdges; i++) {
 108                 edgearray[i]=constraintNegate(edges[i]);
 109         }
 110         Edge eand=constraintAND(cnf, numEdges, edgearray);
 111         return constraintNegate(eand);
 112 }
 113
 114 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
 115         Edge lneg=constraintNegate(left);
 116         Edge rneg=constraintNegate(right);
 117         Edge eand=constraintAND2(cnf, left, right);
 118         return constraintNegate(eand);
 119 }
 120
 121 int comparefunction(const Edge * e1, const Edge * e2) {
 122         return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
 123 }
 124
 125 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 126         qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
 127         int initindex=0;
 128         while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
 129                 initindex++;
 130
 131         uint remainSize=numEdges-initindex;
 132
 133         if (remainSize == 0)
 134                 return E_True;
 135         else if (remainSize == 1)
 136                 return edges[initindex];
 137         else if (equalsEdge(edges[initindex], E_False))
 138                 return E_False;
 139
 140         /** De-duplicate array */
 141         uint lowindex=0;
 142         edges[lowindex++]=edges[initindex++];
 143
 144         for(;initindex<numEdges;initindex++) {
 145                 Edge e1=edges[lowindex];
 146                 Edge e2=edges[initindex];
 147                 if (sameNodeVarEdge(e1, e2)) {
 148                         if (!sameSignEdge(e1, e2)) {
 149                                 return E_False;
 150                         }
 151                 } else
 152                         edges[lowindex++]=edges[initindex];
 153         }
 154         if (lowindex==1)
 155                 return edges[0];
 156
 157         if (enableMatching && lowindex==2 &&
 158                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 159                         getNodeType(edges[0]) == NodeType_AND &&
 160                         getNodeType(edges[1]) == NodeType_AND &&
 161                         getNodeSize(edges[0]) == 2 &&
 162                         getNodeSize(edges[1]) == 2) {
 163                 Edge * e0edges=getEdgeArray(edges[0]);
 164                 Edge * e1edges=getEdgeArray(edges[1]);
 165                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 166                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 167                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 168                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 169                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 170                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 171                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 172                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 173                 }
 174         }
 175
 176         return createNode(cnf, NodeType_AND, numEdges, edges);
 177 }
 178
 179 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
 180         Edge edges[2]={left, right};
 181         return constraintAND(cnf, 2, edges);
 182 }
 183
 184 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 185         Edge array[2];
 186         array[0]=left;
 187         array[1]=constraintNegate(right);
 188         Edge eand=constraintAND(cnf, 2, array);
 189         return constraintNegate(eand);
 190 }
 191
 192 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
 193         bool negate=sameSignEdge(left, right);
 194         Edge lpos=getNonNeg(left);
 195         Edge rpos=getNonNeg(right);
 196
 197         Edge e;
 198         if (equalsEdge(lpos, rpos)) {
 199                 e=E_True;
 200         } else if (ltEdge(lpos, rpos)) {
 201                 Edge edges[]={lpos, rpos};
 202                 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
 203         } else {
 204                 Edge edges[]={rpos, lpos};
 205                 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
 206         }
 207         if (negate)
 208                 e=constraintNegate(e);
 209         return e;
 210 }
 211
 212 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 213         if (isNegEdge(cond)) {
 214                 cond=constraintNegate(cond);
 215                 Edge tmp=thenedge;
 216                 thenedge=elseedge;
 217                 elseedge=tmp;
 218         }
 219
 220         bool negate = isNegEdge(thenedge);
 221         if (negate) {
 222                 thenedge=constraintNegate(thenedge);
 223                 elseedge=constraintNegate(elseedge);
 224         }
 225
 226         Edge result;
 227         if (equalsEdge(cond, E_True)) {
 228                 result=thenedge;
 229         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 230                 result=constraintOR(cnf,  2, (Edge[]) {cond, elseedge});
 231         }       else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 232                 result=constraintIMPLIES(cnf, cond, thenedge);
 233         } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
 234                 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
 235         } else if (equalsEdge(thenedge, elseedge)) {
 236                 result=thenedge;
 237         } else if (sameNodeOppSign(thenedge, elseedge)) {
 238                 if (ltEdge(cond, thenedge)) {
 239                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
 240                 } else {
 241                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
 242                 }
 243         } else {
 244                 Edge edges[]={cond, thenedge, elseedge};
 245                 result=createNode(cnf, NodeType_ITE, 3, edges);
 246         }
 247         if (negate)
 248                 result=constraintNegate(result);
 249         return result;
 250 }
 251
 252 Edge constraintNewVar(CNF *cnf) {
 253         uint varnum=cnf->varcount++;
 254         Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 255         return e;
 256 }