1 #include "constraint.h"
4 #include "inc_solver.h"
8 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
9 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
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:
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
27 Contact Pete Manolios if you want any of these conditions waived.
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.
39 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
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};
51 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
53 cnf->solver = allocIncrementalSolver();
56 cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
57 cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
62 void deleteCNF(CNF *cnf) {
63 deleteIncrementalSolver(cnf->solver);
68 void resetCNF(CNF *cnf) {
69 resetSolver(cnf->solver);
76 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
77 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
79 n->numEdges = numEdges;
80 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
84 Node *allocBaseNode(NodeType type, uint numEdges) {
85 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
87 n->numEdges = numEdges;
91 Node *allocResizeNode(uint capacity) {
92 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
94 n->capacity = capacity;
98 Edge cloneEdge(Edge e) {
99 if (edgeIsVarConst(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]);
108 return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
111 void freeEdgeRec(Edge e) {
112 if (edgeIsVarConst(e))
114 Node * node = getNodePtrFromEdge(e);
115 uint numEdges = node->numEdges;
116 for(uint i=0; i < numEdges; i++) {
117 freeEdgeRec(node->edges[i]);
122 void freeEdge(Edge e) {
123 if (edgeIsVarConst(e))
125 Node * node = getNodePtrFromEdge(e);
129 void freeEdgesRec(uint numEdges, Edge * earray) {
130 for(uint i=0; i < numEdges; i++) {
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);
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));
158 currnode->edges[currnode->numEdges++] = e;
161 void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
162 Node * currnode = *node;
163 uint currEdges = currnode->numEdges;
164 uint inEdges = innode->numEdges;
166 uint newsize = currEdges + inEdges;
167 if (newsize >= currnode->capacity) {
168 if (newsize < innode->capacity) {
172 *node = currnode = tmp;
174 Node *newnode = allocResizeNode( newsize << 1);
175 newnode->numEdges = currnode->numEdges;
176 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
182 if (inEdges > currEdges && newsize < innode->capacity) {
186 *node = currnode = tmp;
189 memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
190 currnode->numEdges += innode->numEdges;
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));
207 memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
208 currnode->numEdges += inEdges;
211 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
212 Edge e = {allocNode(type, numEdges, edges)};
216 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
217 Edge edgearray[numEdges];
219 for (uint i = 0; i < numEdges; i++) {
220 edgearray[i] = constraintNegate(edges[i]);
222 Edge eand = constraintAND(cnf, numEdges, edgearray);
223 return constraintNegate(eand);
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);
233 int comparefunction(const Edge *e1, const Edge *e2) {
234 if (e1->node_ptr == e2->node_ptr)
236 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
242 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
243 ASSERT(numEdges != 0);
245 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
247 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
250 uint remainSize = numEdges - initindex;
254 else if (remainSize == 1)
255 return edges[initindex];
256 else if (equalsEdge(edges[initindex], E_False)) {
257 freeEdgesRec(numEdges, edges);
261 /** De-duplicate array */
263 edges[lowindex] = edges[initindex++];
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]);
276 edges[++lowindex] = edges[initindex];
278 lowindex++; //Make lowindex look like size
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]));
296 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
297 Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
301 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
302 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
306 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
307 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
314 return createNode(NodeType_AND, lowindex, edges);
317 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
318 Edge edges[2] = {left, right};
319 return constraintAND(cnf, 2, edges);
322 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
325 array[1] = constraintNegate(right);
326 Edge eand = constraintAND(cnf, 2, array);
327 return constraintNegate(eand);
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);
336 if (equalsEdge(lpos, rpos)) {
340 } else if (ltEdge(lpos, rpos)) {
341 Edge edges[] = {lpos, rpos};
342 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
344 Edge edges[] = {rpos, lpos};
345 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
348 e = constraintNegate(e);
352 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
353 if (isNegEdge(cond)) {
354 cond = constraintNegate(cond);
360 bool negate = isNegEdge(thenedge);
362 thenedge = constraintNegate(thenedge);
363 elseedge = constraintNegate(elseedge);
367 if (equalsEdge(cond, E_True)) {
368 freeEdgeRec(elseedge);
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)) {
381 } else if (sameNodeOppSign(thenedge, elseedge)) {
382 if (ltEdge(cond, thenedge)) {
383 Edge array[] = {cond, thenedge};
384 result = createNode(NodeType_IFF, 2, array);
386 Edge array[] = {thenedge, cond};
387 result = createNode(NodeType_IFF, 2, array);
390 Edge edges[] = {cond, thenedge, elseedge};
391 result = createNode(NodeType_ITE, 3, edges);
394 result = constraintNegate(result);
398 Edge simplifyCNF(CNF *cnf, Edge input) {
399 if (edgeIsVarConst(input)) {
400 Node *newvec = allocResizeNode(1);
401 addEdgeToResizeNode(&newvec, input);
402 return (Edge) {newvec};
404 bool negated = isNegEdge(input);
405 Node * node = getNodePtrFromEdge(input);
406 NodeType type = node->type;
408 if (type == NodeType_AND) {
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);
416 return (Edge) {newvec};
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};
435 if (type == NodeType_AND) {
437 uint numEdges = node->numEdges;
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;
446 if (etype == NodeType_AND) {
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));
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);
462 return (Edge) {newnode};
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));
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));
481 clause->edges[i] = constraintNegate(thencons);
482 Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
483 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
485 clause->edges[i] = constraintNegate(elsecons);
486 simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
487 mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
489 //free temporary nodes
490 ourfree(getNodePtrFromEdge(thencons));
491 ourfree(getNodePtrFromEdge(elsecons));
493 return (Edge) {newnode};
496 if (etype == NodeType_AND) {
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));
504 memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
505 Edge eclause = {clause};
506 Edge result = simplifyCNF(cnf, constraintNegate(eclause));
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);
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));
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));
538 Node *newvec = allocResizeNode(numEdges);
539 for(uint i=0; i < numEdges; i++) {
540 addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
542 Node * result = allocResizeNode(1);
543 addEdgeToResizeNode(&result, (Edge){newvec});
544 return (Edge) {result};
546 Edge cond = node->edges[0];
547 Edge thenedge = node->edges[1];
548 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
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);
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));
568 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
569 Node * andNode = cnfform.node_ptr;
570 int orvar = getEdgeVar(eorvar);
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);
580 Node * clause = e.node_ptr;
581 uint cnumEdges = clause->numEdges + 1;
582 if (cnumEdges > cnf->asize) {
583 cnf->asize = cnumEdges << 1;
585 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
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);
592 array[cnumEdges - 1] = orvar;
593 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
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);
609 Node * clause = e.node_ptr;
610 uint cnumEdges = clause->numEdges;
611 if (cnumEdges > cnf->asize) {
612 cnf->asize = cnumEdges << 1;
614 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
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);
621 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
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);
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);
643 void addConstraintCNF(CNF *cnf, Edge constraint) {
644 if (equalsEdge(constraint, E_True)) {
646 } else if (equalsEdge(constraint, E_False)) {
651 freeEdgeRec(constraint);
656 model_print("****SATC_ADDING NEW Constraint*****\n");
657 printCNF(constraint);
658 model_print("\n******************************\n");
661 Edge cnfform = simplifyCNF(cnf, constraint);
662 freeEdgeRec(constraint);
663 outputCNF(cnf, cnfform);
664 freeEdgeCNF(cnfform);
667 Edge constraintNewVar(CNF *cnf) {
668 uint varnum = cnf->varcount++;
669 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
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);
686 bool getValueCNF(CNF *cnf, Edge var) {
687 Literal l = getEdgeVar(var);
688 bool isneg = (l < 0);
690 return isneg ^ getValueSolver(cnf->solver, l);
693 void printCNF(Edge e) {
694 if (edgeIsVarConst(e)) {
695 Literal l = getEdgeVar(e);
696 model_print ("%d", l);
699 bool isNeg = isNegEdge(e);
700 if (edgeIsConst(e)) {
707 Node *n = getNodePtrFromEdge(e);
709 //Pretty print things that are equivalent to OR's
710 if (getNodeType(e) == NodeType_AND) {
712 for (uint i = 0; i < n->numEdges; i++) {
713 Edge e = n->edges[i];
716 printCNF(constraintNegate(e));
724 switch (getNodeType(e)) {
736 for (uint i = 0; i < n->numEdges; i++) {
737 Edge e = n->edges[i];
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]);
752 return constraintAND(cnf, numvars, carray);
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];
764 for (uint j = 0; j < numvars; j++) {
766 orarray[ori++] = constraintNegate(vars[j]);
769 //no ones to flip, so bail now...
771 return constraintAND(cnf, andi, andarray);
773 andarray[andi++] = constraintOR(cnf, ori, orarray);
775 value = value + (1 << (__builtin_ctz(value)));
780 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
784 for (uint i = 0; i < numvars; i++) {
785 array[i] = constraintIFF(cnf, var1[i], var2[i]);
787 return constraintAND(cnf, numvars, array);
790 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
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);
802 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
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);