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