src/Backend/constraint.c

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