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