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));
22 cnf->solver = allocIncrementalSolver();
25 cnf->asize = DEFAULT_CNF_ARRAY_SIZE;
26 cnf->array = (int *) ourmalloc(sizeof(int) * DEFAULT_CNF_ARRAY_SIZE);
31 void deleteCNF(CNF *cnf) {
32 deleteIncrementalSolver(cnf->solver);
37 void resetCNF(CNF *cnf) {
38 resetSolver(cnf->solver);
46 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
47 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
50 n->numEdges = numEdges;
51 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
55 Node *allocBaseNode(NodeType type, uint numEdges) {
56 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
59 n->numEdges = numEdges;
63 Node *allocResizeNode(uint capacity) {
64 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
67 n->capacity = capacity;
71 Edge cloneEdge(Edge e) {
72 if (edgeIsVarConst(e))
74 Node *node = getNodePtrFromEdge(e);
75 bool isneg = isNegEdge(e);
76 uint numEdges = node->numEdges;
77 Node *clone = allocBaseNode(node->type, numEdges);
78 for (uint i = 0; i < numEdges; i++) {
79 clone->edges[i] = cloneEdge(node->edges[i]);
81 return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
84 void freeEdgeRec(Edge e) {
85 if (edgeIsVarConst(e))
87 Node *node = getNodePtrFromEdge(e);
88 uint numEdges = node->numEdges;
89 for (uint i = 0; i < numEdges; i++) {
90 freeEdgeRec(node->edges[i]);
95 void freeEdge(Edge e) {
96 if (edgeIsVarConst(e))
98 Node *node = getNodePtrFromEdge(e);
102 void freeEdgesRec(uint numEdges, Edge *earray) {
103 for (uint i = 0; i < numEdges; i++) {
109 void freeEdgeCNF(Edge e) {
110 Node *node = getNodePtrFromEdge(e);
111 uint numEdges = node->numEdges;
112 for (uint i = 0; i < numEdges; i++) {
113 Edge ec = node->edges[i];
114 if (!edgeIsVarConst(ec)) {
115 ourfree(ec.node_ptr);
121 void addEdgeToResizeNode(Node **node, Edge e) {
122 Node *currnode = *node;
123 if (currnode->capacity == currnode->numEdges) {
124 Node *newnode = allocResizeNode( currnode->capacity << 1);
125 newnode->numVars = currnode->numVars;
126 newnode->numEdges = currnode->numEdges;
127 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
132 currnode->edges[currnode->numEdges++] = e;
135 void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
136 Node *currnode = *node;
137 uint currEdges = currnode->numEdges;
138 uint inEdges = innode->numEdges;
140 uint newsize = currEdges + inEdges;
141 if (newsize >= currnode->capacity) {
142 if (newsize < innode->capacity) {
144 innode->numVars = currnode->numVars;
147 *node = currnode = tmp;
149 Node *newnode = allocResizeNode( newsize << 1);
150 newnode->numVars = currnode->numVars;
151 newnode->numEdges = currnode->numEdges;
152 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
158 if (inEdges > currEdges && newsize < innode->capacity) {
160 innode->numVars = currnode->numVars;
163 *node = currnode = tmp;
166 memcpy(&currnode->edges[currnode->numEdges], innode->edges, innode->numEdges * sizeof(Edge));
167 currnode->numEdges += innode->numEdges;
171 void mergeNodeToResizeNode(Node **node, Node *innode) {
172 Node *currnode = *node;
173 uint currEdges = currnode->numEdges;
174 uint inEdges = innode->numEdges;
175 uint newsize = currEdges + inEdges;
176 if (newsize >= currnode->capacity) {
177 Node *newnode = allocResizeNode( newsize << 1);
178 newnode->numVars = currnode->numVars;
179 newnode->numEdges = currnode->numEdges;
180 memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
185 memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
186 currnode->numEdges += inEdges;
189 Edge createNode(NodeType type, uint numEdges, Edge *edges) {
190 Edge e = {allocNode(type, numEdges, edges)};
194 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
195 if (numEdges < 200000) {
196 Edge edgearray[numEdges];
198 for (uint i = 0; i < numEdges; i++) {
199 edgearray[i] = constraintNegate(edges[i]);
201 Edge eand = constraintAND(cnf, numEdges, edgearray);
202 return constraintNegate(eand);
204 Edge *edgearray = (Edge *)ourmalloc(numEdges * sizeof(Edge));
206 for (uint i = 0; i < numEdges; i++) {
207 edgearray[i] = constraintNegate(edges[i]);
209 Edge eand = constraintAND(cnf, numEdges, edgearray);
211 return constraintNegate(eand);
215 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
216 Edge lneg = constraintNegate(left);
217 Edge rneg = constraintNegate(right);
218 Edge eand = constraintAND2(cnf, lneg, rneg);
219 return constraintNegate(eand);
222 int comparefunction(const Edge *e1, const Edge *e2) {
223 if (e1->node_ptr == e2->node_ptr)
225 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
231 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
232 ASSERT(numEdges != 0);
234 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
236 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
239 uint remainSize = numEdges - initindex;
243 else if (remainSize == 1)
244 return edges[initindex];
245 else if (equalsEdge(edges[initindex], E_False)) {
246 freeEdgesRec(numEdges, edges);
250 /** De-duplicate array */
252 edges[lowindex] = edges[initindex++];
254 for (; initindex < numEdges; initindex++) {
255 Edge e1 = edges[lowindex];
256 Edge e2 = edges[initindex];
257 if (sameNodeVarEdge(e1, e2)) {
258 ASSERT(!isNodeEdge(e1));
259 if (!sameSignEdge(e1, e2)) {
260 freeEdgesRec(lowindex + 1, edges);
261 freeEdgesRec(numEdges - initindex, &edges[initindex]);
265 edges[++lowindex] = edges[initindex];
267 lowindex++; //Make lowindex look like size
273 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
274 getNodeType(edges[0]) == NodeType_AND &&
275 getNodeType(edges[1]) == NodeType_AND &&
276 getNodeSize(edges[0]) == 2 &&
277 getNodeSize(edges[1]) == 2) {
278 Edge *e0edges = getEdgeArray(edges[0]);
279 Edge *e1edges = getEdgeArray(edges[1]);
280 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
281 Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
285 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
286 Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
290 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
291 Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
295 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
296 Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
303 return createNode(NodeType_AND, lowindex, edges);
306 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
307 Edge edges[2] = {left, right};
308 return constraintAND(cnf, 2, edges);
311 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
314 array[1] = constraintNegate(right);
315 Edge eand = constraintAND(cnf, 2, array);
316 return constraintNegate(eand);
319 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
320 bool negate = !sameSignEdge(left, right);
321 Edge lpos = getNonNeg(left);
322 Edge rpos = getNonNeg(right);
325 if (equalsEdge(lpos, rpos)) {
329 } else if (ltEdge(lpos, rpos)) {
330 Edge edges[] = {lpos, rpos};
331 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
333 Edge edges[] = {rpos, lpos};
334 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
337 e = constraintNegate(e);
341 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
342 if (isNegEdge(cond)) {
343 cond = constraintNegate(cond);
349 bool negate = isNegEdge(thenedge);
351 thenedge = constraintNegate(thenedge);
352 elseedge = constraintNegate(elseedge);
356 if (equalsEdge(cond, E_True)) {
357 freeEdgeRec(elseedge);
359 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
360 Edge array[] = {cond, elseedge};
361 result = constraintOR(cnf, 2, array);
362 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
363 result = constraintIMPLIES(cnf, cond, thenedge);
364 } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
365 Edge array[] = {cond, thenedge};
366 result = constraintAND(cnf, 2, array);
367 } else if (equalsEdge(thenedge, elseedge)) {
370 } else if (sameNodeOppSign(thenedge, elseedge)) {
371 if (ltEdge(cond, thenedge)) {
372 Edge array[] = {cond, thenedge};
373 result = createNode(NodeType_IFF, 2, array);
375 Edge array[] = {thenedge, cond};
376 result = createNode(NodeType_IFF, 2, array);
379 Edge edges[] = {cond, thenedge, elseedge};
380 result = createNode(NodeType_ITE, 3, edges);
383 result = constraintNegate(result);
387 Edge disjoinLit(Edge vec, Edge lit) {
388 Node *nvec = vec.node_ptr;
389 uint nvecedges = nvec->numEdges;
391 for (uint i = 0; i < nvecedges; i++) {
392 Edge ce = nvec->edges[i];
393 if (!edgeIsVarConst(ce)) {
394 Node *cne = ce.node_ptr;
395 addEdgeToResizeNode(&cne, lit);
396 nvec->edges[i] = (Edge) {cne};
398 Node *clause = allocResizeNode(2);
399 addEdgeToResizeNode(&clause, lit);
400 addEdgeToResizeNode(&clause, ce);
401 nvec->edges[i] = (Edge) {clause};
404 nvec->numVars += nvecedges;
408 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
409 Node *nnewvec = newvec.node_ptr;
410 Node *ncnfform = cnfform.node_ptr;
411 uint newvecedges = nnewvec->numEdges;
412 uint cnfedges = ncnfform->numEdges;
413 uint newvecvars = nnewvec->numVars;
414 uint cnfvars = ncnfform->numVars;
417 ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
418 Edge proxyVar = constraintNewVar(cnf);
419 if (newvecedges > cnfedges) {
420 outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
422 return disjoinLit(cnfform, proxyVar);
424 outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
425 freeEdgeCNF(cnfform);
426 return disjoinLit(newvec, proxyVar);
432 if (newvecedges == 1 || cnfedges == 1) {
437 newvecedges = cnfedges;
440 Edge e = ncnfform->edges[0];
441 if (!edgeIsVarConst(e)) {
442 Node *n = e.node_ptr;
443 for (uint i = 0; i < newvecedges; i++) {
444 Edge ce = nnewvec->edges[i];
445 if (isNodeEdge(ce)) {
446 Node *cne = ce.node_ptr;
447 mergeNodeToResizeNode(&cne, n);
448 nnewvec->edges[i] = (Edge) {cne};
450 Node *clause = allocResizeNode(n->numEdges + 1);
451 mergeNodeToResizeNode(&clause, n);
452 addEdgeToResizeNode(&clause, ce);
453 nnewvec->edges[i] = (Edge) {clause};
456 nnewvec->numVars += newvecedges * n->numVars;
458 for (uint i = 0; i < newvecedges; i++) {
459 Edge ce = nnewvec->edges[i];
460 if (!edgeIsVarConst(ce)) {
461 Node *cne = ce.node_ptr;
462 addEdgeToResizeNode(&cne, e);
463 nnewvec->edges[i] = (Edge) {cne};
465 Node *clause = allocResizeNode(2);
466 addEdgeToResizeNode(&clause, e);
467 addEdgeToResizeNode(&clause, ce);
468 nnewvec->edges[i] = (Edge) {clause};
471 nnewvec->numVars += newvecedges;
473 freeEdgeCNF((Edge) {ncnfform});
474 return (Edge) {nnewvec};
477 Node *result = allocResizeNode(1);
479 for (uint i = 0; i < newvecedges; i++) {
480 Edge nedge = nnewvec->edges[i];
481 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
482 for (uint j = 0; j < cnfedges; j++) {
483 Edge cedge = ncnfform->edges[j];
484 uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
485 if (equalsEdge(cedge, nedge)) {
486 addEdgeToResizeNode(&result, cedge);
487 result->numVars += cSize;
488 } else if (!sameNodeOppSign(nedge, cedge)) {
489 Node *clause = allocResizeNode(cSize + nSize);
490 if (isNodeEdge(nedge)) {
491 mergeNodeToResizeNode(&clause, nedge.node_ptr);
493 addEdgeToResizeNode(&clause, nedge);
495 if (isNodeEdge(cedge)) {
496 mergeNodeToResizeNode(&clause, cedge.node_ptr);
498 addEdgeToResizeNode(&clause, cedge);
500 addEdgeToResizeNode(&result, (Edge) {clause});
501 result->numVars += clause->numEdges;
507 freeEdgeCNF(cnfform);
508 return (Edge) {result};
511 Edge simplifyCNF(CNF *cnf, Edge input) {
512 if (edgeIsVarConst(input)) {
513 Node *newvec = allocResizeNode(1);
514 addEdgeToResizeNode(&newvec, input);
516 return (Edge) {newvec};
518 bool negated = isNegEdge(input);
519 Node *node = getNodePtrFromEdge(input);
520 NodeType type = node->type;
522 if (type == NodeType_AND) {
524 Node *newvec = allocResizeNode(node->numEdges);
525 uint numEdges = node->numEdges;
526 for (uint i = 0; i < numEdges; i++) {
527 Edge e = simplifyCNF(cnf, node->edges[i]);
528 uint enumvars = e.node_ptr->numVars;
529 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
530 newvec->numVars += enumvars;
532 return (Edge) {newvec};
534 Edge cond = node->edges[0];
535 Edge thenedge = node->edges[1];
536 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
537 Edge thenedges[] = {cond, constraintNegate(thenedge)};
538 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
539 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
540 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
541 Edge thencnf = simplifyCNF(cnf, thencons);
542 Edge elsecnf = simplifyCNF(cnf, elsecons);
543 //free temporary nodes
544 ourfree(getNodePtrFromEdge(thencons));
545 ourfree(getNodePtrFromEdge(elsecons));
546 Node *result = thencnf.node_ptr;
547 uint elsenumvars = elsecnf.node_ptr->numVars;
548 mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
549 result->numVars += elsenumvars;
550 return (Edge) {result};
553 if (type == NodeType_AND) {
555 uint numEdges = node->numEdges;
557 Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
558 for (uint i = 1; i < numEdges; i++) {
559 Edge e = node->edges[i];
560 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
561 newvec = disjoinAndFree(cnf, newvec, cnfform);
565 Edge cond = node->edges[0];
566 Edge thenedge = node->edges[1];
567 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
570 Edge thenedges[] = {cond, constraintNegate(thenedge)};
571 Edge thencons = createNode(NodeType_AND, 2, thenedges);
572 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
573 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
575 Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
576 Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
577 Edge result = simplifyCNF(cnf, combined);
578 //free temporary nodes
579 ourfree(getNodePtrFromEdge(thencons));
580 ourfree(getNodePtrFromEdge(elsecons));
581 ourfree(getNodePtrFromEdge(combined));
587 void addClause(CNF *cnf, uint numliterals, int *literals) {
589 addArrayClauseLiteral(cnf->solver, numliterals, literals);
592 void freezeVariable(CNF *cnf, Edge e){
593 int literal = getEdgeVar(e);
594 freeze(cnf->solver, literal);
597 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
598 Node *andNode = cnfform.node_ptr;
599 int orvar = getEdgeVar(eorvar);
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[2] = {getEdgeVar(e), orvar};
606 ASSERT(array[0] != 0);
607 addClause(cnf, 2, array);
609 Node *clause = e.node_ptr;
610 uint cnumEdges = clause->numEdges + 1;
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 - 1); j++) {
618 array[j] = getEdgeVar(clause->edges[j]);
619 ASSERT(array[j] != 0);
621 array[cnumEdges - 1] = orvar;
622 addClause(cnf, cnumEdges, array);
627 void outputCNF(CNF *cnf, Edge cnfform) {
628 Node *andNode = cnfform.node_ptr;
629 uint numEdges = andNode->numEdges;
630 for (uint i = 0; i < numEdges; i++) {
631 Edge e = andNode->edges[i];
632 if (edgeIsVarConst(e)) {
633 int array[1] = {getEdgeVar(e)};
634 ASSERT(array[0] != 0);
635 addClause(cnf, 1, array);
637 Node *clause = e.node_ptr;
638 uint cnumEdges = clause->numEdges;
639 if (cnumEdges > cnf->asize) {
640 cnf->asize = cnumEdges << 1;
642 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
644 int *array = cnf->array;
645 for (uint j = 0; j < cnumEdges; j++) {
646 array[j] = getEdgeVar(clause->edges[j]);
647 ASSERT(array[j] != 0);
649 addClause(cnf, cnumEdges, array);
654 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
655 ASSERT(p != P_UNDEFINED);
656 if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
657 // proxy => expression
658 Edge cnfexpr = simplifyCNF(cnf, expression);
660 freeEdgeRec(expression);
661 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
662 freeEdgeCNF(cnfexpr);
664 if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
665 // expression => proxy
666 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
667 freeEdgeRec(expression);
668 outputCNFOR(cnf, cnfnegexpr, proxy);
669 freeEdgeCNF(cnfnegexpr);
673 void addConstraintCNF(CNF *cnf, Edge constraint) {
674 if (equalsEdge(constraint, E_True)) {
676 } else if (equalsEdge(constraint, E_False)) {
681 freeEdgeRec(constraint);
686 model_print("****SATC_ADDING NEW Constraint*****\n");
687 printCNF(constraint);
688 model_print("\n******************************\n");
691 Edge cnfform = simplifyCNF(cnf, constraint);
692 freeEdgeRec(constraint);
693 outputCNF(cnf, cnfform);
694 freeEdgeCNF(cnfform);
697 Edge constraintNewVar(CNF *cnf) {
698 uint varnum = cnf->varcount++;
699 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
703 int solveCNF(CNF *cnf) {
704 long long startSolve = getTimeNano();
705 model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
706 int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
707 long long finishTime = getTimeNano();
708 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
709 cnf->solveTime = finishTime - startSolve;
710 model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
714 bool getValueCNF(CNF *cnf, Edge var) {
715 Literal l = getEdgeVar(var);
716 bool isneg = (l < 0);
718 return isneg ^ getValueSolver(cnf->solver, l);
721 void printCNF(Edge e) {
722 if (edgeIsVarConst(e)) {
723 Literal l = getEdgeVar(e);
724 model_print ("%d", l);
727 bool isNeg = isNegEdge(e);
728 if (edgeIsConst(e)) {
735 Node *n = getNodePtrFromEdge(e);
737 //Pretty print things that are equivalent to OR's
738 if (getNodeType(e) == NodeType_AND) {
740 for (uint i = 0; i < n->numEdges; i++) {
741 Edge e = n->edges[i];
744 printCNF(constraintNegate(e));
752 switch (getNodeType(e)) {
764 for (uint i = 0; i < n->numEdges; i++) {
765 Edge e = n->edges[i];
773 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
774 Edge carray[numvars];
775 for (uint j = 0; j < numvars; j++) {
776 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
780 return constraintAND(cnf, numvars, carray);
783 /** Generates a constraint to ensure that all encodings are less than value */
784 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
785 Edge orarray[numvars];
786 Edge andarray[numvars];
792 for (uint j = 0; j < numvars; j++) {
794 orarray[ori++] = constraintNegate(vars[j]);
797 //no ones to flip, so bail now...
799 return constraintAND(cnf, andi, andarray);
801 andarray[andi++] = constraintOR(cnf, ori, orarray);
803 value = value + (1 << (__builtin_ctz(value)));
808 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
812 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
816 for (uint i = 0; i < numvars; i++) {
817 array[i] = constraintIFF(cnf, var1[i], var2[i]);
819 return constraintAND(cnf, numvars, array);
822 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
825 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
826 for (uint i = 1; i < numvars; i++) {
827 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
828 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
829 result = constraintOR2(cnf, lt, eq);
834 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
837 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
838 for (uint i = 1; i < numvars; i++) {
839 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
840 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
841 result = constraintOR2(cnf, lt, eq);