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);
 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                                 n->intAnnot[polarity]=1;
 340                                 for (uint i=0;i<n->numEdges;i++) {
 341                                         Edge succ=n->edges[i];
 342                                         succ=constraintNegateIf(succ, polarity);
 343                                         if(!edgeIsVarConst(succ)) {
 344                                                 pushVectorEdge(stack, succ);
 345                                         }
 346                                 }
 347                         }
 348                 }
 349         }
 350 }
 351
 352 void convertPass(CNF *cnf, bool backtrackLit) {
 353         uint numConstraints=getSizeVectorEdge(&cnf->constraints);
 354         VectorEdge *ve=allocDefVectorEdge();
 355         for(uint i=0; i<numConstraints;i++) {
 356                 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
 357         }
 358         deleteVectorEdge(ve);
 359 }
 360
 361 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
 362         Node *nroot=getNodePtrFromEdge(root);
 363
 364         if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
 365                 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
 366         }
 367
 368         if (edgeIsConst(root)) {
 369                 if (isNegEdge(root)) {
 370                         //trivally unsat
 371                         Edge newvar=constraintNewVar(cnf);
 372                         Literal var=getEdgeVar(newvar);
 373                         Literal clause[] = {var};
 374                         addArrayClauseLiteral(cnf->solver, 1, clause);
 375                         clause[0]=-var;
 376                         addArrayClauseLiteral(cnf->solver, 1, clause);
 377                         return;
 378                 } else {
 379                         //trivially true
 380                         return;
 381                 }
 382         } else if (edgeIsVarConst(root)) {
 383                 Literal clause[] = { getEdgeVar(root)};
 384                 addArrayClauseLiteral(cnf->solver, 1, clause);
 385                 return;
 386         }
 387
 388         clearVectorEdge(stack);pushVectorEdge(stack, root);
 389         while(getSizeVectorEdge(stack)!=0) {
 390                 Edge e=lastVectorEdge(stack);
 391                 Node *n=getNodePtrFromEdge(e);
 392
 393                 if (edgeIsVarConst(e)) {
 394                         popVectorEdge(stack);
 395                         continue;
 396                 } else if (n->flags.type==NodeType_ITE ||
 397                                                          n->flags.type==NodeType_IFF) {
 398                         popVectorEdge(stack);
 399                         if (n->ptrAnnot[0]!=NULL)
 400                                 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
 401                         if (n->ptrAnnot[1]!=NULL)
 402                                 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
 403                         continue;
 404                 }
 405
 406                 bool needPos = (n->intAnnot[0] > 0);
 407                 bool needNeg = (n->intAnnot[1] > 0);
 408                 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
 409                                 (!needNeg || n->flags.cnfVisitedUp & 2)) {
 410                         popVectorEdge(stack);
 411                 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
 412                                                          (needNeg && !(n->flags.cnfVisitedDown & 2))) {
 413                         if (needPos)
 414                                 n->flags.cnfVisitedDown|=1;
 415                         if (needNeg)
 416                                 n->flags.cnfVisitedDown|=2;
 417                         for(uint i=0; i<n->numEdges; i++) {
 418                                 Edge arg=n->edges[i];
 419                                 arg=constraintNegateIf(arg, isNegEdge(e));
 420                                 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
 421                         }
 422                 } else {
 423                         popVectorEdge(stack);
 424                         produceCNF(cnf, e);
 425                 }
 426         }
 427         CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
 428         if (isProxy(cnfExp)) {
 429                 Literal l=getProxy(cnfExp);
 430                 Literal clause[] = {l};
 431                 addArrayClauseLiteral(cnf->solver, 1, clause);
 432         } else if (backtrackLit) {
 433                 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
 434                 Literal clause[] = {l};
 435                 addArrayClauseLiteral(cnf->solver, 1, clause);
 436         } else {
 437                 outputCNF(cnf, cnfExp);
 438         }
 439
 440         if (!((intptr_t) cnfExp & 1)) {
 441                 deleteCNFExpr(cnfExp);
 442                 nroot->ptrAnnot[isNegEdge(root)] = NULL;
 443         }
 444 }
 445
 446
 447 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
 448         Literal l = 0;
 449         Node * n = getNodePtrFromEdge(e);
 450
 451         if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
 452                 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
 453                 if (isProxy(otherExp))
 454                         l = -getProxy(otherExp);
 455         } else {
 456                 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
 457                 Node * nsemNeg=getNodePtrFromEdge(semNeg);
 458                 if (nsemNeg != NULL) {
 459                         if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
 460                                 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
 461                                 if (isProxy(otherExp))
 462                                         l = -getProxy(otherExp);
 463                         } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
 464                                 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
 465                                 if (isProxy(otherExp))
 466                                         l = getProxy(otherExp);
 467                         }
 468                 }
 469         }
 470
 471         if (l == 0) {
 472                 Edge newvar = constraintNewVar(cnf);
 473                 l = getEdgeVar(newvar);
 474         }
 475         // Output the constraints on the auxiliary variable
 476         constrainCNF(cnf, l, exp);
 477         deleteCNFExpr(exp);
 478
 479         n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
 480
 481         return l;
 482 }
 483
 484 void produceCNF(CNF * cnf, Edge e) {
 485         CNFExpr* expPos = NULL;
 486         CNFExpr* expNeg = NULL;
 487         Node *n = getNodePtrFromEdge(e);
 488
 489         if (n->intAnnot[0] > 0) {
 490                 expPos = produceConjunction(cnf, e);
 491         }
 492
 493         if (n->intAnnot[1]  > 0) {
 494                 expNeg = produceDisjunction(cnf, e);
 495         }
 496
 497         /// @todo Propagate constants across semantic negations (this can
 498         /// be done similarly to the calls to propagate shown below).  The
 499         /// trick here is that we need to figure out how to get the
 500         /// semantic negation pointers, and ensure that they can have CNF
 501         /// produced for them at the right point
 502         ///
 503         /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
 504
 505         // propagate from positive to negative, negative to positive
 506         propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
 507
 508         // The polarity heuristic entails visiting the discovery polarity first
 509         if (isPosEdge(e)) {
 510                 saveCNF(cnf, expPos, e, false);
 511                 saveCNF(cnf, expNeg, e, true);
 512         } else {
 513                 saveCNF(cnf, expNeg, e, true);
 514                 saveCNF(cnf, expPos, e, false);
 515         }
 516 }
 517
 518 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
 519         if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
 520                 if (dest == NULL) {
 521                         dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 522                 } else if (isProxy(dest)) {
 523                         bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 524                         if (alwaysTrue) {
 525                                 Literal clause[] = {getProxy(dest)};
 526                                 addArrayClauseLiteral(cnf->solver, 1, clause);
 527                         } else {
 528                                 Literal clause[] = {-getProxy(dest)};
 529                                 addArrayClauseLiteral(cnf->solver, 1, clause);
 530                         }
 531
 532                         dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 533                 } else {
 534                         clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 535                 }
 536                 return true;
 537         }
 538         return false;
 539 }
 540
 541 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
 542         Node *n=getNodePtrFromEdge(e);
 543         n->flags.cnfVisitedUp |= (1 << sign);
 544         if (exp == NULL || isProxy(exp)) return;
 545
 546         if (exp->litSize == 1) {
 547                 Literal l = getLiteralLitVector(&exp->singletons, 0);
 548                 deleteCNFExpr(exp);
 549                 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
 550         } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
 551                 introProxy(cnf, e, exp, sign);
 552         } else {
 553                 n->ptrAnnot[sign] = exp;
 554         }
 555 }
 556
 557 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
 558         if (alwaysTrueCNF(expr)) {
 559                 return;
 560         } else if (alwaysFalseCNF(expr)) {
 561                 Literal clause[] = {-lcond};
 562                 addArrayClauseLiteral(cnf->solver, 1, clause);
 563                 return;
 564         }
 565
 566         for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 567                 Literal l=getLiteralLitVector(&expr->singletons,i);
 568                 Literal clause[] = {-lcond, l};
 569                 addArrayClauseLiteral(cnf->solver, 1, clause);
 570         }
 571         for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 572                 LitVector *lv=getVectorLitVector(&expr->clauses,i);
 573                 addClauseLiteral(cnf->solver, -lcond); //Add first literal
 574                 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
 575         }
 576 }
 577
 578 void outputCNF(CNF *cnf, CNFExpr *expr) {
 579         for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 580                 Literal l=getLiteralLitVector(&expr->singletons,i);
 581                 Literal clause[] = {l};
 582                 addArrayClauseLiteral(cnf->solver, 1, clause);
 583         }
 584         for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 585                 LitVector *lv=getVectorLitVector(&expr->clauses,i);
 586                 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
 587         }
 588 }
 589
 590 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
 591         clearVectorEdge(&cnf->args);
 592
 593         *largestEdge = (Edge) {(Node*) NULL};
 594         CNFExpr* largest = NULL;
 595         Node *n=getNodePtrFromEdge(e);
 596         int i = n->numEdges;
 597         while (i != 0) {
 598                 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
 599                 Node * narg = getNodePtrFromEdge(arg);
 600
 601                 if (edgeIsVarConst(arg)) {
 602                         pushVectorEdge(&cnf->args, arg);
 603                         continue;
 604                 }
 605
 606                 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
 607                         arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
 608                 }
 609
 610                 if (narg->intAnnot[isNegEdge(arg)] == 1) {
 611                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 612                         if (!isProxy(argExp)) {
 613                                 if (largest == NULL) {
 614                                         largest = argExp;
 615                                         * largestEdge = arg;
 616                                         continue;
 617                                 } else if (argExp->litSize > largest->litSize) {
 618                                         pushVectorEdge(&cnf->args, *largestEdge);
 619                                         largest = argExp;
 620                                         * largestEdge = arg;
 621                                         continue;
 622                                 }
 623                         }
 624                 }
 625                 pushVectorEdge(&cnf->args, arg);
 626         }
 627
 628         if (largest != NULL) {
 629                 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
 630                 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
 631         }
 632
 633         return largest;
 634 }
 635
 636
 637 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 638         Edge largestEdge;
 639
 640         CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
 641         if (accum == NULL) accum = allocCNFExprBool(true);
 642
 643         int i = getSizeVectorEdge(&cnf->args);
 644         while (i != 0) {
 645                 Edge arg = getVectorEdge(&cnf->args, --i);
 646                 if (edgeIsVarConst(arg)) {
 647                         conjoinCNFLit(accum, getEdgeVar(arg));
 648                 } else {
 649                         Node *narg=getNodePtrFromEdge(arg);
 650                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 651
 652                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 653                         if (isProxy(argExp)) { // variable has been introduced
 654                                 conjoinCNFLit(accum, getProxy(argExp));
 655                         } else {
 656                                 conjoinCNFExpr(accum, argExp, destroy);
 657                                 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 658                         }
 659                 }
 660         }
 661
 662         return accum;
 663 }
 664
 665 #define CLAUSE_MAX 3
 666
 667 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
 668         Edge largestEdge;
 669         CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
 670         if (accum == NULL)
 671                 accum = allocCNFExprBool(false);
 672
 673         // This is necessary to check to make sure that we don't start out
 674         // with an accumulator that is "too large".
 675
 676         /// @todo Strictly speaking, introProxy doesn't *need* to free
 677         /// memory, then this wouldn't have to reallocate CNFExpr
 678
 679         /// @todo When this call to introProxy is made, the semantic
 680         /// negation pointer will have been destroyed.  Thus, it will not
 681         /// be possible to use the correct proxy.  That should be fixed.
 682
 683         // at this point, we will either have NULL, or a destructible expression
 684         if (getClauseSizeCNF(accum) > CLAUSE_MAX)
 685                 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
 686
 687         int i = getSizeVectorEdge(&cnf->args);
 688         while (i != 0) {
 689                 Edge arg=getVectorEdge(&cnf->args, --i);
 690                 Node *narg=getNodePtrFromEdge(arg);
 691                 if (edgeIsVarConst(arg)) {
 692                         disjoinCNFLit(accum, getEdgeVar(arg));
 693                 } else {
 694                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 695
 696                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 697                         if (isProxy(argExp)) { // variable has been introduced
 698                                 disjoinCNFLit(accum, getProxy(argExp));
 699                         } else if (argExp->litSize == 0) {
 700                                 disjoinCNFExpr(accum, argExp, destroy);
 701                         } else {
 702                                 // check to see if we should introduce a proxy
 703                                 int aL = accum->litSize;      // lits in accum
 704                                 int eL = argExp->litSize;     // lits in argument
 705                                 int aC = getClauseSizeCNF(accum);   // clauses in accum
 706                                 int eC = getClauseSizeCNF(argExp);  // clauses in argument
 707
 708                                 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
 709                                         disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
 710                                 } else {
 711                                         disjoinCNFExpr(accum, argExp, destroy);
 712                                         if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 713                                 }
 714                         }
 715                 }
 716         }
 717
 718         return accum;
 719 }