src/Backend/constraint.cc

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