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