src/Backend/nodeedge.c

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