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