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 Edge edgearray[numEdges];
197 for (uint i = 0; i < numEdges; i++) {
198 edgearray[i] = constraintNegate(edges[i]);
200 Edge eand = constraintAND(cnf, numEdges, edgearray);
201 return constraintNegate(eand);
204 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
205 Edge lneg = constraintNegate(left);
206 Edge rneg = constraintNegate(right);
207 Edge eand = constraintAND2(cnf, lneg, rneg);
208 return constraintNegate(eand);
211 int comparefunction(const Edge *e1, const Edge *e2) {
212 if (e1->node_ptr == e2->node_ptr)
214 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
220 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
221 ASSERT(numEdges != 0);
223 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
225 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
228 uint remainSize = numEdges - initindex;
232 else if (remainSize == 1)
233 return edges[initindex];
234 else if (equalsEdge(edges[initindex], E_False)) {
235 freeEdgesRec(numEdges, edges);
239 /** De-duplicate array */
241 edges[lowindex] = edges[initindex++];
243 for (; initindex < numEdges; initindex++) {
244 Edge e1 = edges[lowindex];
245 Edge e2 = edges[initindex];
246 if (sameNodeVarEdge(e1, e2)) {
247 ASSERT(!isNodeEdge(e1));
248 if (!sameSignEdge(e1, e2)) {
249 freeEdgesRec(lowindex + 1, edges);
250 freeEdgesRec(numEdges - initindex, &edges[initindex]);
254 edges[++lowindex] = edges[initindex];
256 lowindex++; //Make lowindex look like size
262 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
263 getNodeType(edges[0]) == NodeType_AND &&
264 getNodeType(edges[1]) == NodeType_AND &&
265 getNodeSize(edges[0]) == 2 &&
266 getNodeSize(edges[1]) == 2) {
267 Edge *e0edges = getEdgeArray(edges[0]);
268 Edge *e1edges = getEdgeArray(edges[1]);
269 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
270 Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
274 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
275 Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
279 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
280 Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
284 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
285 Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
292 return createNode(NodeType_AND, lowindex, edges);
295 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
296 Edge edges[2] = {left, right};
297 return constraintAND(cnf, 2, edges);
300 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
303 array[1] = constraintNegate(right);
304 Edge eand = constraintAND(cnf, 2, array);
305 return constraintNegate(eand);
308 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
309 bool negate = !sameSignEdge(left, right);
310 Edge lpos = getNonNeg(left);
311 Edge rpos = getNonNeg(right);
314 if (equalsEdge(lpos, rpos)) {
318 } else if (ltEdge(lpos, rpos)) {
319 Edge edges[] = {lpos, rpos};
320 e = (edgeIsConst(lpos)) ? rpos : createNode(NodeType_IFF, 2, edges);
322 Edge edges[] = {rpos, lpos};
323 e = (edgeIsConst(rpos)) ? lpos : createNode(NodeType_IFF, 2, edges);
326 e = constraintNegate(e);
330 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
331 if (isNegEdge(cond)) {
332 cond = constraintNegate(cond);
338 bool negate = isNegEdge(thenedge);
340 thenedge = constraintNegate(thenedge);
341 elseedge = constraintNegate(elseedge);
345 if (equalsEdge(cond, E_True)) {
346 freeEdgeRec(elseedge);
348 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
349 Edge array[] = {cond, elseedge};
350 result = constraintOR(cnf, 2, array);
351 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
352 result = constraintIMPLIES(cnf, cond, thenedge);
353 } else if (equalsEdge(elseedge, E_False) || equalsEdge(cond, elseedge)) {
354 Edge array[] = {cond, thenedge};
355 result = constraintAND(cnf, 2, array);
356 } else if (equalsEdge(thenedge, elseedge)) {
359 } else if (sameNodeOppSign(thenedge, elseedge)) {
360 if (ltEdge(cond, thenedge)) {
361 Edge array[] = {cond, thenedge};
362 result = createNode(NodeType_IFF, 2, array);
364 Edge array[] = {thenedge, cond};
365 result = createNode(NodeType_IFF, 2, array);
368 Edge edges[] = {cond, thenedge, elseedge};
369 result = createNode(NodeType_ITE, 3, edges);
372 result = constraintNegate(result);
376 Edge disjoinLit(Edge vec, Edge lit) {
377 Node *nvec = vec.node_ptr;
378 uint nvecedges = nvec->numEdges;
380 for (uint i = 0; i < nvecedges; i++) {
381 Edge ce = nvec->edges[i];
382 if (!edgeIsVarConst(ce)) {
383 Node *cne = ce.node_ptr;
384 addEdgeToResizeNode(&cne, lit);
385 nvec->edges[i] = (Edge) {cne};
387 Node *clause = allocResizeNode(2);
388 addEdgeToResizeNode(&clause, lit);
389 addEdgeToResizeNode(&clause, ce);
390 nvec->edges[i] = (Edge) {clause};
393 nvec->numVars += nvecedges;
397 Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
398 Node *nnewvec = newvec.node_ptr;
399 Node *ncnfform = cnfform.node_ptr;
400 uint newvecedges = nnewvec->numEdges;
401 uint cnfedges = ncnfform->numEdges;
402 uint newvecvars = nnewvec->numVars;
403 uint cnfvars = ncnfform->numVars;
406 ((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
407 Edge proxyVar = constraintNewVar(cnf);
408 if (newvecedges > cnfedges) {
409 outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
411 return disjoinLit(cnfform, proxyVar);
413 outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
414 freeEdgeCNF(cnfform);
415 return disjoinLit(newvec, proxyVar);
421 if (newvecedges == 1 || cnfedges == 1) {
426 newvecedges = cnfedges;
429 Edge e = ncnfform->edges[0];
430 if (!edgeIsVarConst(e)) {
431 Node *n = e.node_ptr;
432 for (uint i = 0; i < newvecedges; i++) {
433 Edge ce = nnewvec->edges[i];
434 if (isNodeEdge(ce)) {
435 Node *cne = ce.node_ptr;
436 mergeNodeToResizeNode(&cne, n);
437 nnewvec->edges[i] = (Edge) {cne};
439 Node *clause = allocResizeNode(n->numEdges + 1);
440 mergeNodeToResizeNode(&clause, n);
441 addEdgeToResizeNode(&clause, ce);
442 nnewvec->edges[i] = (Edge) {clause};
445 nnewvec->numVars += newvecedges * n->numVars;
447 for (uint i = 0; i < newvecedges; i++) {
448 Edge ce = nnewvec->edges[i];
449 if (!edgeIsVarConst(ce)) {
450 Node *cne = ce.node_ptr;
451 addEdgeToResizeNode(&cne, e);
452 nnewvec->edges[i] = (Edge) {cne};
454 Node *clause = allocResizeNode(2);
455 addEdgeToResizeNode(&clause, e);
456 addEdgeToResizeNode(&clause, ce);
457 nnewvec->edges[i] = (Edge) {clause};
460 nnewvec->numVars += newvecedges;
462 freeEdgeCNF((Edge) {ncnfform});
463 return (Edge) {nnewvec};
466 Node *result = allocResizeNode(1);
468 for (uint i = 0; i < newvecedges; i++) {
469 Edge nedge = nnewvec->edges[i];
470 uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
471 for (uint j = 0; j < cnfedges; j++) {
472 Edge cedge = ncnfform->edges[j];
473 uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
474 if (equalsEdge(cedge, nedge)) {
475 addEdgeToResizeNode(&result, cedge);
476 result->numVars += cSize;
477 } else if (!sameNodeOppSign(nedge, cedge)) {
478 Node *clause = allocResizeNode(cSize + nSize);
479 if (isNodeEdge(nedge)) {
480 mergeNodeToResizeNode(&clause, nedge.node_ptr);
482 addEdgeToResizeNode(&clause, nedge);
484 if (isNodeEdge(cedge)) {
485 mergeNodeToResizeNode(&clause, cedge.node_ptr);
487 addEdgeToResizeNode(&clause, cedge);
489 addEdgeToResizeNode(&result, (Edge) {clause});
490 result->numVars += clause->numEdges;
496 freeEdgeCNF(cnfform);
497 return (Edge) {result};
500 Edge simplifyCNF(CNF *cnf, Edge input) {
501 if (edgeIsVarConst(input)) {
502 Node *newvec = allocResizeNode(1);
503 addEdgeToResizeNode(&newvec, input);
505 return (Edge) {newvec};
507 bool negated = isNegEdge(input);
508 Node *node = getNodePtrFromEdge(input);
509 NodeType type = node->type;
511 if (type == NodeType_AND) {
513 Node *newvec = allocResizeNode(node->numEdges);
514 uint numEdges = node->numEdges;
515 for (uint i = 0; i < numEdges; i++) {
516 Edge e = simplifyCNF(cnf, node->edges[i]);
517 uint enumvars = e.node_ptr->numVars;
518 mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
519 newvec->numVars += enumvars;
521 return (Edge) {newvec};
523 Edge cond = node->edges[0];
524 Edge thenedge = node->edges[1];
525 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
526 Edge thenedges[] = {cond, constraintNegate(thenedge)};
527 Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
528 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
529 Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
530 Edge thencnf = simplifyCNF(cnf, thencons);
531 Edge elsecnf = simplifyCNF(cnf, elsecons);
532 //free temporary nodes
533 ourfree(getNodePtrFromEdge(thencons));
534 ourfree(getNodePtrFromEdge(elsecons));
535 Node *result = thencnf.node_ptr;
536 uint elsenumvars = elsecnf.node_ptr->numVars;
537 mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
538 result->numVars += elsenumvars;
539 return (Edge) {result};
542 if (type == NodeType_AND) {
544 uint numEdges = node->numEdges;
546 Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
547 for (uint i = 1; i < numEdges; i++) {
548 Edge e = node->edges[i];
549 Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
550 newvec = disjoinAndFree(cnf, newvec, cnfform);
554 Edge cond = node->edges[0];
555 Edge thenedge = node->edges[1];
556 Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
559 Edge thenedges[] = {cond, constraintNegate(thenedge)};
560 Edge thencons = createNode(NodeType_AND, 2, thenedges);
561 Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
562 Edge elsecons = createNode(NodeType_AND, 2, elseedges);
564 Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
565 Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
566 Edge result = simplifyCNF(cnf, combined);
567 //free temporary nodes
568 ourfree(getNodePtrFromEdge(thencons));
569 ourfree(getNodePtrFromEdge(elsecons));
570 ourfree(getNodePtrFromEdge(combined));
576 void addClause(CNF *cnf, uint numliterals, int *literals) {
578 addArrayClauseLiteral(cnf->solver, numliterals, literals);
581 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
582 Node *andNode = cnfform.node_ptr;
583 int orvar = getEdgeVar(eorvar);
585 uint numEdges = andNode->numEdges;
586 for (uint i = 0; i < numEdges; i++) {
587 Edge e = andNode->edges[i];
588 if (edgeIsVarConst(e)) {
589 int array[2] = {getEdgeVar(e), orvar};
590 ASSERT(array[0] != 0);
591 addClause(cnf, 2, array);
593 Node *clause = e.node_ptr;
594 uint cnumEdges = clause->numEdges + 1;
595 if (cnumEdges > cnf->asize) {
596 cnf->asize = cnumEdges << 1;
598 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
600 int *array = cnf->array;
601 for (uint j = 0; j < (cnumEdges - 1); j++) {
602 array[j] = getEdgeVar(clause->edges[j]);
603 ASSERT(array[j] != 0);
605 array[cnumEdges - 1] = orvar;
606 addClause(cnf, cnumEdges, array);
611 void outputCNF(CNF *cnf, Edge cnfform) {
612 Node *andNode = cnfform.node_ptr;
613 uint numEdges = andNode->numEdges;
614 for (uint i = 0; i < numEdges; i++) {
615 Edge e = andNode->edges[i];
616 if (edgeIsVarConst(e)) {
617 int array[1] = {getEdgeVar(e)};
618 ASSERT(array[0] != 0);
619 addClause(cnf, 1, array);
621 Node *clause = e.node_ptr;
622 uint cnumEdges = clause->numEdges;
623 if (cnumEdges > cnf->asize) {
624 cnf->asize = cnumEdges << 1;
626 cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
628 int *array = cnf->array;
629 for (uint j = 0; j < cnumEdges; j++) {
630 array[j] = getEdgeVar(clause->edges[j]);
631 ASSERT(array[j] != 0);
633 addClause(cnf, cnumEdges, array);
638 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p) {
639 ASSERT(p != P_UNDEFINED);
640 if (p == P_TRUE || p == P_BOTHTRUEFALSE) {
641 // proxy => expression
642 Edge cnfexpr = simplifyCNF(cnf, expression);
644 freeEdgeRec(expression);
645 outputCNFOR(cnf, cnfexpr, constraintNegate(proxy));
646 freeEdgeCNF(cnfexpr);
648 if (p == P_FALSE || p == P_BOTHTRUEFALSE) {
649 // expression => proxy
650 Edge cnfnegexpr = simplifyCNF(cnf, constraintNegate(expression));
651 freeEdgeRec(expression);
652 outputCNFOR(cnf, cnfnegexpr, proxy);
653 freeEdgeCNF(cnfnegexpr);
657 void addConstraintCNF(CNF *cnf, Edge constraint) {
658 if (equalsEdge(constraint, E_True)) {
660 } else if (equalsEdge(constraint, E_False)) {
665 freeEdgeRec(constraint);
670 model_print("****SATC_ADDING NEW Constraint*****\n");
671 printCNF(constraint);
672 model_print("\n******************************\n");
675 Edge cnfform = simplifyCNF(cnf, constraint);
676 freeEdgeRec(constraint);
677 outputCNF(cnf, cnfform);
678 freeEdgeCNF(cnfform);
681 Edge constraintNewVar(CNF *cnf) {
682 uint varnum = cnf->varcount++;
683 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
687 int solveCNF(CNF *cnf) {
688 long long startTime = getTimeNano();
689 finishedClauses(cnf->solver);
690 long long startSolve = getTimeNano();
691 model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
692 int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
693 long long finishTime = getTimeNano();
694 cnf->encodeTime = startSolve - startTime;
695 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
696 cnf->solveTime = finishTime - startSolve;
697 model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
701 bool getValueCNF(CNF *cnf, Edge var) {
702 Literal l = getEdgeVar(var);
703 bool isneg = (l < 0);
705 return isneg ^ getValueSolver(cnf->solver, l);
708 void printCNF(Edge e) {
709 if (edgeIsVarConst(e)) {
710 Literal l = getEdgeVar(e);
711 model_print ("%d", l);
714 bool isNeg = isNegEdge(e);
715 if (edgeIsConst(e)) {
722 Node *n = getNodePtrFromEdge(e);
724 //Pretty print things that are equivalent to OR's
725 if (getNodeType(e) == NodeType_AND) {
727 for (uint i = 0; i < n->numEdges; i++) {
728 Edge e = n->edges[i];
731 printCNF(constraintNegate(e));
739 switch (getNodeType(e)) {
751 for (uint i = 0; i < n->numEdges; i++) {
752 Edge e = n->edges[i];
760 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
761 Edge carray[numvars];
762 for (uint j = 0; j < numvars; j++) {
763 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
767 return constraintAND(cnf, numvars, carray);
770 /** Generates a constraint to ensure that all encodings are less than value */
771 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
772 Edge orarray[numvars];
773 Edge andarray[numvars];
779 for (uint j = 0; j < numvars; j++) {
781 orarray[ori++] = constraintNegate(vars[j]);
784 //no ones to flip, so bail now...
786 return constraintAND(cnf, andi, andarray);
788 andarray[andi++] = constraintOR(cnf, ori, orarray);
790 value = value + (1 << (__builtin_ctz(value)));
795 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
799 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
803 for (uint i = 0; i < numvars; i++) {
804 array[i] = constraintIFF(cnf, var1[i], var2[i]);
806 return constraintAND(cnf, numvars, array);
809 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
812 Edge result = constraintAND2(cnf, constraintNegate( 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);
821 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
824 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
825 for (uint i = 1; i < numvars; i++) {
826 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
827 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
828 result = constraintOR2(cnf, lt, eq);