1 #include "constraint.h"
4 #include "inc_solver.h"
8 CNF SAT Conversion Copyright Brian Demsky 2017.
12 VectorImpl(Edge, Edge, 16)
13 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
14 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
15 Edge E_BOGUS = {(Node *)0xffff5673};
16 Edge E_NULL = {(Node *)NULL};
19 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
21 cnf->solver = allocIncrementalSolver();
24 cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
25 cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
30 void deleteCNF(CNF *cnf) {
31 deleteIncrementalSolver(cnf->solver);
36 void resetCNF(CNF *cnf) {
37 resetSolver(cnf->solver);
44 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
45 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
48 n->numEdges = numEdges;
49 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
53 Node *allocBaseNode(NodeType type, uint numEdges) {
54 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
57 n->numEdges = numEdges;
61 Node *allocResizeNode(uint capacity) {
62 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
65 n->capacity = capacity;
69 Edge cloneEdge(Edge e) {
70 if (edgeIsVarConst(e))
72 Node * node = getNodePtrFromEdge(e);
73 bool isneg = isNegEdge(e);
74 uint numEdges = node->numEdges;
75 Node * clone = allocBaseNode(node->type, numEdges);
76 for(uint i=0; i < numEdges; i++) {
77 clone->edges[i] = cloneEdge(node->edges[i]);
79 return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
82 void freeEdgeRec(Edge e) {
83 if (edgeIsVarConst(e))
85 Node * node = getNodePtrFromEdge(e);
86 uint numEdges = node->numEdges;
87 for(uint i=0; i < numEdges; i++) {
88 freeEdgeRec(node->edges[i]);
93 void freeEdge(Edge e) {
94 if (edgeIsVarConst(e))
96 Node * node = getNodePtrFromEdge(e);
100 void freeEdgesRec(uint numEdges, Edge * earray) {
101 for(uint i=0; i < numEdges; i++) {
107 void freeEdgeCNF(Edge e) {
108 Node * node = getNodePtrFromEdge(e);
109 uint numEdges = node->numEdges;
110 for(uint i=0; i < numEdges; i++) {
111 Edge ec = node->edges[i];
112 if (!edgeIsVarConst(ec)) {
113 ourfree(ec.node_ptr);
119 void addEdgeToResizeNode(Node ** node, Edge e) {
120 Node *currnode = *node;
121 if (currnode->capacity == currnode->numEdges) {
122 Node *newnode = allocResizeNode( currnode->capacity << 1);
123 newnode->numVars = currnode->numVars;
124 newnode->numEdges = currnode->numEdges;
125 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
130 currnode->edges[currnode->numEdges++] = e;
133 void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
134 Node * currnode = *node;
135 uint currEdges = currnode->numEdges;
136 uint inEdges = innode->numEdges;
138 uint newsize = currEdges + inEdges;
139 if (newsize >= currnode->capacity) {
140 if (newsize < innode->capacity) {
142 innode->numVars = currnode->numVars;
145 *node = currnode = tmp;
147 Node *newnode = allocResizeNode( newsize << 1);
148 newnode->numVars = currnode->numVars;
149 newnode->numEdges = currnode->numEdges;
150 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
156 if (inEdges > currEdges && newsize < innode->capacity) {
158 innode->numVars = currnode->numVars;
161 *node = currnode = tmp;
164 memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
165 currnode->numEdges += innode->numEdges;
169 void mergeNodeToResizeNode(Node **node, Node * innode) {
170 Node * currnode = *node;
171 uint currEdges = currnode->numEdges;
172 uint inEdges = innode->numEdges;
173 uint newsize = currEdges + inEdges;
174 if (newsize >= currnode->capacity) {
175 Node *newnode = allocResizeNode( newsize << 1);
176 newnode->numVars = currnode->numVars;
177 newnode->numEdges = currnode->numEdges;
178 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
183 memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
184 currnode->numEdges += inEdges;
187 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
188 Edge e = {allocNode(type, numEdges, edges)};
192 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
193 Edge edgearray[numEdges];
195 for (uint i = 0; i < numEdges; i++) {
196 edgearray[i] = constraintNegate(edges[i]);
198 Edge eand = constraintAND(cnf, numEdges, edgearray);
199 return constraintNegate(eand);
202 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
203 Edge lneg = constraintNegate(left);
204 Edge rneg = constraintNegate(right);
205 Edge eand = constraintAND2(cnf, lneg, rneg);
206 return constraintNegate(eand);
209 int comparefunction(const Edge *e1, const Edge *e2) {
210 if (e1->node_ptr == e2->node_ptr)
212 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
218 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
219 ASSERT(numEdges != 0);
221 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
223 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
226 uint remainSize = numEdges - initindex;
230 else if (remainSize == 1)
231 return edges[initindex];
232 else if (equalsEdge(edges[initindex], E_False)) {
233 freeEdgesRec(numEdges, edges);
237 /** De-duplicate array */
239 edges[lowindex] = edges[initindex++];
241 for (; initindex < numEdges; initindex++) {
242 Edge e1 = edges[lowindex];
243 Edge e2 = edges[initindex];
244 if (sameNodeVarEdge(e1, e2)) {
245 ASSERT(!isNodeEdge(e1));
246 if (!sameSignEdge(e1, e2)) {
247 freeEdgesRec(lowindex + 1, edges);
248 freeEdgesRec(numEdges-initindex, &edges[initindex]);
252 edges[++lowindex] = edges[initindex];
254 lowindex++; //Make lowindex look like size
260 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
261 getNodeType(edges[0]) == NodeType_AND &&
262 getNodeType(edges[1]) == NodeType_AND &&
263 getNodeSize(edges[0]) == 2 &&
264 getNodeSize(edges[1]) == 2) {
265 Edge *e0edges = getEdgeArray(edges[0]);
266 Edge *e1edges = getEdgeArray(edges[1]);
267 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
268 Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
272 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
273 Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
277 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
278 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
282 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
283 Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
290 return createNode(NodeType_AND, lowindex, edges);
293 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
294 Edge edges[2] = {left, right};
295 return constraintAND(cnf, 2, edges);
298 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
301 array[1] = constraintNegate(right);
302 Edge eand = constraintAND(cnf, 2, array);
303 return constraintNegate(eand);
306 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
307 bool negate = !sameSignEdge(left, right);
308 Edge lpos = getNonNeg(left);
309 Edge rpos = getNonNeg(right);
312 if (equalsEdge(lpos, rpos)) {
316 } else if (ltEdge(lpos, rpos)) {
317 Edge edges[] = {lpos, rpos};
318 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
320 Edge edges[] = {rpos, lpos};
321 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
324 e = constraintNegate(e);
328 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
329 if (isNegEdge(cond)) {
330 cond = constraintNegate(cond);
336 bool negate = isNegEdge(thenedge);
338 thenedge = constraintNegate(thenedge);
339 elseedge = constraintNegate(elseedge);
343 if (equalsEdge(cond, E_True)) {
344 freeEdgeRec(elseedge);
346 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
347 Edge array[] = {cond, elseedge};
348 result = constraintOR(cnf, 2, array);
349 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
350 result = constraintIMPLIES(cnf, cond, thenedge);
351 } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
352 Edge array[] = {cond, thenedge};
353 result = constraintAND(cnf, 2, array);
354 } else if (equalsEdge(thenedge, elseedge)) {
357 } else if (sameNodeOppSign(thenedge, elseedge)) {
358 if (ltEdge(cond, thenedge)) {
359 Edge array[] = {cond, thenedge};
360 result = createNode(NodeType_IFF, 2, array);
362 Edge array[] = {thenedge, cond};
363 result = createNode(NodeType_IFF, 2, array);
366 Edge edges[] = {cond, thenedge, elseedge};
367 result = createNode(NodeType_ITE, 3, edges);
370 result = constraintNegate(result);
374 Edge disjoinLit(Edge vec, Edge lit) {
375 Node *nvec = vec.node_ptr;
376 uint nvecedges = nvec->numEdges;
378 for(uint i=0; i < nvecedges; i++) {
379 Edge ce = nvec->edges[i];
380 if (!edgeIsVarConst(ce)) {
381 Node *cne = ce.node_ptr;
382 addEdgeToResizeNode(&cne, lit);
383 nvec->edges[i] = (Edge) {cne};
385 Node *clause = allocResizeNode(2);
386 addEdgeToResizeNode(&clause, lit);
387 addEdgeToResizeNode(&clause, ce);
388 nvec->edges[i] = (Edge) {clause};
391 nvec->numVars+=nvecedges;
395 Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
396 Node *nnewvec = newvec.node_ptr;
397 Node *ncnfform = cnfform.node_ptr;
398 uint newvecedges = nnewvec->numEdges;
399 uint cnfedges = ncnfform->numEdges;
400 uint newvecvars = nnewvec->numVars;
401 uint cnfvars = ncnfform->numVars;
404 ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
405 Edge proxyVar = constraintNewVar(cnf);
406 if (newvecedges > cnfedges) {
407 outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
409 return disjoinLit(cnfform, proxyVar);
411 outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
412 freeEdgeCNF(cnfform);
413 return disjoinLit(newvec, proxyVar);
419 if (newvecedges == 1 || cnfedges ==1) {
424 newvecedges = cnfedges;
427 Edge e = ncnfform->edges[0];
428 if (!edgeIsVarConst(e)) {
429 Node *n = e.node_ptr;
430 for(uint i=0; i < newvecedges; i++) {
431 Edge ce = nnewvec->edges[i];
432 if (isNodeEdge(ce)) {
433 Node *cne = ce.node_ptr;
434 mergeNodeToResizeNode(&cne, n);
435 nnewvec->edges[i] = (Edge) {cne};
437 Node *clause = allocResizeNode(n->numEdges + 1);
438 mergeNodeToResizeNode(&clause, n);
439 addEdgeToResizeNode(&clause, ce);
440 nnewvec->edges[i] = (Edge) {clause};
443 nnewvec->numVars += newvecedges * n->numVars;
445 for(uint i=0; i < newvecedges; i++) {
446 Edge ce = nnewvec->edges[i];
447 if (!edgeIsVarConst(ce)) {
448 Node *cne = ce.node_ptr;
449 addEdgeToResizeNode(&cne, e);
450 nnewvec->edges[i] = (Edge) {cne};
452 Node *clause = allocResizeNode(2);
453 addEdgeToResizeNode(&clause, e);
454 addEdgeToResizeNode(&clause, ce);
455 nnewvec->edges[i] = (Edge) {clause};
458 nnewvec->numVars += newvecedges;
460 freeEdgeCNF((Edge){ncnfform});
461 return (Edge) {nnewvec};
464 Node * result = allocResizeNode(1);
466 for(uint i=0; i <newvecedges; i++) {
467 Edge nedge = nnewvec->edges[i];
468 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
469 for(uint j=0; j < cnfedges; j++) {
470 Edge cedge = ncnfform->edges[j];
471 uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
472 if (equalsEdge(cedge, nedge)) {
473 addEdgeToResizeNode(&result, cedge);
474 result->numVars += cSize;
475 } else if (!sameNodeOppSign(nedge, cedge)) {
476 Node *clause = allocResizeNode(cSize + nSize);
477 if (isNodeEdge(nedge)) {
478 mergeNodeToResizeNode(&clause, nedge.node_ptr);
480 addEdgeToResizeNode(&clause, nedge);
482 if (isNodeEdge(cedge)) {
483 mergeNodeToResizeNode(&clause, cedge.node_ptr);
485 addEdgeToResizeNode(&clause, cedge);
487 addEdgeToResizeNode(&result, (Edge){clause});
488 result->numVars += clause->numEdges;
494 freeEdgeCNF(cnfform);
495 return (Edge) {result};
498 Edge simplifyCNF(CNF *cnf, Edge input) {
499 if (edgeIsVarConst(input)) {
500 Node *newvec = allocResizeNode(1);
501 addEdgeToResizeNode(&newvec, input);
503 return (Edge) {newvec};
505 bool negated = isNegEdge(input);
506 Node * node = getNodePtrFromEdge(input);
507 NodeType type = node->type;
509 if (type == NodeType_AND) {
511 Node *newvec = allocResizeNode(node->numEdges);
512 uint numEdges = node->numEdges;
513 for(uint i = 0; i < numEdges; i++) {
514 Edge e = simplifyCNF(cnf, node->edges[i]);
515 uint enumvars = e.node_ptr->numVars;
516 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
517 newvec->numVars += enumvars;
519 return (Edge) {newvec};
521 Edge cond = node->edges[0];
522 Edge thenedge = node->edges[1];
523 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
524 Edge thenedges[] = {cond, constraintNegate(thenedge)};
525 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
526 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
527 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
528 Edge thencnf = simplifyCNF(cnf, thencons);
529 Edge elsecnf = simplifyCNF(cnf, elsecons);
530 //free temporary nodes
531 ourfree(getNodePtrFromEdge(thencons));
532 ourfree(getNodePtrFromEdge(elsecons));
533 Node * result = thencnf.node_ptr;
534 uint elsenumvars=elsecnf.node_ptr->numVars;
535 mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
536 result->numVars+=elsenumvars;
537 return (Edge) {result};
540 if (type == NodeType_AND) {
542 uint numEdges = node->numEdges;
544 Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
545 for(uint i = 1; i < numEdges; i++) {
546 Edge e = node->edges[i];
547 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
548 newvec = disjoinAndFree(cnf, newvec, cnfform);
552 Edge cond = node->edges[0];
553 Edge thenedge = node->edges[1];
554 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
557 Edge thenedges[] = {cond, constraintNegate(thenedge)};
558 Edge thencons = createNode(NodeType_AND, 2, thenedges);
559 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
560 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
562 Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
563 Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
564 Edge result = simplifyCNF(cnf, combined);
565 //free temporary nodes
566 ourfree(getNodePtrFromEdge(thencons));
567 ourfree(getNodePtrFromEdge(elsecons));
568 ourfree(getNodePtrFromEdge(combined));
574 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
575 Node * andNode = cnfform.node_ptr;
576 int orvar = getEdgeVar(eorvar);
578 uint numEdges = andNode->numEdges;
579 for(uint i=0; i < numEdges; i++) {
580 Edge e = andNode->edges[i];
581 if (edgeIsVarConst(e)) {
582 int array[2] = {getEdgeVar(e), orvar};
583 ASSERT(array[0] != 0);
584 addArrayClauseLiteral(cnf->solver, 2, array);
586 Node * clause = e.node_ptr;
587 uint cnumEdges = clause->numEdges + 1;
588 if (cnumEdges > cnf->asize) {
589 cnf->asize = cnumEdges << 1;
591 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
593 int * array = cnf->array;
594 for(uint j=0; j < (cnumEdges - 1); j++) {
595 array[j] = getEdgeVar(clause->edges[j]);
596 ASSERT(array[j] != 0);
598 array[cnumEdges - 1] = orvar;
599 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
604 void outputCNF(CNF *cnf, Edge cnfform) {
605 Node * andNode = cnfform.node_ptr;
606 uint numEdges = andNode->numEdges;
607 for(uint i=0; i < numEdges; i++) {
608 Edge e = andNode->edges[i];
609 if (edgeIsVarConst(e)) {
610 int array[1] = {getEdgeVar(e)};
611 ASSERT(array[0] != 0);
612 addArrayClauseLiteral(cnf->solver, 1, array);
614 Node * clause = e.node_ptr;
615 uint cnumEdges = clause->numEdges;
616 if (cnumEdges > cnf->asize) {
617 cnf->asize = cnumEdges << 1;
619 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
621 int * array = cnf->array;
622 for(uint j=0; j < cnumEdges; j++) {
623 array[j] = getEdgeVar(clause->edges[j]);
624 ASSERT(array[j] != 0);
626 addArrayClauseLiteral(cnf->solver, cnumEdges, array);
631 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
632 ASSERT(p != P_UNDEFINED);
633 if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
634 // proxy => expression
635 Edge cnfexpr = simplifyCNF(cnf, expression);
637 freeEdgeRec(expression);
638 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
639 freeEdgeCNF(cnfexpr);
641 if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
642 // expression => proxy
643 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
644 freeEdgeRec(expression);
645 outputCNFOR(cnf, cnfnegexpr, proxy);
646 freeEdgeCNF(cnfnegexpr);
650 void addConstraintCNF(CNF *cnf, Edge constraint) {
651 if (equalsEdge(constraint, E_True)) {
653 } else if (equalsEdge(constraint, E_False)) {
658 freeEdgeRec(constraint);
663 model_print("****SATC_ADDING NEW Constraint*****\n");
664 printCNF(constraint);
665 model_print("\n******************************\n");
668 Edge cnfform = simplifyCNF(cnf, constraint);
669 freeEdgeRec(constraint);
670 outputCNF(cnf, cnfform);
671 freeEdgeCNF(cnfform);
674 Edge constraintNewVar(CNF *cnf) {
675 uint varnum = cnf->varcount++;
676 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
680 int solveCNF(CNF *cnf) {
681 long long startTime = getTimeNano();
682 finishedClauses(cnf->solver);
683 long long startSolve = getTimeNano();
684 int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
685 long long finishTime = getTimeNano();
686 cnf->encodeTime = startSolve - startTime;
687 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
688 cnf->solveTime = finishTime - startSolve;
689 model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
693 bool getValueCNF(CNF *cnf, Edge var) {
694 Literal l = getEdgeVar(var);
695 bool isneg = (l < 0);
697 return isneg ^ getValueSolver(cnf->solver, l);
700 void printCNF(Edge e) {
701 if (edgeIsVarConst(e)) {
702 Literal l = getEdgeVar(e);
703 model_print ("%d", l);
706 bool isNeg = isNegEdge(e);
707 if (edgeIsConst(e)) {
714 Node *n = getNodePtrFromEdge(e);
716 //Pretty print things that are equivalent to OR's
717 if (getNodeType(e) == NodeType_AND) {
719 for (uint i = 0; i < n->numEdges; i++) {
720 Edge e = n->edges[i];
723 printCNF(constraintNegate(e));
731 switch (getNodeType(e)) {
743 for (uint i = 0; i < n->numEdges; i++) {
744 Edge e = n->edges[i];
752 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
753 Edge carray[numvars];
754 for (uint j = 0; j < numvars; j++) {
755 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
759 return constraintAND(cnf, numvars, carray);
762 /** Generates a constraint to ensure that all encodings are less than value */
763 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
764 Edge orarray[numvars];
765 Edge andarray[numvars];
771 for (uint j = 0; j < numvars; j++) {
773 orarray[ori++] = constraintNegate(vars[j]);
776 //no ones to flip, so bail now...
778 return constraintAND(cnf, andi, andarray);
780 andarray[andi++] = constraintOR(cnf, ori, orarray);
782 value = value + (1 << (__builtin_ctz(value)));
787 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
791 for (uint i = 0; i < numvars; i++) {
792 array[i] = constraintIFF(cnf, var1[i], var2[i]);
794 return constraintAND(cnf, numvars, array);
797 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
800 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
801 for (uint i = 1; i < numvars; i++) {
802 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
803 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
804 result = constraintOR2(cnf, lt, eq);
809 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
812 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
813 for (uint i = 1; i < numvars; i++) {
814 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
815 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
816 result = constraintOR2(cnf, lt, eq);