src/Backend/nodeedge.c

   1 #include "nodeedge.h"
   2 #include <string.h>
   3 #include <stdlib.h>
   4 #include "inc_solver.h"
   5 #include "cnfexpr.h"
   6
   7 /** Code ported from C++ BAT implementation of NICE-SAT */
   8
   9 VectorImpl(Edge, Edge, 16)
  10
  11 CNF * createCNF() {
  12         CNF * cnf=ourmalloc(sizeof(CNF));
  13         cnf->varcount=1;
  14         cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
  15         cnf->mask=cnf->capacity-1;
  16         cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
  17         cnf->size=0;
  18         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  19         cnf->enableMatching=true;
  20         allocInlineDefVectorEdge(& cnf->constraints);
  21         allocInlineDefVectorEdge(& cnf->args);
  22  return cnf;
  23 }
  24
  25 void deleteCNF(CNF * cnf) {
  26         for(uint i=0;i<cnf->capacity;i++) {
  27                 Node *n=cnf->node_array[i];
  28                 if (n!=NULL)
  29                         ourfree(n);
  30         }
  31         deleteVectorArrayEdge(& cnf->constraints);
  32         deleteVectorArrayEdge(& cnf->args);
  33         ourfree(cnf->node_array);
  34         ourfree(cnf);
  35 }
  36
  37 void resizeCNF(CNF *cnf, uint newCapacity) {
  38         Node **old_array=cnf->node_array;
  39         Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
  40         uint oldCapacity=cnf->capacity;
  41         uint newMask=newCapacity-1;
  42         for(uint i=0;i<oldCapacity;i++) {
  43                 Node *n=old_array[i];
  44                 uint hashCode=n->hashCode;
  45                 uint newindex=hashCode & newMask;
  46                 for(;;newindex=(newindex+1) & newMask) {
  47                         if (new_array[newindex] == NULL) {
  48                                 new_array[newindex]=n;
  49                                 break;
  50                         }
  51                 }
  52         }
  53         ourfree(old_array);
  54         cnf->node_array=new_array;
  55         cnf->capacity=newCapacity;
  56         cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
  57         cnf->mask=newMask;
  58 }
  59
  60 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
  61         Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
  62         memcpy(n->edges, edges, sizeof(Edge)*numEdges);
  63         n->flags.type=type;
  64         n->flags.wasExpanded=0;
  65         n->flags.cnfVisitedDown=0;
  66         n->flags.cnfVisitedUp=0;
  67         n->numEdges=numEdges;
  68         n->hashCode=hashcode;
  69         n->intAnnot[0]=0;n->intAnnot[1]=0;
  70         n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
  71         return n;
  72 }
  73
  74 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
  75         if (cnf->size > cnf->maxsize) {
  76                 resizeCNF(cnf, cnf->capacity << 1);
  77         }
  78         uint hashvalue=hashNode(type, numEdges, edges);
  79         uint mask=cnf->mask;
  80         uint index=hashvalue & mask;
  81         Node **n_ptr;
  82         for(;;index=(index+1)&mask) {
  83                 n_ptr=&cnf->node_array[index];
  84                 if (*n_ptr!=NULL) {
  85                         if ((*n_ptr)->hashCode==hashvalue) {
  86                                 if (compareNodes(*n_ptr, type, numEdges, edges)) {
  87                                         Edge e={*n_ptr};
  88                                         return e;
  89                                 }
  90                         }
  91                 } else {
  92                         break;
  93                 }
  94         }
  95         *n_ptr=allocNode(type, numEdges, edges, hashvalue);
  96         Edge e={*n_ptr};
  97         return e;
  98 }
  99
 100 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
 101         uint hashvalue=type ^ numEdges;
 102         for(uint i=0;i<numEdges;i++) {
 103                 hashvalue ^= (uint) edges[i].node_ptr;
 104                 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
 105         }
 106         return (uint) hashvalue;
 107 }
 108
 109 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
 110         if (node->flags.type!=type || node->numEdges != numEdges)
 111                 return false;
 112         Edge *nodeedges=node->edges;
 113         for(uint i=0;i<numEdges;i++) {
 114                 if (!equalsEdge(nodeedges[i], edges[i]))
 115                         return false;
 116         }
 117         return true;
 118 }
 119
 120 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
 121         Edge edgearray[numEdges];
 122
 123         for(uint i=0; i<numEdges; i++) {
 124                 edgearray[i]=constraintNegate(edges[i]);
 125         }
 126         Edge eand=constraintAND(cnf, numEdges, edgearray);
 127         return constraintNegate(eand);
 128 }
 129
 130 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
 131         Edge lneg=constraintNegate(left);
 132         Edge rneg=constraintNegate(right);
 133         Edge eand=constraintAND2(cnf, left, right);
 134         return constraintNegate(eand);
 135 }
 136
 137 int comparefunction(const Edge * e1, const Edge * e2) {
 138         return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
 139 }
 140
 141 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
 142         qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
 143         int initindex=0;
 144         while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
 145                 initindex++;
 146
 147         uint remainSize=numEdges-initindex;
 148
 149         if (remainSize == 0)
 150                 return E_True;
 151         else if (remainSize == 1)
 152                 return edges[initindex];
 153         else if (equalsEdge(edges[initindex], E_False))
 154                 return E_False;
 155
 156         /** De-duplicate array */
 157         uint lowindex=0;
 158         edges[lowindex++]=edges[initindex++];
 159
 160         for(;initindex<numEdges;initindex++) {
 161                 Edge e1=edges[lowindex];
 162                 Edge e2=edges[initindex];
 163                 if (sameNodeVarEdge(e1, e2)) {
 164                         if (!sameSignEdge(e1, e2)) {
 165                                 return E_False;
 166                         }
 167                 } else
 168                         edges[lowindex++]=edges[initindex];
 169         }
 170         if (lowindex==1)
 171                 return edges[0];
 172
 173         if (cnf->enableMatching && lowindex==2 &&
 174                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 175                         getNodeType(edges[0]) == NodeType_AND &&
 176                         getNodeType(edges[1]) == NodeType_AND &&
 177                         getNodeSize(edges[0]) == 2 &&
 178                         getNodeSize(edges[1]) == 2) {
 179                 Edge * e0edges=getEdgeArray(edges[0]);
 180                 Edge * e1edges=getEdgeArray(edges[1]);
 181                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 182                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 183                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 184                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 185                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 186                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 187                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 188                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 189                 }
 190         }
 191
 192         return createNode(cnf, NodeType_AND, numEdges, edges);
 193 }
 194
 195 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
 196         Edge edges[2]={left, right};
 197         return constraintAND(cnf, 2, edges);
 198 }
 199
 200 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 201         Edge array[2];
 202         array[0]=left;
 203         array[1]=constraintNegate(right);
 204         Edge eand=constraintAND(cnf, 2, array);
 205         return constraintNegate(eand);
 206 }
 207
 208 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
 209         bool negate=sameSignEdge(left, right);
 210         Edge lpos=getNonNeg(left);
 211         Edge rpos=getNonNeg(right);
 212
 213         Edge e;
 214         if (equalsEdge(lpos, rpos)) {
 215                 e=E_True;
 216         } else if (ltEdge(lpos, rpos)) {
 217                 Edge edges[]={lpos, rpos};
 218                 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
 219         } else {
 220                 Edge edges[]={rpos, lpos};
 221                 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
 222         }
 223         if (negate)
 224                 e=constraintNegate(e);
 225         return e;
 226 }
 227
 228 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
 229         if (isNegEdge(cond)) {
 230                 cond=constraintNegate(cond);
 231                 Edge tmp=thenedge;
 232                 thenedge=elseedge;
 233                 elseedge=tmp;
 234         }
 235
 236         bool negate = isNegEdge(thenedge);
 237         if (negate) {
 238                 thenedge=constraintNegate(thenedge);
 239                 elseedge=constraintNegate(elseedge);
 240         }
 241
 242         Edge result;
 243         if (equalsEdge(cond, E_True)) {
 244                 result=thenedge;
 245         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 246                 result=constraintOR(cnf,  2, (Edge[]) {cond, elseedge});
 247         }       else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 248                 result=constraintIMPLIES(cnf, cond, thenedge);
 249         } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
 250                 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
 251         } else if (equalsEdge(thenedge, elseedge)) {
 252                 result=thenedge;
 253         } else if (sameNodeOppSign(thenedge, elseedge)) {
 254                 if (ltEdge(cond, thenedge)) {
 255                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
 256                 } else {
 257                         result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
 258                 }
 259         } else {
 260                 Edge edges[]={cond, thenedge, elseedge};
 261                 result=createNode(cnf, NodeType_ITE, 3, edges);
 262         }
 263         if (negate)
 264                 result=constraintNegate(result);
 265         return result;
 266 }
 267
 268 void addConstraint(CNF *cnf, Edge constraint) {
 269         pushVectorEdge(&cnf->constraints, constraint);
 270 }
 271
 272 Edge constraintNewVar(CNF *cnf) {
 273         uint varnum=cnf->varcount++;
 274         Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 275         return e;
 276 }
 277
 278 void countPass(CNF *cnf) {
 279         uint numConstraints=getSizeVectorEdge(&cnf->constraints);
 280         VectorEdge *ve=allocDefVectorEdge();
 281         for(uint i=0; i<numConstraints;i++) {
 282                 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
 283         }
 284         deleteVectorEdge(ve);
 285 }
 286
 287 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
 288         //Skip constants and variables...
 289         if (edgeIsVarConst(e))
 290                 return;
 291
 292         clearVectorEdge(stack);pushVectorEdge(stack, e);
 293
 294         bool isMatching=cnf->enableMatching;
 295
 296         while(getSizeVectorEdge(stack) != 0) {
 297                 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
 298                 bool polarity=isNegEdge(e);
 299                 Node *n=getNodePtrFromEdge(e);
 300                 if (getExpanded(n,  polarity)) {
 301                         if (n->flags.type == NodeType_IFF ||
 302                                         n->flags.type == NodeType_ITE) {
 303                                 Edge pExp={n->ptrAnnot[polarity]};
 304                                 getNodePtrFromEdge(pExp)->intAnnot[0]++;
 305                         } else {
 306                                 n->intAnnot[polarity]++;
 307                         }
 308                 } else {
 309                         setExpanded(n, polarity); n->intAnnot[polarity]=1;
 310
 311                         if (n->flags.type == NodeType_ITE||
 312                                         n->flags.type == NodeType_IFF) {
 313                                 n->intAnnot[polarity]=0;
 314                                 Edge cond=n->edges[0];
 315                                 Edge thenedge=n->edges[1];
 316                                 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
 317                                 thenedge=constraintNegateIf(thenedge, !polarity);
 318                                 elseedge=constraintNegateIf(elseedge, !polarity);
 319                                 thenedge=constraintAND2(cnf, cond, thenedge);
 320                                 cond=constraintNegate(cond);
 321                                 elseedge=constraintAND2(cnf, cond, elseedge);
 322                                 thenedge=constraintNegate(thenedge);
 323                                 elseedge=constraintNegate(elseedge);
 324                                 cnf->enableMatching=false;
 325                                 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
 326                                 n->ptrAnnot[polarity]=succ1.node_ptr;
 327                                 cnf->enableMatching=isMatching;
 328                                 pushVectorEdge(stack, succ1);
 329                                 if (getExpanded(n, !polarity)) {
 330                                         Edge succ2={(Node *)n->ptrAnnot[!polarity]};
 331                                         Node *n1=getNodePtrFromEdge(succ1);
 332                                         Node *n2=getNodePtrFromEdge(succ2);
 333                                         n1->ptrAnnot[0]=succ2.node_ptr;
 334                                         n2->ptrAnnot[0]=succ1.node_ptr;
 335                                         n1->ptrAnnot[1]=succ2.node_ptr;
 336                                         n2->ptrAnnot[1]=succ1.node_ptr;
 337                                 }
 338                         } else {
 339                                 for (uint i=0;i<n->numEdges;i++) {
 340                                         Edge succ=n->edges[i];
 341                                         succ=constraintNegateIf(succ, polarity);
 342                                         if(!edgeIsVarConst(succ)) {
 343                                                 pushVectorEdge(stack, succ);
 344                                         }
 345                                 }
 346                         }
 347                 }
 348         }
 349 }
 350
 351 void convertPass(CNF *cnf, bool backtrackLit) {
 352         uint numConstraints=getSizeVectorEdge(&cnf->constraints);
 353         VectorEdge *ve=allocDefVectorEdge();
 354         for(uint i=0; i<numConstraints;i++) {
 355                 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
 356         }
 357         deleteVectorEdge(ve);
 358 }
 359
 360 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
 361         Node *nroot=getNodePtrFromEdge(root);
 362
 363         if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
 364                 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
 365         }
 366
 367         if (edgeIsConst(root)) {
 368                 if (isNegEdge(root)) {
 369                         //trivally unsat
 370                         Edge newvar=constraintNewVar(cnf);
 371                         Literal var=getEdgeVar(newvar);
 372                         Literal clause[] = {var, -var, 0};
 373                         addArrayClauseLiteral(cnf->solver, 3, clause);
 374                         return;
 375                 } else {
 376                         //trivially true
 377                         return;
 378                 }
 379         } else if (edgeIsVarConst(root)) {
 380                 Literal clause[] = { getEdgeVar(root), 0};
 381                 addArrayClauseLiteral(cnf->solver, 2, clause);
 382                 return;
 383         }
 384
 385         clearVectorEdge(stack);pushVectorEdge(stack, root);
 386         while(getSizeVectorEdge(stack)!=0) {
 387                 Edge e=lastVectorEdge(stack);
 388                 Node *n=getNodePtrFromEdge(e);
 389
 390                 if (edgeIsVarConst(e)) {
 391                         popVectorEdge(stack);
 392                         continue;
 393                 } else if (n->flags.type==NodeType_ITE ||
 394                                                          n->flags.type==NodeType_IFF) {
 395                         popVectorEdge(stack);
 396                         pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
 397                         pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
 398                         continue;
 399                 }
 400
 401                 bool needPos = (n->intAnnot[0] > 0);
 402                 bool needNeg = (n->intAnnot[1] > 0);
 403                 if ((!needPos || n->flags.cnfVisitedUp & 1) ||
 404                                 (!needNeg || n->flags.cnfVisitedUp & 2)) {
 405                         popVectorEdge(stack);
 406                 } else if ((needPos && !n->flags.cnfVisitedDown & 1) ||
 407                                                          (needNeg && !n->flags.cnfVisitedDown & 2)) {
 408                         if (needPos)
 409                                 n->flags.cnfVisitedDown|=1;
 410                         if (needNeg)
 411                                 n->flags.cnfVisitedDown|=2;
 412                         for(uint i=0; i<n->numEdges; i++) {
 413                                 Edge arg=n->edges[i];
 414                                 arg=constraintNegateIf(arg, isNegEdge(e));
 415                                 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
 416                         }
 417                 } else {
 418                         popVectorEdge(stack);
 419                         produceCNF(cnf, e);
 420                 }
 421         }
 422         CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
 423         if (isProxy(cnfExp)) {
 424                 //solver.add(getProxy(cnfExp))
 425         } else if (backtrackLit) {
 426                 //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
 427         } else {
 428                 //solver.add(*cnfExp);
 429         }
 430
 431         if (!((intptr_t) cnfExp & 1)) {
 432                 //free rootExp
 433                 nroot->ptrAnnot[isNegEdge(root)] = NULL;
 434         }
 435 }
 436
 437
 438 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
 439         Literal l = 0;
 440         Node * n = getNodePtrFromEdge(e);
 441
 442         if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
 443                 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
 444                 if (isProxy(otherExp))
 445                         l = -getProxy(otherExp);
 446         } else {
 447                 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
 448                 Node * nsemNeg=getNodePtrFromEdge(semNeg);
 449                 if (nsemNeg != NULL) {
 450                         if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
 451                                 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
 452                                 if (isProxy(otherExp))
 453                                         l = -getProxy(otherExp);
 454                         } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
 455                                 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
 456                                 if (isProxy(otherExp))
 457                                         l = getProxy(otherExp);
 458                         }
 459                 }
 460         }
 461
 462         if (l == 0) {
 463                 Edge newvar = constraintNewVar(cnf);
 464                 l = getEdgeVar(newvar);
 465         }
 466         // Output the constraints on the auxiliary variable
 467         constrainCNF(cnf, l, exp);
 468         deleteCNFExpr(exp);
 469
 470         n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
 471
 472         return l;
 473 }
 474
 475 //DONE
 476 void produceCNF(CNF * cnf, Edge e) {
 477         CNFExpr* expPos = NULL;
 478         CNFExpr* expNeg = NULL;
 479         Node *n = getNodePtrFromEdge(e);
 480
 481         if (n->intAnnot[0] > 0) {
 482                 expPos = produceConjunction(cnf, e);
 483         }
 484
 485         if (n->intAnnot[1]  > 0) {
 486                 expNeg = produceDisjunction(cnf, e);
 487         }
 488
 489         /// @todo Propagate constants across semantic negations (this can
 490         /// be done similarly to the calls to propagate shown below).  The
 491         /// trick here is that we need to figure out how to get the
 492         /// semantic negation pointers, and ensure that they can have CNF
 493         /// produced for them at the right point
 494         ///
 495         /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
 496
 497         // propagate from positive to negative, negative to positive
 498         propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
 499
 500         // The polarity heuristic entails visiting the discovery polarity first
 501         if (isPosEdge(e)) {
 502                 saveCNF(cnf, expPos, e, false);
 503                 saveCNF(cnf, expNeg, e, true);
 504         } else {
 505                 saveCNF(cnf, expNeg, e, true);
 506                 saveCNF(cnf, expPos, e, false);
 507         }
 508 }
 509
 510 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
 511         if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
 512                 if (dest == NULL) {
 513                         dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 514                 } else if (isProxy(dest)) {
 515                         bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 516                         if (alwaysTrue) {
 517                                 Literal clause[] = {getProxy(dest), 0};
 518                                 addArrayClauseLiteral(cnf->solver, 2, clause);
 519                         } else {
 520                                 Literal clause[] = {-getProxy(dest), 0};
 521                                 addArrayClauseLiteral(cnf->solver, 2, clause);
 522                         }
 523
 524                         dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 525                 } else {
 526                         clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 527                 }
 528                 return true;
 529         }
 530         return false;
 531 }
 532
 533 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
 534         Node *n=getNodePtrFromEdge(e);
 535         n->flags.cnfVisitedUp |= (1 << sign);
 536         if (exp == NULL || isProxy(exp)) return;
 537
 538         if (exp->litSize == 1) {
 539                 Literal l = getLiteralLitVector(&exp->singletons, 0);
 540                 deleteCNFExpr(exp);
 541                 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
 542         } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
 543                 introProxy(cnf, e, exp, sign);
 544         } else {
 545                 n->ptrAnnot[sign] = exp;
 546         }
 547 }
 548
 549 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp) {
 550         if (alwaysTrueCNF(exp)) {
 551                 return;
 552         } else if (alwaysFalseCNF(exp)) {
 553                 Literal clause[] = {-l, 0};
 554                 addArrayClauseLiteral(cnf->solver, 2, clause);
 555                 return;
 556         }
 557         //FIXME
 558
 559 }
 560
 561 void outputCNF(CNF *cnf, CNFExpr *exp) {
 562
 563 }
 564
 565 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
 566         clearVectorEdge(&cnf->args);
 567
 568         *largestEdge = (Edge) {(Node*) NULL};
 569         CNFExpr* largest = NULL;
 570         Node *n=getNodePtrFromEdge(e);
 571         int i = n->numEdges;
 572         while (i != 0) {
 573                 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
 574                 Node * narg = getNodePtrFromEdge(arg);
 575
 576                 if (edgeIsVarConst(arg)) {
 577                         pushVectorEdge(&cnf->args, arg);
 578                         continue;
 579                 }
 580
 581                 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
 582                         arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
 583                 }
 584
 585                 if (narg->intAnnot[isNegEdge(arg)] == 1) {
 586                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 587                         if (!isProxy(argExp)) {
 588                                 if (largest == NULL) {
 589                                         largest = argExp;
 590                                         * largestEdge = arg;
 591                                         continue;
 592                                 } else if (argExp->litSize > largest->litSize) {
 593                                         pushVectorEdge(&cnf->args, *largestEdge);
 594                                         largest = argExp;
 595                                         * largestEdge = arg;
 596                                         continue;
 597                                 }
 598                         }
 599                 }
 600                 pushVectorEdge(&cnf->args, arg);
 601         }
 602
 603         if (largest != NULL) {
 604                 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
 605                 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
 606         }
 607
 608         return largest;
 609 }
 610
 611
 612 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 613         Edge largestEdge;
 614
 615         CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
 616         if (accum == NULL) accum = allocCNFExprBool(true);
 617
 618         int i = getSizeVectorEdge(&cnf->args);
 619         while (i != 0) {
 620                 Edge arg = getVectorEdge(&cnf->args, --i);
 621                 if (edgeIsVarConst(arg)) {
 622                         conjoinCNFLit(accum, getEdgeVar(arg));
 623                 } else {
 624                         Node *narg=getNodePtrFromEdge(arg);
 625                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 626
 627                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 628                         if (isProxy(argExp)) { // variable has been introduced
 629                                 conjoinCNFLit(accum, getProxy(argExp));
 630                         } else {
 631                                 conjoinCNFExpr(accum, argExp, destroy);
 632                                 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 633                         }
 634                 }
 635         }
 636
 637         return accum;
 638 }
 639
 640 #define CLAUSE_MAX 3
 641
 642 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
 643         Edge largestEdge;
 644         CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
 645         if (accum == NULL)
 646                 accum = allocCNFExprBool(false);
 647
 648         // This is necessary to check to make sure that we don't start out
 649         // with an accumulator that is "too large".
 650
 651         /// @todo Strictly speaking, introProxy doesn't *need* to free
 652         /// memory, then this wouldn't have to reallocate CNFExpr
 653
 654         /// @todo When this call to introProxy is made, the semantic
 655         /// negation pointer will have been destroyed.  Thus, it will not
 656         /// be possible to use the correct proxy.  That should be fixed.
 657
 658         // at this point, we will either have NULL, or a destructible expression
 659         if (getClauseSizeCNF(accum) > CLAUSE_MAX)
 660                 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
 661
 662         int i = getSizeVectorEdge(&cnf->args);
 663         while (i != 0) {
 664                 Edge arg=getVectorEdge(&cnf->args, --i);
 665                 Node *narg=getNodePtrFromEdge(arg);
 666                 if (edgeIsVarConst(arg)) {
 667                         disjoinCNFLit(accum, getEdgeVar(arg));
 668                 } else {
 669                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 670
 671                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 672                         if (isProxy(argExp)) { // variable has been introduced
 673                                 disjoinCNFLit(accum, getProxy(argExp));
 674                         } else if (argExp->litSize == 0) {
 675                                 disjoinCNFExpr(accum, argExp, destroy);
 676                         } else {
 677                                 // check to see if we should introduce a proxy
 678                                 int aL = accum->litSize;      // lits in accum
 679                                 int eL = argExp->litSize;     // lits in argument
 680                                 int aC = getClauseSizeCNF(accum);   // clauses in accum
 681                                 int eC = getClauseSizeCNF(argExp);  // clauses in argument
 682
 683                                 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
 684                                         disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
 685                                 } else {
 686                                         disjoinCNFExpr(accum, argExp, destroy);
 687                                         if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 688                                 }
 689                         }
 690                 }
 691         }
 692
 693         return accum;
 694 }