1 #include "constraint.h"
4 #include "inc_solver.h"
9 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
10 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
12 Permission is hereby granted, free of charge, to any person obtaining
13 a copy of this software and associated documentation files (the
14 "Software"), to deal in the Software without restriction, including
15 without limitation the rights to use, copy, modify, merge, publish,
16 distribute, sublicense, and/or sell copies of the Software, and to
17 permit persons to whom the Software is furnished to do so, subject to
18 the following conditions:
20 The above copyright notice and this permission notice shall be
21 included in all copies or substantial portions of the Software. If
22 you download or use the software, send email to Pete Manolios
23 (pete@ccs.neu.edu) with your name, contact information, and a short
24 note describing what you want to use BAT for. For any reuse or
25 distribution, you must make clear to others the license terms of this
28 Contact Pete Manolios if you want any of these conditions waived.
30 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
40 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
44 VectorImpl(Edge, Edge, 16)
45 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
46 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
47 Edge E_BOGUS = {(Node *)0x12345673};
48 Edge E_NULL = {(Node *)NULL};
52 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
54 cnf->capacity = DEFAULT_CNF_ARRAY_SIZE;
55 cnf->mask = cnf->capacity - 1;
56 cnf->node_array = (Node **) ourcalloc(1, sizeof(Node *) * cnf->capacity);
58 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
59 cnf->enableMatching = true;
60 initDefVectorEdge(&cnf->constraints);
61 initDefVectorEdge(&cnf->args);
62 cnf->solver = allocIncrementalSolver();
68 void deleteCNF(CNF *cnf) {
69 for (uint i = 0; i < cnf->capacity; i++) {
70 Node *n = cnf->node_array[i];
74 deleteVectorArrayEdge(&cnf->constraints);
75 deleteVectorArrayEdge(&cnf->args);
76 deleteIncrementalSolver(cnf->solver);
77 ourfree(cnf->node_array);
81 void resizeCNF(CNF *cnf, uint newCapacity) {
82 Node **old_array = cnf->node_array;
83 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
84 uint oldCapacity = cnf->capacity;
85 uint newMask = newCapacity - 1;
86 for (uint i = 0; i < oldCapacity; i++) {
87 Node *n = old_array[i];
90 uint hashCode = n->hashCode;
91 uint newindex = hashCode & newMask;
92 for (;; newindex = (newindex + 1) & newMask) {
93 if (new_array[newindex] == NULL) {
94 new_array[newindex] = n;
100 cnf->node_array = new_array;
101 cnf->capacity = newCapacity;
102 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
106 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
107 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
108 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
109 n->flags.type = type;
110 n->flags.wasExpanded = 0;
111 n->flags.cnfVisitedDown = 0;
112 n->flags.cnfVisitedUp = 0;
113 n->flags.varForced = 0;
114 n->numEdges = numEdges;
115 n->hashCode = hashcode;
116 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
117 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
121 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
122 if (cnf->size > cnf->maxsize) {
123 resizeCNF(cnf, cnf->capacity << 1);
125 uint hashvalue = hashNode(type, numEdges, edges);
126 uint mask = cnf->mask;
127 uint index = hashvalue & mask;
129 for (;; index = (index + 1) & mask) {
130 n_ptr = &cnf->node_array[index];
131 if (*n_ptr != NULL) {
132 if ((*n_ptr)->hashCode == hashvalue) {
133 if (compareNodes(*n_ptr, type, numEdges, edges)) {
142 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
148 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
152 for (uint i = 0; i < numEdges; i++) {
153 uint c = (uint) ((uintptr_t) edges[i].node_ptr);
164 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
165 if (node->flags.type != type || node->numEdges != numEdges)
167 Edge *nodeedges = node->edges;
168 for (uint i = 0; i < numEdges; i++) {
169 if (!equalsEdge(nodeedges[i], edges[i]))
175 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
176 Edge edgearray[numEdges];
178 for (uint i = 0; i < numEdges; i++) {
179 edgearray[i] = constraintNegate(edges[i]);
181 Edge eand = constraintAND(cnf, numEdges, edgearray);
182 return constraintNegate(eand);
185 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
186 Edge lneg = constraintNegate(left);
187 Edge rneg = constraintNegate(right);
188 Edge eand = constraintAND2(cnf, lneg, rneg);
189 return constraintNegate(eand);
192 int comparefunction(const Edge *e1, const Edge *e2) {
193 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
196 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
197 ASSERT(numEdges != 0);
198 bsdqsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
200 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
203 uint remainSize = numEdges - initindex;
207 else if (remainSize == 1)
208 return edges[initindex];
209 else if (equalsEdge(edges[initindex], E_False))
212 /** De-duplicate array */
214 edges[lowindex] = edges[initindex++];
216 for (; initindex < numEdges; initindex++) {
217 Edge e1 = edges[lowindex];
218 Edge e2 = edges[initindex];
219 if (sameNodeVarEdge(e1, e2)) {
220 if (!sameSignEdge(e1, e2)) {
224 edges[++lowindex] = edges[initindex];
226 lowindex++; //Make lowindex look like size
231 if (cnf->enableMatching && lowindex == 2 &&
232 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
233 getNodeType(edges[0]) == NodeType_AND &&
234 getNodeType(edges[1]) == NodeType_AND &&
235 getNodeSize(edges[0]) == 2 &&
236 getNodeSize(edges[1]) == 2) {
237 Edge *e0edges = getEdgeArray(edges[0]);
238 Edge *e1edges = getEdgeArray(edges[1]);
239 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
240 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
241 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
242 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
243 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
244 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
245 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
246 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
250 return createNode(cnf, NodeType_AND, lowindex, edges);
253 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
254 Edge edges[2] = {left, right};
255 return constraintAND(cnf, 2, edges);
258 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
261 array[1] = constraintNegate(right);
262 Edge eand = constraintAND(cnf, 2, array);
263 return constraintNegate(eand);
266 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
267 bool negate = !sameSignEdge(left, right);
268 Edge lpos = getNonNeg(left);
269 Edge rpos = getNonNeg(right);
272 if (equalsEdge(lpos, rpos)) {
274 } else if (ltEdge(lpos, rpos)) {
275 Edge edges[] = {lpos, rpos};
276 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
278 Edge edges[] = {rpos, lpos};
279 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
282 e = constraintNegate(e);
286 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
287 if (isNegEdge(cond)) {
288 cond = constraintNegate(cond);
294 bool negate = isNegEdge(thenedge);
296 thenedge = constraintNegate(thenedge);
297 elseedge = constraintNegate(elseedge);
301 if (equalsEdge(cond, E_True)) {
303 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
304 Edge array[] = {cond, elseedge};
305 result = constraintOR(cnf, 2, array);
306 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
307 result = constraintIMPLIES(cnf, cond, thenedge);
308 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
309 Edge array[] = {cond, thenedge};
310 result = constraintAND(cnf, 2, array);
311 } else if (equalsEdge(thenedge, elseedge)) {
313 } else if (sameNodeOppSign(thenedge, elseedge)) {
314 if (ltEdge(cond, thenedge)) {
315 Edge array[] = {cond, thenedge};
316 result = createNode(cnf, NodeType_IFF, 2, array);
318 Edge array[] = {thenedge, cond};
319 result = createNode(cnf, NodeType_IFF, 2, array);
322 Edge edges[] = {cond, thenedge, elseedge};
323 result = createNode(cnf, NodeType_ITE, 3, edges);
326 result = constraintNegate(result);
330 void addConstraintCNF(CNF *cnf, Edge constraint) {
331 pushVectorEdge(&cnf->constraints, constraint);
333 model_print("****SATC_ADDING NEW Constraint*****\n");
334 printCNF(constraint);
335 model_print("\n******************************\n");
339 Edge constraintNewVar(CNF *cnf) {
340 uint varnum = cnf->varcount++;
341 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
345 int solveCNF(CNF *cnf) {
346 long long startTime = getTimeNano();
348 convertPass(cnf, false);
349 finishedClauses(cnf->solver);
350 long long startSolve = getTimeNano();
351 int result = solve(cnf->solver);
352 long long finishTime = getTimeNano();
353 cnf->encodeTime = startSolve - startTime;
354 cnf->solveTime = finishTime - startSolve;
358 bool getValueCNF(CNF *cnf, Edge var) {
359 Literal l = getEdgeVar(var);
360 bool isneg = (l < 0);
362 return isneg ^ getValueSolver(cnf->solver, l);
365 void countPass(CNF *cnf) {
366 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
367 VectorEdge *ve = allocDefVectorEdge();
368 for (uint i = 0; i < numConstraints; i++) {
369 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
371 deleteVectorEdge(ve);
374 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
375 //Skip constants and variables...
376 if (edgeIsVarConst(eroot))
379 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
381 bool isMatching = cnf->enableMatching;
383 while (getSizeVectorEdge(stack) != 0) {
384 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
385 bool polarity = isNegEdge(e);
386 Node *n = getNodePtrFromEdge(e);
387 if (getExpanded(n, polarity)) {
388 if (n->flags.type == NodeType_IFF ||
389 n->flags.type == NodeType_ITE) {
390 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
391 getNodePtrFromEdge(pExp)->intAnnot[0]++;
393 n->intAnnot[polarity]++;
396 setExpanded(n, polarity);
398 if (n->flags.type == NodeType_ITE ||
399 n->flags.type == NodeType_IFF) {
400 n->intAnnot[polarity] = 0;
401 Edge cond = n->edges[0];
402 Edge thenedge = n->edges[1];
403 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
404 thenedge = constraintNegateIf(thenedge, !polarity);
405 elseedge = constraintNegateIf(elseedge, !polarity);
406 thenedge = constraintAND2(cnf, cond, thenedge);
407 cond = constraintNegate(cond);
408 elseedge = constraintAND2(cnf, cond, elseedge);
409 thenedge = constraintNegate(thenedge);
410 elseedge = constraintNegate(elseedge);
411 cnf->enableMatching = false;
412 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
413 n->ptrAnnot[polarity] = succ1.node_ptr;
414 cnf->enableMatching = isMatching;
415 pushVectorEdge(stack, succ1);
416 if (getExpanded(n, !polarity)) {
417 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
418 Node *n1 = getNodePtrFromEdge(succ1);
419 Node *n2 = getNodePtrFromEdge(succ2);
420 n1->ptrAnnot[0] = succ2.node_ptr;
421 n2->ptrAnnot[0] = succ1.node_ptr;
422 n1->ptrAnnot[1] = succ2.node_ptr;
423 n2->ptrAnnot[1] = succ1.node_ptr;
426 n->intAnnot[polarity] = 1;
427 for (uint i = 0; i < n->numEdges; i++) {
428 Edge succ = n->edges[i];
429 if (!edgeIsVarConst(succ)) {
430 succ = constraintNegateIf(succ, polarity);
431 pushVectorEdge(stack, succ);
439 void convertPass(CNF *cnf, bool backtrackLit) {
440 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
441 VectorEdge *ve = allocDefVectorEdge();
442 for (uint i = 0; i < numConstraints; i++) {
443 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
445 deleteVectorEdge(ve);
448 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
449 Node *nroot = getNodePtrFromEdge(root);
451 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
452 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
453 root = (Edge) { nroot };
455 if (edgeIsConst(root)) {
456 if (isNegEdge(root)) {
458 Edge newvar = constraintNewVar(cnf);
459 Literal var = getEdgeVar(newvar);
460 Literal clause[] = {var};
461 addArrayClauseLiteral(cnf->solver, 1, clause);
463 addArrayClauseLiteral(cnf->solver, 1, clause);
469 } else if (edgeIsVarConst(root)) {
470 Literal clause[] = { getEdgeVar(root)};
471 addArrayClauseLiteral(cnf->solver, 1, clause);
475 clearVectorEdge(stack);pushVectorEdge(stack, root);
476 while (getSizeVectorEdge(stack) != 0) {
477 Edge e = lastVectorEdge(stack);
478 Node *n = getNodePtrFromEdge(e);
480 if (edgeIsVarConst(e)) {
481 popVectorEdge(stack);
483 } else if (n->flags.type == NodeType_ITE ||
484 n->flags.type == NodeType_IFF) {
485 popVectorEdge(stack);
486 if (n->ptrAnnot[0] != NULL)
487 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
488 if (n->ptrAnnot[1] != NULL)
489 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
493 bool needPos = (n->intAnnot[0] > 0);
494 bool needNeg = (n->intAnnot[1] > 0);
495 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
496 (!needNeg || n->flags.cnfVisitedUp & 2)) {
497 popVectorEdge(stack);
498 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
499 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
501 n->flags.cnfVisitedDown |= 1;
503 n->flags.cnfVisitedDown |= 2;
504 for (uint i = 0; i < n->numEdges; i++) {
505 Edge arg = n->edges[i];
506 arg = constraintNegateIf(arg, isNegEdge(e));
507 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
510 popVectorEdge(stack);
514 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
515 ASSERT(cnfExp != NULL);
516 if (isProxy(cnfExp)) {
517 Literal l = getProxy(cnfExp);
518 Literal clause[] = {l};
519 addArrayClauseLiteral(cnf->solver, 1, clause);
520 } else if (backtrackLit) {
521 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
522 Literal clause[] = {l};
523 addArrayClauseLiteral(cnf->solver, 1, clause);
525 outputCNF(cnf, cnfExp);
528 if (!((intptr_t) cnfExp & 1)) {
529 deleteCNFExpr(cnfExp);
530 nroot->ptrAnnot[isNegEdge(root)] = NULL;
535 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
537 Node *n = getNodePtrFromEdge(e);
539 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
540 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
541 if (isProxy(otherExp))
542 l = -getProxy(otherExp);
544 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
545 Node *nsemNeg = getNodePtrFromEdge(semNeg);
546 if (nsemNeg != NULL) {
547 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
548 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
549 if (isProxy(otherExp))
550 l = -getProxy(otherExp);
551 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
552 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
553 if (isProxy(otherExp))
554 l = getProxy(otherExp);
560 Edge newvar = constraintNewVar(cnf);
561 l = getEdgeVar(newvar);
563 // Output the constraints on the auxiliary variable
564 constrainCNF(cnf, l, exp);
567 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
572 void produceCNF(CNF *cnf, Edge e) {
573 CNFExpr *expPos = NULL;
574 CNFExpr *expNeg = NULL;
575 Node *n = getNodePtrFromEdge(e);
577 if (n->intAnnot[0] > 0) {
578 expPos = produceConjunction(cnf, e);
581 if (n->intAnnot[1] > 0) {
582 expNeg = produceDisjunction(cnf, e);
585 /// @todo Propagate constants across semantic negations (this can
586 /// be done similarly to the calls to propagate shown below). The
587 /// trick here is that we need to figure out how to get the
588 /// semantic negation pointers, and ensure that they can have CNF
589 /// produced for them at the right point
591 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
593 // propagate from positive to negative, negative to positive
594 if (!propagate(cnf, &expPos, expNeg, true))
595 propagate(cnf, &expNeg, expPos, true);
597 // The polarity heuristic entails visiting the discovery polarity first
599 saveCNF(cnf, expPos, e, false);
600 saveCNF(cnf, expNeg, e, true);
602 saveCNF(cnf, expNeg, e, true);
603 saveCNF(cnf, expPos, e, false);
607 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
608 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
610 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
611 } else if (isProxy(*dest)) {
612 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
614 Literal clause[] = {getProxy(*dest)};
615 addArrayClauseLiteral(cnf->solver, 1, clause);
617 Literal clause[] = {-getProxy(*dest)};
618 addArrayClauseLiteral(cnf->solver, 1, clause);
621 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
623 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
630 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
631 Node *n = getNodePtrFromEdge(e);
632 n->flags.cnfVisitedUp |= (1 << sign);
633 if (exp == NULL || isProxy(exp)) return;
635 if (exp->litSize == 1) {
636 Literal l = getLiteralLitVector(&exp->singletons, 0);
638 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
639 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
640 introProxy(cnf, e, exp, sign);
642 n->ptrAnnot[sign] = exp;
646 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
647 if (alwaysTrueCNF(expr)) {
649 } else if (alwaysFalseCNF(expr)) {
650 Literal clause[] = {-lcond};
651 addArrayClauseLiteral(cnf->solver, 1, clause);
655 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
656 Literal l = getLiteralLitVector(&expr->singletons,i);
657 Literal clause[] = {-lcond, l};
658 addArrayClauseLiteral(cnf->solver, 2, clause);
660 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
661 LitVector *lv = getVectorLitVector(&expr->clauses,i);
662 addClauseLiteral(cnf->solver, -lcond);//Add first literal
663 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
667 void outputCNF(CNF *cnf, CNFExpr *expr) {
668 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
669 Literal l = getLiteralLitVector(&expr->singletons,i);
670 Literal clause[] = {l};
671 addArrayClauseLiteral(cnf->solver, 1, clause);
673 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
674 LitVector *lv = getVectorLitVector(&expr->clauses,i);
675 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
679 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
680 clearVectorEdge(&cnf->args);
682 *largestEdge = (Edge) {(Node *) NULL};
683 CNFExpr *largest = NULL;
684 Node *n = getNodePtrFromEdge(e);
687 Edge arg = n->edges[--i];
688 arg = constraintNegateIf(arg, isNeg);
689 Node *narg = getNodePtrFromEdge(arg);
691 if (edgeIsVarConst(arg)) {
692 pushVectorEdge(&cnf->args, arg);
696 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
697 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
700 if (narg->intAnnot[isNegEdge(arg)] == 1) {
701 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
702 if (!isProxy(argExp)) {
703 if (largest == NULL) {
707 } else if (argExp->litSize > largest->litSize) {
708 pushVectorEdge(&cnf->args, *largestEdge);
715 pushVectorEdge(&cnf->args, arg);
718 if (largest != NULL) {
719 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
720 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
726 void printCNF(Edge e) {
727 if (edgeIsVarConst(e)) {
728 Literal l = getEdgeVar(e);
729 model_print ("%d", l);
732 bool isNeg = isNegEdge(e);
733 if (edgeIsConst(e)) {
740 Node *n = getNodePtrFromEdge(e);
742 //Pretty print things that are equivalent to OR's
743 if (getNodeType(e) == NodeType_AND) {
745 for (uint i = 0; i < n->numEdges; i++) {
746 Edge e = n->edges[i];
749 printCNF(constraintNegate(e));
757 switch (getNodeType(e)) {
769 for (uint i = 0; i < n->numEdges; i++) {
770 Edge e = n->edges[i];
778 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
781 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
783 accum = allocCNFExprBool(true);
785 int i = getSizeVectorEdge(&cnf->args);
787 Edge arg = getVectorEdge(&cnf->args, --i);
788 if (edgeIsVarConst(arg)) {
789 conjoinCNFLit(accum, getEdgeVar(arg));
791 Node *narg = getNodePtrFromEdge(arg);
792 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
794 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
795 if (isProxy(argExp)) {// variable has been introduced
796 conjoinCNFLit(accum, getProxy(argExp));
798 conjoinCNFExpr(accum, argExp, destroy);
800 narg->ptrAnnot[isNegEdge(arg)] = NULL;
810 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
812 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
814 accum = allocCNFExprBool(false);
816 // This is necessary to check to make sure that we don't start out
817 // with an accumulator that is "too large".
819 /// @todo Strictly speaking, introProxy doesn't *need* to free
820 /// memory, then this wouldn't have to reallocate CNFExpr
822 /// @todo When this call to introProxy is made, the semantic
823 /// negation pointer will have been destroyed. Thus, it will not
824 /// be possible to use the correct proxy. That should be fixed.
826 // at this point, we will either have NULL, or a destructible expression
827 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
828 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
830 int i = getSizeVectorEdge(&cnf->args);
832 Edge arg = getVectorEdge(&cnf->args, --i);
833 Node *narg = getNodePtrFromEdge(arg);
834 if (edgeIsVarConst(arg)) {
835 disjoinCNFLit(accum, getEdgeVar(arg));
837 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
839 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
840 if (isProxy(argExp)) {// variable has been introduced
841 disjoinCNFLit(accum, getProxy(argExp));
842 } else if (argExp->litSize == 0) {
843 disjoinCNFExpr(accum, argExp, destroy);
845 // check to see if we should introduce a proxy
846 int aL = accum->litSize; // lits in accum
847 int eL = argExp->litSize; // lits in argument
848 int aC = getClauseSizeCNF(accum); // clauses in accum
849 int eC = getClauseSizeCNF(argExp); // clauses in argument
850 //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
851 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
852 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
854 disjoinCNFExpr(accum, argExp, destroy);
855 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
864 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
865 Edge carray[numvars];
866 for (uint j = 0; j < numvars; j++) {
867 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
871 return constraintAND(cnf, numvars, carray);
874 /** Generates a constraint to ensure that all encodings are less than value */
875 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
876 Edge orarray[numvars];
877 Edge andarray[numvars];
883 for (uint j = 0; j < numvars; j++) {
885 orarray[ori++] = constraintNegate(vars[j]);
888 //no ones to flip, so bail now...
890 return constraintAND(cnf, andi, andarray);
892 andarray[andi++] = constraintOR(cnf, ori, orarray);
894 value = value + (1 << (__builtin_ctz(value)));
899 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
903 for (uint i = 0; i < numvars; i++) {
904 array[i] = constraintIFF(cnf, var1[i], var2[i]);
906 return constraintAND(cnf, numvars, array);
909 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
912 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
913 for (uint i = 1; i < numvars; i++) {
914 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
915 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
916 result = constraintOR2(cnf, lt, eq);
921 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
924 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
925 for (uint i = 1; i < numvars; i++) {
926 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
927 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
928 result = constraintOR2(cnf, lt, eq);