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 deleteIncrementalSolver(cnf->solver);
90 memset(cnf->node_array, 0, sizeof(Node *) * cnf->capacity);
94 cnf->enableMatching = true;
95 cnf->solver = allocIncrementalSolver();
100 void resizeCNF(CNF *cnf, uint newCapacity) {
101 Node **old_array = cnf->node_array;
102 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
103 uint oldCapacity = cnf->capacity;
104 uint newMask = newCapacity - 1;
105 for (uint i = 0; i < oldCapacity; i++) {
106 Node *n = old_array[i];
109 uint hashCode = n->hashCode;
110 uint newindex = hashCode & newMask;
111 for (;; newindex = (newindex + 1) & newMask) {
112 if (new_array[newindex] == NULL) {
113 new_array[newindex] = n;
119 cnf->node_array = new_array;
120 cnf->capacity = newCapacity;
121 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
125 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
126 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
127 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
128 n->flags.type = type;
129 n->flags.wasExpanded = 0;
130 n->flags.cnfVisitedDown = 0;
131 n->flags.cnfVisitedUp = 0;
132 n->flags.varForced = 0;
133 n->numEdges = numEdges;
134 n->hashCode = hashcode;
135 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
136 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
140 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
141 if (cnf->size > cnf->maxsize) {
142 resizeCNF(cnf, cnf->capacity << 1);
144 uint hashvalue = hashNode(type, numEdges, edges);
145 uint mask = cnf->mask;
146 uint index = hashvalue & mask;
148 for (;; index = (index + 1) & mask) {
149 n_ptr = &cnf->node_array[index];
150 if (*n_ptr != NULL) {
151 if ((*n_ptr)->hashCode == hashvalue) {
152 if (compareNodes(*n_ptr, type, numEdges, edges)) {
161 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
167 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
171 for (uint i = 0; i < numEdges; i++) {
172 uint c = (uint) ((uintptr_t) edges[i].node_ptr);
183 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
184 if (node->flags.type != type || node->numEdges != numEdges)
186 Edge *nodeedges = node->edges;
187 for (uint i = 0; i < numEdges; i++) {
188 if (!equalsEdge(nodeedges[i], edges[i]))
194 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
195 Edge edgearray[numEdges];
197 for (uint i = 0; i < numEdges; i++) {
198 edgearray[i] = constraintNegate(edges[i]);
200 Edge eand = constraintAND(cnf, numEdges, edgearray);
201 return constraintNegate(eand);
204 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
205 Edge lneg = constraintNegate(left);
206 Edge rneg = constraintNegate(right);
207 Edge eand = constraintAND2(cnf, lneg, rneg);
208 return constraintNegate(eand);
211 int comparefunction(const Edge *e1, const Edge *e2) {
212 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
215 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
216 ASSERT(numEdges != 0);
217 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
219 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
222 uint remainSize = numEdges - initindex;
226 else if (remainSize == 1)
227 return edges[initindex];
228 else if (equalsEdge(edges[initindex], E_False))
231 /** De-duplicate array */
233 edges[lowindex] = edges[initindex++];
235 for (; initindex < numEdges; initindex++) {
236 Edge e1 = edges[lowindex];
237 Edge e2 = edges[initindex];
238 if (sameNodeVarEdge(e1, e2)) {
239 if (!sameSignEdge(e1, e2)) {
243 edges[++lowindex] = edges[initindex];
245 lowindex++; //Make lowindex look like size
250 if (cnf->enableMatching && lowindex == 2 &&
251 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
252 getNodeType(edges[0]) == NodeType_AND &&
253 getNodeType(edges[1]) == NodeType_AND &&
254 getNodeSize(edges[0]) == 2 &&
255 getNodeSize(edges[1]) == 2) {
256 Edge *e0edges = getEdgeArray(edges[0]);
257 Edge *e1edges = getEdgeArray(edges[1]);
258 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
259 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
260 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
261 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
262 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
263 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
264 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
265 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
269 return createNode(cnf, NodeType_AND, lowindex, edges);
272 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
273 Edge edges[2] = {left, right};
274 return constraintAND(cnf, 2, edges);
277 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
280 array[1] = constraintNegate(right);
281 Edge eand = constraintAND(cnf, 2, array);
282 return constraintNegate(eand);
285 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
286 bool negate = !sameSignEdge(left, right);
287 Edge lpos = getNonNeg(left);
288 Edge rpos = getNonNeg(right);
291 if (equalsEdge(lpos, rpos)) {
293 } else if (ltEdge(lpos, rpos)) {
294 Edge edges[] = {lpos, rpos};
295 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
297 Edge edges[] = {rpos, lpos};
298 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
301 e = constraintNegate(e);
305 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
306 if (isNegEdge(cond)) {
307 cond = constraintNegate(cond);
313 bool negate = isNegEdge(thenedge);
315 thenedge = constraintNegate(thenedge);
316 elseedge = constraintNegate(elseedge);
320 if (equalsEdge(cond, E_True)) {
322 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
323 Edge array[] = {cond, elseedge};
324 result = constraintOR(cnf, 2, array);
325 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
326 result = constraintIMPLIES(cnf, cond, thenedge);
327 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
328 Edge array[] = {cond, thenedge};
329 result = constraintAND(cnf, 2, array);
330 } else if (equalsEdge(thenedge, elseedge)) {
332 } else if (sameNodeOppSign(thenedge, elseedge)) {
333 if (ltEdge(cond, thenedge)) {
334 Edge array[] = {cond, thenedge};
335 result = createNode(cnf, NodeType_IFF, 2, array);
337 Edge array[] = {thenedge, cond};
338 result = createNode(cnf, NodeType_IFF, 2, array);
341 Edge edges[] = {cond, thenedge, elseedge};
342 result = createNode(cnf, NodeType_ITE, 3, edges);
345 result = constraintNegate(result);
349 void addConstraintCNF(CNF *cnf, Edge constraint) {
350 pushVectorEdge(&cnf->constraints, constraint);
352 model_print("****SATC_ADDING NEW Constraint*****\n");
353 printCNF(constraint);
354 model_print("\n******************************\n");
358 Edge constraintNewVar(CNF *cnf) {
359 uint varnum = cnf->varcount++;
360 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
364 int solveCNF(CNF *cnf) {
365 long long startTime = getTimeNano();
367 convertPass(cnf, false);
368 finishedClauses(cnf->solver);
369 long long startSolve = getTimeNano();
370 int result = solve(cnf->solver);
371 long long finishTime = getTimeNano();
372 cnf->encodeTime = startSolve - startTime;
373 model_print("CNF Encode time: %f\n", cnf->encodeTime/1000000000.0);
374 cnf->solveTime = finishTime - startSolve;
375 model_print("Solve time: %f\n", cnf->solveTime/ 1000000000.0);
379 bool getValueCNF(CNF *cnf, Edge var) {
380 Literal l = getEdgeVar(var);
381 bool isneg = (l < 0);
383 return isneg ^ getValueSolver(cnf->solver, l);
386 void countPass(CNF *cnf) {
387 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
388 VectorEdge *ve = allocDefVectorEdge();
389 for (uint i = 0; i < numConstraints; i++) {
390 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
392 deleteVectorEdge(ve);
395 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
396 //Skip constants and variables...
397 if (edgeIsVarConst(eroot))
400 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
402 bool isMatching = cnf->enableMatching;
404 while (getSizeVectorEdge(stack) != 0) {
405 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
406 bool polarity = isNegEdge(e);
407 Node *n = getNodePtrFromEdge(e);
408 if (getExpanded(n, polarity)) {
409 if (n->flags.type == NodeType_IFF ||
410 n->flags.type == NodeType_ITE) {
411 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
412 getNodePtrFromEdge(pExp)->intAnnot[0]++;
414 n->intAnnot[polarity]++;
417 setExpanded(n, polarity);
419 if (n->flags.type == NodeType_ITE ||
420 n->flags.type == NodeType_IFF) {
421 n->intAnnot[polarity] = 0;
422 Edge cond = n->edges[0];
423 Edge thenedge = n->edges[1];
424 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
425 thenedge = constraintNegateIf(thenedge, !polarity);
426 elseedge = constraintNegateIf(elseedge, !polarity);
427 thenedge = constraintAND2(cnf, cond, thenedge);
428 cond = constraintNegate(cond);
429 elseedge = constraintAND2(cnf, cond, elseedge);
430 thenedge = constraintNegate(thenedge);
431 elseedge = constraintNegate(elseedge);
432 cnf->enableMatching = false;
433 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
434 n->ptrAnnot[polarity] = succ1.node_ptr;
435 cnf->enableMatching = isMatching;
436 pushVectorEdge(stack, succ1);
437 if (getExpanded(n, !polarity)) {
438 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
439 Node *n1 = getNodePtrFromEdge(succ1);
440 Node *n2 = getNodePtrFromEdge(succ2);
441 n1->ptrAnnot[0] = succ2.node_ptr;
442 n2->ptrAnnot[0] = succ1.node_ptr;
443 n1->ptrAnnot[1] = succ2.node_ptr;
444 n2->ptrAnnot[1] = succ1.node_ptr;
447 n->intAnnot[polarity] = 1;
448 for (uint i = 0; i < n->numEdges; i++) {
449 Edge succ = n->edges[i];
450 if (!edgeIsVarConst(succ)) {
451 succ = constraintNegateIf(succ, polarity);
452 pushVectorEdge(stack, succ);
460 void convertPass(CNF *cnf, bool backtrackLit) {
461 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
462 VectorEdge *ve = allocDefVectorEdge();
463 for (uint i = 0; i < numConstraints; i++) {
464 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
466 deleteVectorEdge(ve);
469 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
470 Node *nroot = getNodePtrFromEdge(root);
472 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
473 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
474 root = (Edge) { nroot };
476 if (edgeIsConst(root)) {
477 if (isNegEdge(root)) {
479 Edge newvar = constraintNewVar(cnf);
480 Literal var = getEdgeVar(newvar);
481 Literal clause[] = {var};
482 addArrayClauseLiteral(cnf->solver, 1, clause);
484 addArrayClauseLiteral(cnf->solver, 1, clause);
490 } else if (edgeIsVarConst(root)) {
491 Literal clause[] = { getEdgeVar(root)};
492 addArrayClauseLiteral(cnf->solver, 1, clause);
496 clearVectorEdge(stack);pushVectorEdge(stack, root);
497 while (getSizeVectorEdge(stack) != 0) {
498 Edge e = lastVectorEdge(stack);
499 Node *n = getNodePtrFromEdge(e);
501 if (edgeIsVarConst(e)) {
502 popVectorEdge(stack);
504 } else if (n->flags.type == NodeType_ITE ||
505 n->flags.type == NodeType_IFF) {
506 popVectorEdge(stack);
507 if (n->ptrAnnot[0] != NULL)
508 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
509 if (n->ptrAnnot[1] != NULL)
510 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
514 bool needPos = (n->intAnnot[0] > 0);
515 bool needNeg = (n->intAnnot[1] > 0);
516 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
517 (!needNeg || n->flags.cnfVisitedUp & 2)) {
518 popVectorEdge(stack);
519 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
520 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
522 n->flags.cnfVisitedDown |= 1;
524 n->flags.cnfVisitedDown |= 2;
525 for (uint i = 0; i < n->numEdges; i++) {
526 Edge arg = n->edges[i];
527 arg = constraintNegateIf(arg, isNegEdge(e));
528 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
531 popVectorEdge(stack);
535 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
536 ASSERT(cnfExp != NULL);
537 if (isProxy(cnfExp)) {
538 Literal l = getProxy(cnfExp);
539 Literal clause[] = {l};
540 addArrayClauseLiteral(cnf->solver, 1, clause);
541 } else if (backtrackLit) {
542 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
543 Literal clause[] = {l};
544 addArrayClauseLiteral(cnf->solver, 1, clause);
546 outputCNF(cnf, cnfExp);
549 if (!((intptr_t) cnfExp & 1)) {
550 deleteCNFExpr(cnfExp);
551 nroot->ptrAnnot[isNegEdge(root)] = NULL;
556 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
558 Node *n = getNodePtrFromEdge(e);
560 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
561 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
562 if (isProxy(otherExp))
563 l = -getProxy(otherExp);
565 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
566 Node *nsemNeg = getNodePtrFromEdge(semNeg);
567 if (nsemNeg != NULL) {
568 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
569 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
570 if (isProxy(otherExp))
571 l = -getProxy(otherExp);
572 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
573 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
574 if (isProxy(otherExp))
575 l = getProxy(otherExp);
581 Edge newvar = constraintNewVar(cnf);
582 l = getEdgeVar(newvar);
584 // Output the constraints on the auxiliary variable
585 constrainCNF(cnf, l, exp);
588 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
593 void produceCNF(CNF *cnf, Edge e) {
594 CNFExpr *expPos = NULL;
595 CNFExpr *expNeg = NULL;
596 Node *n = getNodePtrFromEdge(e);
598 if (n->intAnnot[0] > 0) {
599 expPos = produceConjunction(cnf, e);
602 if (n->intAnnot[1] > 0) {
603 expNeg = produceDisjunction(cnf, e);
606 /// @todo Propagate constants across semantic negations (this can
607 /// be done similarly to the calls to propagate shown below). The
608 /// trick here is that we need to figure out how to get the
609 /// semantic negation pointers, and ensure that they can have CNF
610 /// produced for them at the right point
612 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
614 // propagate from positive to negative, negative to positive
615 if (!propagate(cnf, &expPos, expNeg, true))
616 propagate(cnf, &expNeg, expPos, true);
618 // The polarity heuristic entails visiting the discovery polarity first
620 saveCNF(cnf, expPos, e, false);
621 saveCNF(cnf, expNeg, e, true);
623 saveCNF(cnf, expNeg, e, true);
624 saveCNF(cnf, expPos, e, false);
628 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
629 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
631 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
632 } else if (isProxy(*dest)) {
633 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
635 Literal clause[] = {getProxy(*dest)};
636 addArrayClauseLiteral(cnf->solver, 1, clause);
638 Literal clause[] = {-getProxy(*dest)};
639 addArrayClauseLiteral(cnf->solver, 1, clause);
642 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
644 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
651 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
652 Node *n = getNodePtrFromEdge(e);
653 n->flags.cnfVisitedUp |= (1 << sign);
654 if (exp == NULL || isProxy(exp)) return;
656 if (exp->litSize == 1) {
657 Literal l = getLiteralLitVector(&exp->singletons, 0);
659 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
660 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
661 introProxy(cnf, e, exp, sign);
663 n->ptrAnnot[sign] = exp;
667 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
668 if (alwaysTrueCNF(expr)) {
670 } else if (alwaysFalseCNF(expr)) {
671 Literal clause[] = {-lcond};
672 addArrayClauseLiteral(cnf->solver, 1, clause);
676 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
677 Literal l = getLiteralLitVector(&expr->singletons,i);
678 Literal clause[] = {-lcond, l};
679 addArrayClauseLiteral(cnf->solver, 2, clause);
681 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
682 LitVector *lv = getVectorLitVector(&expr->clauses,i);
683 addClauseLiteral(cnf->solver, -lcond);//Add first literal
684 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
688 void outputCNF(CNF *cnf, CNFExpr *expr) {
689 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
690 Literal l = getLiteralLitVector(&expr->singletons,i);
691 Literal clause[] = {l};
692 addArrayClauseLiteral(cnf->solver, 1, clause);
694 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
695 LitVector *lv = getVectorLitVector(&expr->clauses,i);
696 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
700 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
701 clearVectorEdge(&cnf->args);
703 *largestEdge = (Edge) {(Node *) NULL};
704 CNFExpr *largest = NULL;
705 Node *n = getNodePtrFromEdge(e);
708 Edge arg = n->edges[--i];
709 arg = constraintNegateIf(arg, isNeg);
710 Node *narg = getNodePtrFromEdge(arg);
712 if (edgeIsVarConst(arg)) {
713 pushVectorEdge(&cnf->args, arg);
717 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
718 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
721 if (narg->intAnnot[isNegEdge(arg)] == 1) {
722 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
723 if (!isProxy(argExp)) {
724 if (largest == NULL) {
728 } else if (argExp->litSize > largest->litSize) {
729 pushVectorEdge(&cnf->args, *largestEdge);
736 pushVectorEdge(&cnf->args, arg);
739 if (largest != NULL) {
740 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
741 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
747 void printCNF(Edge e) {
748 if (edgeIsVarConst(e)) {
749 Literal l = getEdgeVar(e);
750 model_print ("%d", l);
753 bool isNeg = isNegEdge(e);
754 if (edgeIsConst(e)) {
761 Node *n = getNodePtrFromEdge(e);
763 //Pretty print things that are equivalent to OR's
764 if (getNodeType(e) == NodeType_AND) {
766 for (uint i = 0; i < n->numEdges; i++) {
767 Edge e = n->edges[i];
770 printCNF(constraintNegate(e));
778 switch (getNodeType(e)) {
790 for (uint i = 0; i < n->numEdges; i++) {
791 Edge e = n->edges[i];
799 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
802 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
804 accum = allocCNFExprBool(true);
806 int i = getSizeVectorEdge(&cnf->args);
808 Edge arg = getVectorEdge(&cnf->args, --i);
809 if (edgeIsVarConst(arg)) {
810 conjoinCNFLit(accum, getEdgeVar(arg));
812 Node *narg = getNodePtrFromEdge(arg);
813 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
815 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
816 if (isProxy(argExp)) {// variable has been introduced
817 conjoinCNFLit(accum, getProxy(argExp));
819 conjoinCNFExpr(accum, argExp, destroy);
821 narg->ptrAnnot[isNegEdge(arg)] = NULL;
831 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
833 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
835 accum = allocCNFExprBool(false);
837 // This is necessary to check to make sure that we don't start out
838 // with an accumulator that is "too large".
840 /// @todo Strictly speaking, introProxy doesn't *need* to free
841 /// memory, then this wouldn't have to reallocate CNFExpr
843 /// @todo When this call to introProxy is made, the semantic
844 /// negation pointer will have been destroyed. Thus, it will not
845 /// be possible to use the correct proxy. That should be fixed.
847 // at this point, we will either have NULL, or a destructible expression
848 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
849 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
851 int i = getSizeVectorEdge(&cnf->args);
853 Edge arg = getVectorEdge(&cnf->args, --i);
854 Node *narg = getNodePtrFromEdge(arg);
855 if (edgeIsVarConst(arg)) {
856 disjoinCNFLit(accum, getEdgeVar(arg));
858 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
860 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
861 if (isProxy(argExp)) {// variable has been introduced
862 disjoinCNFLit(accum, getProxy(argExp));
863 } else if (argExp->litSize == 0) {
864 disjoinCNFExpr(accum, argExp, destroy);
866 // check to see if we should introduce a proxy
867 int aL = accum->litSize; // lits in accum
868 int eL = argExp->litSize; // lits in argument
869 int aC = getClauseSizeCNF(accum); // clauses in accum
870 int eC = getClauseSizeCNF(argExp); // clauses in argument
871 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
872 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
873 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
875 disjoinCNFExpr(accum, argExp, destroy);
876 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
885 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
886 Edge carray[numvars];
887 for (uint j = 0; j < numvars; j++) {
888 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
892 return constraintAND(cnf, numvars, carray);
895 /** Generates a constraint to ensure that all encodings are less than value */
896 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
897 Edge orarray[numvars];
898 Edge andarray[numvars];
904 for (uint j = 0; j < numvars; j++) {
906 orarray[ori++] = constraintNegate(vars[j]);
909 //no ones to flip, so bail now...
911 return constraintAND(cnf, andi, andarray);
913 andarray[andi++] = constraintOR(cnf, ori, orarray);
915 value = value + (1 << (__builtin_ctz(value)));
920 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
924 for (uint i = 0; i < numvars; i++) {
925 array[i] = constraintIFF(cnf, var1[i], var2[i]);
927 return constraintAND(cnf, numvars, array);
930 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
933 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
934 for (uint i = 1; i < numvars; i++) {
935 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
936 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
937 result = constraintOR2(cnf, lt, eq);
942 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
945 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
946 for (uint i = 1; i < numvars; i++) {
947 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
948 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
949 result = constraintOR2(cnf, lt, eq);