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)
46 CNF * cnf=ourmalloc(sizeof(CNF));
48 cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
49 cnf->mask=cnf->capacity-1;
50 cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
52 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
53 cnf->enableMatching=true;
54 allocInlineDefVectorEdge(& cnf->constraints);
55 allocInlineDefVectorEdge(& cnf->args);
56 cnf->solver=allocIncrementalSolver();
60 void deleteCNF(CNF * cnf) {
61 for(uint i=0;i<cnf->capacity;i++) {
62 Node *n=cnf->node_array[i];
66 deleteVectorArrayEdge(& cnf->constraints);
67 deleteVectorArrayEdge(& cnf->args);
68 deleteIncrementalSolver(cnf->solver);
69 ourfree(cnf->node_array);
73 void resizeCNF(CNF *cnf, uint newCapacity) {
74 Node **old_array=cnf->node_array;
75 Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
76 uint oldCapacity=cnf->capacity;
77 uint newMask=newCapacity-1;
78 for(uint i=0;i<oldCapacity;i++) {
80 uint hashCode=n->hashCode;
81 uint newindex=hashCode & newMask;
82 for(;;newindex=(newindex+1) & newMask) {
83 if (new_array[newindex] == NULL) {
84 new_array[newindex]=n;
90 cnf->node_array=new_array;
91 cnf->capacity=newCapacity;
92 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
96 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
97 Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
98 memcpy(n->edges, edges, sizeof(Edge)*numEdges);
100 n->flags.wasExpanded=0;
101 n->flags.cnfVisitedDown=0;
102 n->flags.cnfVisitedUp=0;
103 n->flags.varForced=0;
104 n->numEdges=numEdges;
105 n->hashCode=hashcode;
106 n->intAnnot[0]=0;n->intAnnot[1]=0;
107 n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
111 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
112 if (cnf->size > cnf->maxsize) {
113 resizeCNF(cnf, cnf->capacity << 1);
115 uint hashvalue=hashNode(type, numEdges, edges);
117 uint index=hashvalue & mask;
119 for(;;index=(index+1)&mask) {
120 n_ptr=&cnf->node_array[index];
122 if ((*n_ptr)->hashCode==hashvalue) {
123 if (compareNodes(*n_ptr, type, numEdges, edges)) {
132 *n_ptr=allocNode(type, numEdges, edges, hashvalue);
137 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
138 uint hashvalue=type ^ numEdges;
139 for(uint i=0;i<numEdges;i++) {
140 hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
141 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
143 return (uint) hashvalue;
146 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
147 if (node->flags.type!=type || node->numEdges != numEdges)
149 Edge *nodeedges=node->edges;
150 for(uint i=0;i<numEdges;i++) {
151 if (!equalsEdge(nodeedges[i], edges[i]))
157 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
158 Edge edgearray[numEdges];
160 for(uint i=0; i<numEdges; i++) {
161 edgearray[i]=constraintNegate(edges[i]);
163 Edge eand=constraintAND(cnf, numEdges, edgearray);
164 return constraintNegate(eand);
167 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
168 Edge lneg=constraintNegate(left);
169 Edge rneg=constraintNegate(right);
170 Edge eand=constraintAND2(cnf, left, right);
171 return constraintNegate(eand);
174 int comparefunction(const Edge * e1, const Edge * e2) {
175 return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
178 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
179 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
181 while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
184 uint remainSize=numEdges-initindex;
188 else if (remainSize == 1)
189 return edges[initindex];
190 else if (equalsEdge(edges[initindex], E_False))
193 /** De-duplicate array */
195 edges[lowindex]=edges[initindex++];
197 for(;initindex<numEdges;initindex++) {
198 Edge e1=edges[lowindex];
199 Edge e2=edges[initindex];
200 if (sameNodeVarEdge(e1, e2)) {
201 if (!sameSignEdge(e1, e2)) {
205 edges[++lowindex]=edges[initindex];
207 lowindex++; //Make lowindex look like size
212 if (cnf->enableMatching && lowindex==2 &&
213 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
214 getNodeType(edges[0]) == NodeType_AND &&
215 getNodeType(edges[1]) == NodeType_AND &&
216 getNodeSize(edges[0]) == 2 &&
217 getNodeSize(edges[1]) == 2) {
218 Edge * e0edges=getEdgeArray(edges[0]);
219 Edge * e1edges=getEdgeArray(edges[1]);
220 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
221 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
222 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
223 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
224 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
225 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
226 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
227 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
231 return createNode(cnf, NodeType_AND, lowindex, edges);
234 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
235 Edge edges[2]={left, right};
236 return constraintAND(cnf, 2, edges);
239 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
242 array[1]=constraintNegate(right);
243 Edge eand=constraintAND(cnf, 2, array);
244 return constraintNegate(eand);
247 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
248 bool negate=!sameSignEdge(left, right);
249 Edge lpos=getNonNeg(left);
250 Edge rpos=getNonNeg(right);
253 if (equalsEdge(lpos, rpos)) {
255 } else if (ltEdge(lpos, rpos)) {
256 Edge edges[]={lpos, rpos};
257 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
259 Edge edges[]={rpos, lpos};
260 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
263 e=constraintNegate(e);
267 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
268 if (isNegEdge(cond)) {
269 cond=constraintNegate(cond);
275 bool negate = isNegEdge(thenedge);
277 thenedge=constraintNegate(thenedge);
278 elseedge=constraintNegate(elseedge);
282 if (equalsEdge(cond, E_True)) {
284 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
285 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
286 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
287 result=constraintIMPLIES(cnf, cond, thenedge);
288 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
289 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
290 } else if (equalsEdge(thenedge, elseedge)) {
292 } else if (sameNodeOppSign(thenedge, elseedge)) {
293 if (ltEdge(cond, thenedge)) {
294 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
296 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
299 Edge edges[]={cond, thenedge, elseedge};
300 result=createNode(cnf, NodeType_ITE, 3, edges);
303 result=constraintNegate(result);
307 void addConstraint(CNF *cnf, Edge constraint) {
308 pushVectorEdge(&cnf->constraints, constraint);
311 Edge constraintNewVar(CNF *cnf) {
312 uint varnum=cnf->varcount++;
313 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
317 int solveCNF(CNF *cnf) {
319 convertPass(cnf, false);
320 finishedClauses(cnf->solver);
321 return solve(cnf->solver);
324 bool getValueCNF(CNF *cnf, Edge var) {
325 Literal l=getEdgeVar(var);
328 return isneg ^ getValueSolver(cnf->solver, l);
331 void countPass(CNF *cnf) {
332 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
333 VectorEdge *ve=allocDefVectorEdge();
334 for(uint i=0; i<numConstraints;i++) {
335 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
337 deleteVectorEdge(ve);
340 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
341 //Skip constants and variables...
342 if (edgeIsVarConst(eroot))
345 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
347 bool isMatching=cnf->enableMatching;
349 while(getSizeVectorEdge(stack) != 0) {
350 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
351 bool polarity=isNegEdge(e);
352 Node *n=getNodePtrFromEdge(e);
353 if (getExpanded(n, polarity)) {
354 if (n->flags.type == NodeType_IFF ||
355 n->flags.type == NodeType_ITE) {
356 Edge pExp={n->ptrAnnot[polarity]};
357 getNodePtrFromEdge(pExp)->intAnnot[0]++;
359 n->intAnnot[polarity]++;
362 setExpanded(n, polarity);
364 if (n->flags.type == NodeType_ITE||
365 n->flags.type == NodeType_IFF) {
366 n->intAnnot[polarity]=0;
367 Edge cond=n->edges[0];
368 Edge thenedge=n->edges[1];
369 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
370 thenedge=constraintNegateIf(thenedge, !polarity);
371 elseedge=constraintNegateIf(elseedge, !polarity);
372 thenedge=constraintAND2(cnf, cond, thenedge);
373 cond=constraintNegate(cond);
374 elseedge=constraintAND2(cnf, cond, elseedge);
375 thenedge=constraintNegate(thenedge);
376 elseedge=constraintNegate(elseedge);
377 cnf->enableMatching=false;
378 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
379 n->ptrAnnot[polarity]=succ1.node_ptr;
380 cnf->enableMatching=isMatching;
381 pushVectorEdge(stack, succ1);
382 if (getExpanded(n, !polarity)) {
383 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
384 Node *n1=getNodePtrFromEdge(succ1);
385 Node *n2=getNodePtrFromEdge(succ2);
386 n1->ptrAnnot[0]=succ2.node_ptr;
387 n2->ptrAnnot[0]=succ1.node_ptr;
388 n1->ptrAnnot[1]=succ2.node_ptr;
389 n2->ptrAnnot[1]=succ1.node_ptr;
392 n->intAnnot[polarity]=1;
393 for (uint i=0;i<n->numEdges;i++) {
394 Edge succ=n->edges[i];
395 succ=constraintNegateIf(succ, polarity);
396 if(!edgeIsVarConst(succ)) {
397 pushVectorEdge(stack, succ);
405 void convertPass(CNF *cnf, bool backtrackLit) {
406 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
407 VectorEdge *ve=allocDefVectorEdge();
408 for(uint i=0; i<numConstraints;i++) {
409 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
411 deleteVectorEdge(ve);
414 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
415 Node *nroot=getNodePtrFromEdge(root);
417 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
418 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
421 if (edgeIsConst(root)) {
422 if (isNegEdge(root)) {
424 Edge newvar=constraintNewVar(cnf);
425 Literal var=getEdgeVar(newvar);
426 Literal clause[] = {var};
427 addArrayClauseLiteral(cnf->solver, 1, clause);
429 addArrayClauseLiteral(cnf->solver, 1, clause);
435 } else if (edgeIsVarConst(root)) {
436 Literal clause[] = { getEdgeVar(root)};
437 addArrayClauseLiteral(cnf->solver, 1, clause);
441 clearVectorEdge(stack);pushVectorEdge(stack, root);
442 while(getSizeVectorEdge(stack)!=0) {
443 Edge e=lastVectorEdge(stack);
444 Node *n=getNodePtrFromEdge(e);
446 if (edgeIsVarConst(e)) {
447 popVectorEdge(stack);
449 } else if (n->flags.type==NodeType_ITE ||
450 n->flags.type==NodeType_IFF) {
451 popVectorEdge(stack);
452 if (n->ptrAnnot[0]!=NULL)
453 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
454 if (n->ptrAnnot[1]!=NULL)
455 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
459 bool needPos = (n->intAnnot[0] > 0);
460 bool needNeg = (n->intAnnot[1] > 0);
461 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
462 (!needNeg || n->flags.cnfVisitedUp & 2)) {
463 popVectorEdge(stack);
464 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
465 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
467 n->flags.cnfVisitedDown|=1;
469 n->flags.cnfVisitedDown|=2;
470 for(uint i=0; i<n->numEdges; i++) {
471 Edge arg=n->edges[i];
472 arg=constraintNegateIf(arg, isNegEdge(e));
473 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
476 popVectorEdge(stack);
480 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
481 if (isProxy(cnfExp)) {
482 Literal l=getProxy(cnfExp);
483 Literal clause[] = {l};
484 addArrayClauseLiteral(cnf->solver, 1, clause);
485 } else if (backtrackLit) {
486 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
487 Literal clause[] = {l};
488 addArrayClauseLiteral(cnf->solver, 1, clause);
490 outputCNF(cnf, cnfExp);
493 if (!((intptr_t) cnfExp & 1)) {
494 deleteCNFExpr(cnfExp);
495 nroot->ptrAnnot[isNegEdge(root)] = NULL;
500 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
502 Node * n = getNodePtrFromEdge(e);
504 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
505 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
506 if (isProxy(otherExp))
507 l = -getProxy(otherExp);
509 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
510 Node * nsemNeg=getNodePtrFromEdge(semNeg);
511 if (nsemNeg != NULL) {
512 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
513 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
514 if (isProxy(otherExp))
515 l = -getProxy(otherExp);
516 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
517 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
518 if (isProxy(otherExp))
519 l = getProxy(otherExp);
525 Edge newvar = constraintNewVar(cnf);
526 l = getEdgeVar(newvar);
528 // Output the constraints on the auxiliary variable
529 constrainCNF(cnf, l, exp);
532 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
537 void produceCNF(CNF * cnf, Edge e) {
538 CNFExpr* expPos = NULL;
539 CNFExpr* expNeg = NULL;
540 Node *n = getNodePtrFromEdge(e);
542 if (n->intAnnot[0] > 0) {
543 expPos = produceConjunction(cnf, e);
546 if (n->intAnnot[1] > 0) {
547 expNeg = produceDisjunction(cnf, e);
550 /// @todo Propagate constants across semantic negations (this can
551 /// be done similarly to the calls to propagate shown below). The
552 /// trick here is that we need to figure out how to get the
553 /// semantic negation pointers, and ensure that they can have CNF
554 /// produced for them at the right point
556 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
558 // propagate from positive to negative, negative to positive
559 if (!propagate(cnf, & expPos, expNeg, true))
560 propagate(cnf, & expNeg, expPos, true);
562 // The polarity heuristic entails visiting the discovery polarity first
564 saveCNF(cnf, expPos, e, false);
565 saveCNF(cnf, expNeg, e, true);
567 saveCNF(cnf, expNeg, e, true);
568 saveCNF(cnf, expPos, e, false);
572 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
573 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
575 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
576 } else if (isProxy(*dest)) {
577 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
579 Literal clause[] = {getProxy(*dest)};
580 addArrayClauseLiteral(cnf->solver, 1, clause);
582 Literal clause[] = {-getProxy(*dest)};
583 addArrayClauseLiteral(cnf->solver, 1, clause);
586 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
588 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
595 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
596 Node *n=getNodePtrFromEdge(e);
597 n->flags.cnfVisitedUp |= (1 << sign);
598 if (exp == NULL || isProxy(exp)) return;
600 if (exp->litSize == 1) {
601 Literal l = getLiteralLitVector(&exp->singletons, 0);
603 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
604 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
605 introProxy(cnf, e, exp, sign);
607 n->ptrAnnot[sign] = exp;
611 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
612 if (alwaysTrueCNF(expr)) {
614 } else if (alwaysFalseCNF(expr)) {
615 Literal clause[] = {-lcond};
616 addArrayClauseLiteral(cnf->solver, 1, clause);
620 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
621 Literal l=getLiteralLitVector(&expr->singletons,i);
622 Literal clause[] = {-lcond, l};
623 addArrayClauseLiteral(cnf->solver, 1, clause);
625 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
626 LitVector *lv=getVectorLitVector(&expr->clauses,i);
627 addClauseLiteral(cnf->solver, -lcond); //Add first literal
628 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
632 void outputCNF(CNF *cnf, CNFExpr *expr) {
633 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
634 Literal l=getLiteralLitVector(&expr->singletons,i);
635 Literal clause[] = {l};
636 addArrayClauseLiteral(cnf->solver, 1, clause);
638 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
639 LitVector *lv=getVectorLitVector(&expr->clauses,i);
640 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
644 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
645 clearVectorEdge(&cnf->args);
647 *largestEdge = (Edge) {(Node*) NULL};
648 CNFExpr* largest = NULL;
649 Node *n=getNodePtrFromEdge(e);
652 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
653 Node * narg = getNodePtrFromEdge(arg);
655 if (edgeIsVarConst(arg)) {
656 pushVectorEdge(&cnf->args, arg);
660 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
661 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
664 if (narg->intAnnot[isNegEdge(arg)] == 1) {
665 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
666 if (!isProxy(argExp)) {
667 if (largest == NULL) {
671 } else if (argExp->litSize > largest->litSize) {
672 pushVectorEdge(&cnf->args, *largestEdge);
679 pushVectorEdge(&cnf->args, arg);
682 if (largest != NULL) {
683 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
684 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
690 void printCNF(Edge e) {
691 if (edgeIsVarConst(e)) {
692 Literal l=getEdgeVar(e);
696 bool isNeg=isNegEdge(e);
697 if (edgeIsConst(e)) {
704 Node *n=getNodePtrFromEdge(e);
707 switch(getNodeType(e)) {
719 for(uint i=0;i<n->numEdges;i++) {
728 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
731 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
732 if (accum == NULL) accum = allocCNFExprBool(true);
734 int i = getSizeVectorEdge(&cnf->args);
736 Edge arg = getVectorEdge(&cnf->args, --i);
737 if (edgeIsVarConst(arg)) {
738 conjoinCNFLit(accum, getEdgeVar(arg));
740 Node *narg=getNodePtrFromEdge(arg);
741 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
743 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
744 if (isProxy(argExp)) { // variable has been introduced
745 conjoinCNFLit(accum, getProxy(argExp));
747 conjoinCNFExpr(accum, argExp, destroy);
748 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
758 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
760 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
762 accum = allocCNFExprBool(false);
764 // This is necessary to check to make sure that we don't start out
765 // with an accumulator that is "too large".
767 /// @todo Strictly speaking, introProxy doesn't *need* to free
768 /// memory, then this wouldn't have to reallocate CNFExpr
770 /// @todo When this call to introProxy is made, the semantic
771 /// negation pointer will have been destroyed. Thus, it will not
772 /// be possible to use the correct proxy. That should be fixed.
774 // at this point, we will either have NULL, or a destructible expression
775 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
776 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
778 int i = getSizeVectorEdge(&cnf->args);
780 Edge arg=getVectorEdge(&cnf->args, --i);
781 Node *narg=getNodePtrFromEdge(arg);
782 if (edgeIsVarConst(arg)) {
783 disjoinCNFLit(accum, getEdgeVar(arg));
785 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
787 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
788 if (isProxy(argExp)) { // variable has been introduced
789 disjoinCNFLit(accum, getProxy(argExp));
790 } else if (argExp->litSize == 0) {
791 disjoinCNFExpr(accum, argExp, destroy);
793 // check to see if we should introduce a proxy
794 int aL = accum->litSize; // lits in accum
795 int eL = argExp->litSize; // lits in argument
796 int aC = getClauseSizeCNF(accum); // clauses in accum
797 int eC = getClauseSizeCNF(argExp); // clauses in argument
799 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
800 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
802 disjoinCNFExpr(accum, argExp, destroy);
803 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;