1 #include "constraint.h"
4 #include "inc_solver.h"
8 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
9 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
11 Permission is hereby granted, free of charge, to any person obtaining
12 a copy of this software and associated documentation files (the
13 "Software"), to deal in the Software without restriction, including
14 without limitation the rights to use, copy, modify, merge, publish,
15 distribute, sublicense, and/or sell copies of the Software, and to
16 permit persons to whom the Software is furnished to do so, subject to
17 the following conditions:
19 The above copyright notice and this permission notice shall be
20 included in all copies or substantial portions of the Software. If
21 you download or use the software, send email to Pete Manolios
22 (pete@ccs.neu.edu) with your name, contact information, and a short
23 note describing what you want to use BAT for. For any reuse or
24 distribution, you must make clear to others the license terms of this
27 Contact Pete Manolios if you want any of these conditions waived.
29 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
30 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
31 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
32 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
33 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
34 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
35 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
39 C port of CNF SAT Conversion Copyright Brian Demsky 2017.
43 VectorImpl(Edge, Edge, 16)
44 Edge E_True = {(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
45 Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
46 Edge E_BOGUS = {(Node *)0x12345673};
47 Edge E_NULL = {(Node *)NULL};
51 CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
53 cnf->capacity = DEFAULT_CNF_ARRAY_SIZE;
54 cnf->mask = cnf->capacity - 1;
55 cnf->node_array = (Node **) ourcalloc(1, sizeof(Node *) * cnf->capacity);
57 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
58 cnf->enableMatching = true;
59 initDefVectorEdge(&cnf->constraints);
60 initDefVectorEdge(&cnf->args);
61 cnf->solver = allocIncrementalSolver();
65 void deleteCNF(CNF *cnf) {
66 for (uint i = 0; i < cnf->capacity; i++) {
67 Node *n = cnf->node_array[i];
71 deleteVectorArrayEdge(&cnf->constraints);
72 deleteVectorArrayEdge(&cnf->args);
73 deleteIncrementalSolver(cnf->solver);
74 ourfree(cnf->node_array);
78 void resizeCNF(CNF *cnf, uint newCapacity) {
79 Node **old_array = cnf->node_array;
80 Node **new_array = (Node **) ourcalloc(1, sizeof(Node *) * newCapacity);
81 uint oldCapacity = cnf->capacity;
82 uint newMask = newCapacity - 1;
83 for (uint i = 0; i < oldCapacity; i++) {
84 Node *n = old_array[i];
85 uint hashCode = n->hashCode;
86 uint newindex = hashCode & newMask;
87 for (;; newindex = (newindex + 1) & newMask) {
88 if (new_array[newindex] == NULL) {
89 new_array[newindex] = n;
95 cnf->node_array = new_array;
96 cnf->capacity = newCapacity;
97 cnf->maxsize = (uint)(((double)cnf->capacity) * LOAD_FACTOR);
101 Node *allocNode(NodeType type, uint numEdges, Edge *edges, uint hashcode) {
102 Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
103 memcpy(n->edges, edges, sizeof(Edge) * numEdges);
104 n->flags.type = type;
105 n->flags.wasExpanded = 0;
106 n->flags.cnfVisitedDown = 0;
107 n->flags.cnfVisitedUp = 0;
108 n->flags.varForced = 0;
109 n->numEdges = numEdges;
110 n->hashCode = hashcode;
111 n->intAnnot[0] = 0;n->intAnnot[1] = 0;
112 n->ptrAnnot[0] = NULL;n->ptrAnnot[1] = NULL;
116 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge *edges) {
117 if (cnf->size > cnf->maxsize) {
118 resizeCNF(cnf, cnf->capacity << 1);
120 uint hashvalue = hashNode(type, numEdges, edges);
121 uint mask = cnf->mask;
122 uint index = hashvalue & mask;
124 for (;; index = (index + 1) & mask) {
125 n_ptr = &cnf->node_array[index];
126 if (*n_ptr != NULL) {
127 if ((*n_ptr)->hashCode == hashvalue) {
128 if (compareNodes(*n_ptr, type, numEdges, edges)) {
137 *n_ptr = allocNode(type, numEdges, edges, hashvalue);
142 uint hashNode(NodeType type, uint numEdges, Edge *edges) {
143 uint hashvalue = type ^ numEdges;
144 for (uint i = 0; i < numEdges; i++) {
145 hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
146 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
148 return (uint) hashvalue;
151 bool compareNodes(Node *node, NodeType type, uint numEdges, Edge *edges) {
152 if (node->flags.type != type || node->numEdges != numEdges)
154 Edge *nodeedges = node->edges;
155 for (uint i = 0; i < numEdges; i++) {
156 if (!equalsEdge(nodeedges[i], edges[i]))
162 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
163 Edge edgearray[numEdges];
165 for (uint i = 0; i < numEdges; i++) {
166 edgearray[i] = constraintNegate(edges[i]);
168 Edge eand = constraintAND(cnf, numEdges, edgearray);
169 return constraintNegate(eand);
172 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
173 Edge lneg = constraintNegate(left);
174 Edge rneg = constraintNegate(right);
175 Edge eand = constraintAND2(cnf, lneg, rneg);
176 return constraintNegate(eand);
179 int comparefunction(const Edge *e1, const Edge *e2) {
180 return ((uintptr_t)e1->node_ptr) - ((uintptr_t)e2->node_ptr);
183 Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
184 ASSERT(numEdges != 0);
185 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *))comparefunction);
187 while (initindex < numEdges && equalsEdge(edges[initindex], E_True))
190 uint remainSize = numEdges - initindex;
194 else if (remainSize == 1)
195 return edges[initindex];
196 else if (equalsEdge(edges[initindex], E_False))
199 /** De-duplicate array */
201 edges[lowindex] = edges[initindex++];
203 for (; initindex < numEdges; initindex++) {
204 Edge e1 = edges[lowindex];
205 Edge e2 = edges[initindex];
206 if (sameNodeVarEdge(e1, e2)) {
207 if (!sameSignEdge(e1, e2)) {
211 edges[++lowindex] = edges[initindex];
213 lowindex++; //Make lowindex look like size
218 if (cnf->enableMatching && lowindex == 2 &&
219 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
220 getNodeType(edges[0]) == NodeType_AND &&
221 getNodeType(edges[1]) == NodeType_AND &&
222 getNodeSize(edges[0]) == 2 &&
223 getNodeSize(edges[1]) == 2) {
224 Edge *e0edges = getEdgeArray(edges[0]);
225 Edge *e1edges = getEdgeArray(edges[1]);
226 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
227 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
228 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
229 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
230 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
231 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
232 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
233 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
237 return createNode(cnf, NodeType_AND, lowindex, edges);
240 Edge constraintAND2(CNF *cnf, Edge left, Edge right) {
241 Edge edges[2] = {left, right};
242 return constraintAND(cnf, 2, edges);
245 Edge constraintIMPLIES(CNF *cnf, Edge left, Edge right) {
248 array[1] = constraintNegate(right);
249 Edge eand = constraintAND(cnf, 2, array);
250 return constraintNegate(eand);
253 Edge constraintIFF(CNF *cnf, Edge left, Edge right) {
254 bool negate = !sameSignEdge(left, right);
255 Edge lpos = getNonNeg(left);
256 Edge rpos = getNonNeg(right);
259 if (equalsEdge(lpos, rpos)) {
261 } else if (ltEdge(lpos, rpos)) {
262 Edge edges[] = {lpos, rpos};
263 e = (edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
265 Edge edges[] = {rpos, lpos};
266 e = (edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
269 e = constraintNegate(e);
273 Edge constraintITE(CNF *cnf, Edge cond, Edge thenedge, Edge elseedge) {
274 if (isNegEdge(cond)) {
275 cond = constraintNegate(cond);
281 bool negate = isNegEdge(thenedge);
283 thenedge = constraintNegate(thenedge);
284 elseedge = constraintNegate(elseedge);
288 if (equalsEdge(cond, E_True)) {
290 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
291 Edge array[] = {cond, elseedge};
292 result = constraintOR(cnf, 2, array);
293 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
294 result = constraintIMPLIES(cnf, cond, thenedge);
295 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
296 Edge array[] = {cond, thenedge};
297 result = constraintAND(cnf, 2, array);
298 } else if (equalsEdge(thenedge, elseedge)) {
300 } else if (sameNodeOppSign(thenedge, elseedge)) {
301 if (ltEdge(cond, thenedge)) {
302 Edge array[] = {cond, thenedge};
303 result = createNode(cnf, NodeType_IFF, 2, array);
305 Edge array[] = {thenedge, cond};
306 result = createNode(cnf, NodeType_IFF, 2, array);
309 Edge edges[] = {cond, thenedge, elseedge};
310 result = createNode(cnf, NodeType_ITE, 3, edges);
313 result = constraintNegate(result);
317 void addConstraintCNF(CNF *cnf, Edge constraint) {
318 pushVectorEdge(&cnf->constraints, constraint);
319 model_print("****ADDING NEW Constraint*****\n");
320 printCNF(constraint);
321 model_print("\n******************************\n");
324 Edge constraintNewVar(CNF *cnf) {
325 uint varnum = cnf->varcount++;
326 Edge e = {(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
330 int solveCNF(CNF *cnf) {
332 convertPass(cnf, false);
333 finishedClauses(cnf->solver);
334 return solve(cnf->solver);
337 bool getValueCNF(CNF *cnf, Edge var) {
338 Literal l = getEdgeVar(var);
339 bool isneg = (l < 0);
341 return isneg ^ getValueSolver(cnf->solver, l);
344 void countPass(CNF *cnf) {
345 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
346 VectorEdge *ve = allocDefVectorEdge();
347 for (uint i = 0; i < numConstraints; i++) {
348 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
350 deleteVectorEdge(ve);
353 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
354 //Skip constants and variables...
355 if (edgeIsVarConst(eroot))
358 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
360 bool isMatching = cnf->enableMatching;
362 while (getSizeVectorEdge(stack) != 0) {
363 Edge e = lastVectorEdge(stack); popVectorEdge(stack);
364 bool polarity = isNegEdge(e);
365 Node *n = getNodePtrFromEdge(e);
366 if (getExpanded(n, polarity)) {
367 if (n->flags.type == NodeType_IFF ||
368 n->flags.type == NodeType_ITE) {
369 Edge pExp = {(Node *)n->ptrAnnot[polarity]};
370 getNodePtrFromEdge(pExp)->intAnnot[0]++;
372 n->intAnnot[polarity]++;
375 setExpanded(n, polarity);
377 if (n->flags.type == NodeType_ITE ||
378 n->flags.type == NodeType_IFF) {
379 n->intAnnot[polarity] = 0;
380 Edge cond = n->edges[0];
381 Edge thenedge = n->edges[1];
382 Edge elseedge = n->flags.type == NodeType_IFF ? constraintNegate(thenedge) : n->edges[2];
383 thenedge = constraintNegateIf(thenedge, !polarity);
384 elseedge = constraintNegateIf(elseedge, !polarity);
385 thenedge = constraintAND2(cnf, cond, thenedge);
386 cond = constraintNegate(cond);
387 elseedge = constraintAND2(cnf, cond, elseedge);
388 thenedge = constraintNegate(thenedge);
389 elseedge = constraintNegate(elseedge);
390 cnf->enableMatching = false;
391 Edge succ1 = constraintAND2(cnf, thenedge, elseedge);
392 n->ptrAnnot[polarity] = succ1.node_ptr;
393 cnf->enableMatching = isMatching;
394 pushVectorEdge(stack, succ1);
395 if (getExpanded(n, !polarity)) {
396 Edge succ2 = {(Node *)n->ptrAnnot[!polarity]};
397 Node *n1 = getNodePtrFromEdge(succ1);
398 Node *n2 = getNodePtrFromEdge(succ2);
399 n1->ptrAnnot[0] = succ2.node_ptr;
400 n2->ptrAnnot[0] = succ1.node_ptr;
401 n1->ptrAnnot[1] = succ2.node_ptr;
402 n2->ptrAnnot[1] = succ1.node_ptr;
405 n->intAnnot[polarity] = 1;
406 for (uint i = 0; i < n->numEdges; i++) {
407 Edge succ = n->edges[i];
408 if (!edgeIsVarConst(succ)) {
409 succ = constraintNegateIf(succ, polarity);
410 pushVectorEdge(stack, succ);
418 void convertPass(CNF *cnf, bool backtrackLit) {
419 uint numConstraints = getSizeVectorEdge(&cnf->constraints);
420 VectorEdge *ve = allocDefVectorEdge();
421 for (uint i = 0; i < numConstraints; i++) {
422 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
424 deleteVectorEdge(ve);
427 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
428 Node *nroot = getNodePtrFromEdge(root);
430 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
431 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
432 root = (Edge) { nroot };
434 if (edgeIsConst(root)) {
435 if (isNegEdge(root)) {
437 Edge newvar = constraintNewVar(cnf);
438 Literal var = getEdgeVar(newvar);
439 Literal clause[] = {var};
440 addArrayClauseLiteral(cnf->solver, 1, clause);
442 addArrayClauseLiteral(cnf->solver, 1, clause);
448 } else if (edgeIsVarConst(root)) {
449 Literal clause[] = { getEdgeVar(root)};
450 addArrayClauseLiteral(cnf->solver, 1, clause);
454 clearVectorEdge(stack);pushVectorEdge(stack, root);
455 while (getSizeVectorEdge(stack) != 0) {
456 Edge e = lastVectorEdge(stack);
457 Node *n = getNodePtrFromEdge(e);
459 if (edgeIsVarConst(e)) {
460 popVectorEdge(stack);
462 } else if (n->flags.type == NodeType_ITE ||
463 n->flags.type == NodeType_IFF) {
464 popVectorEdge(stack);
465 if (n->ptrAnnot[0] != NULL)
466 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
467 if (n->ptrAnnot[1] != NULL)
468 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
472 bool needPos = (n->intAnnot[0] > 0);
473 bool needNeg = (n->intAnnot[1] > 0);
474 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
475 (!needNeg || n->flags.cnfVisitedUp & 2)) {
476 popVectorEdge(stack);
477 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
478 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
480 n->flags.cnfVisitedDown |= 1;
482 n->flags.cnfVisitedDown |= 2;
483 for (uint i = 0; i < n->numEdges; i++) {
484 Edge arg = n->edges[i];
485 arg = constraintNegateIf(arg, isNegEdge(e));
486 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
489 popVectorEdge(stack);
493 CNFExpr *cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
494 ASSERT(cnfExp != NULL);
495 if (isProxy(cnfExp)) {
496 Literal l = getProxy(cnfExp);
497 Literal clause[] = {l};
498 addArrayClauseLiteral(cnf->solver, 1, clause);
499 } else if (backtrackLit) {
500 Literal l = introProxy(cnf, root, cnfExp, isNegEdge(root));
501 Literal clause[] = {l};
502 addArrayClauseLiteral(cnf->solver, 1, clause);
504 outputCNF(cnf, cnfExp);
507 if (!((intptr_t) cnfExp & 1)) {
508 deleteCNFExpr(cnfExp);
509 nroot->ptrAnnot[isNegEdge(root)] = NULL;
514 Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg) {
516 Node *n = getNodePtrFromEdge(e);
518 if (n->flags.cnfVisitedUp & (1 << !isNeg)) {
519 CNFExpr *otherExp = (CNFExpr *) n->ptrAnnot[!isNeg];
520 if (isProxy(otherExp))
521 l = -getProxy(otherExp);
523 Edge semNeg = {(Node *) n->ptrAnnot[isNeg]};
524 Node *nsemNeg = getNodePtrFromEdge(semNeg);
525 if (nsemNeg != NULL) {
526 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
527 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[isNeg];
528 if (isProxy(otherExp))
529 l = -getProxy(otherExp);
530 } else if (nsemNeg->flags.cnfVisitedUp & (1 << !isNeg)) {
531 CNFExpr *otherExp = (CNFExpr *) nsemNeg->ptrAnnot[!isNeg];
532 if (isProxy(otherExp))
533 l = getProxy(otherExp);
539 Edge newvar = constraintNewVar(cnf);
540 l = getEdgeVar(newvar);
542 // Output the constraints on the auxiliary variable
543 constrainCNF(cnf, l, exp);
546 n->ptrAnnot[isNeg] = (void *) ((intptr_t) (l << 1) | 1);
551 void produceCNF(CNF *cnf, Edge e) {
552 CNFExpr *expPos = NULL;
553 CNFExpr *expNeg = NULL;
554 Node *n = getNodePtrFromEdge(e);
556 if (n->intAnnot[0] > 0) {
557 expPos = produceConjunction(cnf, e);
560 if (n->intAnnot[1] > 0) {
561 expNeg = produceDisjunction(cnf, e);
564 /// @todo Propagate constants across semantic negations (this can
565 /// be done similarly to the calls to propagate shown below). The
566 /// trick here is that we need to figure out how to get the
567 /// semantic negation pointers, and ensure that they can have CNF
568 /// produced for them at the right point
570 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
572 // propagate from positive to negative, negative to positive
573 if (!propagate(cnf, &expPos, expNeg, true))
574 propagate(cnf, &expNeg, expPos, true);
576 // The polarity heuristic entails visiting the discovery polarity first
578 saveCNF(cnf, expPos, e, false);
579 saveCNF(cnf, expNeg, e, true);
581 saveCNF(cnf, expNeg, e, true);
582 saveCNF(cnf, expPos, e, false);
586 bool propagate(CNF *cnf, CNFExpr **dest, CNFExpr *src, bool negate) {
587 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
589 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
590 } else if (isProxy(*dest)) {
591 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
593 Literal clause[] = {getProxy(*dest)};
594 addArrayClauseLiteral(cnf->solver, 1, clause);
596 Literal clause[] = {-getProxy(*dest)};
597 addArrayClauseLiteral(cnf->solver, 1, clause);
600 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
602 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
609 void saveCNF(CNF *cnf, CNFExpr *exp, Edge e, bool sign) {
610 Node *n = getNodePtrFromEdge(e);
611 n->flags.cnfVisitedUp |= (1 << sign);
612 if (exp == NULL || isProxy(exp)) return;
614 if (exp->litSize == 1) {
615 Literal l = getLiteralLitVector(&exp->singletons, 0);
617 n->ptrAnnot[sign] = (void *) ((((intptr_t) l) << 1) | 1);
618 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
619 introProxy(cnf, e, exp, sign);
621 n->ptrAnnot[sign] = exp;
625 void constrainCNF(CNF *cnf, Literal lcond, CNFExpr *expr) {
626 if (alwaysTrueCNF(expr)) {
628 } else if (alwaysFalseCNF(expr)) {
629 Literal clause[] = {-lcond};
630 addArrayClauseLiteral(cnf->solver, 1, clause);
634 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
635 Literal l = getLiteralLitVector(&expr->singletons,i);
636 Literal clause[] = {-lcond, l};
637 addArrayClauseLiteral(cnf->solver, 2, clause);
639 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
640 LitVector *lv = getVectorLitVector(&expr->clauses,i);
641 addClauseLiteral(cnf->solver, -lcond);//Add first literal
642 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
646 void outputCNF(CNF *cnf, CNFExpr *expr) {
647 for (uint i = 0; i < getSizeLitVector(&expr->singletons); i++) {
648 Literal l = getLiteralLitVector(&expr->singletons,i);
649 Literal clause[] = {l};
650 addArrayClauseLiteral(cnf->solver, 1, clause);
652 for (uint i = 0; i < getSizeVectorLitVector(&expr->clauses); i++) {
653 LitVector *lv = getVectorLitVector(&expr->clauses,i);
654 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
658 CNFExpr *fillArgs(CNF *cnf, Edge e, bool isNeg, Edge *largestEdge) {
659 clearVectorEdge(&cnf->args);
661 *largestEdge = (Edge) {(Node *) NULL};
662 CNFExpr *largest = NULL;
663 Node *n = getNodePtrFromEdge(e);
666 Edge arg = n->edges[--i];
667 arg = constraintNegateIf(arg, isNeg);
668 Node *narg = getNodePtrFromEdge(arg);
670 if (edgeIsVarConst(arg)) {
671 pushVectorEdge(&cnf->args, arg);
675 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
676 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
679 if (narg->intAnnot[isNegEdge(arg)] == 1) {
680 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
681 if (!isProxy(argExp)) {
682 if (largest == NULL) {
686 } else if (argExp->litSize > largest->litSize) {
687 pushVectorEdge(&cnf->args, *largestEdge);
694 pushVectorEdge(&cnf->args, arg);
697 if (largest != NULL) {
698 Node *nlargestEdge = getNodePtrFromEdge(*largestEdge);
699 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
705 void printCNF(Edge e) {
706 if (edgeIsVarConst(e)) {
707 Literal l = getEdgeVar(e);
708 model_print ("%d", l);
711 bool isNeg = isNegEdge(e);
712 if (edgeIsConst(e)) {
719 Node *n = getNodePtrFromEdge(e);
721 //Pretty print things that are equivalent to OR's
722 if (getNodeType(e) == NodeType_AND) {
724 for (uint i = 0; i < n->numEdges; i++) {
725 Edge e = n->edges[i];
728 printCNF(constraintNegate(e));
736 switch (getNodeType(e)) {
748 for (uint i = 0; i < n->numEdges; i++) {
749 Edge e = n->edges[i];
757 CNFExpr *produceConjunction(CNF *cnf, Edge e) {
760 CNFExpr *accum = fillArgs(cnf, e, false, &largestEdge);
762 accum = allocCNFExprBool(true);
764 int i = getSizeVectorEdge(&cnf->args);
766 Edge arg = getVectorEdge(&cnf->args, --i);
767 if (edgeIsVarConst(arg)) {
768 conjoinCNFLit(accum, getEdgeVar(arg));
770 Node *narg = getNodePtrFromEdge(arg);
771 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
773 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
774 if (isProxy(argExp)) {// variable has been introduced
775 conjoinCNFLit(accum, getProxy(argExp));
777 conjoinCNFExpr(accum, argExp, destroy);
779 narg->ptrAnnot[isNegEdge(arg)] = NULL;
789 CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
791 CNFExpr *accum = fillArgs(cnf, e, true, &largestEdge);
793 accum = allocCNFExprBool(false);
795 // This is necessary to check to make sure that we don't start out
796 // with an accumulator that is "too large".
798 /// @todo Strictly speaking, introProxy doesn't *need* to free
799 /// memory, then this wouldn't have to reallocate CNFExpr
801 /// @todo When this call to introProxy is made, the semantic
802 /// negation pointer will have been destroyed. Thus, it will not
803 /// be possible to use the correct proxy. That should be fixed.
805 // at this point, we will either have NULL, or a destructible expression
806 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
807 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
809 int i = getSizeVectorEdge(&cnf->args);
811 Edge arg = getVectorEdge(&cnf->args, --i);
812 Node *narg = getNodePtrFromEdge(arg);
813 if (edgeIsVarConst(arg)) {
814 disjoinCNFLit(accum, getEdgeVar(arg));
816 CNFExpr *argExp = (CNFExpr *) narg->ptrAnnot[isNegEdge(arg)];
818 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
819 if (isProxy(argExp)) {// variable has been introduced
820 disjoinCNFLit(accum, getProxy(argExp));
821 } else if (argExp->litSize == 0) {
822 disjoinCNFExpr(accum, argExp, destroy);
824 // check to see if we should introduce a proxy
825 int aL = accum->litSize; // lits in accum
826 int eL = argExp->litSize; // lits in argument
827 int aC = getClauseSizeCNF(accum); // clauses in accum
828 int eC = getClauseSizeCNF(argExp); // clauses in argument
830 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
831 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
833 disjoinCNFExpr(accum, argExp, destroy);
834 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
843 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
844 Edge carray[numvars];
845 for (uint j = 0; j < numvars; j++) {
846 carray[j] = ((value & 1) == 1) ? vars[j] : constraintNegate(vars[j]);
850 return constraintAND(cnf, numvars, carray);
853 /** Generates a constraint to ensure that all encodings are less than value */
854 Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
855 Edge orarray[numvars];
856 Edge andarray[numvars];
862 for (uint j = 0; j < numvars; j++) {
864 orarray[ori++] = constraintNegate(vars[j]);
867 //no ones to flip, so bail now...
869 return constraintAND(cnf, andi, andarray);
871 andarray[andi++] = constraintOR(cnf, ori, orarray);
873 value = value + (1 << (__builtin_ctz(value)));
878 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
882 for (uint i = 0; i < numvars; i++) {
883 array[i] = constraintIFF(cnf, var1[i], var2[i]);
885 return constraintAND(cnf, numvars, array);
888 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
891 Edge result = constraintAND2(cnf, constraintNegate( var1[0]), var2[0]);
892 for (uint i = 1; i < numvars; i++) {
893 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
894 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
895 result = constraintOR2(cnf, lt, eq);
900 Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
903 Edge result = constraintIMPLIES(cnf, var1[0], var2[0]);
904 for (uint i = 1; i < numvars; i++) {
905 Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]);
906 Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result);
907 result = constraintOR2(cnf, lt, eq);