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