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