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();
67 void deleteCNF(CNF *cnf) {
68 for (uint i = 0; i < cnf->capacity; i++) {
69 Node *n = cnf->node_array[i];
73 deleteVectorArrayEdge(&cnf->constraints);
74 deleteVectorArrayEdge(&cnf->args);
75 deleteIncrementalSolver(cnf->solver);
76 ourfree(cnf->node_array);
80 void resizeCNF(CNF *cnf, uint newCapacity) {
81 Node **old_array = cnf->node_array;
82 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
83 uint oldCapacity = cnf->capacity;
84 uint newMask = newCapacity - 1;
85 for (uint i = 0; i < oldCapacity; i++) {
86 Node *n = old_array[i];
89 uint hashCode = n->hashCode;
90 uint newindex = hashCode & newMask;
91 for (;; newindex = (newindex + 1) & newMask) {
92 if (new_array[newindex] == NULL) {
93 new_array[newindex] = n;
99 cnf->node_array = new_array;
100 cnf->capacity = newCapacity;
101 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
105 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
106 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
107 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
108 n->flags.type = type;
109 n->flags.wasExpanded = 0;
110 n->flags.cnfVisitedDown = 0;
111 n->flags.cnfVisitedUp = 0;
112 n->flags.varForced = 0;
113 n->numEdges = numEdges;
114 n->hashCode = hashcode;
115 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
116 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
120 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
121 if (cnf->size > cnf->maxsize) {
122 resizeCNF(cnf, cnf->capacity << 1);
124 uint hashvalue = hashNode(type, numEdges, edges);
125 uint mask = cnf->mask;
126 uint index = hashvalue & mask;
128 for (;; index = (index + 1) & mask) {
129 n_ptr = &cnf->node_array[index];
130 if (*n_ptr != NULL) {
131 if ((*n_ptr)->hashCode == hashvalue) {
132 if (compareNodes(*n_ptr, type, numEdges, edges)) {
141 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
147 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
148 uint hashvalue = type ^ numEdges;
149 for (uint i = 0; i < numEdges; i++) {
150 hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
151 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
153 return (uint) hashvalue;
156 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
157 if (node->flags.type != type || node->numEdges != numEdges)
159 Edge *nodeedges = node->edges;
160 for (uint i = 0; i < numEdges; i++) {
161 if (!equalsEdge(nodeedges[i], edges[i]))
167 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
168 Edge edgearray[numEdges];
170 for (uint i = 0; i < numEdges; i++) {
171 edgearray[i] = constraintNegate(edges[i]);
173 Edge eand = constraintAND(cnf, numEdges, edgearray);
174 return constraintNegate(eand);
177 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
178 Edge lneg = constraintNegate(left);
179 Edge rneg = constraintNegate(right);
180 Edge eand = constraintAND2(cnf, lneg, rneg);
181 return constraintNegate(eand);
184 int comparefunction(const Edge *e1, const Edge *e2) {
185 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
188 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
189 ASSERT(numEdges != 0);
190 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
192 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
195 uint remainSize = numEdges - initindex;
199 else if (remainSize == 1)
200 return edges[initindex];
201 else if (equalsEdge(edges[initindex], E_False))
204 /** De-duplicate array */
206 edges[lowindex] = edges[initindex++];
208 for (; initindex < numEdges; initindex++) {
209 Edge e1 = edges[lowindex];
210 Edge e2 = edges[initindex];
211 if (sameNodeVarEdge(e1, e2)) {
212 if (!sameSignEdge(e1, e2)) {
216 edges[++lowindex] = edges[initindex];
218 lowindex++; //Make lowindex look like size
223 if (cnf->enableMatching && lowindex == 2 &&
224 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
225 getNodeType(edges[0]) == NodeType_AND &&
226 getNodeType(edges[1]) == NodeType_AND &&
227 getNodeSize(edges[0]) == 2 &&
228 getNodeSize(edges[1]) == 2) {
229 Edge *e0edges = getEdgeArray(edges[0]);
230 Edge *e1edges = getEdgeArray(edges[1]);
231 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
232 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
233 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
234 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
235 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
236 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
237 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
238 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
242 return createNode(cnf, NodeType_AND, lowindex, edges);
245 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
246 Edge edges[2] = {left, right};
247 return constraintAND(cnf, 2, edges);
250 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
253 array[1] = constraintNegate(right);
254 Edge eand = constraintAND(cnf, 2, array);
255 return constraintNegate(eand);
258 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
259 bool negate = !sameSignEdge(left, right);
260 Edge lpos = getNonNeg(left);
261 Edge rpos = getNonNeg(right);
264 if (equalsEdge(lpos, rpos)) {
266 } else if (ltEdge(lpos, rpos)) {
267 Edge edges[] = {lpos, rpos};
268 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
270 Edge edges[] = {rpos, lpos};
271 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
274 e = constraintNegate(e);
278 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
279 if (isNegEdge(cond)) {
280 cond = constraintNegate(cond);
286 bool negate = isNegEdge(thenedge);
288 thenedge = constraintNegate(thenedge);
289 elseedge = constraintNegate(elseedge);
293 if (equalsEdge(cond, E_True)) {
295 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
296 Edge array[] = {cond, elseedge};
297 result = constraintOR(cnf, 2, array);
298 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
299 result = constraintIMPLIES(cnf, cond, thenedge);
300 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
301 Edge array[] = {cond, thenedge};
302 result = constraintAND(cnf, 2, array);
303 } else if (equalsEdge(thenedge, elseedge)) {
305 } else if (sameNodeOppSign(thenedge, elseedge)) {
306 if (ltEdge(cond, thenedge)) {
307 Edge array[] = {cond, thenedge};
308 result = createNode(cnf, NodeType_IFF, 2, array);
310 Edge array[] = {thenedge, cond};
311 result = createNode(cnf, NodeType_IFF, 2, array);
314 Edge edges[] = {cond, thenedge, elseedge};
315 result = createNode(cnf, NodeType_ITE, 3, edges);
318 result = constraintNegate(result);
322 void addConstraintCNF(CNF *cnf, Edge constraint) {
323 pushVectorEdge(&cnf->constraints, constraint);
325 model_print("****SATC_ADDING NEW Constraint*****\n");
326 printCNF(constraint);
327 model_print("\n******************************\n");
331 Edge constraintNewVar(CNF *cnf) {
332 uint varnum = cnf->varcount++;
333 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
337 int solveCNF(CNF *cnf) {
338 long long startTime = getTimeNano();
340 convertPass(cnf, false);
341 finishedClauses(cnf->solver);
342 long long startSolve = getTimeNano();
343 int result = solve(cnf->solver);
344 long long finishTime = getTimeNano();
345 cnf->encodeTime = startSolve - startTime;
346 cnf->solveTime = finishTime - startSolve;
350 bool getValueCNF(CNF *cnf, Edge var) {
351 Literal l = getEdgeVar(var);
352 bool isneg = (l < 0);
354 return isneg ^ getValueSolver(cnf->solver, l);
357 void countPass(CNF *cnf) {
358 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
359 VectorEdge *ve = allocDefVectorEdge();
360 for (uint i = 0; i < numConstraints; i++) {
361 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
363 deleteVectorEdge(ve);
366 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
367 //Skip constants and variables...
368 if (edgeIsVarConst(eroot))
371 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
373 bool isMatching = cnf->enableMatching;
375 while (getSizeVectorEdge(stack) != 0) {
376 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
377 bool polarity = isNegEdge(e);
378 Node *n = getNodePtrFromEdge(e);
379 if (getExpanded(n, polarity)) {
380 if (n->flags.type == NodeType_IFF ||
381 n->flags.type == NodeType_ITE) {
382 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
383 getNodePtrFromEdge(pExp)->intAnnot[0]++;
385 n->intAnnot[polarity]++;
388 setExpanded(n, polarity);
390 if (n->flags.type == NodeType_ITE ||
391 n->flags.type == NodeType_IFF) {
392 n->intAnnot[polarity] = 0;
393 Edge cond = n->edges[0];
394 Edge thenedge = n->edges[1];
395 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
396 thenedge = constraintNegateIf(thenedge, !polarity);
397 elseedge = constraintNegateIf(elseedge, !polarity);
398 thenedge = constraintAND2(cnf, cond, thenedge);
399 cond = constraintNegate(cond);
400 elseedge = constraintAND2(cnf, cond, elseedge);
401 thenedge = constraintNegate(thenedge);
402 elseedge = constraintNegate(elseedge);
403 cnf->enableMatching = false;
404 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
405 n->ptrAnnot[polarity] = succ1.node_ptr;
406 cnf->enableMatching = isMatching;
407 pushVectorEdge(stack, succ1);
408 if (getExpanded(n, !polarity)) {
409 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
410 Node *n1 = getNodePtrFromEdge(succ1);
411 Node *n2 = getNodePtrFromEdge(succ2);
412 n1->ptrAnnot[0] = succ2.node_ptr;
413 n2->ptrAnnot[0] = succ1.node_ptr;
414 n1->ptrAnnot[1] = succ2.node_ptr;
415 n2->ptrAnnot[1] = succ1.node_ptr;
418 n->intAnnot[polarity] = 1;
419 for (uint i = 0; i < n->numEdges; i++) {
420 Edge succ = n->edges[i];
421 if (!edgeIsVarConst(succ)) {
422 succ = constraintNegateIf(succ, polarity);
423 pushVectorEdge(stack, succ);
431 void convertPass(CNF *cnf, bool backtrackLit) {
432 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
433 VectorEdge *ve = allocDefVectorEdge();
434 for (uint i = 0; i < numConstraints; i++) {
435 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
437 deleteVectorEdge(ve);
440 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
441 Node *nroot = getNodePtrFromEdge(root);
443 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
444 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
445 root = (Edge) { nroot };
447 if (edgeIsConst(root)) {
448 if (isNegEdge(root)) {
450 Edge newvar = constraintNewVar(cnf);
451 Literal var = getEdgeVar(newvar);
452 Literal clause[] = {var};
453 addArrayClauseLiteral(cnf->solver, 1, clause);
455 addArrayClauseLiteral(cnf->solver, 1, clause);
461 } else if (edgeIsVarConst(root)) {
462 Literal clause[] = { getEdgeVar(root)};
463 addArrayClauseLiteral(cnf->solver, 1, clause);
467 clearVectorEdge(stack);pushVectorEdge(stack, root);
468 while (getSizeVectorEdge(stack) != 0) {
469 Edge e = lastVectorEdge(stack);
470 Node *n = getNodePtrFromEdge(e);
472 if (edgeIsVarConst(e)) {
473 popVectorEdge(stack);
475 } else if (n->flags.type == NodeType_ITE ||
476 n->flags.type == NodeType_IFF) {
477 popVectorEdge(stack);
478 if (n->ptrAnnot[0] != NULL)
479 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
480 if (n->ptrAnnot[1] != NULL)
481 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
485 bool needPos = (n->intAnnot[0] > 0);
486 bool needNeg = (n->intAnnot[1] > 0);
487 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
488 (!needNeg || n->flags.cnfVisitedUp & 2)) {
489 popVectorEdge(stack);
490 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
491 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
493 n->flags.cnfVisitedDown |= 1;
495 n->flags.cnfVisitedDown |= 2;
496 for (uint i = 0; i < n->numEdges; i++) {
497 Edge arg = n->edges[i];
498 arg = constraintNegateIf(arg, isNegEdge(e));
499 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
502 popVectorEdge(stack);
506 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
507 ASSERT(cnfExp != NULL);
508 if (isProxy(cnfExp)) {
509 Literal l = getProxy(cnfExp);
510 Literal clause[] = {l};
511 addArrayClauseLiteral(cnf->solver, 1, clause);
512 } else if (backtrackLit) {
513 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
514 Literal clause[] = {l};
515 addArrayClauseLiteral(cnf->solver, 1, clause);
517 outputCNF(cnf, cnfExp);
520 if (!((intptr_t) cnfExp & 1)) {
521 deleteCNFExpr(cnfExp);
522 nroot->ptrAnnot[isNegEdge(root)] = NULL;
527 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
529 Node *n = getNodePtrFromEdge(e);
531 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
532 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
533 if (isProxy(otherExp))
534 l = -getProxy(otherExp);
536 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
537 Node *nsemNeg = getNodePtrFromEdge(semNeg);
538 if (nsemNeg != NULL) {
539 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
540 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
541 if (isProxy(otherExp))
542 l = -getProxy(otherExp);
543 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
544 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
545 if (isProxy(otherExp))
546 l = getProxy(otherExp);
552 Edge newvar = constraintNewVar(cnf);
553 l = getEdgeVar(newvar);
555 // Output the constraints on the auxiliary variable
556 constrainCNF(cnf, l, exp);
559 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
564 void produceCNF(CNF *cnf, Edge e) {
565 CNFExpr *expPos = NULL;
566 CNFExpr *expNeg = NULL;
567 Node *n = getNodePtrFromEdge(e);
569 if (n->intAnnot[0] > 0) {
570 expPos = produceConjunction(cnf, e);
573 if (n->intAnnot[1] > 0) {
574 expNeg = produceDisjunction(cnf, e);
577 /// @todo Propagate constants across semantic negations (this can
578 /// be done similarly to the calls to propagate shown below). The
579 /// trick here is that we need to figure out how to get the
580 /// semantic negation pointers, and ensure that they can have CNF
581 /// produced for them at the right point
583 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
585 // propagate from positive to negative, negative to positive
586 if (!propagate(cnf, &expPos, expNeg, true))
587 propagate(cnf, &expNeg, expPos, true);
589 // The polarity heuristic entails visiting the discovery polarity first
591 saveCNF(cnf, expPos, e, false);
592 saveCNF(cnf, expNeg, e, true);
594 saveCNF(cnf, expNeg, e, true);
595 saveCNF(cnf, expPos, e, false);
599 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
600 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
602 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
603 } else if (isProxy(*dest)) {
604 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
606 Literal clause[] = {getProxy(*dest)};
607 addArrayClauseLiteral(cnf->solver, 1, clause);
609 Literal clause[] = {-getProxy(*dest)};
610 addArrayClauseLiteral(cnf->solver, 1, clause);
613 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
615 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
622 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
623 Node *n = getNodePtrFromEdge(e);
624 n->flags.cnfVisitedUp |= (1 << sign);
625 if (exp == NULL || isProxy(exp)) return;
627 if (exp->litSize == 1) {
628 Literal l = getLiteralLitVector(&exp->singletons, 0);
630 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
631 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
632 introProxy(cnf, e, exp, sign);
634 n->ptrAnnot[sign] = exp;
638 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
639 if (alwaysTrueCNF(expr)) {
641 } else if (alwaysFalseCNF(expr)) {
642 Literal clause[] = {-lcond};
643 addArrayClauseLiteral(cnf->solver, 1, clause);
647 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
648 Literal l = getLiteralLitVector(&expr->singletons,i);
649 Literal clause[] = {-lcond, l};
650 addArrayClauseLiteral(cnf->solver, 2, clause);
652 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
653 LitVector *lv = getVectorLitVector(&expr->clauses,i);
654 addClauseLiteral(cnf->solver, -lcond);//Add first literal
655 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
659 void outputCNF(CNF *cnf, CNFExpr *expr) {
660 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
661 Literal l = getLiteralLitVector(&expr->singletons,i);
662 Literal clause[] = {l};
663 addArrayClauseLiteral(cnf->solver, 1, clause);
665 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
666 LitVector *lv = getVectorLitVector(&expr->clauses,i);
667 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
671 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
672 clearVectorEdge(&cnf->args);
674 *largestEdge = (Edge) {(Node *) NULL};
675 CNFExpr *largest = NULL;
676 Node *n = getNodePtrFromEdge(e);
679 Edge arg = n->edges[--i];
680 arg = constraintNegateIf(arg, isNeg);
681 Node *narg = getNodePtrFromEdge(arg);
683 if (edgeIsVarConst(arg)) {
684 pushVectorEdge(&cnf->args, arg);
688 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
689 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
692 if (narg->intAnnot[isNegEdge(arg)] == 1) {
693 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
694 if (!isProxy(argExp)) {
695 if (largest == NULL) {
699 } else if (argExp->litSize > largest->litSize) {
700 pushVectorEdge(&cnf->args, *largestEdge);
707 pushVectorEdge(&cnf->args, arg);
710 if (largest != NULL) {
711 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
712 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
718 void printCNF(Edge e) {
719 if (edgeIsVarConst(e)) {
720 Literal l = getEdgeVar(e);
721 model_print ("%d", l);
724 bool isNeg = isNegEdge(e);
725 if (edgeIsConst(e)) {
732 Node *n = getNodePtrFromEdge(e);
734 //Pretty print things that are equivalent to OR's
735 if (getNodeType(e) == NodeType_AND) {
737 for (uint i = 0; i < n->numEdges; i++) {
738 Edge e = n->edges[i];
741 printCNF(constraintNegate(e));
749 switch (getNodeType(e)) {
761 for (uint i = 0; i < n->numEdges; i++) {
762 Edge e = n->edges[i];
770 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
773 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
775 accum = allocCNFExprBool(true);
777 int i = getSizeVectorEdge(&cnf->args);
779 Edge arg = getVectorEdge(&cnf->args, --i);
780 if (edgeIsVarConst(arg)) {
781 conjoinCNFLit(accum, getEdgeVar(arg));
783 Node *narg = getNodePtrFromEdge(arg);
784 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
786 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
787 if (isProxy(argExp)) {// variable has been introduced
788 conjoinCNFLit(accum, getProxy(argExp));
790 conjoinCNFExpr(accum, argExp, destroy);
792 narg->ptrAnnot[isNegEdge(arg)] = NULL;
802 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
804 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
806 accum = allocCNFExprBool(false);
808 // This is necessary to check to make sure that we don't start out
809 // with an accumulator that is "too large".
811 /// @todo Strictly speaking, introProxy doesn't *need* to free
812 /// memory, then this wouldn't have to reallocate CNFExpr
814 /// @todo When this call to introProxy is made, the semantic
815 /// negation pointer will have been destroyed. Thus, it will not
816 /// be possible to use the correct proxy. That should be fixed.
818 // at this point, we will either have NULL, or a destructible expression
819 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
820 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
822 int i = getSizeVectorEdge(&cnf->args);
824 Edge arg = getVectorEdge(&cnf->args, --i);
825 Node *narg = getNodePtrFromEdge(arg);
826 if (edgeIsVarConst(arg)) {
827 disjoinCNFLit(accum, getEdgeVar(arg));
829 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
831 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
832 if (isProxy(argExp)) {// variable has been introduced
833 disjoinCNFLit(accum, getProxy(argExp));
834 } else if (argExp->litSize == 0) {
835 disjoinCNFExpr(accum, argExp, destroy);
837 // check to see if we should introduce a proxy
838 int aL = accum->litSize; // lits in accum
839 int eL = argExp->litSize; // lits in argument
840 int aC = getClauseSizeCNF(accum); // clauses in accum
841 int eC = getClauseSizeCNF(argExp); // clauses in argument
842 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
843 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
844 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
846 disjoinCNFExpr(accum, argExp, destroy);
847 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
856 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
857 Edge carray[numvars];
858 for (uint j = 0; j < numvars; j++) {
859 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
863 return constraintAND(cnf, numvars, carray);
866 /** Generates a constraint to ensure that all encodings are less than value */
867 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
868 Edge orarray[numvars];
869 Edge andarray[numvars];
875 for (uint j = 0; j < numvars; j++) {
877 orarray[ori++] = constraintNegate(vars[j]);
880 //no ones to flip, so bail now...
882 return constraintAND(cnf, andi, andarray);
884 andarray[andi++] = constraintOR(cnf, ori, orarray);
886 value = value + (1 << (__builtin_ctz(value)));
891 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
895 for (uint i = 0; i < numvars; i++) {
896 array[i] = constraintIFF(cnf, var1[i], var2[i]);
898 return constraintAND(cnf, numvars, array);
901 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
904 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
905 for (uint i = 1; i < numvars; i++) {
906 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
907 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
908 result = constraintOR2(cnf, lt, eq);
913 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
916 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
917 for (uint i = 1; i < numvars; i++) {
918 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
919 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
920 result = constraintOR2(cnf, lt, eq);