1 #include "constraint.h"
4 #include "inc_solver.h"
8 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
9 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
11 Permission is hereby granted, free of charge, to any person obtaining
12 a copy of this software and associated documentation files (the
13 "Software"), to deal in the Software without restriction, including
14 without limitation the rights to use, copy, modify, merge, publish,
15 distribute, sublicense, and/or sell copies of the Software, and to
16 permit persons to whom the Software is furnished to do so, subject to
17 the following conditions:
19 The above copyright notice and this permission notice shall be
20 included in all copies or substantial portions of the Software. If
21 you download or use the software, send email to Pete Manolios
22 (pete@ccs.neu.edu) with your name, contact information, and a short
23 note describing what you want to use BAT for. For any reuse or
24 distribution, you must make clear to others the license terms of this
27 Contact Pete Manolios if you want any of these conditions waived.
29 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
30 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
31 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
32 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
33 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
34 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
35 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
43 VectorImpl(Edge, Edge, 16)
44 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
45 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
46 Edge E_BOGUS = {(Node *)0x12345673};
47 Edge E_NULL = {(Node *)NULL};
51 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
53 cnf->capacity = DEFAULT_CNF_ARRAY_SIZE;
54 cnf->mask = cnf->capacity - 1;
55 cnf->node_array = (Node **) ourcalloc(1, sizeof(Node *) * cnf->capacity);
57 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
58 cnf->enableMatching = true;
59 initDefVectorEdge(&cnf->constraints);
60 initDefVectorEdge(&cnf->args);
61 cnf->solver = allocIncrementalSolver();
65 void deleteCNF(CNF *cnf) {
66 for (uint i = 0; i < cnf->capacity; i++) {
67 Node *n = cnf->node_array[i];
71 deleteVectorArrayEdge(&cnf->constraints);
72 deleteVectorArrayEdge(&cnf->args);
73 deleteIncrementalSolver(cnf->solver);
74 ourfree(cnf->node_array);
78 void resizeCNF(CNF *cnf, uint newCapacity) {
79 Node **old_array = cnf->node_array;
80 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
81 uint oldCapacity = cnf->capacity;
82 uint newMask = newCapacity - 1;
83 for (uint i = 0; i < oldCapacity; i++) {
84 Node *n = old_array[i];
87 uint hashCode = n->hashCode;
88 uint newindex = hashCode & newMask;
89 for (;; newindex = (newindex + 1) & newMask) {
90 if (new_array[newindex] == NULL) {
91 new_array[newindex] = n;
97 cnf->node_array = new_array;
98 cnf->capacity = newCapacity;
99 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
103 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
104 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
105 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
106 n->flags.type = type;
107 n->flags.wasExpanded = 0;
108 n->flags.cnfVisitedDown = 0;
109 n->flags.cnfVisitedUp = 0;
110 n->flags.varForced = 0;
111 n->numEdges = numEdges;
112 n->hashCode = hashcode;
113 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
114 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
118 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
119 if (cnf->size > cnf->maxsize) {
120 resizeCNF(cnf, cnf->capacity << 1);
122 uint hashvalue = hashNode(type, numEdges, edges);
123 uint mask = cnf->mask;
124 uint index = hashvalue & mask;
126 for (;; index = (index + 1) & mask) {
127 n_ptr = &cnf->node_array[index];
128 if (*n_ptr != NULL) {
129 if ((*n_ptr)->hashCode == hashvalue) {
130 if (compareNodes(*n_ptr, type, numEdges, edges)) {
139 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
145 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
146 uint hashvalue = type ^ numEdges;
147 for (uint i = 0; i < numEdges; i++) {
148 hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
149 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
151 return (uint) hashvalue;
154 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
155 if (node->flags.type != type || node->numEdges != numEdges)
157 Edge *nodeedges = node->edges;
158 for (uint i = 0; i < numEdges; i++) {
159 if (!equalsEdge(nodeedges[i], edges[i]))
165 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
166 Edge edgearray[numEdges];
168 for (uint i = 0; i < numEdges; i++) {
169 edgearray[i] = constraintNegate(edges[i]);
171 Edge eand = constraintAND(cnf, numEdges, edgearray);
172 return constraintNegate(eand);
175 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
176 Edge lneg = constraintNegate(left);
177 Edge rneg = constraintNegate(right);
178 Edge eand = constraintAND2(cnf, lneg, rneg);
179 return constraintNegate(eand);
182 int comparefunction(const Edge *e1, const Edge *e2) {
183 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
186 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
187 ASSERT(numEdges != 0);
188 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
190 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
193 uint remainSize = numEdges - initindex;
197 else if (remainSize == 1)
198 return edges[initindex];
199 else if (equalsEdge(edges[initindex], E_False))
202 /** De-duplicate array */
204 edges[lowindex] = edges[initindex++];
206 for (; initindex < numEdges; initindex++) {
207 Edge e1 = edges[lowindex];
208 Edge e2 = edges[initindex];
209 if (sameNodeVarEdge(e1, e2)) {
210 if (!sameSignEdge(e1, e2)) {
214 edges[++lowindex] = edges[initindex];
216 lowindex++; //Make lowindex look like size
221 if (cnf->enableMatching && lowindex == 2 &&
222 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
223 getNodeType(edges[0]) == NodeType_AND &&
224 getNodeType(edges[1]) == NodeType_AND &&
225 getNodeSize(edges[0]) == 2 &&
226 getNodeSize(edges[1]) == 2) {
227 Edge *e0edges = getEdgeArray(edges[0]);
228 Edge *e1edges = getEdgeArray(edges[1]);
229 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
230 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
231 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
232 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
233 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
234 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
235 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
236 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
240 return createNode(cnf, NodeType_AND, lowindex, edges);
243 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
244 Edge edges[2] = {left, right};
245 return constraintAND(cnf, 2, edges);
248 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
251 array[1] = constraintNegate(right);
252 Edge eand = constraintAND(cnf, 2, array);
253 return constraintNegate(eand);
256 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
257 bool negate = !sameSignEdge(left, right);
258 Edge lpos = getNonNeg(left);
259 Edge rpos = getNonNeg(right);
262 if (equalsEdge(lpos, rpos)) {
264 } else if (ltEdge(lpos, rpos)) {
265 Edge edges[] = {lpos, rpos};
266 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
268 Edge edges[] = {rpos, lpos};
269 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
272 e = constraintNegate(e);
276 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
277 if (isNegEdge(cond)) {
278 cond = constraintNegate(cond);
284 bool negate = isNegEdge(thenedge);
286 thenedge = constraintNegate(thenedge);
287 elseedge = constraintNegate(elseedge);
291 if (equalsEdge(cond, E_True)) {
293 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
294 Edge array[] = {cond, elseedge};
295 result = constraintOR(cnf, 2, array);
296 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
297 result = constraintIMPLIES(cnf, cond, thenedge);
298 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
299 Edge array[] = {cond, thenedge};
300 result = constraintAND(cnf, 2, array);
301 } else if (equalsEdge(thenedge, elseedge)) {
303 } else if (sameNodeOppSign(thenedge, elseedge)) {
304 if (ltEdge(cond, thenedge)) {
305 Edge array[] = {cond, thenedge};
306 result = createNode(cnf, NodeType_IFF, 2, array);
308 Edge array[] = {thenedge, cond};
309 result = createNode(cnf, NodeType_IFF, 2, array);
312 Edge edges[] = {cond, thenedge, elseedge};
313 result = createNode(cnf, NodeType_ITE, 3, edges);
316 result = constraintNegate(result);
320 void addConstraintCNF(CNF *cnf, Edge constraint) {
321 pushVectorEdge(&cnf->constraints, constraint);
323 model_print("****SATC_ADDING NEW Constraint*****\n");
324 printCNF(constraint);
325 model_print("\n******************************\n");
329 Edge constraintNewVar(CNF *cnf) {
330 uint varnum = cnf->varcount++;
331 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
335 int solveCNF(CNF *cnf) {
336 long long startTime=getTimeNano();
338 convertPass(cnf, false);
339 finishedClauses(cnf->solver);
340 long long startSolve=getTimeNano();
341 int result = solve(cnf->solver);
342 long long finishTime=getTimeNano();
343 cnf->encodeTime=startSolve-startTime;
344 cnf->solveTime=finishTime-startSolve;
348 bool getValueCNF(CNF *cnf, Edge var) {
349 Literal l = getEdgeVar(var);
350 bool isneg = (l < 0);
352 return isneg ^ getValueSolver(cnf->solver, l);
355 void countPass(CNF *cnf) {
356 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
357 VectorEdge *ve = allocDefVectorEdge();
358 for (uint i = 0; i < numConstraints; i++) {
359 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
361 deleteVectorEdge(ve);
364 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
365 //Skip constants and variables...
366 if (edgeIsVarConst(eroot))
369 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
371 bool isMatching = cnf->enableMatching;
373 while (getSizeVectorEdge(stack) != 0) {
374 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
375 bool polarity = isNegEdge(e);
376 Node *n = getNodePtrFromEdge(e);
377 if (getExpanded(n, polarity)) {
378 if (n->flags.type == NodeType_IFF ||
379 n->flags.type == NodeType_ITE) {
380 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
381 getNodePtrFromEdge(pExp)->intAnnot[0]++;
383 n->intAnnot[polarity]++;
386 setExpanded(n, polarity);
388 if (n->flags.type == NodeType_ITE ||
389 n->flags.type == NodeType_IFF) {
390 n->intAnnot[polarity] = 0;
391 Edge cond = n->edges[0];
392 Edge thenedge = n->edges[1];
393 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
394 thenedge = constraintNegateIf(thenedge, !polarity);
395 elseedge = constraintNegateIf(elseedge, !polarity);
396 thenedge = constraintAND2(cnf, cond, thenedge);
397 cond = constraintNegate(cond);
398 elseedge = constraintAND2(cnf, cond, elseedge);
399 thenedge = constraintNegate(thenedge);
400 elseedge = constraintNegate(elseedge);
401 cnf->enableMatching = false;
402 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
403 n->ptrAnnot[polarity] = succ1.node_ptr;
404 cnf->enableMatching = isMatching;
405 pushVectorEdge(stack, succ1);
406 if (getExpanded(n, !polarity)) {
407 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
408 Node *n1 = getNodePtrFromEdge(succ1);
409 Node *n2 = getNodePtrFromEdge(succ2);
410 n1->ptrAnnot[0] = succ2.node_ptr;
411 n2->ptrAnnot[0] = succ1.node_ptr;
412 n1->ptrAnnot[1] = succ2.node_ptr;
413 n2->ptrAnnot[1] = succ1.node_ptr;
416 n->intAnnot[polarity] = 1;
417 for (uint i = 0; i < n->numEdges; i++) {
418 Edge succ = n->edges[i];
419 if (!edgeIsVarConst(succ)) {
420 succ = constraintNegateIf(succ, polarity);
421 pushVectorEdge(stack, succ);
429 void convertPass(CNF *cnf, bool backtrackLit) {
430 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
431 VectorEdge *ve = allocDefVectorEdge();
432 for (uint i = 0; i < numConstraints; i++) {
433 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
435 deleteVectorEdge(ve);
438 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
439 Node *nroot = getNodePtrFromEdge(root);
441 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
442 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
443 root = (Edge) { nroot };
445 if (edgeIsConst(root)) {
446 if (isNegEdge(root)) {
448 Edge newvar = constraintNewVar(cnf);
449 Literal var = getEdgeVar(newvar);
450 Literal clause[] = {var};
451 addArrayClauseLiteral(cnf->solver, 1, clause);
453 addArrayClauseLiteral(cnf->solver, 1, clause);
459 } else if (edgeIsVarConst(root)) {
460 Literal clause[] = { getEdgeVar(root)};
461 addArrayClauseLiteral(cnf->solver, 1, clause);
465 clearVectorEdge(stack);pushVectorEdge(stack, root);
466 while (getSizeVectorEdge(stack) != 0) {
467 Edge e = lastVectorEdge(stack);
468 Node *n = getNodePtrFromEdge(e);
470 if (edgeIsVarConst(e)) {
471 popVectorEdge(stack);
473 } else if (n->flags.type == NodeType_ITE ||
474 n->flags.type == NodeType_IFF) {
475 popVectorEdge(stack);
476 if (n->ptrAnnot[0] != NULL)
477 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
478 if (n->ptrAnnot[1] != NULL)
479 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
483 bool needPos = (n->intAnnot[0] > 0);
484 bool needNeg = (n->intAnnot[1] > 0);
485 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
486 (!needNeg || n->flags.cnfVisitedUp & 2)) {
487 popVectorEdge(stack);
488 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
489 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
491 n->flags.cnfVisitedDown |= 1;
493 n->flags.cnfVisitedDown |= 2;
494 for (uint i = 0; i < n->numEdges; i++) {
495 Edge arg = n->edges[i];
496 arg = constraintNegateIf(arg, isNegEdge(e));
497 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
500 popVectorEdge(stack);
504 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
505 ASSERT(cnfExp != NULL);
506 if (isProxy(cnfExp)) {
507 Literal l = getProxy(cnfExp);
508 Literal clause[] = {l};
509 addArrayClauseLiteral(cnf->solver, 1, clause);
510 } else if (backtrackLit) {
511 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
512 Literal clause[] = {l};
513 addArrayClauseLiteral(cnf->solver, 1, clause);
515 outputCNF(cnf, cnfExp);
518 if (!((intptr_t) cnfExp & 1)) {
519 deleteCNFExpr(cnfExp);
520 nroot->ptrAnnot[isNegEdge(root)] = NULL;
525 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
527 Node *n = getNodePtrFromEdge(e);
529 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
530 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
531 if (isProxy(otherExp))
532 l = -getProxy(otherExp);
534 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
535 Node *nsemNeg = getNodePtrFromEdge(semNeg);
536 if (nsemNeg != NULL) {
537 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
538 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
539 if (isProxy(otherExp))
540 l = -getProxy(otherExp);
541 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
542 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
543 if (isProxy(otherExp))
544 l = getProxy(otherExp);
550 Edge newvar = constraintNewVar(cnf);
551 l = getEdgeVar(newvar);
553 // Output the constraints on the auxiliary variable
554 constrainCNF(cnf, l, exp);
557 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
562 void produceCNF(CNF *cnf, Edge e) {
563 CNFExpr *expPos = NULL;
564 CNFExpr *expNeg = NULL;
565 Node *n = getNodePtrFromEdge(e);
567 if (n->intAnnot[0] > 0) {
568 expPos = produceConjunction(cnf, e);
571 if (n->intAnnot[1] > 0) {
572 expNeg = produceDisjunction(cnf, e);
575 /// @todo Propagate constants across semantic negations (this can
576 /// be done similarly to the calls to propagate shown below). The
577 /// trick here is that we need to figure out how to get the
578 /// semantic negation pointers, and ensure that they can have CNF
579 /// produced for them at the right point
581 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
583 // propagate from positive to negative, negative to positive
584 if (!propagate(cnf, &expPos, expNeg, true))
585 propagate(cnf, &expNeg, expPos, true);
587 // The polarity heuristic entails visiting the discovery polarity first
589 saveCNF(cnf, expPos, e, false);
590 saveCNF(cnf, expNeg, e, true);
592 saveCNF(cnf, expNeg, e, true);
593 saveCNF(cnf, expPos, e, false);
597 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
598 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
600 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
601 } else if (isProxy(*dest)) {
602 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
604 Literal clause[] = {getProxy(*dest)};
605 addArrayClauseLiteral(cnf->solver, 1, clause);
607 Literal clause[] = {-getProxy(*dest)};
608 addArrayClauseLiteral(cnf->solver, 1, clause);
611 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
613 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
620 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
621 Node *n = getNodePtrFromEdge(e);
622 n->flags.cnfVisitedUp |= (1 << sign);
623 if (exp == NULL || isProxy(exp)) return;
625 if (exp->litSize == 1) {
626 Literal l = getLiteralLitVector(&exp->singletons, 0);
628 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
629 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
630 introProxy(cnf, e, exp, sign);
632 n->ptrAnnot[sign] = exp;
636 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
637 if (alwaysTrueCNF(expr)) {
639 } else if (alwaysFalseCNF(expr)) {
640 Literal clause[] = {-lcond};
641 addArrayClauseLiteral(cnf->solver, 1, clause);
645 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
646 Literal l = getLiteralLitVector(&expr->singletons,i);
647 Literal clause[] = {-lcond, l};
648 addArrayClauseLiteral(cnf->solver, 2, clause);
650 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
651 LitVector *lv = getVectorLitVector(&expr->clauses,i);
652 addClauseLiteral(cnf->solver, -lcond);//Add first literal
653 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
657 void outputCNF(CNF *cnf, CNFExpr *expr) {
658 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
659 Literal l = getLiteralLitVector(&expr->singletons,i);
660 Literal clause[] = {l};
661 addArrayClauseLiteral(cnf->solver, 1, clause);
663 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
664 LitVector *lv = getVectorLitVector(&expr->clauses,i);
665 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
669 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
670 clearVectorEdge(&cnf->args);
672 *largestEdge = (Edge) {(Node *) NULL};
673 CNFExpr *largest = NULL;
674 Node *n = getNodePtrFromEdge(e);
677 Edge arg = n->edges[--i];
678 arg = constraintNegateIf(arg, isNeg);
679 Node *narg = getNodePtrFromEdge(arg);
681 if (edgeIsVarConst(arg)) {
682 pushVectorEdge(&cnf->args, arg);
686 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
687 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
690 if (narg->intAnnot[isNegEdge(arg)] == 1) {
691 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
692 if (!isProxy(argExp)) {
693 if (largest == NULL) {
697 } else if (argExp->litSize > largest->litSize) {
698 pushVectorEdge(&cnf->args, *largestEdge);
705 pushVectorEdge(&cnf->args, arg);
708 if (largest != NULL) {
709 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
710 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
716 void printCNF(Edge e) {
717 if (edgeIsVarConst(e)) {
718 Literal l = getEdgeVar(e);
719 model_print ("%d", l);
722 bool isNeg = isNegEdge(e);
723 if (edgeIsConst(e)) {
730 Node *n = getNodePtrFromEdge(e);
732 //Pretty print things that are equivalent to OR's
733 if (getNodeType(e) == NodeType_AND) {
735 for (uint i = 0; i < n->numEdges; i++) {
736 Edge e = n->edges[i];
739 printCNF(constraintNegate(e));
747 switch (getNodeType(e)) {
759 for (uint i = 0; i < n->numEdges; i++) {
760 Edge e = n->edges[i];
768 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
771 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
773 accum = allocCNFExprBool(true);
775 int i = getSizeVectorEdge(&cnf->args);
777 Edge arg = getVectorEdge(&cnf->args, --i);
778 if (edgeIsVarConst(arg)) {
779 conjoinCNFLit(accum, getEdgeVar(arg));
781 Node *narg = getNodePtrFromEdge(arg);
782 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
784 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
785 if (isProxy(argExp)) {// variable has been introduced
786 conjoinCNFLit(accum, getProxy(argExp));
788 conjoinCNFExpr(accum, argExp, destroy);
790 narg->ptrAnnot[isNegEdge(arg)] = NULL;
800 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
802 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
804 accum = allocCNFExprBool(false);
806 // This is necessary to check to make sure that we don't start out
807 // with an accumulator that is "too large".
809 /// @todo Strictly speaking, introProxy doesn't *need* to free
810 /// memory, then this wouldn't have to reallocate CNFExpr
812 /// @todo When this call to introProxy is made, the semantic
813 /// negation pointer will have been destroyed. Thus, it will not
814 /// be possible to use the correct proxy. That should be fixed.
816 // at this point, we will either have NULL, or a destructible expression
817 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
818 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
820 int i = getSizeVectorEdge(&cnf->args);
822 Edge arg = getVectorEdge(&cnf->args, --i);
823 Node *narg = getNodePtrFromEdge(arg);
824 if (edgeIsVarConst(arg)) {
825 disjoinCNFLit(accum, getEdgeVar(arg));
827 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
829 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
830 if (isProxy(argExp)) {// variable has been introduced
831 disjoinCNFLit(accum, getProxy(argExp));
832 } else if (argExp->litSize == 0) {
833 disjoinCNFExpr(accum, argExp, destroy);
835 // check to see if we should introduce a proxy
836 int aL = accum->litSize; // lits in accum
837 int eL = argExp->litSize; // lits in argument
838 int aC = getClauseSizeCNF(accum); // clauses in accum
839 int eC = getClauseSizeCNF(argExp); // clauses in argument
841 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
842 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
844 disjoinCNFExpr(accum, argExp, destroy);
845 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
854 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
855 Edge carray[numvars];
856 for (uint j = 0; j < numvars; j++) {
857 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
861 return constraintAND(cnf, numvars, carray);
864 /** Generates a constraint to ensure that all encodings are less than value */
865 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
866 Edge orarray[numvars];
867 Edge andarray[numvars];
873 for (uint j = 0; j < numvars; j++) {
875 orarray[ori++] = constraintNegate(vars[j]);
878 //no ones to flip, so bail now...
880 return constraintAND(cnf, andi, andarray);
882 andarray[andi++] = constraintOR(cnf, ori, orarray);
884 value = value + (1 << (__builtin_ctz(value)));
889 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
893 for (uint i = 0; i < numvars; i++) {
894 array[i] = constraintIFF(cnf, var1[i], var2[i]);
896 return constraintAND(cnf, numvars, array);
899 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
902 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
903 for (uint i = 1; i < numvars; i++) {
904 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
905 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
906 result = constraintOR2(cnf, lt, eq);
911 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
914 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
915 for (uint i = 1; i < numvars; i++) {
916 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
917 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
918 result = constraintOR2(cnf, lt, eq);