src/Backend/constraint.cc

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