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