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