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