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) {
149 uint hashvalue = type ^ numEdges;
150 for (uint i = 0; i < numEdges; i++) {
151 hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
152 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
154 return (uint) hashvalue;
157 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
158 if (node->flags.type != type || node->numEdges != numEdges)
160 Edge *nodeedges = node->edges;
161 for (uint i = 0; i < numEdges; i++) {
162 if (!equalsEdge(nodeedges[i], edges[i]))
168 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
169 Edge edgearray[numEdges];
171 for (uint i = 0; i < numEdges; i++) {
172 edgearray[i] = constraintNegate(edges[i]);
174 Edge eand = constraintAND(cnf, numEdges, edgearray);
175 return constraintNegate(eand);
178 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
179 Edge lneg = constraintNegate(left);
180 Edge rneg = constraintNegate(right);
181 Edge eand = constraintAND2(cnf, lneg, rneg);
182 return constraintNegate(eand);
185 int comparefunction(const Edge *e1, const Edge *e2) {
186 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
189 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
190 ASSERT(numEdges != 0);
191 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
193 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
196 uint remainSize = numEdges - initindex;
200 else if (remainSize == 1)
201 return edges[initindex];
202 else if (equalsEdge(edges[initindex], E_False))
205 /** De-duplicate array */
207 edges[lowindex] = edges[initindex++];
209 for (; initindex < numEdges; initindex++) {
210 Edge e1 = edges[lowindex];
211 Edge e2 = edges[initindex];
212 if (sameNodeVarEdge(e1, e2)) {
213 if (!sameSignEdge(e1, e2)) {
217 edges[++lowindex] = edges[initindex];
219 lowindex++; //Make lowindex look like size
224 if (cnf->enableMatching && lowindex == 2 &&
225 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
226 getNodeType(edges[0]) == NodeType_AND &&
227 getNodeType(edges[1]) == NodeType_AND &&
228 getNodeSize(edges[0]) == 2 &&
229 getNodeSize(edges[1]) == 2) {
230 Edge *e0edges = getEdgeArray(edges[0]);
231 Edge *e1edges = getEdgeArray(edges[1]);
232 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
233 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
234 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
235 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
236 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
237 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
238 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
239 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
243 return createNode(cnf, NodeType_AND, lowindex, edges);
246 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
247 Edge edges[2] = {left, right};
248 return constraintAND(cnf, 2, edges);
251 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
254 array[1] = constraintNegate(right);
255 Edge eand = constraintAND(cnf, 2, array);
256 return constraintNegate(eand);
259 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
260 bool negate = !sameSignEdge(left, right);
261 Edge lpos = getNonNeg(left);
262 Edge rpos = getNonNeg(right);
265 if (equalsEdge(lpos, rpos)) {
267 } else if (ltEdge(lpos, rpos)) {
268 Edge edges[] = {lpos, rpos};
269 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
271 Edge edges[] = {rpos, lpos};
272 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
275 e = constraintNegate(e);
279 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
280 if (isNegEdge(cond)) {
281 cond = constraintNegate(cond);
287 bool negate = isNegEdge(thenedge);
289 thenedge = constraintNegate(thenedge);
290 elseedge = constraintNegate(elseedge);
294 if (equalsEdge(cond, E_True)) {
296 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
297 Edge array[] = {cond, elseedge};
298 result = constraintOR(cnf, 2, array);
299 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
300 result = constraintIMPLIES(cnf, cond, thenedge);
301 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
302 Edge array[] = {cond, thenedge};
303 result = constraintAND(cnf, 2, array);
304 } else if (equalsEdge(thenedge, elseedge)) {
306 } else if (sameNodeOppSign(thenedge, elseedge)) {
307 if (ltEdge(cond, thenedge)) {
308 Edge array[] = {cond, thenedge};
309 result = createNode(cnf, NodeType_IFF, 2, array);
311 Edge array[] = {thenedge, cond};
312 result = createNode(cnf, NodeType_IFF, 2, array);
315 Edge edges[] = {cond, thenedge, elseedge};
316 result = createNode(cnf, NodeType_ITE, 3, edges);
319 result = constraintNegate(result);
323 void addConstraintCNF(CNF *cnf, Edge constraint) {
324 pushVectorEdge(&cnf->constraints, constraint);
326 model_print("****SATC_ADDING NEW Constraint*****\n");
327 printCNF(constraint);
328 model_print("\n******************************\n");
332 Edge constraintNewVar(CNF *cnf) {
333 uint varnum = cnf->varcount++;
334 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
338 int solveCNF(CNF *cnf) {
339 long long startTime = getTimeNano();
341 convertPass(cnf, false);
342 finishedClauses(cnf->solver);
343 long long startSolve = getTimeNano();
344 int result = solve(cnf->solver);
345 long long finishTime = getTimeNano();
346 cnf->encodeTime = startSolve - startTime;
347 cnf->solveTime = finishTime - startSolve;
351 bool getValueCNF(CNF *cnf, Edge var) {
352 Literal l = getEdgeVar(var);
353 bool isneg = (l < 0);
355 return isneg ^ getValueSolver(cnf->solver, l);
358 void countPass(CNF *cnf) {
359 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
360 VectorEdge *ve = allocDefVectorEdge();
361 for (uint i = 0; i < numConstraints; i++) {
362 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
364 deleteVectorEdge(ve);
367 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
368 //Skip constants and variables...
369 if (edgeIsVarConst(eroot))
372 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
374 bool isMatching = cnf->enableMatching;
376 while (getSizeVectorEdge(stack) != 0) {
377 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
378 bool polarity = isNegEdge(e);
379 Node *n = getNodePtrFromEdge(e);
380 if (getExpanded(n, polarity)) {
381 if (n->flags.type == NodeType_IFF ||
382 n->flags.type == NodeType_ITE) {
383 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
384 getNodePtrFromEdge(pExp)->intAnnot[0]++;
386 n->intAnnot[polarity]++;
389 setExpanded(n, polarity);
391 if (n->flags.type == NodeType_ITE ||
392 n->flags.type == NodeType_IFF) {
393 n->intAnnot[polarity] = 0;
394 Edge cond = n->edges[0];
395 Edge thenedge = n->edges[1];
396 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
397 thenedge = constraintNegateIf(thenedge, !polarity);
398 elseedge = constraintNegateIf(elseedge, !polarity);
399 thenedge = constraintAND2(cnf, cond, thenedge);
400 cond = constraintNegate(cond);
401 elseedge = constraintAND2(cnf, cond, elseedge);
402 thenedge = constraintNegate(thenedge);
403 elseedge = constraintNegate(elseedge);
404 cnf->enableMatching = false;
405 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
406 n->ptrAnnot[polarity] = succ1.node_ptr;
407 cnf->enableMatching = isMatching;
408 pushVectorEdge(stack, succ1);
409 if (getExpanded(n, !polarity)) {
410 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
411 Node *n1 = getNodePtrFromEdge(succ1);
412 Node *n2 = getNodePtrFromEdge(succ2);
413 n1->ptrAnnot[0] = succ2.node_ptr;
414 n2->ptrAnnot[0] = succ1.node_ptr;
415 n1->ptrAnnot[1] = succ2.node_ptr;
416 n2->ptrAnnot[1] = succ1.node_ptr;
419 n->intAnnot[polarity] = 1;
420 for (uint i = 0; i < n->numEdges; i++) {
421 Edge succ = n->edges[i];
422 if (!edgeIsVarConst(succ)) {
423 succ = constraintNegateIf(succ, polarity);
424 pushVectorEdge(stack, succ);
432 void convertPass(CNF *cnf, bool backtrackLit) {
433 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
434 VectorEdge *ve = allocDefVectorEdge();
435 for (uint i = 0; i < numConstraints; i++) {
436 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
438 deleteVectorEdge(ve);
441 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
442 Node *nroot = getNodePtrFromEdge(root);
444 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
445 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
446 root = (Edge) { nroot };
448 if (edgeIsConst(root)) {
449 if (isNegEdge(root)) {
451 Edge newvar = constraintNewVar(cnf);
452 Literal var = getEdgeVar(newvar);
453 Literal clause[] = {var};
454 addArrayClauseLiteral(cnf->solver, 1, clause);
456 addArrayClauseLiteral(cnf->solver, 1, clause);
462 } else if (edgeIsVarConst(root)) {
463 Literal clause[] = { getEdgeVar(root)};
464 addArrayClauseLiteral(cnf->solver, 1, clause);
468 clearVectorEdge(stack);pushVectorEdge(stack, root);
469 while (getSizeVectorEdge(stack) != 0) {
470 Edge e = lastVectorEdge(stack);
471 Node *n = getNodePtrFromEdge(e);
473 if (edgeIsVarConst(e)) {
474 popVectorEdge(stack);
476 } else if (n->flags.type == NodeType_ITE ||
477 n->flags.type == NodeType_IFF) {
478 popVectorEdge(stack);
479 if (n->ptrAnnot[0] != NULL)
480 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
481 if (n->ptrAnnot[1] != NULL)
482 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
486 bool needPos = (n->intAnnot[0] > 0);
487 bool needNeg = (n->intAnnot[1] > 0);
488 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
489 (!needNeg || n->flags.cnfVisitedUp & 2)) {
490 popVectorEdge(stack);
491 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
492 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
494 n->flags.cnfVisitedDown |= 1;
496 n->flags.cnfVisitedDown |= 2;
497 for (uint i = 0; i < n->numEdges; i++) {
498 Edge arg = n->edges[i];
499 arg = constraintNegateIf(arg, isNegEdge(e));
500 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
503 popVectorEdge(stack);
507 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
508 ASSERT(cnfExp != NULL);
509 if (isProxy(cnfExp)) {
510 Literal l = getProxy(cnfExp);
511 Literal clause[] = {l};
512 addArrayClauseLiteral(cnf->solver, 1, clause);
513 } else if (backtrackLit) {
514 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
515 Literal clause[] = {l};
516 addArrayClauseLiteral(cnf->solver, 1, clause);
518 outputCNF(cnf, cnfExp);
521 if (!((intptr_t) cnfExp & 1)) {
522 deleteCNFExpr(cnfExp);
523 nroot->ptrAnnot[isNegEdge(root)] = NULL;
528 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
530 Node *n = getNodePtrFromEdge(e);
532 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
533 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
534 if (isProxy(otherExp))
535 l = -getProxy(otherExp);
537 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
538 Node *nsemNeg = getNodePtrFromEdge(semNeg);
539 if (nsemNeg != NULL) {
540 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
541 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
542 if (isProxy(otherExp))
543 l = -getProxy(otherExp);
544 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
545 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
546 if (isProxy(otherExp))
547 l = getProxy(otherExp);
553 Edge newvar = constraintNewVar(cnf);
554 l = getEdgeVar(newvar);
556 // Output the constraints on the auxiliary variable
557 constrainCNF(cnf, l, exp);
560 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
565 void produceCNF(CNF *cnf, Edge e) {
566 CNFExpr *expPos = NULL;
567 CNFExpr *expNeg = NULL;
568 Node *n = getNodePtrFromEdge(e);
570 if (n->intAnnot[0] > 0) {
571 expPos = produceConjunction(cnf, e);
574 if (n->intAnnot[1] > 0) {
575 expNeg = produceDisjunction(cnf, e);
578 /// @todo Propagate constants across semantic negations (this can
579 /// be done similarly to the calls to propagate shown below). The
580 /// trick here is that we need to figure out how to get the
581 /// semantic negation pointers, and ensure that they can have CNF
582 /// produced for them at the right point
584 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
586 // propagate from positive to negative, negative to positive
587 if (!propagate(cnf, &expPos, expNeg, true))
588 propagate(cnf, &expNeg, expPos, true);
590 // The polarity heuristic entails visiting the discovery polarity first
592 saveCNF(cnf, expPos, e, false);
593 saveCNF(cnf, expNeg, e, true);
595 saveCNF(cnf, expNeg, e, true);
596 saveCNF(cnf, expPos, e, false);
600 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
601 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
603 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
604 } else if (isProxy(*dest)) {
605 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
607 Literal clause[] = {getProxy(*dest)};
608 addArrayClauseLiteral(cnf->solver, 1, clause);
610 Literal clause[] = {-getProxy(*dest)};
611 addArrayClauseLiteral(cnf->solver, 1, clause);
614 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
616 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
623 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
624 Node *n = getNodePtrFromEdge(e);
625 n->flags.cnfVisitedUp |= (1 << sign);
626 if (exp == NULL || isProxy(exp)) return;
628 if (exp->litSize == 1) {
629 Literal l = getLiteralLitVector(&exp->singletons, 0);
631 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
632 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
633 introProxy(cnf, e, exp, sign);
635 n->ptrAnnot[sign] = exp;
639 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
640 if (alwaysTrueCNF(expr)) {
642 } else if (alwaysFalseCNF(expr)) {
643 Literal clause[] = {-lcond};
644 addArrayClauseLiteral(cnf->solver, 1, clause);
648 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
649 Literal l = getLiteralLitVector(&expr->singletons,i);
650 Literal clause[] = {-lcond, l};
651 addArrayClauseLiteral(cnf->solver, 2, clause);
653 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
654 LitVector *lv = getVectorLitVector(&expr->clauses,i);
655 addClauseLiteral(cnf->solver, -lcond);//Add first literal
656 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
660 void outputCNF(CNF *cnf, CNFExpr *expr) {
661 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
662 Literal l = getLiteralLitVector(&expr->singletons,i);
663 Literal clause[] = {l};
664 addArrayClauseLiteral(cnf->solver, 1, clause);
666 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
667 LitVector *lv = getVectorLitVector(&expr->clauses,i);
668 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
672 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
673 clearVectorEdge(&cnf->args);
675 *largestEdge = (Edge) {(Node *) NULL};
676 CNFExpr *largest = NULL;
677 Node *n = getNodePtrFromEdge(e);
680 Edge arg = n->edges[--i];
681 arg = constraintNegateIf(arg, isNeg);
682 Node *narg = getNodePtrFromEdge(arg);
684 if (edgeIsVarConst(arg)) {
685 pushVectorEdge(&cnf->args, arg);
689 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
690 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
693 if (narg->intAnnot[isNegEdge(arg)] == 1) {
694 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
695 if (!isProxy(argExp)) {
696 if (largest == NULL) {
700 } else if (argExp->litSize > largest->litSize) {
701 pushVectorEdge(&cnf->args, *largestEdge);
708 pushVectorEdge(&cnf->args, arg);
711 if (largest != NULL) {
712 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
713 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
719 void printCNF(Edge e) {
720 if (edgeIsVarConst(e)) {
721 Literal l = getEdgeVar(e);
722 model_print ("%d", l);
725 bool isNeg = isNegEdge(e);
726 if (edgeIsConst(e)) {
733 Node *n = getNodePtrFromEdge(e);
735 //Pretty print things that are equivalent to OR's
736 if (getNodeType(e) == NodeType_AND) {
738 for (uint i = 0; i < n->numEdges; i++) {
739 Edge e = n->edges[i];
742 printCNF(constraintNegate(e));
750 switch (getNodeType(e)) {
762 for (uint i = 0; i < n->numEdges; i++) {
763 Edge e = n->edges[i];
771 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
774 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
776 accum = allocCNFExprBool(true);
778 int i = getSizeVectorEdge(&cnf->args);
780 Edge arg = getVectorEdge(&cnf->args, --i);
781 if (edgeIsVarConst(arg)) {
782 conjoinCNFLit(accum, getEdgeVar(arg));
784 Node *narg = getNodePtrFromEdge(arg);
785 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
787 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
788 if (isProxy(argExp)) {// variable has been introduced
789 conjoinCNFLit(accum, getProxy(argExp));
791 conjoinCNFExpr(accum, argExp, destroy);
793 narg->ptrAnnot[isNegEdge(arg)] = NULL;
803 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
805 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
807 accum = allocCNFExprBool(false);
809 // This is necessary to check to make sure that we don't start out
810 // with an accumulator that is "too large".
812 /// @todo Strictly speaking, introProxy doesn't *need* to free
813 /// memory, then this wouldn't have to reallocate CNFExpr
815 /// @todo When this call to introProxy is made, the semantic
816 /// negation pointer will have been destroyed. Thus, it will not
817 /// be possible to use the correct proxy. That should be fixed.
819 // at this point, we will either have NULL, or a destructible expression
820 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
821 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
823 int i = getSizeVectorEdge(&cnf->args);
825 Edge arg = getVectorEdge(&cnf->args, --i);
826 Node *narg = getNodePtrFromEdge(arg);
827 if (edgeIsVarConst(arg)) {
828 disjoinCNFLit(accum, getEdgeVar(arg));
830 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
832 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
833 if (isProxy(argExp)) {// variable has been introduced
834 disjoinCNFLit(accum, getProxy(argExp));
835 } else if (argExp->litSize == 0) {
836 disjoinCNFExpr(accum, argExp, destroy);
838 // check to see if we should introduce a proxy
839 int aL = accum->litSize; // lits in accum
840 int eL = argExp->litSize; // lits in argument
841 int aC = getClauseSizeCNF(accum); // clauses in accum
842 int eC = getClauseSizeCNF(argExp); // clauses in argument
843 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
844 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
845 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
847 disjoinCNFExpr(accum, argExp, destroy);
848 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
857 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
858 Edge carray[numvars];
859 for (uint j = 0; j < numvars; j++) {
860 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
864 return constraintAND(cnf, numvars, carray);
867 /** Generates a constraint to ensure that all encodings are less than value */
868 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
869 Edge orarray[numvars];
870 Edge andarray[numvars];
876 for (uint j = 0; j < numvars; j++) {
878 orarray[ori++] = constraintNegate(vars[j]);
881 //no ones to flip, so bail now...
883 return constraintAND(cnf, andi, andarray);
885 andarray[andi++] = constraintOR(cnf, ori, orarray);
887 value = value + (1 << (__builtin_ctz(value)));
892 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
896 for (uint i = 0; i < numvars; i++) {
897 array[i] = constraintIFF(cnf, var1[i], var2[i]);
899 return constraintAND(cnf, numvars, array);
902 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
905 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
906 for (uint i = 1; i < numvars; i++) {
907 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
908 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
909 result = constraintOR2(cnf, lt, eq);
914 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
917 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
918 for (uint i = 1; i < numvars; i++) {
919 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
920 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
921 result = constraintOR2(cnf, lt, eq);