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         if (numEdges < 200000) {
 196                 Edge edgearray[numEdges];
 197
 198                 for (uint i = 0; i < numEdges; i++) {
 199                         edgearray[i] = constraintNegate(edges[i]);
 200                 }
 201                 Edge eand = constraintAND(cnf, numEdges, edgearray);
 202                 return constraintNegate(eand);
 203         } else {
 204                 Edge *edgearray = (Edge *)ourmalloc(numEdges * sizeof(Edge));
 205
 206                 for (uint i = 0; i < numEdges; i++) {
 207                         edgearray[i] = constraintNegate(edges[i]);
 208                 }
 209                 Edge eand = constraintAND(cnf, numEdges, edgearray);
 210                 ourfree(edgearray);
 211                 return constraintNegate(eand);
 212         }
 213 }
 214
 215 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
 216         Edge lneg = constraintNegate(left);
 217         Edge rneg = constraintNegate(right);
 218         Edge eand = constraintAND2(cnf, lneg, rneg);
 219         return constraintNegate(eand);
 220 }
 221
 222 int comparefunction(const Edge *e1, const Edge *e2) {
 223         if (e1->node_ptr == e2->node_ptr)
 224                 return 0;
 225         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
 226                 return -1;
 227         else
 228                 return 1;
 229 }
 230
 231 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 232         ASSERT(numEdges != 0);
 233
 234         bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
 235         uint initindex = 0;
 236         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
 237                 initindex++;
 238
 239         uint remainSize = numEdges - initindex;
 240
 241         if (remainSize == 0)
 242                 return E_True;
 243         else if (remainSize == 1)
 244                 return edges[initindex];
 245         else if (equalsEdge(edges[initindex], E_False)) {
 246                 freeEdgesRec(numEdges, edges);
 247                 return E_False;
 248         }
 249
 250         /** De-duplicate array */
 251         uint lowindex = 0;
 252         edges[lowindex] = edges[initindex++];
 253
 254         for (; initindex < numEdges; initindex++) {
 255                 Edge e1 = edges[lowindex];
 256                 Edge e2 = edges[initindex];
 257                 if (sameNodeVarEdge(e1, e2)) {
 258                         ASSERT(!isNodeEdge(e1));
 259                         if (!sameSignEdge(e1, e2)) {
 260                                 freeEdgesRec(lowindex + 1, edges);
 261                                 freeEdgesRec(numEdges - initindex, &edges[initindex]);
 262                                 return E_False;
 263                         }
 264                 } else
 265                         edges[++lowindex] = edges[initindex];
 266         }
 267         lowindex++;     //Make lowindex look like size
 268
 269         if (lowindex == 1)
 270                 return edges[0];
 271
 272         if (lowindex == 2 &&
 273                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 274                         getNodeType(edges[0]) == NodeType_AND &&
 275                         getNodeType(edges[1]) == NodeType_AND &&
 276                         getNodeSize(edges[0]) == 2 &&
 277                         getNodeSize(edges[1]) == 2) {
 278                 Edge *e0edges = getEdgeArray(edges[0]);
 279                 Edge *e1edges = getEdgeArray(edges[1]);
 280                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 281                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 282                         freeEdge(edges[0]);
 283                         freeEdge(edges[1]);
 284                         return result;
 285                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 286                         Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 287                         freeEdge(edges[0]);
 288                         freeEdge(edges[1]);
 289                         return result;
 290                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 291                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 292                         freeEdge(edges[0]);
 293                         freeEdge(edges[1]);
 294                         return result;
 295                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 296                         Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 297                         freeEdge(edges[0]);
 298                         freeEdge(edges[1]);
 299                         return result;
 300                 }
 301         }
 302
 303         return createNode(NodeType_AND, lowindex, edges);
 304 }
 305
 306 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
 307         Edge edges[2] = {left, right};
 308         return constraintAND(cnf, 2, edges);
 309 }
 310
 311 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
 312         Edge array[2];
 313         array[0] = left;
 314         array[1] = constraintNegate(right);
 315         Edge eand = constraintAND(cnf, 2, array);
 316         return constraintNegate(eand);
 317 }
 318
 319 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
 320         bool negate = !sameSignEdge(left, right);
 321         Edge lpos = getNonNeg(left);
 322         Edge rpos = getNonNeg(right);
 323
 324         Edge e;
 325         if (equalsEdge(lpos, rpos)) {
 326                 freeEdgeRec(left);
 327                 freeEdgeRec(right);
 328                 e = E_True;
 329         } else if (ltEdge(lpos, rpos)) {
 330                 Edge edges[] = {lpos, rpos};
 331                 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
 332         } else {
 333                 Edge edges[] = {rpos, lpos};
 334                 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
 335         }
 336         if (negate)
 337                 e = constraintNegate(e);
 338         return e;
 339 }
 340
 341 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 342         if (isNegEdge(cond)) {
 343                 cond = constraintNegate(cond);
 344                 Edge tmp = thenedge;
 345                 thenedge = elseedge;
 346                 elseedge = tmp;
 347         }
 348
 349         bool negate = isNegEdge(thenedge);
 350         if (negate) {
 351                 thenedge = constraintNegate(thenedge);
 352                 elseedge = constraintNegate(elseedge);
 353         }
 354
 355         Edge result;
 356         if (equalsEdge(cond, E_True)) {
 357                 freeEdgeRec(elseedge);
 358                 result = thenedge;
 359         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 360                 Edge array[] = {cond, elseedge};
 361                 result = constraintOR(cnf,  2, array);
 362         } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 363                 result = constraintIMPLIES(cnf, cond, thenedge);
 364         } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
 365                 Edge array[] = {cond, thenedge};
 366                 result = constraintAND(cnf, 2, array);
 367         } else if (equalsEdge(thenedge, elseedge)) {
 368                 freeEdgeRec(cond);
 369                 result = thenedge;
 370         } else if (sameNodeOppSign(thenedge, elseedge)) {
 371                 if (ltEdge(cond, thenedge)) {
 372                         Edge array[] = {cond, thenedge};
 373                         result = createNode(NodeType_IFF, 2, array);
 374                 } else {
 375                         Edge array[] = {thenedge, cond};
 376                         result = createNode(NodeType_IFF, 2, array);
 377                 }
 378         } else {
 379                 Edge edges[] = {cond, thenedge, elseedge};
 380                 result = createNode(NodeType_ITE, 3, edges);
 381         }
 382         if (negate)
 383                 result = constraintNegate(result);
 384         return result;
 385 }
 386
 387 Edge disjoinLit(Edge vec, Edge lit) {
 388         Node *nvec = vec.node_ptr;
 389         uint nvecedges = nvec->numEdges;
 390
 391         for (uint i = 0; i < nvecedges; i++) {
 392                 Edge ce = nvec->edges[i];
 393                 if (!edgeIsVarConst(ce)) {
 394                         Node *cne = ce.node_ptr;
 395                         addEdgeToResizeNode(&cne, lit);
 396                         nvec->edges[i] = (Edge) {cne};
 397                 } else {
 398                         Node *clause = allocResizeNode(2);
 399                         addEdgeToResizeNode(&clause, lit);
 400                         addEdgeToResizeNode(&clause, ce);
 401                         nvec->edges[i] = (Edge) {clause};
 402                 }
 403         }
 404         nvec->numVars += nvecedges;
 405         return vec;
 406 }
 407
 408 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
 409         Node *nnewvec = newvec.node_ptr;
 410         Node *ncnfform = cnfform.node_ptr;
 411         uint newvecedges = nnewvec->numEdges;
 412         uint cnfedges = ncnfform->numEdges;
 413         uint newvecvars = nnewvec->numVars;
 414         uint cnfvars = ncnfform->numVars;
 415
 416         if (cnfedges > 3 ||
 417                         ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
 418                 Edge proxyVar = constraintNewVar(cnf);
 419                 if (newvecedges > cnfedges) {
 420                         outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
 421                         freeEdgeCNF(newvec);
 422                         return disjoinLit(cnfform, proxyVar);
 423                 } else {
 424                         outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
 425                         freeEdgeCNF(cnfform);
 426                         return disjoinLit(newvec, proxyVar);
 427                 }
 428         }
 429
 430
 431
 432         if (newvecedges == 1 || cnfedges == 1) {
 433                 if (cnfedges != 1) {
 434                         Node *tmp = nnewvec;
 435                         nnewvec = ncnfform;
 436                         ncnfform = tmp;
 437                         newvecedges = cnfedges;
 438                         cnfedges = 1;
 439                 }
 440                 Edge e = ncnfform->edges[0];
 441                 if (!edgeIsVarConst(e)) {
 442                         Node *n = e.node_ptr;
 443                         for (uint i = 0; i < newvecedges; i++) {
 444                                 Edge ce = nnewvec->edges[i];
 445                                 if (isNodeEdge(ce)) {
 446                                         Node *cne = ce.node_ptr;
 447                                         mergeNodeToResizeNode(&cne, n);
 448                                         nnewvec->edges[i] = (Edge) {cne};
 449                                 } else {
 450                                         Node *clause = allocResizeNode(n->numEdges + 1);
 451                                         mergeNodeToResizeNode(&clause, n);
 452                                         addEdgeToResizeNode(&clause, ce);
 453                                         nnewvec->edges[i] = (Edge) {clause};
 454                                 }
 455                         }
 456                         nnewvec->numVars += newvecedges * n->numVars;
 457                 } else {
 458                         for (uint i = 0; i < newvecedges; i++) {
 459                                 Edge ce = nnewvec->edges[i];
 460                                 if (!edgeIsVarConst(ce)) {
 461                                         Node *cne = ce.node_ptr;
 462                                         addEdgeToResizeNode(&cne, e);
 463                                         nnewvec->edges[i] = (Edge) {cne};
 464                                 } else {
 465                                         Node *clause = allocResizeNode(2);
 466                                         addEdgeToResizeNode(&clause, e);
 467                                         addEdgeToResizeNode(&clause, ce);
 468                                         nnewvec->edges[i] = (Edge) {clause};
 469                                 }
 470                         }
 471                         nnewvec->numVars += newvecedges;
 472                 }
 473                 freeEdgeCNF((Edge) {ncnfform});
 474                 return (Edge) {nnewvec};
 475         }
 476
 477         Node *result = allocResizeNode(1);
 478
 479         for (uint i = 0; i < newvecedges; i++) {
 480                 Edge nedge = nnewvec->edges[i];
 481                 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
 482                 for (uint j = 0; j < cnfedges; j++) {
 483                         Edge cedge = ncnfform->edges[j];
 484                         uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
 485                         if (equalsEdge(cedge, nedge)) {
 486                                 addEdgeToResizeNode(&result, cedge);
 487                                 result->numVars += cSize;
 488                         } else if (!sameNodeOppSign(nedge, cedge)) {
 489                                 Node *clause = allocResizeNode(cSize + nSize);
 490                                 if (isNodeEdge(nedge)) {
 491                                         mergeNodeToResizeNode(&clause, nedge.node_ptr);
 492                                 } else {
 493                                         addEdgeToResizeNode(&clause, nedge);
 494                                 }
 495                                 if (isNodeEdge(cedge)) {
 496                                         mergeNodeToResizeNode(&clause, cedge.node_ptr);
 497                                 } else {
 498                                         addEdgeToResizeNode(&clause, cedge);
 499                                 }
 500                                 addEdgeToResizeNode(&result, (Edge) {clause});
 501                                 result->numVars += clause->numEdges;
 502                         }
 503                         //otherwise skip
 504                 }
 505         }
 506         freeEdgeCNF(newvec);
 507         freeEdgeCNF(cnfform);
 508         return (Edge) {result};
 509 }
 510
 511 Edge simplifyCNF(CNF *cnf, Edge input) {
 512         if (edgeIsVarConst(input)) {
 513                 Node *newvec = allocResizeNode(1);
 514                 addEdgeToResizeNode(&newvec, input);
 515                 newvec->numVars = 1;
 516                 return (Edge) {newvec};
 517         }
 518         bool negated = isNegEdge(input);
 519         Node *node = getNodePtrFromEdge(input);
 520         NodeType type = node->type;
 521         if (!negated) {
 522                 if (type == NodeType_AND) {
 523                         //AND case
 524                         Node *newvec = allocResizeNode(node->numEdges);
 525                         uint numEdges = node->numEdges;
 526                         for (uint i = 0; i < numEdges; i++) {
 527                                 Edge e = simplifyCNF(cnf, node->edges[i]);
 528                                 uint enumvars = e.node_ptr->numVars;
 529                                 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
 530                                 newvec->numVars += enumvars;
 531                         }
 532                         return (Edge) {newvec};
 533                 } else {
 534                         Edge cond = node->edges[0];
 535                         Edge thenedge = node->edges[1];
 536                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 537                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 538                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
 539                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 540                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
 541                         Edge thencnf = simplifyCNF(cnf, thencons);
 542                         Edge elsecnf = simplifyCNF(cnf, elsecons);
 543                         //free temporary nodes
 544                         ourfree(getNodePtrFromEdge(thencons));
 545                         ourfree(getNodePtrFromEdge(elsecons));
 546                         Node *result = thencnf.node_ptr;
 547                         uint elsenumvars = elsecnf.node_ptr->numVars;
 548                         mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
 549                         result->numVars += elsenumvars;
 550                         return (Edge) {result};
 551                 }
 552         } else {
 553                 if (type == NodeType_AND) {
 554                         //OR Case
 555                         uint numEdges = node->numEdges;
 556
 557                         Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
 558                         for (uint i = 1; i < numEdges; i++) {
 559                                 Edge e = node->edges[i];
 560                                 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
 561                                 newvec = disjoinAndFree(cnf, newvec, cnfform);
 562                         }
 563                         return newvec;
 564                 } else {
 565                         Edge cond = node->edges[0];
 566                         Edge thenedge = node->edges[1];
 567                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 568
 569
 570                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 571                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
 572                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 573                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
 574
 575                         Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
 576                         Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
 577                         Edge result = simplifyCNF(cnf, combined);
 578                         //free temporary nodes
 579                         ourfree(getNodePtrFromEdge(thencons));
 580                         ourfree(getNodePtrFromEdge(elsecons));
 581                         ourfree(getNodePtrFromEdge(combined));
 582                         return result;
 583                 }
 584         }
 585 }
 586
 587 void addClause(CNF *cnf, uint numliterals, int *literals) {
 588         cnf->clausecount++;
 589         addArrayClauseLiteral(cnf->solver, numliterals, literals);
 590 }
 591
 592 void freezeVariable(CNF *cnf, Edge e){
 593         int literal = getEdgeVar(e);
 594         freeze(cnf->solver, literal);
 595 }
 596
 597 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 598         Node *andNode = cnfform.node_ptr;
 599         int orvar = getEdgeVar(eorvar);
 600         ASSERT(orvar != 0);
 601         uint numEdges = andNode->numEdges;
 602         for (uint i = 0; i < numEdges; i++) {
 603                 Edge e = andNode->edges[i];
 604                 if (edgeIsVarConst(e)) {
 605                         int array[2] = {getEdgeVar(e), orvar};
 606                         ASSERT(array[0] != 0);
 607                         addClause(cnf, 2, array);
 608                 } else {
 609                         Node *clause = e.node_ptr;
 610                         uint cnumEdges = clause->numEdges + 1;
 611                         if (cnumEdges > cnf->asize) {
 612                                 cnf->asize = cnumEdges << 1;
 613                                 ourfree(cnf->array);
 614                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 615                         }
 616                         int *array = cnf->array;
 617                         for (uint j = 0; j < (cnumEdges - 1); j++) {
 618                                 array[j] = getEdgeVar(clause->edges[j]);
 619                                 ASSERT(array[j] != 0);
 620                         }
 621                         array[cnumEdges - 1] = orvar;
 622                         addClause(cnf, cnumEdges, array);
 623                 }
 624         }
 625 }
 626
 627 void outputCNF(CNF *cnf, Edge cnfform) {
 628         Node *andNode = cnfform.node_ptr;
 629         uint numEdges = andNode->numEdges;
 630         for (uint i = 0; i < numEdges; i++) {
 631                 Edge e = andNode->edges[i];
 632                 if (edgeIsVarConst(e)) {
 633                         int array[1] = {getEdgeVar(e)};
 634                         ASSERT(array[0] != 0);
 635                         addClause(cnf, 1, array);
 636                 } else {
 637                         Node *clause = e.node_ptr;
 638                         uint cnumEdges = clause->numEdges;
 639                         if (cnumEdges > cnf->asize) {
 640                                 cnf->asize = cnumEdges << 1;
 641                                 ourfree(cnf->array);
 642                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 643                         }
 644                         int *array = cnf->array;
 645                         for (uint j = 0; j < cnumEdges; j++) {
 646                                 array[j] = getEdgeVar(clause->edges[j]);
 647                                 ASSERT(array[j] != 0);
 648                         }
 649                         addClause(cnf, cnumEdges, array);
 650                 }
 651         }
 652 }
 653
 654 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
 655         ASSERT(p != P_UNDEFINED);
 656         if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
 657                 // proxy => expression
 658                 Edge cnfexpr = simplifyCNF(cnf, expression);
 659                 if (p == P_TRUE)
 660                         freeEdgeRec(expression);
 661                 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
 662                 freeEdgeCNF(cnfexpr);
 663         }
 664         if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
 665                 // expression => proxy
 666                 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
 667                 freeEdgeRec(expression);
 668                 outputCNFOR(cnf, cnfnegexpr, proxy);
 669                 freeEdgeCNF(cnfnegexpr);
 670         }
 671 }
 672
 673 void addConstraintCNF(CNF *cnf, Edge constraint) {
 674         if (equalsEdge(constraint, E_True)) {
 675                 return;
 676         } else if (equalsEdge(constraint, E_False)) {
 677                 cnf->unsat = true;
 678                 return;
 679         }
 680         if (cnf->unsat) {
 681                 freeEdgeRec(constraint);
 682                 return;
 683         }
 684
 685 #if 0
 686         model_print("****SATC_ADDING NEW Constraint*****\n");
 687         printCNF(constraint);
 688         model_print("\n******************************\n");
 689 #endif
 690
 691         Edge cnfform = simplifyCNF(cnf, constraint);
 692         freeEdgeRec(constraint);
 693         outputCNF(cnf, cnfform);
 694         freeEdgeCNF(cnfform);
 695 }
 696
 697 Edge constraintNewVar(CNF *cnf) {
 698         uint varnum = cnf->varcount++;
 699         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 700         return e;
 701 }
 702
 703 int solveCNF(CNF *cnf) {
 704         long long startSolve = getTimeNano();
 705         model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
 706         int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
 707         long long finishTime = getTimeNano();
 708         model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
 709         cnf->solveTime = finishTime - startSolve;
 710         model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
 711         return result;
 712 }
 713
 714 bool getValueCNF(CNF *cnf, Edge var) {
 715         Literal l = getEdgeVar(var);
 716         bool isneg = (l < 0);
 717         l = abs(l);
 718         return isneg ^ getValueSolver(cnf->solver, l);
 719 }
 720
 721 void printCNF(Edge e) {
 722         if (edgeIsVarConst(e)) {
 723                 Literal l = getEdgeVar(e);
 724                 model_print ("%d", l);
 725                 return;
 726         }
 727         bool isNeg = isNegEdge(e);
 728         if (edgeIsConst(e)) {
 729                 if (isNeg)
 730                         model_print("T");
 731                 else
 732                         model_print("F");
 733                 return;
 734         }
 735         Node *n = getNodePtrFromEdge(e);
 736         if (isNeg) {
 737                 //Pretty print things that are equivalent to OR's
 738                 if (getNodeType(e) == NodeType_AND) {
 739                         model_print("or(");
 740                         for (uint i = 0; i < n->numEdges; i++) {
 741                                 Edge e = n->edges[i];
 742                                 if (i != 0)
 743                                         model_print(" ");
 744                                 printCNF(constraintNegate(e));
 745                         }
 746                         model_print(")");
 747                         return;
 748                 }
 749
 750                 model_print("!");
 751         }
 752         switch (getNodeType(e)) {
 753         case NodeType_AND:
 754                 model_print("and");
 755                 break;
 756         case NodeType_ITE:
 757                 model_print("ite");
 758                 break;
 759         case NodeType_IFF:
 760                 model_print("iff");
 761                 break;
 762         }
 763         model_print("(");
 764         for (uint i = 0; i < n->numEdges; i++) {
 765                 Edge e = n->edges[i];
 766                 if (i != 0)
 767                         model_print(" ");
 768                 printCNF(e);
 769         }
 770         model_print(")");
 771 }
 772
 773 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 774         Edge carray[numvars];
 775         for (uint j = 0; j < numvars; j++) {
 776                 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
 777                 value = value >> 1;
 778         }
 779
 780         return constraintAND(cnf, numvars, carray);
 781 }
 782
 783 /** Generates a constraint to ensure that all encodings are less than value */
 784 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 785         Edge orarray[numvars];
 786         Edge andarray[numvars];
 787         uint andi = 0;
 788
 789         while (true) {
 790                 uint val = value;
 791                 uint ori = 0;
 792                 for (uint j = 0; j < numvars; j++) {
 793                         if ((val & 1) == 1)
 794                                 orarray[ori++] = constraintNegate(vars[j]);
 795                         val = val >> 1;
 796                 }
 797                 //no ones to flip, so bail now...
 798                 if (ori == 0) {
 799                         return constraintAND(cnf, andi, andarray);
 800                 }
 801                 andarray[andi++] = constraintOR(cnf, ori, orarray);
 802
 803                 value = value + (1 << (__builtin_ctz(value)));
 804                 //flip the last one
 805         }
 806 }
 807
 808 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
 809         //TO WRITE....
 810 }
 811
 812 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 813         if (numvars == 0)
 814                 return E_True;
 815         Edge array[numvars];
 816         for (uint i = 0; i < numvars; i++) {
 817                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
 818         }
 819         return constraintAND(cnf, numvars, array);
 820 }
 821
 822 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 823         if (numvars == 0 )
 824                 return E_False;
 825         Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
 826         for (uint i = 1; i < numvars; i++) {
 827                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 828                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 829                 result = constraintOR2(cnf, lt, eq);
 830         }
 831         return result;
 832 }
 833
 834 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 835         if (numvars == 0 )
 836                 return E_True;
 837         Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
 838         for (uint i = 1; i < numvars; i++) {
 839                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 840                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 841                 result = constraintOR2(cnf, lt, eq);
 842         }
 843         return result;
 844 }