src/Backend/constraint.cc

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