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