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=ourmalloc(sizeof(CNF));
53 cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
54 cnf->mask=cnf->capacity-1;
55 cnf->node_array=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=ourcalloc(1, sizeof(Node *)*newCapacity);
81 uint oldCapacity=cnf->capacity;
82 uint newMask=newCapacity-1;
83 for(uint i=0;i<oldCapacity;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);
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);
122 uint index=hashvalue & mask;
124 for(;;index=(index+1)&mask) {
125 n_ptr=&cnf->node_array[index];
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) {
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 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
292 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
293 result=constraintIMPLIES(cnf, cond, thenedge);
294 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
295 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
296 } else if (equalsEdge(thenedge, elseedge)) {
298 } else if (sameNodeOppSign(thenedge, elseedge)) {
299 if (ltEdge(cond, thenedge)) {
300 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
302 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
305 Edge edges[]={cond, thenedge, elseedge};
306 result=createNode(cnf, NodeType_ITE, 3, edges);
309 result=constraintNegate(result);
313 void addConstraintCNF(CNF *cnf, Edge constraint) {
314 pushVectorEdge(&cnf->constraints, constraint);
315 model_print("****ADDING NEW Constraint*****\n");
316 printCNF(constraint);
317 model_print("\n******************************\n");
320 Edge constraintNewVar(CNF *cnf) {
321 uint varnum=cnf->varcount++;
322 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
326 int solveCNF(CNF *cnf) {
328 convertPass(cnf, false);
329 finishedClauses(cnf->solver);
330 return solve(cnf->solver);
333 bool getValueCNF(CNF *cnf, Edge var) {
334 Literal l=getEdgeVar(var);
337 return isneg ^ getValueSolver(cnf->solver, l);
340 void countPass(CNF *cnf) {
341 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
342 VectorEdge *ve=allocDefVectorEdge();
343 for(uint i=0; i<numConstraints;i++) {
344 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
346 deleteVectorEdge(ve);
349 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
350 //Skip constants and variables...
351 if (edgeIsVarConst(eroot))
354 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
356 bool isMatching=cnf->enableMatching;
358 while(getSizeVectorEdge(stack) != 0) {
359 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
360 bool polarity=isNegEdge(e);
361 Node *n=getNodePtrFromEdge(e);
362 if (getExpanded(n, polarity)) {
363 if (n->flags.type == NodeType_IFF ||
364 n->flags.type == NodeType_ITE) {
365 Edge pExp={n->ptrAnnot[polarity]};
366 getNodePtrFromEdge(pExp)->intAnnot[0]++;
368 n->intAnnot[polarity]++;
371 setExpanded(n, polarity);
373 if (n->flags.type == NodeType_ITE||
374 n->flags.type == NodeType_IFF) {
375 n->intAnnot[polarity]=0;
376 Edge cond=n->edges[0];
377 Edge thenedge=n->edges[1];
378 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
379 thenedge=constraintNegateIf(thenedge, !polarity);
380 elseedge=constraintNegateIf(elseedge, !polarity);
381 thenedge=constraintAND2(cnf, cond, thenedge);
382 cond=constraintNegate(cond);
383 elseedge=constraintAND2(cnf, cond, elseedge);
384 thenedge=constraintNegate(thenedge);
385 elseedge=constraintNegate(elseedge);
386 cnf->enableMatching=false;
387 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
388 n->ptrAnnot[polarity]=succ1.node_ptr;
389 cnf->enableMatching=isMatching;
390 pushVectorEdge(stack, succ1);
391 if (getExpanded(n, !polarity)) {
392 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
393 Node *n1=getNodePtrFromEdge(succ1);
394 Node *n2=getNodePtrFromEdge(succ2);
395 n1->ptrAnnot[0]=succ2.node_ptr;
396 n2->ptrAnnot[0]=succ1.node_ptr;
397 n1->ptrAnnot[1]=succ2.node_ptr;
398 n2->ptrAnnot[1]=succ1.node_ptr;
401 n->intAnnot[polarity]=1;
402 for (uint i=0;i<n->numEdges;i++) {
403 Edge succ=n->edges[i];
404 if(!edgeIsVarConst(succ)) {
405 succ=constraintNegateIf(succ, polarity);
406 pushVectorEdge(stack, succ);
414 void convertPass(CNF *cnf, bool backtrackLit) {
415 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
416 VectorEdge *ve=allocDefVectorEdge();
417 for(uint i=0; i<numConstraints;i++) {
418 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
420 deleteVectorEdge(ve);
423 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
424 Node *nroot=getNodePtrFromEdge(root);
426 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
427 nroot = (Node *) nroot->ptrAnnot[isNegEdge(root)];
428 root = (Edge) { nroot };
430 if (edgeIsConst(root)) {
431 if (isNegEdge(root)) {
433 Edge newvar=constraintNewVar(cnf);
434 Literal var=getEdgeVar(newvar);
435 Literal clause[] = {var};
436 addArrayClauseLiteral(cnf->solver, 1, clause);
438 addArrayClauseLiteral(cnf->solver, 1, clause);
444 } else if (edgeIsVarConst(root)) {
445 Literal clause[] = { getEdgeVar(root)};
446 addArrayClauseLiteral(cnf->solver, 1, clause);
450 clearVectorEdge(stack);pushVectorEdge(stack, root);
451 while(getSizeVectorEdge(stack)!=0) {
452 Edge e=lastVectorEdge(stack);
453 Node *n=getNodePtrFromEdge(e);
455 if (edgeIsVarConst(e)) {
456 popVectorEdge(stack);
458 } else if (n->flags.type==NodeType_ITE ||
459 n->flags.type==NodeType_IFF) {
460 popVectorEdge(stack);
461 if (n->ptrAnnot[0]!=NULL)
462 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
463 if (n->ptrAnnot[1]!=NULL)
464 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
468 bool needPos = (n->intAnnot[0] > 0);
469 bool needNeg = (n->intAnnot[1] > 0);
470 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
471 (!needNeg || n->flags.cnfVisitedUp & 2)) {
472 popVectorEdge(stack);
473 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
474 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
476 n->flags.cnfVisitedDown|=1;
478 n->flags.cnfVisitedDown|=2;
479 for(uint i=0; i<n->numEdges; i++) {
480 Edge arg=n->edges[i];
481 arg=constraintNegateIf(arg, isNegEdge(e));
482 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
485 popVectorEdge(stack);
489 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
490 ASSERT(cnfExp!=NULL);
491 if (isProxy(cnfExp)) {
492 Literal l=getProxy(cnfExp);
493 Literal clause[] = {l};
494 addArrayClauseLiteral(cnf->solver, 1, clause);
495 } else if (backtrackLit) {
496 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
497 Literal clause[] = {l};
498 addArrayClauseLiteral(cnf->solver, 1, clause);
500 outputCNF(cnf, cnfExp);
503 if (!((intptr_t) cnfExp & 1)) {
504 deleteCNFExpr(cnfExp);
505 nroot->ptrAnnot[isNegEdge(root)] = NULL;
510 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
512 Node * n = getNodePtrFromEdge(e);
514 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
515 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
516 if (isProxy(otherExp))
517 l = -getProxy(otherExp);
519 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
520 Node * nsemNeg=getNodePtrFromEdge(semNeg);
521 if (nsemNeg != NULL) {
522 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
523 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
524 if (isProxy(otherExp))
525 l = -getProxy(otherExp);
526 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
527 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
528 if (isProxy(otherExp))
529 l = getProxy(otherExp);
535 Edge newvar = constraintNewVar(cnf);
536 l = getEdgeVar(newvar);
538 // Output the constraints on the auxiliary variable
539 constrainCNF(cnf, l, exp);
542 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
547 void produceCNF(CNF * cnf, Edge e) {
548 CNFExpr* expPos = NULL;
549 CNFExpr* expNeg = NULL;
550 Node *n = getNodePtrFromEdge(e);
552 if (n->intAnnot[0] > 0) {
553 expPos = produceConjunction(cnf, e);
556 if (n->intAnnot[1] > 0) {
557 expNeg = produceDisjunction(cnf, e);
560 /// @todo Propagate constants across semantic negations (this can
561 /// be done similarly to the calls to propagate shown below). The
562 /// trick here is that we need to figure out how to get the
563 /// semantic negation pointers, and ensure that they can have CNF
564 /// produced for them at the right point
566 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
568 // propagate from positive to negative, negative to positive
569 if (!propagate(cnf, & expPos, expNeg, true))
570 propagate(cnf, & expNeg, expPos, true);
572 // The polarity heuristic entails visiting the discovery polarity first
574 saveCNF(cnf, expPos, e, false);
575 saveCNF(cnf, expNeg, e, true);
577 saveCNF(cnf, expNeg, e, true);
578 saveCNF(cnf, expPos, e, false);
582 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
583 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
585 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
586 } else if (isProxy(*dest)) {
587 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
589 Literal clause[] = {getProxy(*dest)};
590 addArrayClauseLiteral(cnf->solver, 1, clause);
592 Literal clause[] = {-getProxy(*dest)};
593 addArrayClauseLiteral(cnf->solver, 1, clause);
596 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
598 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
605 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
606 Node *n=getNodePtrFromEdge(e);
607 n->flags.cnfVisitedUp |= (1 << sign);
608 if (exp == NULL || isProxy(exp)) return;
610 if (exp->litSize == 1) {
611 Literal l = getLiteralLitVector(&exp->singletons, 0);
613 n->ptrAnnot[sign] = (void*) ((((intptr_t) l) << 1) | 1);
614 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
615 introProxy(cnf, e, exp, sign);
617 n->ptrAnnot[sign] = exp;
621 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
622 if (alwaysTrueCNF(expr)) {
624 } else if (alwaysFalseCNF(expr)) {
625 Literal clause[] = {-lcond};
626 addArrayClauseLiteral(cnf->solver, 1, clause);
630 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
631 Literal l=getLiteralLitVector(&expr->singletons,i);
632 Literal clause[] = {-lcond, l};
633 addArrayClauseLiteral(cnf->solver, 2, clause);
635 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
636 LitVector *lv=getVectorLitVector(&expr->clauses,i);
637 addClauseLiteral(cnf->solver, -lcond); //Add first literal
638 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
642 void outputCNF(CNF *cnf, CNFExpr *expr) {
643 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
644 Literal l=getLiteralLitVector(&expr->singletons,i);
645 Literal clause[] = {l};
646 addArrayClauseLiteral(cnf->solver, 1, clause);
648 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
649 LitVector *lv=getVectorLitVector(&expr->clauses,i);
650 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
654 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
655 clearVectorEdge(&cnf->args);
657 *largestEdge = (Edge) {(Node*) NULL};
658 CNFExpr* largest = NULL;
659 Node *n=getNodePtrFromEdge(e);
662 Edge arg = n->edges[--i];
663 arg=constraintNegateIf(arg, isNeg);
664 Node * narg = getNodePtrFromEdge(arg);
666 if (edgeIsVarConst(arg)) {
667 pushVectorEdge(&cnf->args, arg);
671 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
672 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
675 if (narg->intAnnot[isNegEdge(arg)] == 1) {
676 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
677 if (!isProxy(argExp)) {
678 if (largest == NULL) {
682 } else if (argExp->litSize > largest->litSize) {
683 pushVectorEdge(&cnf->args, *largestEdge);
690 pushVectorEdge(&cnf->args, arg);
693 if (largest != NULL) {
694 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
695 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
701 void printCNF(Edge e) {
702 if (edgeIsVarConst(e)) {
703 Literal l=getEdgeVar(e);
704 model_print ("%d", l);
707 bool isNeg=isNegEdge(e);
708 if (edgeIsConst(e)) {
715 Node *n=getNodePtrFromEdge(e);
717 //Pretty print things that are equivalent to OR's
718 if (getNodeType(e)==NodeType_AND) {
720 for(uint i=0;i<n->numEdges;i++) {
724 printCNF(constraintNegate(e));
732 switch(getNodeType(e)) {
744 for(uint i=0;i<n->numEdges;i++) {
753 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
756 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
758 accum = allocCNFExprBool(true);
760 int i = getSizeVectorEdge(&cnf->args);
762 Edge arg = getVectorEdge(&cnf->args, --i);
763 if (edgeIsVarConst(arg)) {
764 conjoinCNFLit(accum, getEdgeVar(arg));
766 Node *narg=getNodePtrFromEdge(arg);
767 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
769 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
770 if (isProxy(argExp)) { // variable has been introduced
771 conjoinCNFLit(accum, getProxy(argExp));
773 conjoinCNFExpr(accum, argExp, destroy);
775 narg->ptrAnnot[isNegEdge(arg)] = NULL;
785 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
787 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
789 accum = allocCNFExprBool(false);
791 // This is necessary to check to make sure that we don't start out
792 // with an accumulator that is "too large".
794 /// @todo Strictly speaking, introProxy doesn't *need* to free
795 /// memory, then this wouldn't have to reallocate CNFExpr
797 /// @todo When this call to introProxy is made, the semantic
798 /// negation pointer will have been destroyed. Thus, it will not
799 /// be possible to use the correct proxy. That should be fixed.
801 // at this point, we will either have NULL, or a destructible expression
802 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
803 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
805 int i = getSizeVectorEdge(&cnf->args);
807 Edge arg=getVectorEdge(&cnf->args, --i);
808 Node *narg=getNodePtrFromEdge(arg);
809 if (edgeIsVarConst(arg)) {
810 disjoinCNFLit(accum, getEdgeVar(arg));
812 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
814 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
815 if (isProxy(argExp)) { // variable has been introduced
816 disjoinCNFLit(accum, getProxy(argExp));
817 } else if (argExp->litSize == 0) {
818 disjoinCNFExpr(accum, argExp, destroy);
820 // check to see if we should introduce a proxy
821 int aL = accum->litSize; // lits in accum
822 int eL = argExp->litSize; // lits in argument
823 int aC = getClauseSizeCNF(accum); // clauses in accum
824 int eC = getClauseSizeCNF(argExp); // clauses in argument
826 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
827 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
829 disjoinCNFExpr(accum, argExp, destroy);
830 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
839 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
840 Edge carray[numvars];
841 for(uint j=0;j<numvars;j++) {
842 carray[j]=((value&1)==1) ? vars[j] : constraintNegate(vars[j]);
846 return constraintAND(cnf, numvars, carray);
849 /** Generates a constraint to ensure that all encodings are less than value */
850 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
851 Edge orarray[numvars];
852 Edge andarray[numvars];
858 for(uint j=0;j<numvars;j++) {
860 orarray[ori++]=constraintNegate(vars[j]);
863 //no ones to flip, so bail now...
865 return constraintAND(cnf, andi, andarray);
867 andarray[andi++]=constraintOR(cnf, ori, orarray);
869 value=value+(1<<(__builtin_ctz(value)));
874 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
878 for(uint i=0;i<numvars;i++) {
879 array[i]=constraintIFF(cnf, var1[i], var2[i]);
881 return constraintAND(cnf, numvars, array);