src/Backend/constraint.cc

   1 #include "constraint.h"
   2 #include <string.h>
   3 #include <stdlib.h>
   4 #include "inc_solver.h"
   5 #include "common.h"
   6 #include "qsort.h"
   7 /*
   8    CNF SAT Conversion Copyright Brian Demsky 2017.
   9  */
  10
  11
  12 VectorImpl(Edge, Edge, 16)
  13 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
  14 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
  15 Edge E_BOGUS = {(Node *)0xffff5673};
  16 Edge E_NULL = {(Node *)NULL};
  17
  18 CNF *createCNF() {
  19         CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
  20         cnf->varcount = 1;
  21         cnf->clausecount = 0;
  22         cnf->solver = allocIncrementalSolver();
  23         cnf->solveTime = 0;
  24         cnf->encodeTime = 0;
  25         cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
  26         cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
  27         cnf->unsat = false;
  28         return cnf;
  29 }
  30
  31 void deleteCNF(CNF *cnf) {
  32         deleteIncrementalSolver(cnf->solver);
  33         ourfree(cnf->array);
  34         ourfree(cnf);
  35 }
  36
  37 void resetCNF(CNF *cnf) {
  38         resetSolver(cnf->solver);
  39         cnf->varcount = 1;
  40         cnf->clausecount = 0;
  41         cnf->solveTime = 0;
  42         cnf->encodeTime = 0;
  43         cnf->unsat = false;
  44 }
  45
  46 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
  47         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
  48         n->numVars = 0;
  49         n->type = type;
  50         n->numEdges = numEdges;
  51         memcpy(n->edges, edges, sizeof(Edge) * numEdges);
  52         return n;
  53 }
  54
  55 Node *allocBaseNode(NodeType type, uint numEdges) {
  56         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
  57         n->numVars = 0;
  58         n->type = type;
  59         n->numEdges = numEdges;
  60         return n;
  61 }
  62
  63 Node *allocResizeNode(uint capacity) {
  64         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
  65         n->numVars = 0;
  66         n->numEdges = 0;
  67         n->capacity = capacity;
  68         return n;
  69 }
  70
  71 Edge cloneEdge(Edge e) {
  72         if (edgeIsVarConst(e))
  73                 return e;
  74         Node *node = getNodePtrFromEdge(e);
  75         bool isneg = isNegEdge(e);
  76         uint numEdges = node->numEdges;
  77         Node *clone = allocBaseNode(node->type, numEdges);
  78         for (uint i = 0; i < numEdges; i++) {
  79                 clone->edges[i] = cloneEdge(node->edges[i]);
  80         }
  81         return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
  82 }
  83
  84 void freeEdgeRec(Edge e) {
  85         if (edgeIsVarConst(e))
  86                 return;
  87         Node *node = getNodePtrFromEdge(e);
  88         uint numEdges = node->numEdges;
  89         for (uint i = 0; i < numEdges; i++) {
  90                 freeEdgeRec(node->edges[i]);
  91         }
  92         ourfree(node);
  93 }
  94
  95 void freeEdge(Edge e) {
  96         if (edgeIsVarConst(e))
  97                 return;
  98         Node *node = getNodePtrFromEdge(e);
  99         ourfree(node);
 100 }
 101
 102 void freeEdgesRec(uint numEdges, Edge *earray) {
 103         for (uint i = 0; i < numEdges; i++) {
 104                 Edge e = earray[i];
 105                 freeEdgeRec(e);
 106         }
 107 }
 108
 109 void freeEdgeCNF(Edge e) {
 110         Node *node = getNodePtrFromEdge(e);
 111         uint numEdges = node->numEdges;
 112         for (uint i = 0; i < numEdges; i++) {
 113                 Edge ec = node->edges[i];
 114                 if (!edgeIsVarConst(ec)) {
 115                         ourfree(ec.node_ptr);
 116                 }
 117         }
 118         ourfree(node);
 119 }
 120
 121 void addEdgeToResizeNode(Node **node, Edge e) {
 122         Node *currnode = *node;
 123         if (currnode->capacity == currnode->numEdges) {
 124                 Node *newnode = allocResizeNode( currnode->capacity << 1);
 125                 newnode->numVars = currnode->numVars;
 126                 newnode->numEdges = currnode->numEdges;
 127                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 128                 ourfree(currnode);
 129                 *node = newnode;
 130                 currnode = newnode;
 131         }
 132         currnode->edges[currnode->numEdges++] = e;
 133 }
 134
 135 void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
 136         Node *currnode = *node;
 137         uint currEdges = currnode->numEdges;
 138         uint inEdges = innode->numEdges;
 139
 140         uint newsize = currEdges + inEdges;
 141         if (newsize >= currnode->capacity) {
 142                 if (newsize < innode->capacity) {
 143                         //just swap
 144                         innode->numVars = currnode->numVars;
 145                         Node *tmp = innode;
 146                         innode = currnode;
 147                         *node = currnode = tmp;
 148                 } else {
 149                         Node *newnode = allocResizeNode( newsize << 1);
 150                         newnode->numVars = currnode->numVars;
 151                         newnode->numEdges = currnode->numEdges;
 152                         memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 153                         ourfree(currnode);
 154                         *node = newnode;
 155                         currnode = newnode;
 156                 }
 157         } else {
 158                 if (inEdges > currEdges && newsize < innode->capacity) {
 159                         //just swap
 160                         innode->numVars = currnode->numVars;
 161                         Node *tmp = innode;
 162                         innode = currnode;
 163                         *node = currnode = tmp;
 164                 }
 165         }
 166         memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
 167         currnode->numEdges += innode->numEdges;
 168         ourfree(innode);
 169 }
 170
 171 void mergeNodeToResizeNode(Node **node, Node *innode) {
 172         Node *currnode = *node;
 173         uint currEdges = currnode->numEdges;
 174         uint inEdges = innode->numEdges;
 175         uint newsize = currEdges + inEdges;
 176         if (newsize >= currnode->capacity) {
 177                 Node *newnode = allocResizeNode( newsize << 1);
 178                 newnode->numVars = currnode->numVars;
 179                 newnode->numEdges = currnode->numEdges;
 180                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 181                 ourfree(currnode);
 182                 *node = newnode;
 183                 currnode = newnode;
 184         }
 185         memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
 186         currnode->numEdges += inEdges;
 187 }
 188
 189 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
 190         Edge e = {allocNode(type, numEdges, edges)};
 191         return e;
 192 }
 193
 194 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
 195         Edge edgearray[numEdges];
 196
 197         for (uint i = 0; i < numEdges; i++) {
 198                 edgearray[i] = constraintNegate(edges[i]);
 199         }
 200         Edge eand = constraintAND(cnf, numEdges, edgearray);
 201         return constraintNegate(eand);
 202 }
 203
 204 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
 205         Edge lneg = constraintNegate(left);
 206         Edge rneg = constraintNegate(right);
 207         Edge eand = constraintAND2(cnf, lneg, rneg);
 208         return constraintNegate(eand);
 209 }
 210
 211 int comparefunction(const Edge *e1, const Edge *e2) {
 212         if (e1->node_ptr == e2->node_ptr)
 213                 return 0;
 214         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
 215                 return -1;
 216         else
 217                 return 1;
 218 }
 219
 220 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 221         ASSERT(numEdges != 0);
 222
 223         bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
 224         uint initindex = 0;
 225         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
 226                 initindex++;
 227
 228         uint remainSize = numEdges - initindex;
 229
 230         if (remainSize == 0)
 231                 return E_True;
 232         else if (remainSize == 1)
 233                 return edges[initindex];
 234         else if (equalsEdge(edges[initindex], E_False)) {
 235                 freeEdgesRec(numEdges, edges);
 236                 return E_False;
 237         }
 238
 239         /** De-duplicate array */
 240         uint lowindex = 0;
 241         edges[lowindex] = edges[initindex++];
 242
 243         for (; initindex < numEdges; initindex++) {
 244                 Edge e1 = edges[lowindex];
 245                 Edge e2 = edges[initindex];
 246                 if (sameNodeVarEdge(e1, e2)) {
 247                         ASSERT(!isNodeEdge(e1));
 248                         if (!sameSignEdge(e1, e2)) {
 249                                 freeEdgesRec(lowindex + 1, edges);
 250                                 freeEdgesRec(numEdges - initindex, &edges[initindex]);
 251                                 return E_False;
 252                         }
 253                 } else
 254                         edges[++lowindex] = edges[initindex];
 255         }
 256         lowindex++;     //Make lowindex look like size
 257
 258         if (lowindex == 1)
 259                 return edges[0];
 260
 261         if (lowindex == 2 &&
 262                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 263                         getNodeType(edges[0]) == NodeType_AND &&
 264                         getNodeType(edges[1]) == NodeType_AND &&
 265                         getNodeSize(edges[0]) == 2 &&
 266                         getNodeSize(edges[1]) == 2) {
 267                 Edge *e0edges = getEdgeArray(edges[0]);
 268                 Edge *e1edges = getEdgeArray(edges[1]);
 269                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 270                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 271                         freeEdge(edges[0]);
 272                         freeEdge(edges[1]);
 273                         return result;
 274                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 275                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 276                         freeEdge(edges[0]);
 277                         freeEdge(edges[1]);
 278                         return result;
 279                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 280                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 281                         freeEdge(edges[0]);
 282                         freeEdge(edges[1]);
 283                         return result;
 284                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 285                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 286                         freeEdge(edges[0]);
 287                         freeEdge(edges[1]);
 288                         return result;
 289                 }
 290         }
 291
 292         return createNode(NodeType_AND, lowindex, edges);
 293 }
 294
 295 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
 296         Edge edges[2] = {left, right};
 297         return constraintAND(cnf, 2, edges);
 298 }
 299
 300 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
 301         Edge array[2];
 302         array[0] = left;
 303         array[1] = constraintNegate(right);
 304         Edge eand = constraintAND(cnf, 2, array);
 305         return constraintNegate(eand);
 306 }
 307
 308 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
 309         bool negate = !sameSignEdge(left, right);
 310         Edge lpos = getNonNeg(left);
 311         Edge rpos = getNonNeg(right);
 312
 313         Edge e;
 314         if (equalsEdge(lpos, rpos)) {
 315                 freeEdgeRec(left);
 316                 freeEdgeRec(right);
 317                 e = E_True;
 318         } else if (ltEdge(lpos, rpos)) {
 319                 Edge edges[] = {lpos, rpos};
 320                 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
 321         } else {
 322                 Edge edges[] = {rpos, lpos};
 323                 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
 324         }
 325         if (negate)
 326                 e = constraintNegate(e);
 327         return e;
 328 }
 329
 330 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 331         if (isNegEdge(cond)) {
 332                 cond = constraintNegate(cond);
 333                 Edge tmp = thenedge;
 334                 thenedge = elseedge;
 335                 elseedge = tmp;
 336         }
 337
 338         bool negate = isNegEdge(thenedge);
 339         if (negate) {
 340                 thenedge = constraintNegate(thenedge);
 341                 elseedge = constraintNegate(elseedge);
 342         }
 343
 344         Edge result;
 345         if (equalsEdge(cond, E_True)) {
 346                 freeEdgeRec(elseedge);
 347                 result = thenedge;
 348         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 349                 Edge array[] = {cond, elseedge};
 350                 result = constraintOR(cnf,  2, array);
 351         } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 352                 result = constraintIMPLIES(cnf, cond, thenedge);
 353         } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
 354                 Edge array[] = {cond, thenedge};
 355                 result = constraintAND(cnf, 2, array);
 356         } else if (equalsEdge(thenedge, elseedge)) {
 357                 freeEdgeRec(cond);
 358                 result = thenedge;
 359         } else if (sameNodeOppSign(thenedge, elseedge)) {
 360                 if (ltEdge(cond, thenedge)) {
 361                         Edge array[] = {cond, thenedge};
 362                         result = createNode(NodeType_IFF, 2, array);
 363                 } else {
 364                         Edge array[] = {thenedge, cond};
 365                         result = createNode(NodeType_IFF, 2, array);
 366                 }
 367         } else {
 368                 Edge edges[] = {cond, thenedge, elseedge};
 369                 result = createNode(NodeType_ITE, 3, edges);
 370         }
 371         if (negate)
 372                 result = constraintNegate(result);
 373         return result;
 374 }
 375
 376 Edge disjoinLit(Edge vec, Edge lit) {
 377         Node *nvec = vec.node_ptr;
 378         uint nvecedges = nvec->numEdges;
 379
 380         for (uint i = 0; i < nvecedges; i++) {
 381                 Edge ce = nvec->edges[i];
 382                 if (!edgeIsVarConst(ce)) {
 383                         Node *cne = ce.node_ptr;
 384                         addEdgeToResizeNode(&cne, lit);
 385                         nvec->edges[i] = (Edge) {cne};
 386                 } else {
 387                         Node *clause = allocResizeNode(2);
 388                         addEdgeToResizeNode(&clause, lit);
 389                         addEdgeToResizeNode(&clause, ce);
 390                         nvec->edges[i] = (Edge) {clause};
 391                 }
 392         }
 393         nvec->numVars += nvecedges;
 394         return vec;
 395 }
 396
 397 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
 398         Node *nnewvec = newvec.node_ptr;
 399         Node *ncnfform = cnfform.node_ptr;
 400         uint newvecedges = nnewvec->numEdges;
 401         uint cnfedges = ncnfform->numEdges;
 402         uint newvecvars = nnewvec->numVars;
 403         uint cnfvars = ncnfform->numVars;
 404
 405         if (cnfedges > 3 ||
 406                         ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
 407                 Edge proxyVar = constraintNewVar(cnf);
 408                 if (newvecedges > cnfedges) {
 409                         outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
 410                         freeEdgeCNF(newvec);
 411                         return disjoinLit(cnfform, proxyVar);
 412                 } else {
 413                         outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
 414                         freeEdgeCNF(cnfform);
 415                         return disjoinLit(newvec, proxyVar);
 416                 }
 417         }
 418
 419
 420
 421         if (newvecedges == 1 || cnfedges == 1) {
 422                 if (cnfedges != 1) {
 423                         Node *tmp = nnewvec;
 424                         nnewvec = ncnfform;
 425                         ncnfform = tmp;
 426                         newvecedges = cnfedges;
 427                         cnfedges = 1;
 428                 }
 429                 Edge e = ncnfform->edges[0];
 430                 if (!edgeIsVarConst(e)) {
 431                         Node *n = e.node_ptr;
 432                         for (uint i = 0; i < newvecedges; i++) {
 433                                 Edge ce = nnewvec->edges[i];
 434                                 if (isNodeEdge(ce)) {
 435                                         Node *cne = ce.node_ptr;
 436                                         mergeNodeToResizeNode(&cne, n);
 437                                         nnewvec->edges[i] = (Edge) {cne};
 438                                 } else {
 439                                         Node *clause = allocResizeNode(n->numEdges + 1);
 440                                         mergeNodeToResizeNode(&clause, n);
 441                                         addEdgeToResizeNode(&clause, ce);
 442                                         nnewvec->edges[i] = (Edge) {clause};
 443                                 }
 444                         }
 445                         nnewvec->numVars += newvecedges * n->numVars;
 446                 } else {
 447                         for (uint i = 0; i < newvecedges; i++) {
 448                                 Edge ce = nnewvec->edges[i];
 449                                 if (!edgeIsVarConst(ce)) {
 450                                         Node *cne = ce.node_ptr;
 451                                         addEdgeToResizeNode(&cne, e);
 452                                         nnewvec->edges[i] = (Edge) {cne};
 453                                 } else {
 454                                         Node *clause = allocResizeNode(2);
 455                                         addEdgeToResizeNode(&clause, e);
 456                                         addEdgeToResizeNode(&clause, ce);
 457                                         nnewvec->edges[i] = (Edge) {clause};
 458                                 }
 459                         }
 460                         nnewvec->numVars += newvecedges;
 461                 }
 462                 freeEdgeCNF((Edge) {ncnfform});
 463                 return (Edge) {nnewvec};
 464         }
 465
 466         Node *result = allocResizeNode(1);
 467
 468         for (uint i = 0; i < newvecedges; i++) {
 469                 Edge nedge = nnewvec->edges[i];
 470                 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
 471                 for (uint j = 0; j < cnfedges; j++) {
 472                         Edge cedge = ncnfform->edges[j];
 473                         uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
 474                         if (equalsEdge(cedge, nedge)) {
 475                                 addEdgeToResizeNode(&result, cedge);
 476                                 result->numVars += cSize;
 477                         } else if (!sameNodeOppSign(nedge, cedge)) {
 478                                 Node *clause = allocResizeNode(cSize + nSize);
 479                                 if (isNodeEdge(nedge)) {
 480                                         mergeNodeToResizeNode(&clause, nedge.node_ptr);
 481                                 } else {
 482                                         addEdgeToResizeNode(&clause, nedge);
 483                                 }
 484                                 if (isNodeEdge(cedge)) {
 485                                         mergeNodeToResizeNode(&clause, cedge.node_ptr);
 486                                 } else {
 487                                         addEdgeToResizeNode(&clause, cedge);
 488                                 }
 489                                 addEdgeToResizeNode(&result, (Edge) {clause});
 490                                 result->numVars += clause->numEdges;
 491                         }
 492                         //otherwise skip
 493                 }
 494         }
 495         freeEdgeCNF(newvec);
 496         freeEdgeCNF(cnfform);
 497         return (Edge) {result};
 498 }
 499
 500 Edge simplifyCNF(CNF *cnf, Edge input) {
 501         if (edgeIsVarConst(input)) {
 502                 Node *newvec = allocResizeNode(1);
 503                 addEdgeToResizeNode(&newvec, input);
 504                 newvec->numVars = 1;
 505                 return (Edge) {newvec};
 506         }
 507         bool negated = isNegEdge(input);
 508         Node *node = getNodePtrFromEdge(input);
 509         NodeType type = node->type;
 510         if (!negated) {
 511                 if (type == NodeType_AND) {
 512                         //AND case
 513                         Node *newvec = allocResizeNode(node->numEdges);
 514                         uint numEdges = node->numEdges;
 515                         for (uint i = 0; i < numEdges; i++) {
 516                                 Edge e = simplifyCNF(cnf, node->edges[i]);
 517                                 uint enumvars = e.node_ptr->numVars;
 518                                 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
 519                                 newvec->numVars += enumvars;
 520                         }
 521                         return (Edge) {newvec};
 522                 } else {
 523                         Edge cond = node->edges[0];
 524                         Edge thenedge = node->edges[1];
 525                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 526                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 527                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
 528                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 529                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
 530                         Edge thencnf = simplifyCNF(cnf, thencons);
 531                         Edge elsecnf = simplifyCNF(cnf, elsecons);
 532                         //free temporary nodes
 533                         ourfree(getNodePtrFromEdge(thencons));
 534                         ourfree(getNodePtrFromEdge(elsecons));
 535                         Node *result = thencnf.node_ptr;
 536                         uint elsenumvars = elsecnf.node_ptr->numVars;
 537                         mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
 538                         result->numVars += elsenumvars;
 539                         return (Edge) {result};
 540                 }
 541         } else {
 542                 if (type == NodeType_AND) {
 543                         //OR Case
 544                         uint numEdges = node->numEdges;
 545
 546                         Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
 547                         for (uint i = 1; i < numEdges; i++) {
 548                                 Edge e = node->edges[i];
 549                                 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
 550                                 newvec = disjoinAndFree(cnf, newvec, cnfform);
 551                         }
 552                         return newvec;
 553                 } else {
 554                         Edge cond = node->edges[0];
 555                         Edge thenedge = node->edges[1];
 556                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 557
 558
 559                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 560                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
 561                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 562                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
 563
 564                         Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
 565                         Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
 566                         Edge result = simplifyCNF(cnf, combined);
 567                         //free temporary nodes
 568                         ourfree(getNodePtrFromEdge(thencons));
 569                         ourfree(getNodePtrFromEdge(elsecons));
 570                         ourfree(getNodePtrFromEdge(combined));
 571                         return result;
 572                 }
 573         }
 574 }
 575
 576 void addClause(CNF *cnf, uint numliterals, int *literals){
 577         cnf->clausecount++;
 578         for(uint i=0; i< numliterals; i++)
 579                 model_print("%d ", literals[i]);
 580         model_print("\n");
 581         addArrayClauseLiteral(cnf->solver, numliterals, literals);
 582 }
 583
 584 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 585         Node *andNode = cnfform.node_ptr;
 586         int orvar = getEdgeVar(eorvar);
 587         ASSERT(orvar != 0);
 588         uint numEdges = andNode->numEdges;
 589         for (uint i = 0; i < numEdges; i++) {
 590                 Edge e = andNode->edges[i];
 591                 if (edgeIsVarConst(e)) {
 592                         int array[2] = {getEdgeVar(e), orvar};
 593                         ASSERT(array[0] != 0);
 594                         addClause(cnf, 2, array);
 595                 } else {
 596                         Node *clause = e.node_ptr;
 597                         uint cnumEdges = clause->numEdges + 1;
 598                         if (cnumEdges > cnf->asize) {
 599                                 cnf->asize = cnumEdges << 1;
 600                                 ourfree(cnf->array);
 601                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 602                         }
 603                         int *array = cnf->array;
 604                         for (uint j = 0; j < (cnumEdges - 1); j++) {
 605                                 array[j] = getEdgeVar(clause->edges[j]);
 606                                 ASSERT(array[j] != 0);
 607                         }
 608                         array[cnumEdges - 1] = orvar;
 609                         addClause(cnf, cnumEdges, array);
 610                 }
 611         }
 612 }
 613
 614 void outputCNF(CNF *cnf, Edge cnfform) {
 615         Node *andNode = cnfform.node_ptr;
 616         uint numEdges = andNode->numEdges;
 617         for (uint i = 0; i < numEdges; i++) {
 618                 Edge e = andNode->edges[i];
 619                 if (edgeIsVarConst(e)) {
 620                         int array[1] = {getEdgeVar(e)};
 621                         ASSERT(array[0] != 0);
 622                         addClause(cnf, 1, array);
 623                 } else {
 624                         Node *clause = e.node_ptr;
 625                         uint cnumEdges = clause->numEdges;
 626                         if (cnumEdges > cnf->asize) {
 627                                 cnf->asize = cnumEdges << 1;
 628                                 ourfree(cnf->array);
 629                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 630                         }
 631                         int *array = cnf->array;
 632                         for (uint j = 0; j < cnumEdges; j++) {
 633                                 array[j] = getEdgeVar(clause->edges[j]);
 634                                 ASSERT(array[j] != 0);
 635                         }
 636                         addClause(cnf, cnumEdges, array);
 637                 }
 638         }
 639 }
 640
 641 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
 642         ASSERT(p != P_UNDEFINED);
 643         if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
 644                 // proxy => expression
 645                 Edge cnfexpr = simplifyCNF(cnf, expression);
 646                 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
 647                 if (p == P_TRUE)
 648                         freeEdgeRec(expression);
 649                 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
 650                 outputCNFOR(cnf, cnfnegexpr, proxy);
 651                 freeEdgeCNF(cnfexpr);
 652                 freeEdgeCNF(cnfnegexpr);
 653         }
 654         if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
 655                 // expression => proxy
 656                 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
 657                 Edge cnfexpr = simplifyCNF(cnf, expression);
 658                 freeEdgeRec(expression);
 659                 outputCNFOR(cnf, cnfnegexpr, proxy);
 660                 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
 661                 freeEdgeCNF(cnfnegexpr);
 662                 freeEdgeCNF(cnfexpr);
 663         }
 664 }
 665
 666 void addConstraintCNF(CNF *cnf, Edge constraint) {
 667         if (equalsEdge(constraint, E_True)) {
 668                 return;
 669         } else if (equalsEdge(constraint, E_False)) {
 670                 cnf->unsat = true;
 671                 return;
 672         }
 673         if (cnf->unsat) {
 674                 freeEdgeRec(constraint);
 675                 return;
 676         }
 677
 678 #if 0
 679         model_print("****SATC_ADDING NEW Constraint*****\n");
 680         printCNF(constraint);
 681         model_print("\n******************************\n");
 682 #endif
 683
 684         Edge cnfform = simplifyCNF(cnf, constraint);
 685         freeEdgeRec(constraint);
 686         outputCNF(cnf, cnfform);
 687         freeEdgeCNF(cnfform);
 688 }
 689
 690 Edge constraintNewVar(CNF *cnf) {
 691         uint varnum = cnf->varcount++;
 692         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 693         return e;
 694 }
 695
 696 int solveCNF(CNF *cnf) {
 697         long long startTime = getTimeNano();
 698         finishedClauses(cnf->solver);
 699         long long startSolve = getTimeNano();
 700         model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
 701         int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
 702         long long finishTime = getTimeNano();
 703         cnf->encodeTime = startSolve - startTime;
 704         model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
 705         cnf->solveTime = finishTime - startSolve;
 706         model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
 707         return result;
 708 }
 709
 710 bool getValueCNF(CNF *cnf, Edge var) {
 711         Literal l = getEdgeVar(var);
 712         bool isneg = (l < 0);
 713         l = abs(l);
 714         return isneg ^ getValueSolver(cnf->solver, l);
 715 }
 716
 717 void printCNF(Edge e) {
 718         if (edgeIsVarConst(e)) {
 719                 Literal l = getEdgeVar(e);
 720                 model_print ("%d", l);
 721                 return;
 722         }
 723         bool isNeg = isNegEdge(e);
 724         if (edgeIsConst(e)) {
 725                 if (isNeg)
 726                         model_print("T");
 727                 else
 728                         model_print("F");
 729                 return;
 730         }
 731         Node *n = getNodePtrFromEdge(e);
 732         if (isNeg) {
 733                 //Pretty print things that are equivalent to OR's
 734                 if (getNodeType(e) == NodeType_AND) {
 735                         model_print("or(");
 736                         for (uint i = 0; i < n->numEdges; i++) {
 737                                 Edge e = n->edges[i];
 738                                 if (i != 0)
 739                                         model_print(" ");
 740                                 printCNF(constraintNegate(e));
 741                         }
 742                         model_print(")");
 743                         return;
 744                 }
 745
 746                 model_print("!");
 747         }
 748         switch (getNodeType(e)) {
 749         case NodeType_AND:
 750                 model_print("and");
 751                 break;
 752         case NodeType_ITE:
 753                 model_print("ite");
 754                 break;
 755         case NodeType_IFF:
 756                 model_print("iff");
 757                 break;
 758         }
 759         model_print("(");
 760         for (uint i = 0; i < n->numEdges; i++) {
 761                 Edge e = n->edges[i];
 762                 if (i != 0)
 763                         model_print(" ");
 764                 printCNF(e);
 765         }
 766         model_print(")");
 767 }
 768
 769 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 770         Edge carray[numvars];
 771         for (uint j = 0; j < numvars; j++) {
 772                 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
 773                 value = value >> 1;
 774         }
 775
 776         return constraintAND(cnf, numvars, carray);
 777 }
 778
 779 /** Generates a constraint to ensure that all encodings are less than value */
 780 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 781         Edge orarray[numvars];
 782         Edge andarray[numvars];
 783         uint andi = 0;
 784
 785         while (true) {
 786                 uint val = value;
 787                 uint ori = 0;
 788                 for (uint j = 0; j < numvars; j++) {
 789                         if ((val & 1) == 1)
 790                                 orarray[ori++] = constraintNegate(vars[j]);
 791                         val = val >> 1;
 792                 }
 793                 //no ones to flip, so bail now...
 794                 if (ori == 0) {
 795                         return constraintAND(cnf, andi, andarray);
 796                 }
 797                 andarray[andi++] = constraintOR(cnf, ori, orarray);
 798
 799                 value = value + (1 << (__builtin_ctz(value)));
 800                 //flip the last one
 801         }
 802 }
 803
 804 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
 805         //TO WRITE....
 806 }
 807
 808 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 809         if (numvars == 0)
 810                 return E_True;
 811         Edge array[numvars];
 812         for (uint i = 0; i < numvars; i++) {
 813                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
 814         }
 815         return constraintAND(cnf, numvars, array);
 816 }
 817
 818 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 819         if (numvars == 0 )
 820                 return E_False;
 821         Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
 822         for (uint i = 1; i < numvars; i++) {
 823                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 824                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 825                 result = constraintOR2(cnf, lt, eq);
 826         }
 827         return result;
 828 }
 829
 830 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 831         if (numvars == 0 )
 832                 return E_True;
 833         Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
 834         for (uint i = 1; i < numvars; i++) {
 835                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 836                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 837                 result = constraintOR2(cnf, lt, eq);
 838         }
 839         return result;
 840 }