1 #include "constraint.h"
4 #include "inc_solver.h"
9 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
10 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
12 Permission is hereby granted, free of charge, to any person obtaining
13 a copy of this software and associated documentation files (the
14 "Software"), to deal in the Software without restriction, including
15 without limitation the rights to use, copy, modify, merge, publish,
16 distribute, sublicense, and/or sell copies of the Software, and to
17 permit persons to whom the Software is furnished to do so, subject to
18 the following conditions:
20 The above copyright notice and this permission notice shall be
21 included in all copies or substantial portions of the Software. If
22 you download or use the software, send email to Pete Manolios
23 (pete@ccs.neu.edu) with your name, contact information, and a short
24 note describing what you want to use BAT for. For any reuse or
25 distribution, you must make clear to others the license terms of this
28 Contact Pete Manolios if you want any of these conditions waived.
30 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
40 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
44 VectorImpl(Edge, Edge, 16)
45 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
46 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
47 Edge E_BOGUS = {(Node *)0x12345673};
48 Edge E_NULL = {(Node *)NULL};
52 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
54 cnf->capacity = DEFAULT_CNF_ARRAY_SIZE;
55 cnf->mask = cnf->capacity - 1;
56 cnf->node_array = (Node **) ourcalloc(1, sizeof(Node *) * cnf->capacity);
58 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
59 cnf->enableMatching = true;
60 initDefVectorEdge(&cnf->constraints);
61 initDefVectorEdge(&cnf->args);
62 cnf->solver = allocIncrementalSolver();
68 void deleteCNF(CNF *cnf) {
69 for (uint i = 0; i < cnf->capacity; i++) {
70 Node *n = cnf->node_array[i];
74 deleteVectorArrayEdge(&cnf->constraints);
75 deleteVectorArrayEdge(&cnf->args);
76 deleteIncrementalSolver(cnf->solver);
77 ourfree(cnf->node_array);
81 void resizeCNF(CNF *cnf, uint newCapacity) {
82 Node **old_array = cnf->node_array;
83 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
84 uint oldCapacity = cnf->capacity;
85 uint newMask = newCapacity - 1;
86 for (uint i = 0; i < oldCapacity; i++) {
87 Node *n = old_array[i];
90 uint hashCode = n->hashCode;
91 uint newindex = hashCode & newMask;
92 for (;; newindex = (newindex + 1) & newMask) {
93 if (new_array[newindex] == NULL) {
94 new_array[newindex] = n;
100 cnf->node_array = new_array;
101 cnf->capacity = newCapacity;
102 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
106 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
107 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
108 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
109 n->flags.type = type;
110 n->flags.wasExpanded = 0;
111 n->flags.cnfVisitedDown = 0;
112 n->flags.cnfVisitedUp = 0;
113 n->flags.varForced = 0;
114 n->numEdges = numEdges;
115 n->hashCode = hashcode;
116 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
117 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
121 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
122 if (cnf->size > cnf->maxsize) {
123 resizeCNF(cnf, cnf->capacity << 1);
125 uint hashvalue = hashNode(type, numEdges, edges);
126 uint mask = cnf->mask;
127 uint index = hashvalue & mask;
129 for (;; index = (index + 1) & mask) {
130 n_ptr = &cnf->node_array[index];
131 if (*n_ptr != NULL) {
132 if ((*n_ptr)->hashCode == hashvalue) {
133 if (compareNodes(*n_ptr, type, numEdges, edges)) {
142 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
148 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
152 for (uint i = 0; i < numEdges; i++) {
153 uint c = (uint) ((uintptr_t) edges[i].node_ptr);
164 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
165 if (node->flags.type != type || node->numEdges != numEdges)
167 Edge *nodeedges = node->edges;
168 for (uint i = 0; i < numEdges; i++) {
169 if (!equalsEdge(nodeedges[i], edges[i]))
175 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
176 Edge edgearray[numEdges];
178 for (uint i = 0; i < numEdges; i++) {
179 edgearray[i] = constraintNegate(edges[i]);
181 Edge eand = constraintAND(cnf, numEdges, edgearray);
182 return constraintNegate(eand);
185 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
186 Edge lneg = constraintNegate(left);
187 Edge rneg = constraintNegate(right);
188 Edge eand = constraintAND2(cnf, lneg, rneg);
189 return constraintNegate(eand);
192 int comparefunction(const Edge *e1, const Edge *e2) {
193 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
196 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
197 ASSERT(numEdges != 0);
198 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
200 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
203 uint remainSize = numEdges - initindex;
207 else if (remainSize == 1)
208 return edges[initindex];
209 else if (equalsEdge(edges[initindex], E_False))
212 /** De-duplicate array */
214 edges[lowindex] = edges[initindex++];
216 for (; initindex < numEdges; initindex++) {
217 Edge e1 = edges[lowindex];
218 Edge e2 = edges[initindex];
219 if (sameNodeVarEdge(e1, e2)) {
220 if (!sameSignEdge(e1, e2)) {
224 edges[++lowindex] = edges[initindex];
226 lowindex++; //Make lowindex look like size
231 if (cnf->enableMatching && lowindex == 2 &&
232 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
233 getNodeType(edges[0]) == NodeType_AND &&
234 getNodeType(edges[1]) == NodeType_AND &&
235 getNodeSize(edges[0]) == 2 &&
236 getNodeSize(edges[1]) == 2) {
237 Edge *e0edges = getEdgeArray(edges[0]);
238 Edge *e1edges = getEdgeArray(edges[1]);
239 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
240 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
241 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
242 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
243 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
244 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
245 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
246 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
250 return createNode(cnf, NodeType_AND, lowindex, edges);
253 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
254 Edge edges[2] = {left, right};
255 return constraintAND(cnf, 2, edges);
258 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
261 array[1] = constraintNegate(right);
262 Edge eand = constraintAND(cnf, 2, array);
263 return constraintNegate(eand);
266 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
267 bool negate = !sameSignEdge(left, right);
268 Edge lpos = getNonNeg(left);
269 Edge rpos = getNonNeg(right);
272 if (equalsEdge(lpos, rpos)) {
274 } else if (ltEdge(lpos, rpos)) {
275 Edge edges[] = {lpos, rpos};
276 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
278 Edge edges[] = {rpos, lpos};
279 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
282 e = constraintNegate(e);
286 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
287 if (isNegEdge(cond)) {
288 cond = constraintNegate(cond);
294 bool negate = isNegEdge(thenedge);
296 thenedge = constraintNegate(thenedge);
297 elseedge = constraintNegate(elseedge);
301 if (equalsEdge(cond, E_True)) {
303 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
304 Edge array[] = {cond, elseedge};
305 result = constraintOR(cnf, 2, array);
306 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
307 result = constraintIMPLIES(cnf, cond, thenedge);
308 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
309 Edge array[] = {cond, thenedge};
310 result = constraintAND(cnf, 2, array);
311 } else if (equalsEdge(thenedge, elseedge)) {
313 } else if (sameNodeOppSign(thenedge, elseedge)) {
314 if (ltEdge(cond, thenedge)) {
315 Edge array[] = {cond, thenedge};
316 result = createNode(cnf, NodeType_IFF, 2, array);
318 Edge array[] = {thenedge, cond};
319 result = createNode(cnf, NodeType_IFF, 2, array);
322 Edge edges[] = {cond, thenedge, elseedge};
323 result = createNode(cnf, NodeType_ITE, 3, edges);
326 result = constraintNegate(result);
330 void addConstraintCNF(CNF *cnf, Edge constraint) {
331 pushVectorEdge(&cnf->constraints, constraint);
333 model_print("****SATC_ADDING NEW Constraint*****\n");
334 printCNF(constraint);
335 model_print("\n******************************\n");
339 Edge constraintNewVar(CNF *cnf) {
340 uint varnum = cnf->varcount++;
341 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
345 int solveCNF(CNF *cnf) {
346 long long startTime = getTimeNano();
348 convertPass(cnf, false);
349 finishedClauses(cnf->solver);
350 long long startSolve = getTimeNano();
351 int result = solve(cnf->solver);
352 long long finishTime = getTimeNano();
353 cnf->encodeTime = startSolve - startTime;
354 cnf->solveTime = finishTime - startSolve;
355 model_print("CNF Encode time: %f\n Solve time: %f\n", cnf->encodeTime/1000000000.0, cnf->solveTime/ 1000000000.0);
359 bool getValueCNF(CNF *cnf, Edge var) {
360 Literal l = getEdgeVar(var);
361 bool isneg = (l < 0);
363 return isneg ^ getValueSolver(cnf->solver, l);
366 void countPass(CNF *cnf) {
367 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
368 VectorEdge *ve = allocDefVectorEdge();
369 for (uint i = 0; i < numConstraints; i++) {
370 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
372 deleteVectorEdge(ve);
375 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
376 //Skip constants and variables...
377 if (edgeIsVarConst(eroot))
380 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
382 bool isMatching = cnf->enableMatching;
384 while (getSizeVectorEdge(stack) != 0) {
385 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
386 bool polarity = isNegEdge(e);
387 Node *n = getNodePtrFromEdge(e);
388 if (getExpanded(n, polarity)) {
389 if (n->flags.type == NodeType_IFF ||
390 n->flags.type == NodeType_ITE) {
391 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
392 getNodePtrFromEdge(pExp)->intAnnot[0]++;
394 n->intAnnot[polarity]++;
397 setExpanded(n, polarity);
399 if (n->flags.type == NodeType_ITE ||
400 n->flags.type == NodeType_IFF) {
401 n->intAnnot[polarity] = 0;
402 Edge cond = n->edges[0];
403 Edge thenedge = n->edges[1];
404 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
405 thenedge = constraintNegateIf(thenedge, !polarity);
406 elseedge = constraintNegateIf(elseedge, !polarity);
407 thenedge = constraintAND2(cnf, cond, thenedge);
408 cond = constraintNegate(cond);
409 elseedge = constraintAND2(cnf, cond, elseedge);
410 thenedge = constraintNegate(thenedge);
411 elseedge = constraintNegate(elseedge);
412 cnf->enableMatching = false;
413 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
414 n->ptrAnnot[polarity] = succ1.node_ptr;
415 cnf->enableMatching = isMatching;
416 pushVectorEdge(stack, succ1);
417 if (getExpanded(n, !polarity)) {
418 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
419 Node *n1 = getNodePtrFromEdge(succ1);
420 Node *n2 = getNodePtrFromEdge(succ2);
421 n1->ptrAnnot[0] = succ2.node_ptr;
422 n2->ptrAnnot[0] = succ1.node_ptr;
423 n1->ptrAnnot[1] = succ2.node_ptr;
424 n2->ptrAnnot[1] = succ1.node_ptr;
427 n->intAnnot[polarity] = 1;
428 for (uint i = 0; i < n->numEdges; i++) {
429 Edge succ = n->edges[i];
430 if (!edgeIsVarConst(succ)) {
431 succ = constraintNegateIf(succ, polarity);
432 pushVectorEdge(stack, succ);
440 void convertPass(CNF *cnf, bool backtrackLit) {
441 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
442 VectorEdge *ve = allocDefVectorEdge();
443 for (uint i = 0; i < numConstraints; i++) {
444 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
446 deleteVectorEdge(ve);
449 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
450 Node *nroot = getNodePtrFromEdge(root);
452 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
453 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
454 root = (Edge) { nroot };
456 if (edgeIsConst(root)) {
457 if (isNegEdge(root)) {
459 Edge newvar = constraintNewVar(cnf);
460 Literal var = getEdgeVar(newvar);
461 Literal clause[] = {var};
462 addArrayClauseLiteral(cnf->solver, 1, clause);
464 addArrayClauseLiteral(cnf->solver, 1, clause);
470 } else if (edgeIsVarConst(root)) {
471 Literal clause[] = { getEdgeVar(root)};
472 addArrayClauseLiteral(cnf->solver, 1, clause);
476 clearVectorEdge(stack);pushVectorEdge(stack, root);
477 while (getSizeVectorEdge(stack) != 0) {
478 Edge e = lastVectorEdge(stack);
479 Node *n = getNodePtrFromEdge(e);
481 if (edgeIsVarConst(e)) {
482 popVectorEdge(stack);
484 } else if (n->flags.type == NodeType_ITE ||
485 n->flags.type == NodeType_IFF) {
486 popVectorEdge(stack);
487 if (n->ptrAnnot[0] != NULL)
488 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
489 if (n->ptrAnnot[1] != NULL)
490 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
494 bool needPos = (n->intAnnot[0] > 0);
495 bool needNeg = (n->intAnnot[1] > 0);
496 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
497 (!needNeg || n->flags.cnfVisitedUp & 2)) {
498 popVectorEdge(stack);
499 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
500 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
502 n->flags.cnfVisitedDown |= 1;
504 n->flags.cnfVisitedDown |= 2;
505 for (uint i = 0; i < n->numEdges; i++) {
506 Edge arg = n->edges[i];
507 arg = constraintNegateIf(arg, isNegEdge(e));
508 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
511 popVectorEdge(stack);
515 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
516 ASSERT(cnfExp != NULL);
517 if (isProxy(cnfExp)) {
518 Literal l = getProxy(cnfExp);
519 Literal clause[] = {l};
520 addArrayClauseLiteral(cnf->solver, 1, clause);
521 } else if (backtrackLit) {
522 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
523 Literal clause[] = {l};
524 addArrayClauseLiteral(cnf->solver, 1, clause);
526 outputCNF(cnf, cnfExp);
529 if (!((intptr_t) cnfExp & 1)) {
530 deleteCNFExpr(cnfExp);
531 nroot->ptrAnnot[isNegEdge(root)] = NULL;
536 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
538 Node *n = getNodePtrFromEdge(e);
540 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
541 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
542 if (isProxy(otherExp))
543 l = -getProxy(otherExp);
545 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
546 Node *nsemNeg = getNodePtrFromEdge(semNeg);
547 if (nsemNeg != NULL) {
548 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
549 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
550 if (isProxy(otherExp))
551 l = -getProxy(otherExp);
552 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
553 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
554 if (isProxy(otherExp))
555 l = getProxy(otherExp);
561 Edge newvar = constraintNewVar(cnf);
562 l = getEdgeVar(newvar);
564 // Output the constraints on the auxiliary variable
565 constrainCNF(cnf, l, exp);
568 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
573 void produceCNF(CNF *cnf, Edge e) {
574 CNFExpr *expPos = NULL;
575 CNFExpr *expNeg = NULL;
576 Node *n = getNodePtrFromEdge(e);
578 if (n->intAnnot[0] > 0) {
579 expPos = produceConjunction(cnf, e);
582 if (n->intAnnot[1] > 0) {
583 expNeg = produceDisjunction(cnf, e);
586 /// @todo Propagate constants across semantic negations (this can
587 /// be done similarly to the calls to propagate shown below). The
588 /// trick here is that we need to figure out how to get the
589 /// semantic negation pointers, and ensure that they can have CNF
590 /// produced for them at the right point
592 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
594 // propagate from positive to negative, negative to positive
595 if (!propagate(cnf, &expPos, expNeg, true))
596 propagate(cnf, &expNeg, expPos, true);
598 // The polarity heuristic entails visiting the discovery polarity first
600 saveCNF(cnf, expPos, e, false);
601 saveCNF(cnf, expNeg, e, true);
603 saveCNF(cnf, expNeg, e, true);
604 saveCNF(cnf, expPos, e, false);
608 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
609 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
611 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
612 } else if (isProxy(*dest)) {
613 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
615 Literal clause[] = {getProxy(*dest)};
616 addArrayClauseLiteral(cnf->solver, 1, clause);
618 Literal clause[] = {-getProxy(*dest)};
619 addArrayClauseLiteral(cnf->solver, 1, clause);
622 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
624 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
631 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
632 Node *n = getNodePtrFromEdge(e);
633 n->flags.cnfVisitedUp |= (1 << sign);
634 if (exp == NULL || isProxy(exp)) return;
636 if (exp->litSize == 1) {
637 Literal l = getLiteralLitVector(&exp->singletons, 0);
639 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
640 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
641 introProxy(cnf, e, exp, sign);
643 n->ptrAnnot[sign] = exp;
647 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
648 if (alwaysTrueCNF(expr)) {
650 } else if (alwaysFalseCNF(expr)) {
651 Literal clause[] = {-lcond};
652 addArrayClauseLiteral(cnf->solver, 1, clause);
656 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
657 Literal l = getLiteralLitVector(&expr->singletons,i);
658 Literal clause[] = {-lcond, l};
659 addArrayClauseLiteral(cnf->solver, 2, clause);
661 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
662 LitVector *lv = getVectorLitVector(&expr->clauses,i);
663 addClauseLiteral(cnf->solver, -lcond);//Add first literal
664 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
668 void outputCNF(CNF *cnf, CNFExpr *expr) {
669 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
670 Literal l = getLiteralLitVector(&expr->singletons,i);
671 Literal clause[] = {l};
672 addArrayClauseLiteral(cnf->solver, 1, clause);
674 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
675 LitVector *lv = getVectorLitVector(&expr->clauses,i);
676 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
680 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
681 clearVectorEdge(&cnf->args);
683 *largestEdge = (Edge) {(Node *) NULL};
684 CNFExpr *largest = NULL;
685 Node *n = getNodePtrFromEdge(e);
688 Edge arg = n->edges[--i];
689 arg = constraintNegateIf(arg, isNeg);
690 Node *narg = getNodePtrFromEdge(arg);
692 if (edgeIsVarConst(arg)) {
693 pushVectorEdge(&cnf->args, arg);
697 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
698 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
701 if (narg->intAnnot[isNegEdge(arg)] == 1) {
702 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
703 if (!isProxy(argExp)) {
704 if (largest == NULL) {
708 } else if (argExp->litSize > largest->litSize) {
709 pushVectorEdge(&cnf->args, *largestEdge);
716 pushVectorEdge(&cnf->args, arg);
719 if (largest != NULL) {
720 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
721 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
727 void printCNF(Edge e) {
728 if (edgeIsVarConst(e)) {
729 Literal l = getEdgeVar(e);
730 model_print ("%d", l);
733 bool isNeg = isNegEdge(e);
734 if (edgeIsConst(e)) {
741 Node *n = getNodePtrFromEdge(e);
743 //Pretty print things that are equivalent to OR's
744 if (getNodeType(e) == NodeType_AND) {
746 for (uint i = 0; i < n->numEdges; i++) {
747 Edge e = n->edges[i];
750 printCNF(constraintNegate(e));
758 switch (getNodeType(e)) {
770 for (uint i = 0; i < n->numEdges; i++) {
771 Edge e = n->edges[i];
779 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
782 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
784 accum = allocCNFExprBool(true);
786 int i = getSizeVectorEdge(&cnf->args);
788 Edge arg = getVectorEdge(&cnf->args, --i);
789 if (edgeIsVarConst(arg)) {
790 conjoinCNFLit(accum, getEdgeVar(arg));
792 Node *narg = getNodePtrFromEdge(arg);
793 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
795 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
796 if (isProxy(argExp)) {// variable has been introduced
797 conjoinCNFLit(accum, getProxy(argExp));
799 conjoinCNFExpr(accum, argExp, destroy);
801 narg->ptrAnnot[isNegEdge(arg)] = NULL;
811 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
813 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
815 accum = allocCNFExprBool(false);
817 // This is necessary to check to make sure that we don't start out
818 // with an accumulator that is "too large".
820 /// @todo Strictly speaking, introProxy doesn't *need* to free
821 /// memory, then this wouldn't have to reallocate CNFExpr
823 /// @todo When this call to introProxy is made, the semantic
824 /// negation pointer will have been destroyed. Thus, it will not
825 /// be possible to use the correct proxy. That should be fixed.
827 // at this point, we will either have NULL, or a destructible expression
828 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
829 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
831 int i = getSizeVectorEdge(&cnf->args);
833 Edge arg = getVectorEdge(&cnf->args, --i);
834 Node *narg = getNodePtrFromEdge(arg);
835 if (edgeIsVarConst(arg)) {
836 disjoinCNFLit(accum, getEdgeVar(arg));
838 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
840 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
841 if (isProxy(argExp)) {// variable has been introduced
842 disjoinCNFLit(accum, getProxy(argExp));
843 } else if (argExp->litSize == 0) {
844 disjoinCNFExpr(accum, argExp, destroy);
846 // check to see if we should introduce a proxy
847 int aL = accum->litSize; // lits in accum
848 int eL = argExp->litSize; // lits in argument
849 int aC = getClauseSizeCNF(accum); // clauses in accum
850 int eC = getClauseSizeCNF(argExp); // clauses in argument
851 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
852 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
853 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
855 disjoinCNFExpr(accum, argExp, destroy);
856 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
865 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
866 Edge carray[numvars];
867 for (uint j = 0; j < numvars; j++) {
868 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
872 return constraintAND(cnf, numvars, carray);
875 /** Generates a constraint to ensure that all encodings are less than value */
876 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
877 Edge orarray[numvars];
878 Edge andarray[numvars];
884 for (uint j = 0; j < numvars; j++) {
886 orarray[ori++] = constraintNegate(vars[j]);
889 //no ones to flip, so bail now...
891 return constraintAND(cnf, andi, andarray);
893 andarray[andi++] = constraintOR(cnf, ori, orarray);
895 value = value + (1 << (__builtin_ctz(value)));
900 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
904 for (uint i = 0; i < numvars; i++) {
905 array[i] = constraintIFF(cnf, var1[i], var2[i]);
907 return constraintAND(cnf, numvars, array);
910 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
913 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
914 for (uint i = 1; i < numvars; i++) {
915 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
916 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
917 result = constraintOR2(cnf, lt, eq);
922 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
925 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
926 for (uint i = 1; i < numvars; i++) {
927 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
928 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
929 result = constraintOR2(cnf, lt, eq);