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    V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
   9    Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
  10
  11    Permission is hereby granted, free of charge, to any person obtaining
  12    a copy of this software and associated documentation files (the
  13    "Software"), to deal in the Software without restriction, including
  14    without limitation the rights to use, copy, modify, merge, publish,
  15    distribute, sublicense, and/or sell copies of the Software, and to
  16    permit persons to whom the Software is furnished to do so, subject to
  17    the following conditions:
  18
  19    The above copyright notice and this permission notice shall be
  20    included in all copies or substantial portions of the Software.  If
  21    you download or use the software, send email to Pete Manolios
  22    (pete@ccs.neu.edu) with your name, contact information, and a short
  23    note describing what you want to use BAT for.  For any reuse or
  24    distribution, you must make clear to others the license terms of this
  25    work.
  26
  27    Contact Pete Manolios if you want any of these conditions waived.
  28
  29    THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  30    EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  31    MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  32    NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
  33    LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
  34    OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
  35    WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  36  */
  37
  38 /*
  39    C port of CNF SAT Conversion Copyright Brian Demsky 2017.
  40  */
  41
  42
  43 VectorImpl(Edge, Edge, 16)
  44 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
  45 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
  46 Edge E_BOGUS = {(Node *)0xffff5673};
  47 Edge E_NULL = {(Node *)NULL};
  48
  49
  50 CNF *createCNF() {
  51         CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
  52         cnf->varcount = 1;
  53         cnf->solver = allocIncrementalSolver();
  54         cnf->solveTime = 0;
  55         cnf->encodeTime = 0;
  56         cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
  57         cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
  58         cnf->unsat = false;
  59         return cnf;
  60 }
  61
  62 void deleteCNF(CNF *cnf) {
  63         deleteIncrementalSolver(cnf->solver);
  64         ourfree(cnf->array);
  65         ourfree(cnf);
  66 }
  67
  68 void resetCNF(CNF *cnf) {
  69         resetSolver(cnf->solver);
  70         cnf->varcount = 1;
  71         cnf->solveTime = 0;
  72         cnf->encodeTime = 0;
  73         cnf->unsat = false;
  74 }
  75
  76 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
  77         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
  78         n->type = type;
  79         n->numEdges = numEdges;
  80         memcpy(n->edges, edges, sizeof(Edge) * numEdges);
  81         return n;
  82 }
  83
  84 Node *allocBaseNode(NodeType type, uint numEdges) {
  85         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
  86         n->type = type;
  87         n->numEdges = numEdges;
  88         return n;
  89 }
  90
  91 Node *allocResizeNode(uint capacity) {
  92         Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
  93         n->numEdges = 0;
  94         n->capacity = capacity;
  95         return n;
  96 }
  97
  98 Edge cloneEdge(Edge e) {
  99         if (edgeIsVarConst(e))
 100                 return e;
 101         Node * node = getNodePtrFromEdge(e);
 102         bool isneg = isNegEdge(e);
 103         uint numEdges = node->numEdges;
 104         Node * clone = allocBaseNode(node->type, numEdges);
 105         for(uint i=0; i < numEdges; i++) {
 106                 clone->edges[i] = cloneEdge(node->edges[i]);
 107         }
 108         return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
 109 }
 110
 111 void freeEdgeRec(Edge e) {
 112         if (edgeIsVarConst(e))
 113                 return;
 114         Node * node = getNodePtrFromEdge(e);
 115         uint numEdges = node->numEdges;
 116         for(uint i=0; i < numEdges; i++) {
 117                 freeEdgeRec(node->edges[i]);
 118         }
 119 }
 120
 121 void freeEdgeCNF(Edge e) {
 122         Node * node = getNodePtrFromEdge(e);
 123         uint numEdges = node->numEdges;
 124         for(uint i=0; i < numEdges; i++) {
 125                 Edge ec = node->edges[i];
 126                 if (!edgeIsVarConst(ec)) {
 127                         ourfree(ec.node_ptr);
 128                 }
 129         }
 130         ourfree(node);
 131 }
 132
 133 void addEdgeToResizeNode(Node ** node, Edge e) {
 134         Node *currnode = *node;
 135         if (currnode->capacity == currnode->numEdges) {
 136                 Node *newnode = allocResizeNode( currnode->capacity << 1);
 137                 newnode->numEdges = currnode->numEdges;
 138                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 139                 ourfree(currnode);
 140                 *node=newnode;
 141                 currnode = newnode;
 142         }
 143         currnode->edges[currnode->numEdges++] = e;
 144 }
 145
 146 void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
 147         Node * currnode = *node;
 148         uint currEdges = currnode->numEdges;
 149         uint inEdges = innode->numEdges;
 150
 151         uint newsize = currEdges + inEdges;
 152         if (newsize >= currnode->capacity) {
 153                 if (newsize < innode->capacity) {
 154                         //just swap
 155                         Node *tmp = innode;
 156                         innode = currnode;
 157                         *node = currnode = tmp;
 158                 } else {
 159                         Node *newnode = allocResizeNode( newsize << 1);
 160                         newnode->numEdges = currnode->numEdges;
 161                         memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 162                         ourfree(currnode);
 163                         *node=newnode;
 164                         currnode = newnode;
 165                 }
 166         } else {
 167                 if (inEdges > currEdges && newsize < innode->capacity) {
 168                         //just swap
 169                         Node *tmp = innode;
 170                         innode = currnode;
 171                         *node = currnode = tmp;
 172                 }
 173         }
 174         memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
 175         currnode->numEdges += innode->numEdges;
 176         ourfree(innode);
 177 }
 178
 179 void mergeNodeToResizeNode(Node **node, Node * innode) {
 180         Node * currnode = *node;
 181         uint currEdges = currnode->numEdges;
 182         uint inEdges = innode->numEdges;
 183         uint newsize = currEdges + inEdges;
 184         if (newsize >= currnode->capacity) {
 185                 Node *newnode = allocResizeNode( newsize << 1);
 186                 newnode->numEdges = currnode->numEdges;
 187                 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 188                 ourfree(currnode);
 189                 *node=newnode;
 190                 currnode = newnode;
 191         }
 192         memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
 193         currnode->numEdges += inEdges;
 194 }
 195
 196 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
 197         Edge e = {allocNode(type, numEdges, edges)};
 198         return e;
 199 }
 200
 201 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
 202         Edge edgearray[numEdges];
 203
 204         for (uint i = 0; i < numEdges; i++) {
 205                 edgearray[i] = constraintNegate(edges[i]);
 206         }
 207         Edge eand = constraintAND(cnf, numEdges, edgearray);
 208         return constraintNegate(eand);
 209 }
 210
 211 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
 212         Edge lneg = constraintNegate(left);
 213         Edge rneg = constraintNegate(right);
 214         Edge eand = constraintAND2(cnf, lneg, rneg);
 215         return constraintNegate(eand);
 216 }
 217
 218 int comparefunction(const Edge *e1, const Edge *e2) {
 219         if (e1->node_ptr == e2->node_ptr)
 220                 return 0;
 221         if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
 222                 return -1;
 223         else
 224                 return 1;
 225 }
 226
 227 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 228         ASSERT(numEdges != 0);
 229
 230         bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
 231         uint initindex = 0;
 232         while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
 233                 initindex++;
 234
 235         uint remainSize = numEdges - initindex;
 236
 237         if (remainSize == 0)
 238                 return E_True;
 239         else if (remainSize == 1)
 240                 return edges[initindex];
 241         else if (equalsEdge(edges[initindex], E_False))
 242                 return E_False;
 243
 244         /** De-duplicate array */
 245         uint lowindex = 0;
 246         edges[lowindex] = edges[initindex++];
 247
 248         for (; initindex < numEdges; initindex++) {
 249                 Edge e1 = edges[lowindex];
 250                 Edge e2 = edges[initindex];
 251                 if (sameNodeVarEdge(e1, e2)) {
 252                         if (!sameSignEdge(e1, e2)) {
 253                                 return E_False;
 254                         }
 255                 } else
 256                         edges[++lowindex] = edges[initindex];
 257         }
 258         lowindex++;     //Make lowindex look like size
 259
 260         if (lowindex == 1)
 261                 return edges[0];
 262
 263         if (lowindex == 2 &&
 264                         isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
 265                         getNodeType(edges[0]) == NodeType_AND &&
 266                         getNodeType(edges[1]) == NodeType_AND &&
 267                         getNodeSize(edges[0]) == 2 &&
 268                         getNodeSize(edges[1]) == 2) {
 269                 Edge *e0edges = getEdgeArray(edges[0]);
 270                 Edge *e1edges = getEdgeArray(edges[1]);
 271                 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
 272                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 273                 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
 274                         return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 275                 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
 276                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 277                 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
 278                         return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 279                 }
 280         }
 281
 282         return createNode(NodeType_AND, lowindex, edges);
 283 }
 284
 285 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
 286         Edge edges[2] = {left, right};
 287         return constraintAND(cnf, 2, edges);
 288 }
 289
 290 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
 291         Edge array[2];
 292         array[0] = left;
 293         array[1] = constraintNegate(right);
 294         Edge eand = constraintAND(cnf, 2, array);
 295         return constraintNegate(eand);
 296 }
 297
 298 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
 299         bool negate = !sameSignEdge(left, right);
 300         Edge lpos = getNonNeg(left);
 301         Edge rpos = getNonNeg(right);
 302
 303         Edge e;
 304         if (equalsEdge(lpos, rpos)) {
 305                 e = E_True;
 306         } else if (ltEdge(lpos, rpos)) {
 307                 Edge edges[] = {lpos, rpos};
 308                 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
 309         } else {
 310                 Edge edges[] = {rpos, lpos};
 311                 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
 312         }
 313         if (negate)
 314                 e = constraintNegate(e);
 315         return e;
 316 }
 317
 318 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
 319         if (isNegEdge(cond)) {
 320                 cond = constraintNegate(cond);
 321                 Edge tmp = thenedge;
 322                 thenedge = elseedge;
 323                 elseedge = tmp;
 324         }
 325
 326         bool negate = isNegEdge(thenedge);
 327         if (negate) {
 328                 thenedge = constraintNegate(thenedge);
 329                 elseedge = constraintNegate(elseedge);
 330         }
 331
 332         Edge result;
 333         if (equalsEdge(cond, E_True)) {
 334                 result = thenedge;
 335         } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
 336                 Edge array[] = {cond, elseedge};
 337                 result = constraintOR(cnf,  2, array);
 338         } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
 339                 result = constraintIMPLIES(cnf, cond, thenedge);
 340         } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
 341                 Edge array[] = {cond, thenedge};
 342                 result = constraintAND(cnf, 2, array);
 343         } else if (equalsEdge(thenedge, elseedge)) {
 344                 result = thenedge;
 345         } else if (sameNodeOppSign(thenedge, elseedge)) {
 346                 if (ltEdge(cond, thenedge)) {
 347                         Edge array[] = {cond, thenedge};
 348                         result = createNode(NodeType_IFF, 2, array);
 349                 } else {
 350                         Edge array[] = {thenedge, cond};
 351                         result = createNode(NodeType_IFF, 2, array);
 352                 }
 353         } else {
 354                 Edge edges[] = {cond, thenedge, elseedge};
 355                 result = createNode(NodeType_ITE, 3, edges);
 356         }
 357         if (negate)
 358                 result = constraintNegate(result);
 359         return result;
 360 }
 361
 362 Edge simplifyCNF(CNF *cnf, Edge input) {
 363         if (edgeIsVarConst(input)) {
 364                 Node *newvec = allocResizeNode(1);
 365                 addEdgeToResizeNode(&newvec, input);
 366                 return (Edge) {newvec};
 367         }
 368         bool negated = isNegEdge(input);
 369         Node * node = getNodePtrFromEdge(input);
 370         NodeType type = node->type;
 371         if (!negated) {
 372                 if (type == NodeType_AND) {
 373                         //AND case
 374                         Node *newvec = allocResizeNode(node->numEdges);
 375                         uint numEdges = node->numEdges;
 376                         for(uint i = 0; i < numEdges; i++) {
 377                                 Edge e = simplifyCNF(cnf, node->edges[i]);
 378                                 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
 379                         }
 380                         return (Edge) {newvec};
 381                 } else {
 382                         Edge cond = node->edges[0];
 383                         Edge thenedge = node->edges[1];
 384                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 385                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 386                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
 387                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 388                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
 389                         Edge thencnf = simplifyCNF(cnf, thencons);
 390                         Edge elsecnf = simplifyCNF(cnf, elsecons);
 391                         //free temporary nodes
 392                         ourfree(getNodePtrFromEdge(thencons));
 393                         ourfree(getNodePtrFromEdge(elsecons));
 394                         Node * result = thencnf.node_ptr;
 395                         mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
 396                         return (Edge) {result};
 397                 }
 398         } else {
 399                 if (type == NodeType_AND) {
 400                         //OR Case
 401                         uint numEdges = node->numEdges;
 402
 403                         for(uint i = 0; i < numEdges; i++) {
 404                                 Edge e = node->edges[i];
 405                                 bool enegate = isNegEdge(e);
 406                                 if (!edgeIsVarConst(e)) {
 407                                         Node * enode = getNodePtrFromEdge(e);
 408                                         NodeType etype = enode->type;
 409                                         if (enegate) {
 410                                                 if (etype == NodeType_AND) {
 411                                                         //OR of AND Case
 412                                                         uint eNumEdges = enode->numEdges;
 413                                                         Node * newnode = allocResizeNode(0);
 414                                                         Node * clause = allocBaseNode(NodeType_AND, numEdges);
 415                                                         memcpy(clause->edges, node->edges, sizeof(Edge) * i);
 416                                                         if ((i + 1) < numEdges) {
 417                                                                 memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
 418                                                         }
 419
 420                                                         for(uint j = 0; j < eNumEdges; j++) {
 421                                                                 clause->edges[i] = constraintNegate(enode->edges[j]);
 422                                                                 Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
 423                                                                 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
 424                                                         }
 425                                                         ourfree(clause);
 426                                                         return (Edge) {newnode};
 427                                                 } else {
 428                                                         //OR of IFF or ITE
 429                                                         Edge cond = enode->edges[0];
 430                                                         Edge thenedge = enode->edges[1];
 431                                                         Edge elseedge = (enode->type == NodeType_IFF) ? constraintNegate(thenedge) : enode->edges[2];
 432                                                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 433                                                         Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
 434                                                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 435                                                         Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
 436
 437                                                         //OR of AND Case
 438                                                         Node * newnode = allocResizeNode(0);
 439                                                         Node * clause = allocBaseNode(NodeType_AND, numEdges);
 440                                                         memcpy(clause->edges, node->edges, sizeof(Edge) * i);
 441                                                         if ((i + 1) < numEdges) {
 442                                                                 memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
 443                                                         }
 444
 445                                                         clause->edges[i] = constraintNegate(thencons);
 446                                                         Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
 447                                                         mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
 448
 449                                                         clause->edges[i] = constraintNegate(elsecons);
 450                                                         simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
 451                                                         mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
 452
 453                                                         //free temporary nodes
 454                                                         ourfree(getNodePtrFromEdge(thencons));
 455                                                         ourfree(getNodePtrFromEdge(elsecons));
 456                                                         ourfree(clause);
 457                                                         return (Edge) {newnode};
 458                                                 }
 459                                         } else {
 460                                                 if (etype == NodeType_AND) {
 461                                                         //OR of OR Case
 462                                                         uint eNumEdges = enode->numEdges;
 463                                                         Node * clause = allocBaseNode(NodeType_AND, eNumEdges + numEdges - 1);
 464                                                         memcpy(clause->edges, node->edges, sizeof(Edge) * i);
 465                                                         if ((i + 1) < numEdges) {
 466                                                                 memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
 467                                                         }
 468                                                         memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
 469                                                         Edge eclause = {clause};
 470                                                         Edge result = simplifyCNF(cnf, constraintNegate(eclause));
 471                                                         ourfree(clause);
 472                                                         return result;
 473                                                 } else {
 474                                                         //OR of !(IFF or ITE)
 475                                                         Edge cond = node->edges[0];
 476                                                         Edge thenedge = node->edges[1];
 477                                                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 478                                                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 479                                                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
 480                                                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 481                                                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
 482
 483
 484                                                         Node * clause = allocBaseNode(NodeType_AND, numEdges + 1);
 485                                                         memcpy(clause->edges, node->edges, sizeof(Edge) * i);
 486                                                         if ((i + 1) < numEdges) {
 487                                                                 memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
 488                                                         }
 489                                                         clause->edges[numEdges-1] = constraintNegate(thencons);
 490                                                         clause->edges[numEdges] = constraintNegate(elsecons);
 491                                                         Edge result = simplifyCNF(cnf, constraintNegate((Edge) {clause}));
 492                                                         //free temporary nodes
 493                                                         ourfree(getNodePtrFromEdge(thencons));
 494                                                         ourfree(getNodePtrFromEdge(elsecons));
 495                                                         ourfree(clause);
 496                                                         return result;
 497                                                 }
 498                                         }
 499                                 }
 500                         }
 501
 502                         Node *newvec = allocResizeNode(numEdges);
 503                         for(uint i=0; i < numEdges; i++) {
 504                                 addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
 505                         }
 506                         Node * result = allocResizeNode(1);
 507                         addEdgeToResizeNode(&result, (Edge){newvec});
 508                         return (Edge) {result};
 509                 } else {
 510                         Edge cond = node->edges[0];
 511                         Edge thenedge = node->edges[1];
 512                         Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
 513
 514
 515                         Edge thenedges[] = {cond, constraintNegate(thenedge)};
 516                         Edge thencons = createNode(NodeType_AND, 2, thenedges);
 517                         Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 518                         Edge elsecons = createNode(NodeType_AND, 2, elseedges);
 519
 520                         Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
 521                         Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
 522                         Edge result = simplifyCNF(cnf, combined);
 523                         //free temporary nodes
 524                         ourfree(getNodePtrFromEdge(thencons));
 525                         ourfree(getNodePtrFromEdge(elsecons));
 526                         ourfree(getNodePtrFromEdge(combined));
 527                         return result;
 528                 }
 529         }
 530 }
 531
 532 void outputCNF(CNF *cnf, Edge cnfform) {
 533         Node * andNode = cnfform.node_ptr;
 534         uint numEdges = andNode->numEdges;
 535         for(uint i=0; i < numEdges; i++) {
 536                 Edge e = andNode->edges[i];
 537                 if (edgeIsVarConst(e)) {
 538                         int array[1] = {getEdgeVar(e)};
 539                         ASSERT(array[0] != 0);
 540                         addArrayClauseLiteral(cnf->solver, 1, array);
 541                 } else {
 542                         Node * clause = e.node_ptr;
 543                         uint cnumEdges = clause->numEdges;
 544                         if (cnumEdges > cnf->asize) {
 545                                 cnf->asize = cnumEdges << 1;
 546                                 ourfree(cnf->array);
 547                                 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 548                         }
 549                         int * array = cnf->array;
 550                         for(uint j=0; j < cnumEdges; j++) {
 551                                 array[j] = getEdgeVar(clause->edges[j]);
 552                                 ASSERT(array[j] != 0);
 553                         }
 554                         addArrayClauseLiteral(cnf->solver, cnumEdges, array);
 555                 }
 556         }
 557 }
 558
 559 void addConstraintCNF(CNF *cnf, Edge constraint) {
 560         if (equalsEdge(constraint, E_True))
 561                 return;
 562         else if (equalsEdge(constraint, E_False)) {
 563                 cnf->unsat = true;
 564                 return;
 565         }
 566
 567         Edge cnfform = simplifyCNF(cnf, constraint);
 568         freeEdgeRec(constraint);
 569         outputCNF(cnf, cnfform);
 570         freeEdgeCNF(cnfform);
 571 #ifdef CONFIG_DEBUG
 572         model_print("****SATC_ADDING NEW Constraint*****\n");
 573         printCNF(constraint);
 574         model_print("\n******************************\n");
 575 #endif
 576 }
 577
 578 Edge constraintNewVar(CNF *cnf) {
 579         uint varnum = cnf->varcount++;
 580         Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
 581         return e;
 582 }
 583
 584 int solveCNF(CNF *cnf) {
 585         long long startTime = getTimeNano();
 586         finishedClauses(cnf->solver);
 587         long long startSolve = getTimeNano();
 588         int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
 589         long long finishTime = getTimeNano();
 590         cnf->encodeTime = startSolve - startTime;
 591         model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
 592         cnf->solveTime = finishTime - startSolve;
 593         model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
 594         return result;
 595 }
 596
 597 bool getValueCNF(CNF *cnf, Edge var) {
 598         Literal l = getEdgeVar(var);
 599         bool isneg = (l < 0);
 600         l = abs(l);
 601         return isneg ^ getValueSolver(cnf->solver, l);
 602 }
 603
 604 void printCNF(Edge e) {
 605         if (edgeIsVarConst(e)) {
 606                 Literal l = getEdgeVar(e);
 607                 model_print ("%d", l);
 608                 return;
 609         }
 610         bool isNeg = isNegEdge(e);
 611         if (edgeIsConst(e)) {
 612                 if (isNeg)
 613                         model_print("T");
 614                 else
 615                         model_print("F");
 616                 return;
 617         }
 618         Node *n = getNodePtrFromEdge(e);
 619         if (isNeg) {
 620                 //Pretty print things that are equivalent to OR's
 621                 if (getNodeType(e) == NodeType_AND) {
 622                         model_print("or(");
 623                         for (uint i = 0; i < n->numEdges; i++) {
 624                                 Edge e = n->edges[i];
 625                                 if (i != 0)
 626                                         model_print(" ");
 627                                 printCNF(constraintNegate(e));
 628                         }
 629                         model_print(")");
 630                         return;
 631                 }
 632
 633                 model_print("!");
 634         }
 635         switch (getNodeType(e)) {
 636         case NodeType_AND:
 637                 model_print("and");
 638                 break;
 639         case NodeType_ITE:
 640                 model_print("ite");
 641                 break;
 642         case NodeType_IFF:
 643                 model_print("iff");
 644                 break;
 645         }
 646         model_print("(");
 647         for (uint i = 0; i < n->numEdges; i++) {
 648                 Edge e = n->edges[i];
 649                 if (i != 0)
 650                         model_print(" ");
 651                 printCNF(e);
 652         }
 653         model_print(")");
 654 }
 655
 656 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 657         Edge carray[numvars];
 658         for (uint j = 0; j < numvars; j++) {
 659                 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
 660                 value = value >> 1;
 661         }
 662
 663         return constraintAND(cnf, numvars, carray);
 664 }
 665
 666 /** Generates a constraint to ensure that all encodings are less than value */
 667 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 668         Edge orarray[numvars];
 669         Edge andarray[numvars];
 670         uint andi = 0;
 671
 672         while (true) {
 673                 uint val = value;
 674                 uint ori = 0;
 675                 for (uint j = 0; j < numvars; j++) {
 676                         if ((val & 1) == 1)
 677                                 orarray[ori++] = constraintNegate(vars[j]);
 678                         val = val >> 1;
 679                 }
 680                 //no ones to flip, so bail now...
 681                 if (ori == 0) {
 682                         return constraintAND(cnf, andi, andarray);
 683                 }
 684                 andarray[andi++] = constraintOR(cnf, ori, orarray);
 685
 686                 value = value + (1 << (__builtin_ctz(value)));
 687                 //flip the last one
 688         }
 689 }
 690
 691 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 692         if (numvars == 0)
 693                 return E_True;
 694         Edge array[numvars];
 695         for (uint i = 0; i < numvars; i++) {
 696                 array[i] = constraintIFF(cnf, var1[i], var2[i]);
 697         }
 698         return constraintAND(cnf, numvars, array);
 699 }
 700
 701 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 702         if (numvars == 0 )
 703                 return E_False;
 704         Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
 705         for (uint i = 1; i < numvars; i++) {
 706                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 707                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 708                 result = constraintOR2(cnf, lt, eq);
 709         }
 710         return result;
 711 }
 712
 713 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 714         if (numvars == 0 )
 715                 return E_True;
 716         Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
 717         for (uint i = 1; i < numvars; i++) {
 718                 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
 719                 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
 720                 result = constraintOR2(cnf, lt, eq);
 721         }
 722         return result;
 723 }