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) 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         propagate(cnf, & expPos, expNeg, true) || propagate(cnf, & expNeg, expPos, true);
 550
 551         // The polarity heuristic entails visiting the discovery polarity first
 552         if (isPosEdge(e)) {
 553                 saveCNF(cnf, expPos, e, false);
 554                 saveCNF(cnf, expNeg, e, true);
 555         } else {
 556                 saveCNF(cnf, expNeg, e, true);
 557                 saveCNF(cnf, expPos, e, false);
 558         }
 559 }
 560
 561 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
 562         if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
 563                 if (dest == NULL) {
 564                         *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 565                 } else if (isProxy(*dest)) {
 566                         bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 567                         if (alwaysTrue) {
 568                                 Literal clause[] = {getProxy(*dest)};
 569                                 addArrayClauseLiteral(cnf->solver, 1, clause);
 570                         } else {
 571                                 Literal clause[] = {-getProxy(*dest)};
 572                                 addArrayClauseLiteral(cnf->solver, 1, clause);
 573                         }
 574
 575                         *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 576                 } else {
 577                         clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 578                 }
 579                 return true;
 580         }
 581         return false;
 582 }
 583
 584 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
 585         Node *n=getNodePtrFromEdge(e);
 586         n->flags.cnfVisitedUp |= (1 << sign);
 587         if (exp == NULL || isProxy(exp)) return;
 588
 589         if (exp->litSize == 1) {
 590                 Literal l = getLiteralLitVector(&exp->singletons, 0);
 591                 deleteCNFExpr(exp);
 592                 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
 593         } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
 594                 introProxy(cnf, e, exp, sign);
 595         } else {
 596                 n->ptrAnnot[sign] = exp;
 597         }
 598 }
 599
 600 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
 601         if (alwaysTrueCNF(expr)) {
 602                 return;
 603         } else if (alwaysFalseCNF(expr)) {
 604                 Literal clause[] = {-lcond};
 605                 addArrayClauseLiteral(cnf->solver, 1, clause);
 606                 return;
 607         }
 608
 609         for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 610                 Literal l=getLiteralLitVector(&expr->singletons,i);
 611                 Literal clause[] = {-lcond, l};
 612                 addArrayClauseLiteral(cnf->solver, 1, clause);
 613         }
 614         for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 615                 LitVector *lv=getVectorLitVector(&expr->clauses,i);
 616                 addClauseLiteral(cnf->solver, -lcond); //Add first literal
 617                 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
 618         }
 619 }
 620
 621 void outputCNF(CNF *cnf, CNFExpr *expr) {
 622         for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
 623                 Literal l=getLiteralLitVector(&expr->singletons,i);
 624                 Literal clause[] = {l};
 625                 addArrayClauseLiteral(cnf->solver, 1, clause);
 626         }
 627         for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
 628                 LitVector *lv=getVectorLitVector(&expr->clauses,i);
 629                 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
 630         }
 631 }
 632
 633 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
 634         clearVectorEdge(&cnf->args);
 635
 636         *largestEdge = (Edge) {(Node*) NULL};
 637         CNFExpr* largest = NULL;
 638         Node *n=getNodePtrFromEdge(e);
 639         int i = n->numEdges;
 640         while (i != 0) {
 641                 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
 642                 Node * narg = getNodePtrFromEdge(arg);
 643
 644                 if (edgeIsVarConst(arg)) {
 645                         pushVectorEdge(&cnf->args, arg);
 646                         continue;
 647                 }
 648
 649                 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
 650                         arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
 651                 }
 652
 653                 if (narg->intAnnot[isNegEdge(arg)] == 1) {
 654                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 655                         if (!isProxy(argExp)) {
 656                                 if (largest == NULL) {
 657                                         largest = argExp;
 658                                         * largestEdge = arg;
 659                                         continue;
 660                                 } else if (argExp->litSize > largest->litSize) {
 661                                         pushVectorEdge(&cnf->args, *largestEdge);
 662                                         largest = argExp;
 663                                         * largestEdge = arg;
 664                                         continue;
 665                                 }
 666                         }
 667                 }
 668                 pushVectorEdge(&cnf->args, arg);
 669         }
 670
 671         if (largest != NULL) {
 672                 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
 673                 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
 674         }
 675
 676         return largest;
 677 }
 678
 679
 680 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 681         Edge largestEdge;
 682
 683         CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
 684         if (accum == NULL) accum = allocCNFExprBool(true);
 685
 686         int i = getSizeVectorEdge(&cnf->args);
 687         while (i != 0) {
 688                 Edge arg = getVectorEdge(&cnf->args, --i);
 689                 if (edgeIsVarConst(arg)) {
 690                         conjoinCNFLit(accum, getEdgeVar(arg));
 691                 } else {
 692                         Node *narg=getNodePtrFromEdge(arg);
 693                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 694
 695                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 696                         if (isProxy(argExp)) { // variable has been introduced
 697                                 conjoinCNFLit(accum, getProxy(argExp));
 698                         } else {
 699                                 conjoinCNFExpr(accum, argExp, destroy);
 700                                 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 701                         }
 702                 }
 703         }
 704
 705         return accum;
 706 }
 707
 708 #define CLAUSE_MAX 3
 709
 710 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
 711         Edge largestEdge;
 712         CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
 713         if (accum == NULL)
 714                 accum = allocCNFExprBool(false);
 715
 716         // This is necessary to check to make sure that we don't start out
 717         // with an accumulator that is "too large".
 718
 719         /// @todo Strictly speaking, introProxy doesn't *need* to free
 720         /// memory, then this wouldn't have to reallocate CNFExpr
 721
 722         /// @todo When this call to introProxy is made, the semantic
 723         /// negation pointer will have been destroyed.  Thus, it will not
 724         /// be possible to use the correct proxy.  That should be fixed.
 725
 726         // at this point, we will either have NULL, or a destructible expression
 727         if (getClauseSizeCNF(accum) > CLAUSE_MAX)
 728                 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
 729
 730         int i = getSizeVectorEdge(&cnf->args);
 731         while (i != 0) {
 732                 Edge arg=getVectorEdge(&cnf->args, --i);
 733                 Node *narg=getNodePtrFromEdge(arg);
 734                 if (edgeIsVarConst(arg)) {
 735                         disjoinCNFLit(accum, getEdgeVar(arg));
 736                 } else {
 737                         CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
 738
 739                         bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
 740                         if (isProxy(argExp)) { // variable has been introduced
 741                                 disjoinCNFLit(accum, getProxy(argExp));
 742                         } else if (argExp->litSize == 0) {
 743                                 disjoinCNFExpr(accum, argExp, destroy);
 744                         } else {
 745                                 // check to see if we should introduce a proxy
 746                                 int aL = accum->litSize;      // lits in accum
 747                                 int eL = argExp->litSize;     // lits in argument
 748                                 int aC = getClauseSizeCNF(accum);   // clauses in accum
 749                                 int eC = getClauseSizeCNF(argExp);  // clauses in argument
 750
 751                                 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
 752                                         disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
 753                                 } else {
 754                                         disjoinCNFExpr(accum, argExp, destroy);
 755                                         if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
 756                                 }
 757                         }
 758                 }
 759         }
 760
 761         return accum;
 762 }