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