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