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