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