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