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) {
184 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
186 while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
189 uint remainSize=numEdges-initindex;
193 else if (remainSize == 1)
194 return edges[initindex];
195 else if (equalsEdge(edges[initindex], E_False))
198 /** De-duplicate array */
200 edges[lowindex]=edges[initindex++];
202 for(;initindex<numEdges;initindex++) {
203 Edge e1=edges[lowindex];
204 Edge e2=edges[initindex];
205 if (sameNodeVarEdge(e1, e2)) {
206 if (!sameSignEdge(e1, e2)) {
210 edges[++lowindex]=edges[initindex];
212 lowindex++; //Make lowindex look like size
217 if (cnf->enableMatching && lowindex==2 &&
218 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
219 getNodeType(edges[0]) == NodeType_AND &&
220 getNodeType(edges[1]) == NodeType_AND &&
221 getNodeSize(edges[0]) == 2 &&
222 getNodeSize(edges[1]) == 2) {
223 Edge * e0edges=getEdgeArray(edges[0]);
224 Edge * e1edges=getEdgeArray(edges[1]);
225 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
226 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
227 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
228 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
229 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
230 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
231 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
232 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
236 return createNode(cnf, NodeType_AND, lowindex, edges);
239 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
240 Edge edges[2]={left, right};
241 return constraintAND(cnf, 2, edges);
244 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
247 array[1]=constraintNegate(right);
248 Edge eand=constraintAND(cnf, 2, array);
249 return constraintNegate(eand);
252 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
253 bool negate=!sameSignEdge(left, right);
254 Edge lpos=getNonNeg(left);
255 Edge rpos=getNonNeg(right);
258 if (equalsEdge(lpos, rpos)) {
260 } else if (ltEdge(lpos, rpos)) {
261 Edge edges[]={lpos, rpos};
262 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
264 Edge edges[]={rpos, lpos};
265 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
268 e=constraintNegate(e);
272 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
273 if (isNegEdge(cond)) {
274 cond=constraintNegate(cond);
280 bool negate = isNegEdge(thenedge);
282 thenedge=constraintNegate(thenedge);
283 elseedge=constraintNegate(elseedge);
287 if (equalsEdge(cond, E_True)) {
289 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
290 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
291 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
292 result=constraintIMPLIES(cnf, cond, thenedge);
293 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
294 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
295 } else if (equalsEdge(thenedge, elseedge)) {
297 } else if (sameNodeOppSign(thenedge, elseedge)) {
298 if (ltEdge(cond, thenedge)) {
299 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
301 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
304 Edge edges[]={cond, thenedge, elseedge};
305 result=createNode(cnf, NodeType_ITE, 3, edges);
308 result=constraintNegate(result);
312 void addConstraintCNF(CNF *cnf, Edge constraint) {
313 pushVectorEdge(&cnf->constraints, constraint);
316 Edge constraintNewVar(CNF *cnf) {
317 uint varnum=cnf->varcount++;
318 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
322 int solveCNF(CNF *cnf) {
324 convertPass(cnf, false);
325 finishedClauses(cnf->solver);
326 return solve(cnf->solver);
329 bool getValueCNF(CNF *cnf, Edge var) {
330 Literal l=getEdgeVar(var);
333 return isneg ^ getValueSolver(cnf->solver, l);
336 void countPass(CNF *cnf) {
337 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
338 VectorEdge *ve=allocDefVectorEdge();
339 for(uint i=0; i<numConstraints;i++) {
340 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
342 deleteVectorEdge(ve);
345 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
346 //Skip constants and variables...
347 if (edgeIsVarConst(eroot))
350 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
352 bool isMatching=cnf->enableMatching;
354 while(getSizeVectorEdge(stack) != 0) {
355 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
356 bool polarity=isNegEdge(e);
357 Node *n=getNodePtrFromEdge(e);
358 if (getExpanded(n, polarity)) {
359 if (n->flags.type == NodeType_IFF ||
360 n->flags.type == NodeType_ITE) {
361 Edge pExp={n->ptrAnnot[polarity]};
362 getNodePtrFromEdge(pExp)->intAnnot[0]++;
364 n->intAnnot[polarity]++;
367 setExpanded(n, polarity);
369 if (n->flags.type == NodeType_ITE||
370 n->flags.type == NodeType_IFF) {
371 n->intAnnot[polarity]=0;
372 Edge cond=n->edges[0];
373 Edge thenedge=n->edges[1];
374 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
375 thenedge=constraintNegateIf(thenedge, !polarity);
376 elseedge=constraintNegateIf(elseedge, !polarity);
377 thenedge=constraintAND2(cnf, cond, thenedge);
378 cond=constraintNegate(cond);
379 elseedge=constraintAND2(cnf, cond, elseedge);
380 thenedge=constraintNegate(thenedge);
381 elseedge=constraintNegate(elseedge);
382 cnf->enableMatching=false;
383 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
384 n->ptrAnnot[polarity]=succ1.node_ptr;
385 cnf->enableMatching=isMatching;
386 pushVectorEdge(stack, succ1);
387 if (getExpanded(n, !polarity)) {
388 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
389 Node *n1=getNodePtrFromEdge(succ1);
390 Node *n2=getNodePtrFromEdge(succ2);
391 n1->ptrAnnot[0]=succ2.node_ptr;
392 n2->ptrAnnot[0]=succ1.node_ptr;
393 n1->ptrAnnot[1]=succ2.node_ptr;
394 n2->ptrAnnot[1]=succ1.node_ptr;
397 n->intAnnot[polarity]=1;
398 for (uint i=0;i<n->numEdges;i++) {
399 Edge succ=n->edges[i];
400 if(!edgeIsVarConst(succ)) {
401 succ=constraintNegateIf(succ, polarity);
402 pushVectorEdge(stack, succ);
410 void convertPass(CNF *cnf, bool backtrackLit) {
411 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
412 VectorEdge *ve=allocDefVectorEdge();
413 for(uint i=0; i<numConstraints;i++) {
414 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
416 deleteVectorEdge(ve);
419 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
420 Node *nroot=getNodePtrFromEdge(root);
422 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
423 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
426 if (edgeIsConst(root)) {
427 if (isNegEdge(root)) {
429 Edge newvar=constraintNewVar(cnf);
430 Literal var=getEdgeVar(newvar);
431 Literal clause[] = {var};
432 addArrayClauseLiteral(cnf->solver, 1, clause);
434 addArrayClauseLiteral(cnf->solver, 1, clause);
440 } else if (edgeIsVarConst(root)) {
441 Literal clause[] = { getEdgeVar(root)};
442 addArrayClauseLiteral(cnf->solver, 1, clause);
446 clearVectorEdge(stack);pushVectorEdge(stack, root);
447 while(getSizeVectorEdge(stack)!=0) {
448 Edge e=lastVectorEdge(stack);
449 Node *n=getNodePtrFromEdge(e);
451 if (edgeIsVarConst(e)) {
452 popVectorEdge(stack);
454 } else if (n->flags.type==NodeType_ITE ||
455 n->flags.type==NodeType_IFF) {
456 popVectorEdge(stack);
457 if (n->ptrAnnot[0]!=NULL)
458 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
459 if (n->ptrAnnot[1]!=NULL)
460 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
464 bool needPos = (n->intAnnot[0] > 0);
465 bool needNeg = (n->intAnnot[1] > 0);
466 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
467 (!needNeg || n->flags.cnfVisitedUp & 2)) {
468 popVectorEdge(stack);
469 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
470 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
472 n->flags.cnfVisitedDown|=1;
474 n->flags.cnfVisitedDown|=2;
475 for(uint i=0; i<n->numEdges; i++) {
476 Edge arg=n->edges[i];
477 arg=constraintNegateIf(arg, isNegEdge(e));
478 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
481 popVectorEdge(stack);
485 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
486 if (isProxy(cnfExp)) {
487 Literal l=getProxy(cnfExp);
488 Literal clause[] = {l};
489 addArrayClauseLiteral(cnf->solver, 1, clause);
490 } else if (backtrackLit) {
491 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
492 Literal clause[] = {l};
493 addArrayClauseLiteral(cnf->solver, 1, clause);
495 outputCNF(cnf, cnfExp);
498 if (!((intptr_t) cnfExp & 1)) {
499 deleteCNFExpr(cnfExp);
500 nroot->ptrAnnot[isNegEdge(root)] = NULL;
505 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
507 Node * n = getNodePtrFromEdge(e);
509 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
510 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
511 if (isProxy(otherExp))
512 l = -getProxy(otherExp);
514 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
515 Node * nsemNeg=getNodePtrFromEdge(semNeg);
516 if (nsemNeg != NULL) {
517 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
518 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
519 if (isProxy(otherExp))
520 l = -getProxy(otherExp);
521 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
522 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
523 if (isProxy(otherExp))
524 l = getProxy(otherExp);
530 Edge newvar = constraintNewVar(cnf);
531 l = getEdgeVar(newvar);
533 // Output the constraints on the auxiliary variable
534 constrainCNF(cnf, l, exp);
537 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
542 void produceCNF(CNF * cnf, Edge e) {
543 CNFExpr* expPos = NULL;
544 CNFExpr* expNeg = NULL;
545 Node *n = getNodePtrFromEdge(e);
547 if (n->intAnnot[0] > 0) {
548 expPos = produceConjunction(cnf, e);
551 if (n->intAnnot[1] > 0) {
552 expNeg = produceDisjunction(cnf, e);
555 /// @todo Propagate constants across semantic negations (this can
556 /// be done similarly to the calls to propagate shown below). The
557 /// trick here is that we need to figure out how to get the
558 /// semantic negation pointers, and ensure that they can have CNF
559 /// produced for them at the right point
561 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
563 // propagate from positive to negative, negative to positive
564 if (!propagate(cnf, & expPos, expNeg, true))
565 propagate(cnf, & expNeg, expPos, true);
567 // The polarity heuristic entails visiting the discovery polarity first
569 saveCNF(cnf, expPos, e, false);
570 saveCNF(cnf, expNeg, e, true);
572 saveCNF(cnf, expNeg, e, true);
573 saveCNF(cnf, expPos, e, false);
577 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
578 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
580 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
581 } else if (isProxy(*dest)) {
582 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
584 Literal clause[] = {getProxy(*dest)};
585 addArrayClauseLiteral(cnf->solver, 1, clause);
587 Literal clause[] = {-getProxy(*dest)};
588 addArrayClauseLiteral(cnf->solver, 1, clause);
591 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
593 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
600 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
601 Node *n=getNodePtrFromEdge(e);
602 n->flags.cnfVisitedUp |= (1 << sign);
603 if (exp == NULL || isProxy(exp)) return;
605 if (exp->litSize == 1) {
606 Literal l = getLiteralLitVector(&exp->singletons, 0);
608 n->ptrAnnot[sign] = (void*) ((((intptr_t) l) << 1) | 1);
609 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
610 introProxy(cnf, e, exp, sign);
612 n->ptrAnnot[sign] = exp;
616 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
617 if (alwaysTrueCNF(expr)) {
619 } else if (alwaysFalseCNF(expr)) {
620 Literal clause[] = {-lcond};
621 addArrayClauseLiteral(cnf->solver, 1, clause);
625 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
626 Literal l=getLiteralLitVector(&expr->singletons,i);
627 Literal clause[] = {-lcond, l};
628 addArrayClauseLiteral(cnf->solver, 2, clause);
630 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
631 LitVector *lv=getVectorLitVector(&expr->clauses,i);
632 addClauseLiteral(cnf->solver, -lcond); //Add first literal
633 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
637 void outputCNF(CNF *cnf, CNFExpr *expr) {
638 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
639 Literal l=getLiteralLitVector(&expr->singletons,i);
640 Literal clause[] = {l};
641 addArrayClauseLiteral(cnf->solver, 1, clause);
643 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
644 LitVector *lv=getVectorLitVector(&expr->clauses,i);
645 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
649 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
650 clearVectorEdge(&cnf->args);
652 *largestEdge = (Edge) {(Node*) NULL};
653 CNFExpr* largest = NULL;
654 Node *n=getNodePtrFromEdge(e);
657 Edge arg = n->edges[--i];
658 arg=constraintNegateIf(arg, isNeg);
659 Node * narg = getNodePtrFromEdge(arg);
661 if (edgeIsVarConst(arg)) {
662 pushVectorEdge(&cnf->args, arg);
666 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
667 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
670 if (narg->intAnnot[isNegEdge(arg)] == 1) {
671 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
672 if (!isProxy(argExp)) {
673 if (largest == NULL) {
677 } else if (argExp->litSize > largest->litSize) {
678 pushVectorEdge(&cnf->args, *largestEdge);
685 pushVectorEdge(&cnf->args, arg);
688 if (largest != NULL) {
689 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
690 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
696 void printCNF(Edge e) {
697 if (edgeIsVarConst(e)) {
698 Literal l=getEdgeVar(e);
702 bool isNeg=isNegEdge(e);
703 if (edgeIsConst(e)) {
710 Node *n=getNodePtrFromEdge(e);
713 switch(getNodeType(e)) {
725 for(uint i=0;i<n->numEdges;i++) {
734 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
737 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
739 accum = allocCNFExprBool(true);
741 int i = getSizeVectorEdge(&cnf->args);
743 Edge arg = getVectorEdge(&cnf->args, --i);
744 if (edgeIsVarConst(arg)) {
745 conjoinCNFLit(accum, getEdgeVar(arg));
747 Node *narg=getNodePtrFromEdge(arg);
748 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
750 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
751 if (isProxy(argExp)) { // variable has been introduced
752 conjoinCNFLit(accum, getProxy(argExp));
754 conjoinCNFExpr(accum, argExp, destroy);
756 narg->ptrAnnot[isNegEdge(arg)] = NULL;
766 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
768 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
770 accum = allocCNFExprBool(false);
772 // This is necessary to check to make sure that we don't start out
773 // with an accumulator that is "too large".
775 /// @todo Strictly speaking, introProxy doesn't *need* to free
776 /// memory, then this wouldn't have to reallocate CNFExpr
778 /// @todo When this call to introProxy is made, the semantic
779 /// negation pointer will have been destroyed. Thus, it will not
780 /// be possible to use the correct proxy. That should be fixed.
782 // at this point, we will either have NULL, or a destructible expression
783 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
784 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
786 int i = getSizeVectorEdge(&cnf->args);
788 Edge arg=getVectorEdge(&cnf->args, --i);
789 Node *narg=getNodePtrFromEdge(arg);
790 if (edgeIsVarConst(arg)) {
791 disjoinCNFLit(accum, getEdgeVar(arg));
793 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
795 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
796 if (isProxy(argExp)) { // variable has been introduced
797 disjoinCNFLit(accum, getProxy(argExp));
798 } else if (argExp->litSize == 0) {
799 disjoinCNFExpr(accum, argExp, destroy);
801 // check to see if we should introduce a proxy
802 int aL = accum->litSize; // lits in accum
803 int eL = argExp->litSize; // lits in argument
804 int aC = getClauseSizeCNF(accum); // clauses in accum
805 int eC = getClauseSizeCNF(argExp); // clauses in argument
807 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
808 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
810 disjoinCNFExpr(accum, argExp, destroy);
811 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
820 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
821 Edge carray[numvars];
822 for(uint j=0;j<numvars;j++) {
823 carray[j]=((value&1)==1) ? vars[j] : constraintNegate(vars[j]);
827 return constraintAND(cnf, numvars, carray);
830 /** Generates a constraint to ensure that all encodings are less than value */
831 Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
832 Edge orarray[numvars];
833 Edge andarray[numvars];
839 for(uint j=0;j<numvars;j++) {
841 orarray[ori++]=constraintNegate(vars[j]);
844 //no ones to flip, so bail now...
846 return constraintAND(cnf, andi, andarray);
848 andarray[andi++]=constraintOR(cnf, ori, orarray);
850 value=value+(1<<(__builtin_ctz(value)));
855 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
859 for(uint i=0;i<numvars;i++) {
860 array[i]=constraintIFF(cnf, var1[i], var2[i]);
862 return constraintAND(cnf, numvars, array);