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