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