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 resetCNF(CNF *cnf) {
82 for (uint i = 0; i < cnf->capacity; i++) {
83 Node *n = cnf->node_array[i];
87 clearVectorEdge(&cnf->constraints);
88 clearVectorEdge(&cnf->args);
89 resetSolver(cnf->solver);
90 memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
94 cnf->enableMatching = true;
99 void resizeCNF(CNF *cnf, uint newCapacity) {
100 Node **old_array = cnf->node_array;
101 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
102 uint oldCapacity = cnf->capacity;
103 uint newMask = newCapacity - 1;
104 for (uint i = 0; i < oldCapacity; i++) {
105 Node *n = old_array[i];
108 uint hashCode = n->hashCode;
109 uint newindex = hashCode & newMask;
110 for (;; newindex = (newindex + 1) & newMask) {
111 if (new_array[newindex] == NULL) {
112 new_array[newindex] = n;
118 cnf->node_array = new_array;
119 cnf->capacity = newCapacity;
120 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
124 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
125 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
126 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
127 n->flags.type = type;
128 n->flags.wasExpanded = 0;
129 n->flags.cnfVisitedDown = 0;
130 n->flags.cnfVisitedUp = 0;
131 n->flags.varForced = 0;
132 n->numEdges = numEdges;
133 n->hashCode = hashcode;
134 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
135 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
139 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
140 if (cnf->size > cnf->maxsize) {
141 resizeCNF(cnf, cnf->capacity << 1);
143 uint hashvalue = hashNode(type, numEdges, edges);
144 uint mask = cnf->mask;
145 uint index = hashvalue & mask;
147 for (;; index = (index + 1) & mask) {
148 n_ptr = &cnf->node_array[index];
149 if (*n_ptr != NULL) {
150 if ((*n_ptr)->hashCode == hashvalue) {
151 if (compareNodes(*n_ptr, type, numEdges, edges)) {
160 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
166 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
170 for (uint i = 0; i < numEdges; i++) {
171 uint c = (uint) ((uintptr_t) edges[i].node_ptr);
182 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
183 if (node->flags.type != type || node->numEdges != numEdges)
185 Edge *nodeedges = node->edges;
186 for (uint i = 0; i < numEdges; i++) {
187 if (!equalsEdge(nodeedges[i], edges[i]))
193 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
194 Edge edgearray[numEdges];
196 for (uint i = 0; i < numEdges; i++) {
197 edgearray[i] = constraintNegate(edges[i]);
199 Edge eand = constraintAND(cnf, numEdges, edgearray);
200 return constraintNegate(eand);
203 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
204 Edge lneg = constraintNegate(left);
205 Edge rneg = constraintNegate(right);
206 Edge eand = constraintAND2(cnf, lneg, rneg);
207 return constraintNegate(eand);
210 int comparefunction(const Edge *e1, const Edge *e2) {
211 if (e1->node_ptr == e2->node_ptr)
213 if (((uintptr_t)e1->node_ptr) < ((uintptr_t) e2->node_ptr))
219 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
220 ASSERT(numEdges != 0);
221 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
223 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
226 uint remainSize = numEdges - initindex;
230 else if (remainSize == 1)
231 return edges[initindex];
232 else if (equalsEdge(edges[initindex], E_False))
235 /** De-duplicate array */
237 edges[lowindex] = edges[initindex++];
239 for (; initindex < numEdges; initindex++) {
240 Edge e1 = edges[lowindex];
241 Edge e2 = edges[initindex];
242 if (sameNodeVarEdge(e1, e2)) {
243 if (!sameSignEdge(e1, e2)) {
247 edges[++lowindex] = edges[initindex];
249 lowindex++; //Make lowindex look like size
254 if (cnf->enableMatching && lowindex == 2 &&
255 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
256 getNodeType(edges[0]) == NodeType_AND &&
257 getNodeType(edges[1]) == NodeType_AND &&
258 getNodeSize(edges[0]) == 2 &&
259 getNodeSize(edges[1]) == 2) {
260 Edge *e0edges = getEdgeArray(edges[0]);
261 Edge *e1edges = getEdgeArray(edges[1]);
262 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
263 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
264 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
265 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
266 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
267 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
268 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
269 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
273 return createNode(cnf, NodeType_AND, lowindex, edges);
276 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
277 Edge edges[2] = {left, right};
278 return constraintAND(cnf, 2, edges);
281 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
284 array[1] = constraintNegate(right);
285 Edge eand = constraintAND(cnf, 2, array);
286 return constraintNegate(eand);
289 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
290 bool negate = !sameSignEdge(left, right);
291 Edge lpos = getNonNeg(left);
292 Edge rpos = getNonNeg(right);
295 if (equalsEdge(lpos, rpos)) {
297 } else if (ltEdge(lpos, rpos)) {
298 Edge edges[] = {lpos, rpos};
299 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
301 Edge edges[] = {rpos, lpos};
302 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
305 e = constraintNegate(e);
309 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
310 if (isNegEdge(cond)) {
311 cond = constraintNegate(cond);
317 bool negate = isNegEdge(thenedge);
319 thenedge = constraintNegate(thenedge);
320 elseedge = constraintNegate(elseedge);
324 if (equalsEdge(cond, E_True)) {
326 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
327 Edge array[] = {cond, elseedge};
328 result = constraintOR(cnf, 2, array);
329 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
330 result = constraintIMPLIES(cnf, cond, thenedge);
331 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
332 Edge array[] = {cond, thenedge};
333 result = constraintAND(cnf, 2, array);
334 } else if (equalsEdge(thenedge, elseedge)) {
336 } else if (sameNodeOppSign(thenedge, elseedge)) {
337 if (ltEdge(cond, thenedge)) {
338 Edge array[] = {cond, thenedge};
339 result = createNode(cnf, NodeType_IFF, 2, array);
341 Edge array[] = {thenedge, cond};
342 result = createNode(cnf, NodeType_IFF, 2, array);
345 Edge edges[] = {cond, thenedge, elseedge};
346 result = createNode(cnf, NodeType_ITE, 3, edges);
349 result = constraintNegate(result);
353 void addConstraintCNF(CNF *cnf, Edge constraint) {
354 pushVectorEdge(&cnf->constraints, constraint);
356 model_print("****SATC_ADDING NEW Constraint*****\n");
357 printCNF(constraint);
358 model_print("\n******************************\n");
362 Edge constraintNewVar(CNF *cnf) {
363 uint varnum = cnf->varcount++;
364 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
368 int solveCNF(CNF *cnf) {
369 long long startTime = getTimeNano();
371 convertPass(cnf, false);
372 finishedClauses(cnf->solver);
373 long long startSolve = getTimeNano();
374 int result = solve(cnf->solver);
375 long long finishTime = getTimeNano();
376 cnf->encodeTime = startSolve - startTime;
377 model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
378 cnf->solveTime = finishTime - startSolve;
379 model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
383 bool getValueCNF(CNF *cnf, Edge var) {
384 Literal l = getEdgeVar(var);
385 bool isneg = (l < 0);
387 return isneg ^ getValueSolver(cnf->solver, l);
390 void countPass(CNF *cnf) {
391 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
392 VectorEdge *ve = allocDefVectorEdge();
393 for (uint i = 0; i < numConstraints; i++) {
394 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
396 deleteVectorEdge(ve);
399 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
400 //Skip constants and variables...
401 if (edgeIsVarConst(eroot))
404 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
406 bool isMatching = cnf->enableMatching;
408 while (getSizeVectorEdge(stack) != 0) {
409 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
410 bool polarity = isNegEdge(e);
411 Node *n = getNodePtrFromEdge(e);
412 if (getExpanded(n, polarity)) {
413 if (n->flags.type == NodeType_IFF ||
414 n->flags.type == NodeType_ITE) {
415 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
416 getNodePtrFromEdge(pExp)->intAnnot[0]++;
418 n->intAnnot[polarity]++;
421 setExpanded(n, polarity);
423 if (n->flags.type == NodeType_ITE ||
424 n->flags.type == NodeType_IFF) {
425 n->intAnnot[polarity] = 0;
426 Edge cond = n->edges[0];
427 Edge thenedge = n->edges[1];
428 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
429 thenedge = constraintNegateIf(thenedge, !polarity);
430 elseedge = constraintNegateIf(elseedge, !polarity);
431 thenedge = constraintAND2(cnf, cond, thenedge);
432 cond = constraintNegate(cond);
433 elseedge = constraintAND2(cnf, cond, elseedge);
434 thenedge = constraintNegate(thenedge);
435 elseedge = constraintNegate(elseedge);
436 cnf->enableMatching = false;
437 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
438 n->ptrAnnot[polarity] = succ1.node_ptr;
439 cnf->enableMatching = isMatching;
440 pushVectorEdge(stack, succ1);
441 if (getExpanded(n, !polarity)) {
442 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
443 Node *n1 = getNodePtrFromEdge(succ1);
444 Node *n2 = getNodePtrFromEdge(succ2);
445 n1->ptrAnnot[0] = succ2.node_ptr;
446 n2->ptrAnnot[0] = succ1.node_ptr;
447 n1->ptrAnnot[1] = succ2.node_ptr;
448 n2->ptrAnnot[1] = succ1.node_ptr;
451 n->intAnnot[polarity] = 1;
452 for (uint i = 0; i < n->numEdges; i++) {
453 Edge succ = n->edges[i];
454 if (!edgeIsVarConst(succ)) {
455 succ = constraintNegateIf(succ, polarity);
456 pushVectorEdge(stack, succ);
464 void convertPass(CNF *cnf, bool backtrackLit) {
465 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
466 VectorEdge *ve = allocDefVectorEdge();
467 for (uint i = 0; i < numConstraints; i++) {
468 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
470 deleteVectorEdge(ve);
473 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
474 Node *nroot = getNodePtrFromEdge(root);
476 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
477 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
478 root = (Edge) { nroot };
480 if (edgeIsConst(root)) {
481 if (isNegEdge(root)) {
483 Edge newvar = constraintNewVar(cnf);
484 Literal var = getEdgeVar(newvar);
485 Literal clause[] = {var};
486 addArrayClauseLiteral(cnf->solver, 1, clause);
488 addArrayClauseLiteral(cnf->solver, 1, clause);
494 } else if (edgeIsVarConst(root)) {
495 Literal clause[] = { getEdgeVar(root)};
496 addArrayClauseLiteral(cnf->solver, 1, clause);
500 clearVectorEdge(stack);pushVectorEdge(stack, root);
501 while (getSizeVectorEdge(stack) != 0) {
502 Edge e = lastVectorEdge(stack);
503 Node *n = getNodePtrFromEdge(e);
505 if (edgeIsVarConst(e)) {
506 popVectorEdge(stack);
508 } else if (n->flags.type == NodeType_ITE ||
509 n->flags.type == NodeType_IFF) {
510 popVectorEdge(stack);
511 if (n->ptrAnnot[0] != NULL)
512 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
513 if (n->ptrAnnot[1] != NULL)
514 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
518 bool needPos = (n->intAnnot[0] > 0);
519 bool needNeg = (n->intAnnot[1] > 0);
520 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
521 (!needNeg || n->flags.cnfVisitedUp & 2)) {
522 popVectorEdge(stack);
523 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
524 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
526 n->flags.cnfVisitedDown |= 1;
528 n->flags.cnfVisitedDown |= 2;
529 for (uint i = 0; i < n->numEdges; i++) {
530 Edge arg = n->edges[i];
531 arg = constraintNegateIf(arg, isNegEdge(e));
532 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
535 popVectorEdge(stack);
539 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
540 ASSERT(cnfExp != NULL);
541 if (isProxy(cnfExp)) {
542 Literal l = getProxy(cnfExp);
543 Literal clause[] = {l};
544 addArrayClauseLiteral(cnf->solver, 1, clause);
545 } else if (backtrackLit) {
546 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
547 Literal clause[] = {l};
548 addArrayClauseLiteral(cnf->solver, 1, clause);
550 outputCNF(cnf, cnfExp);
553 if (!((intptr_t) cnfExp & 1)) {
554 deleteCNFExpr(cnfExp);
555 nroot->ptrAnnot[isNegEdge(root)] = NULL;
560 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
562 Node *n = getNodePtrFromEdge(e);
564 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
565 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
566 if (isProxy(otherExp))
567 l = -getProxy(otherExp);
569 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
570 Node *nsemNeg = getNodePtrFromEdge(semNeg);
571 if (nsemNeg != NULL) {
572 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
573 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
574 if (isProxy(otherExp))
575 l = -getProxy(otherExp);
576 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
577 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
578 if (isProxy(otherExp))
579 l = getProxy(otherExp);
585 Edge newvar = constraintNewVar(cnf);
586 l = getEdgeVar(newvar);
588 // Output the constraints on the auxiliary variable
589 constrainCNF(cnf, l, exp);
592 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
597 void produceCNF(CNF *cnf, Edge e) {
598 CNFExpr *expPos = NULL;
599 CNFExpr *expNeg = NULL;
600 Node *n = getNodePtrFromEdge(e);
602 if (n->intAnnot[0] > 0) {
603 expPos = produceConjunction(cnf, e);
606 if (n->intAnnot[1] > 0) {
607 expNeg = produceDisjunction(cnf, e);
610 /// @todo Propagate constants across semantic negations (this can
611 /// be done similarly to the calls to propagate shown below). The
612 /// trick here is that we need to figure out how to get the
613 /// semantic negation pointers, and ensure that they can have CNF
614 /// produced for them at the right point
616 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
618 // propagate from positive to negative, negative to positive
619 if (!propagate(cnf, &expPos, expNeg, true))
620 propagate(cnf, &expNeg, expPos, true);
622 // The polarity heuristic entails visiting the discovery polarity first
624 saveCNF(cnf, expPos, e, false);
625 saveCNF(cnf, expNeg, e, true);
627 saveCNF(cnf, expNeg, e, true);
628 saveCNF(cnf, expPos, e, false);
632 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
633 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
635 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
636 } else if (isProxy(*dest)) {
637 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
639 Literal clause[] = {getProxy(*dest)};
640 addArrayClauseLiteral(cnf->solver, 1, clause);
642 Literal clause[] = {-getProxy(*dest)};
643 addArrayClauseLiteral(cnf->solver, 1, clause);
646 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
648 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
655 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
656 Node *n = getNodePtrFromEdge(e);
657 n->flags.cnfVisitedUp |= (1 << sign);
658 if (exp == NULL || isProxy(exp)) return;
660 if (exp->litSize == 1) {
661 Literal l = getLiteralLitVector(&exp->singletons, 0);
663 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
664 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
665 introProxy(cnf, e, exp, sign);
667 n->ptrAnnot[sign] = exp;
671 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
672 if (alwaysTrueCNF(expr)) {
674 } else if (alwaysFalseCNF(expr)) {
675 Literal clause[] = {-lcond};
676 addArrayClauseLiteral(cnf->solver, 1, clause);
680 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
681 Literal l = getLiteralLitVector(&expr->singletons,i);
682 Literal clause[] = {-lcond, l};
683 addArrayClauseLiteral(cnf->solver, 2, clause);
685 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
686 LitVector *lv = getVectorLitVector(&expr->clauses,i);
687 addClauseLiteral(cnf->solver, -lcond);//Add first literal
688 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
692 void outputCNF(CNF *cnf, CNFExpr *expr) {
693 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
694 Literal l = getLiteralLitVector(&expr->singletons,i);
695 Literal clause[] = {l};
696 addArrayClauseLiteral(cnf->solver, 1, clause);
698 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
699 LitVector *lv = getVectorLitVector(&expr->clauses,i);
700 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
704 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
705 clearVectorEdge(&cnf->args);
707 *largestEdge = (Edge) {(Node *) NULL};
708 CNFExpr *largest = NULL;
709 Node *n = getNodePtrFromEdge(e);
712 Edge arg = n->edges[--i];
713 arg = constraintNegateIf(arg, isNeg);
714 Node *narg = getNodePtrFromEdge(arg);
716 if (edgeIsVarConst(arg)) {
717 pushVectorEdge(&cnf->args, arg);
721 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
722 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
725 if (narg->intAnnot[isNegEdge(arg)] == 1) {
726 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
727 if (!isProxy(argExp)) {
728 if (largest == NULL) {
732 } else if (argExp->litSize > largest->litSize) {
733 pushVectorEdge(&cnf->args, *largestEdge);
740 pushVectorEdge(&cnf->args, arg);
743 if (largest != NULL) {
744 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
745 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
751 void printCNF(Edge e) {
752 if (edgeIsVarConst(e)) {
753 Literal l = getEdgeVar(e);
754 model_print ("%d", l);
757 bool isNeg = isNegEdge(e);
758 if (edgeIsConst(e)) {
765 Node *n = getNodePtrFromEdge(e);
767 //Pretty print things that are equivalent to OR's
768 if (getNodeType(e) == NodeType_AND) {
770 for (uint i = 0; i < n->numEdges; i++) {
771 Edge e = n->edges[i];
774 printCNF(constraintNegate(e));
782 switch (getNodeType(e)) {
794 for (uint i = 0; i < n->numEdges; i++) {
795 Edge e = n->edges[i];
803 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
806 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
808 accum = allocCNFExprBool(true);
810 int i = getSizeVectorEdge(&cnf->args);
812 Edge arg = getVectorEdge(&cnf->args, --i);
813 if (edgeIsVarConst(arg)) {
814 conjoinCNFLit(accum, getEdgeVar(arg));
816 Node *narg = getNodePtrFromEdge(arg);
817 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
819 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
820 if (isProxy(argExp)) {// variable has been introduced
821 conjoinCNFLit(accum, getProxy(argExp));
823 conjoinCNFExpr(accum, argExp, destroy);
825 narg->ptrAnnot[isNegEdge(arg)] = NULL;
835 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
837 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
839 accum = allocCNFExprBool(false);
841 // This is necessary to check to make sure that we don't start out
842 // with an accumulator that is "too large".
844 /// @todo Strictly speaking, introProxy doesn't *need* to free
845 /// memory, then this wouldn't have to reallocate CNFExpr
847 /// @todo When this call to introProxy is made, the semantic
848 /// negation pointer will have been destroyed. Thus, it will not
849 /// be possible to use the correct proxy. That should be fixed.
851 // at this point, we will either have NULL, or a destructible expression
852 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
853 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
855 int i = getSizeVectorEdge(&cnf->args);
857 Edge arg = getVectorEdge(&cnf->args, --i);
858 Node *narg = getNodePtrFromEdge(arg);
859 if (edgeIsVarConst(arg)) {
860 disjoinCNFLit(accum, getEdgeVar(arg));
862 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
864 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
865 if (isProxy(argExp)) {// variable has been introduced
866 disjoinCNFLit(accum, getProxy(argExp));
867 } else if (argExp->litSize == 0) {
868 disjoinCNFExpr(accum, argExp, destroy);
870 // check to see if we should introduce a proxy
871 int aL = accum->litSize; // lits in accum
872 int eL = argExp->litSize; // lits in argument
873 int aC = getClauseSizeCNF(accum); // clauses in accum
874 int eC = getClauseSizeCNF(argExp); // clauses in argument
875 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
876 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
877 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
879 disjoinCNFExpr(accum, argExp, destroy);
880 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
889 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
890 Edge carray[numvars];
891 for (uint j = 0; j < numvars; j++) {
892 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
896 return constraintAND(cnf, numvars, carray);
899 /** Generates a constraint to ensure that all encodings are less than value */
900 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
901 Edge orarray[numvars];
902 Edge andarray[numvars];
908 for (uint j = 0; j < numvars; j++) {
910 orarray[ori++] = constraintNegate(vars[j]);
913 //no ones to flip, so bail now...
915 return constraintAND(cnf, andi, andarray);
917 andarray[andi++] = constraintOR(cnf, ori, orarray);
919 value = value + (1 << (__builtin_ctz(value)));
924 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
928 for (uint i = 0; i < numvars; i++) {
929 array[i] = constraintIFF(cnf, var1[i], var2[i]);
931 return constraintAND(cnf, numvars, array);
934 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
937 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
938 for (uint i = 1; i < numvars; i++) {
939 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
940 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
941 result = constraintOR2(cnf, lt, eq);
946 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
949 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
950 for (uint i = 1; i < numvars; i++) {
951 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
952 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
953 result = constraintOR2(cnf, lt, eq);