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