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