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