src/Backend/nodeedge.c

   1 #include "nodeedge.h"
   2 #include <string.h>
   3 #include <stdlib.h>
   4
   5 VectorImpl(Edge, Edge, 16)
   6
   7 CNF * createCNF() {
   8         CNF * cnf=ourmalloc(sizeof(CNF));
   9         cnf->varcount=1;
  10         cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
  11         cnf->mask=cnf->capacity-1;
  12         cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
  13         cnf->size=0;
  14         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  15         cnf->enableMatching=true;
  16         allocInlineDefVectorEdge(& cnf->constraints);
  17  return cnf;
  18 }
  19
  20 void deleteCNF(CNF * cnf) {
  21         for(uint i=0;i<cnf->capacity;i++) {
  22                 Node *n=cnf->node_array[i];
  23                 if (n!=NULL)
  24                         ourfree(n);
  25         }
  26         deleteVectorArrayEdge(& cnf->constraints);
  27         ourfree(cnf->node_array);
  28         ourfree(cnf);
  29 }
  30
  31 void resizeCNF(CNF *cnf, uint newCapacity) {
  32         Node **old_array=cnf->node_array;
  33         Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
  34         uint oldCapacity=cnf->capacity;
  35         uint newMask=newCapacity-1;
  36         for(uint i=0;i<oldCapacity;i++) {
  37                 Node *n=old_array[i];
  38                 uint hashCode=n->hashCode;
  39                 uint newindex=hashCode & newMask;
  40                 for(;;newindex=(newindex+1) & newMask) {
  41                         if (new_array[newindex] == NULL) {
  42                                 new_array[newindex]=n;
  43                                 break;
  44                         }
  45                 }
  46         }
  47         ourfree(old_array);
  48         cnf->node_array=new_array;
  49         cnf->capacity=newCapacity;
  50         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  51         cnf->mask=newMask;
  52 }
  53
  54 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
  55         Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
  56         memcpy(n->edges, edges, sizeof(Edge)*numEdges);
  57         n->flags.type=type;
  58         n->flags.wasExpanded=0;
  59         n->numEdges=numEdges;
  60         n->hashCode=hashcode;
  61         n->intAnnot[0]=0;n->intAnnot[1]=0;
  62         n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
  63         return n;
  64 }
  65
  66 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
  67         if (cnf->size > cnf->maxsize) {
  68                 resizeCNF(cnf, cnf->capacity << 1);
  69         }
  70         uint hashvalue=hashNode(type, numEdges, edges);
  71         uint mask=cnf->mask;
  72         uint index=hashvalue & mask;
  73         Node **n_ptr;
  74         for(;;index=(index+1)&mask) {
  75                 n_ptr=&cnf->node_array[index];
  76                 if (*n_ptr!=NULL) {
  77                         if ((*n_ptr)->hashCode==hashvalue) {
  78                                 if (compareNodes(*n_ptr, type, numEdges, edges)) {
  79                                         Edge e={*n_ptr};
  80                                         return e;
  81                                 }
  82                         }
  83                 } else {
  84                         break;
  85                 }
  86         }
  87         *n_ptr=allocNode(type, numEdges, edges, hashvalue);
  88         Edge e={*n_ptr};
  89         return e;
  90 }
  91
  92 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
  93         uint hashvalue=type ^ numEdges;
  94         for(uint i=0;i<numEdges;i++) {
  95                 hashvalue ^= (uint) edges[i].node_ptr;
  96                 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
  97         }
  98         return (uint) hashvalue;
  99 }
 100
 101 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
 102         if (node->flags.type!=type || node->numEdges != numEdges)
 103                 return false;
 104         Edge *nodeedges=node->edges;
 105         for(uint i=0;i<numEdges;i++) {
 106                 if (!equalsEdge(nodeedges[i], edges[i]))
 107                         return false;
 108         }
 109         return true;
 110 }
 111
 112 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
 113         Edge edgearray[numEdges];
 114
 115         for(uint i=0; i<numEdges; i++) {
 116                 edgearray[i]=constraintNegate(edges[i]);
 117         }
 118         Edge eand=constraintAND(cnf, numEdges, edgearray);
 119         return constraintNegate(eand);
 120 }
 121
 122 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
 123         Edge lneg=constraintNegate(left);
 124         Edge rneg=constraintNegate(right);
 125         Edge eand=constraintAND2(cnf, left, right);
 126         return constraintNegate(eand);
 127 }
 128
 129 int comparefunction(const Edge * e1, const Edge * e2) {
 130         return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
 131 }
 132
 133 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 134         qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
 135         int initindex=0;
 136         while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
 137                 initindex++;
 138
 139         uint remainSize=numEdges-initindex;
 140
 141         if (remainSize == 0)
 142                 return E_True;
 143         else if (remainSize == 1)
 144                 return edges[initindex];
 145         else if (equalsEdge(edges[initindex], E_False))
 146                 return E_False;
 147
 148         /** De-duplicate array */
 149         uint lowindex=0;
 150         edges[lowindex++]=edges[initindex++];
 151
 152         for(;initindex<numEdges;initindex++) {
 153                 Edge e1=edges[lowindex];
 154                 Edge e2=edges[initindex];
 155                 if (sameNodeVarEdge(e1, e2)) {
 156                         if (!sameSignEdge(e1, e2)) {
 157                                 return E_False;
 158                         }
 159                 } else
 160                         edges[lowindex++]=edges[initindex];
 161         }
 162         if (lowindex==1)
 163                 return edges[0];
 164
 165         if (cnf->enableMatching && lowindex==2 &&
 166                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 167                         getNodeType(edges[0]) == NodeType_AND &&
 168                         getNodeType(edges[1]) == NodeType_AND &&
 169                         getNodeSize(edges[0]) == 2 &&
 170                         getNodeSize(edges[1]) == 2) {
 171                 Edge * e0edges=getEdgeArray(edges[0]);
 172                 Edge * e1edges=getEdgeArray(edges[1]);
 173                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 174                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 175                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 176                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 177                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 178                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 179                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 180                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 181                 }
 182         }
 183
 184         return createNode(cnf, NodeType_AND, numEdges, edges);
 185 }
 186
 187 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
 188         Edge edges[2]={left, right};
 189         return constraintAND(cnf, 2, edges);
 190 }
 191
 192 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 193         Edge array[2];
 194         array[0]=left;
 195         array[1]=constraintNegate(right);
 196         Edge eand=constraintAND(cnf, 2, array);
 197         return constraintNegate(eand);
 198 }
 199
 200 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
 201         bool negate=sameSignEdge(left, right);
 202         Edge lpos=getNonNeg(left);
 203         Edge rpos=getNonNeg(right);
 204
 205         Edge e;
 206         if (equalsEdge(lpos, rpos)) {
 207                 e=E_True;
 208         } else if (ltEdge(lpos, rpos)) {
 209                 Edge edges[]={lpos, rpos};
 210                 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
 211         } else {
 212                 Edge edges[]={rpos, lpos};
 213                 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
 214         }
 215         if (negate)
 216                 e=constraintNegate(e);
 217         return e;
 218 }
 219
 220 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 221         if (isNegEdge(cond)) {
 222                 cond=constraintNegate(cond);
 223                 Edge tmp=thenedge;
 224                 thenedge=elseedge;
 225                 elseedge=tmp;
 226         }
 227
 228         bool negate = isNegEdge(thenedge);
 229         if (negate) {
 230                 thenedge=constraintNegate(thenedge);
 231                 elseedge=constraintNegate(elseedge);
 232         }
 233
 234         Edge result;
 235         if (equalsEdge(cond, E_True)) {
 236                 result=thenedge;
 237         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 238                 result=constraintOR(cnf,  2, (Edge[]) {cond, elseedge});
 239         }       else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 240                 result=constraintIMPLIES(cnf, cond, thenedge);
 241         } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
 242                 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
 243         } else if (equalsEdge(thenedge, elseedge)) {
 244                 result=thenedge;
 245         } else if (sameNodeOppSign(thenedge, elseedge)) {
 246                 if (ltEdge(cond, thenedge)) {
 247                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
 248                 } else {
 249                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
 250                 }
 251         } else {
 252                 Edge edges[]={cond, thenedge, elseedge};
 253                 result=createNode(cnf, NodeType_ITE, 3, edges);
 254         }
 255         if (negate)
 256                 result=constraintNegate(result);
 257         return result;
 258 }
 259
 260 void addConstraint(CNF *cnf, Edge constraint) {
 261         pushVectorEdge(&cnf->constraints, constraint);
 262 }
 263
 264 Edge constraintNewVar(CNF *cnf) {
 265         uint varnum=cnf->varcount++;
 266         Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 267         return e;
 268 }
 269
 270 void countPass(CNF *cnf) {
 271         uint numConstraints=getSizeVectorEdge(&cnf->constraints);
 272         VectorEdge *ve=allocDefVectorEdge();
 273         for(uint i=0; i<numConstraints;i++) {
 274                 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
 275         }
 276         deleteVectorEdge(ve);
 277 }
 278
 279 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
 280         //Skip constants and variables...
 281         if (edgeIsVarConst(e))
 282                 return;
 283
 284         clearVectorEdge(stack);pushVectorEdge(stack, e);
 285
 286         bool isMatching=cnf->enableMatching;
 287
 288         while(getSizeVectorEdge(stack) != 0) {
 289                 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
 290                 bool polarity=isNegEdge(e);
 291                 Node *n=getNodePtrFromEdge(e);
 292                 if (getExpanded(n,  polarity)) {
 293                         if (n->flags.type == NodeType_IFF ||
 294                                         n->flags.type == NodeType_ITE) {
 295                                 Edge pExp={n->ptrAnnot[polarity]};
 296                                 getNodePtrFromEdge(pExp)->intAnnot[0]++;
 297                         } else {
 298                                 n->intAnnot[polarity]++;
 299                         }
 300                 } else {
 301                         setExpanded(n, polarity); n->intAnnot[polarity]=1;
 302
 303                         if (n->flags.type == NodeType_ITE||
 304                                         n->flags.type == NodeType_IFF) {
 305                                 n->intAnnot[polarity]=0;
 306                                 Edge cond=n->edges[0];
 307                                 Edge thenedge=n->edges[1];
 308                                 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
 309                                 thenedge=constraintNegateIf(thenedge, !polarity);
 310                                 elseedge=constraintNegateIf(elseedge, !polarity);
 311                                 thenedge=constraintAND2(cnf, cond, thenedge);
 312                                 cond=constraintNegate(cond);
 313                                 elseedge=constraintAND2(cnf, cond, elseedge);
 314                                 thenedge=constraintNegate(thenedge);
 315                                 elseedge=constraintNegate(elseedge);
 316                                 cnf->enableMatching=false;
 317                                 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
 318                                 n->ptrAnnot[polarity]=succ1.node_ptr;
 319                                 cnf->enableMatching=isMatching;
 320                                 pushVectorEdge(stack, succ1);
 321                                 if (getExpanded(n, !polarity)) {
 322                                         Edge succ2={(Node *)n->ptrAnnot[!polarity]};
 323                                         Node *n1=getNodePtrFromEdge(succ1);
 324                                         Node *n2=getNodePtrFromEdge(succ2);
 325                                         n1->ptrAnnot[0]=succ2.node_ptr;
 326                                         n2->ptrAnnot[0]=succ1.node_ptr;
 327                                         n1->ptrAnnot[1]=succ2.node_ptr;
 328                                         n2->ptrAnnot[1]=succ1.node_ptr;
 329                                 }
 330                         } else {
 331                                 for (uint i=0;i<n->numEdges;i++) {
 332                                         Edge succ=n->edges[i];
 333                                         succ=constraintNegateIf(succ, polarity);
 334                                         if(!edgeIsVarConst(succ)) {
 335                                                 pushVectorEdge(stack, succ);
 336                                         }
 337                                 }
 338                         }
 339                 }
 340         }
 341 }