4 #include "inc_solver.h"
7 /** Code ported from C++ BAT implementation of NICE-SAT */
9 VectorImpl(Edge, Edge, 16)
12 CNF * cnf=ourmalloc(sizeof(CNF));
14 cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
15 cnf->mask=cnf->capacity-1;
16 cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
18 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
19 cnf->enableMatching=true;
20 allocInlineDefVectorEdge(& cnf->constraints);
21 allocInlineDefVectorEdge(& cnf->args);
25 void deleteCNF(CNF * cnf) {
26 for(uint i=0;i<cnf->capacity;i++) {
27 Node *n=cnf->node_array[i];
31 deleteVectorArrayEdge(& cnf->constraints);
32 deleteVectorArrayEdge(& cnf->args);
33 ourfree(cnf->node_array);
37 void resizeCNF(CNF *cnf, uint newCapacity) {
38 Node **old_array=cnf->node_array;
39 Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
40 uint oldCapacity=cnf->capacity;
41 uint newMask=newCapacity-1;
42 for(uint i=0;i<oldCapacity;i++) {
44 uint hashCode=n->hashCode;
45 uint newindex=hashCode & newMask;
46 for(;;newindex=(newindex+1) & newMask) {
47 if (new_array[newindex] == NULL) {
48 new_array[newindex]=n;
54 cnf->node_array=new_array;
55 cnf->capacity=newCapacity;
56 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
60 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
61 Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
62 memcpy(n->edges, edges, sizeof(Edge)*numEdges);
64 n->flags.wasExpanded=0;
65 n->flags.cnfVisitedDown=0;
66 n->flags.cnfVisitedUp=0;
69 n->intAnnot[0]=0;n->intAnnot[1]=0;
70 n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
74 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
75 if (cnf->size > cnf->maxsize) {
76 resizeCNF(cnf, cnf->capacity << 1);
78 uint hashvalue=hashNode(type, numEdges, edges);
80 uint index=hashvalue & mask;
82 for(;;index=(index+1)&mask) {
83 n_ptr=&cnf->node_array[index];
85 if ((*n_ptr)->hashCode==hashvalue) {
86 if (compareNodes(*n_ptr, type, numEdges, edges)) {
95 *n_ptr=allocNode(type, numEdges, edges, hashvalue);
100 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
101 uint hashvalue=type ^ numEdges;
102 for(uint i=0;i<numEdges;i++) {
103 hashvalue ^= (uint) edges[i].node_ptr;
104 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
106 return (uint) hashvalue;
109 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
110 if (node->flags.type!=type || node->numEdges != numEdges)
112 Edge *nodeedges=node->edges;
113 for(uint i=0;i<numEdges;i++) {
114 if (!equalsEdge(nodeedges[i], edges[i]))
120 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
121 Edge edgearray[numEdges];
123 for(uint i=0; i<numEdges; i++) {
124 edgearray[i]=constraintNegate(edges[i]);
126 Edge eand=constraintAND(cnf, numEdges, edgearray);
127 return constraintNegate(eand);
130 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
131 Edge lneg=constraintNegate(left);
132 Edge rneg=constraintNegate(right);
133 Edge eand=constraintAND2(cnf, left, right);
134 return constraintNegate(eand);
137 int comparefunction(const Edge * e1, const Edge * e2) {
138 return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
141 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
142 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
144 while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
147 uint remainSize=numEdges-initindex;
151 else if (remainSize == 1)
152 return edges[initindex];
153 else if (equalsEdge(edges[initindex], E_False))
156 /** De-duplicate array */
158 edges[lowindex++]=edges[initindex++];
160 for(;initindex<numEdges;initindex++) {
161 Edge e1=edges[lowindex];
162 Edge e2=edges[initindex];
163 if (sameNodeVarEdge(e1, e2)) {
164 if (!sameSignEdge(e1, e2)) {
168 edges[lowindex++]=edges[initindex];
173 if (cnf->enableMatching && lowindex==2 &&
174 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
175 getNodeType(edges[0]) == NodeType_AND &&
176 getNodeType(edges[1]) == NodeType_AND &&
177 getNodeSize(edges[0]) == 2 &&
178 getNodeSize(edges[1]) == 2) {
179 Edge * e0edges=getEdgeArray(edges[0]);
180 Edge * e1edges=getEdgeArray(edges[1]);
181 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
182 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
183 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
184 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
185 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
186 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
187 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
188 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
192 return createNode(cnf, NodeType_AND, numEdges, edges);
195 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
196 Edge edges[2]={left, right};
197 return constraintAND(cnf, 2, edges);
200 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
203 array[1]=constraintNegate(right);
204 Edge eand=constraintAND(cnf, 2, array);
205 return constraintNegate(eand);
208 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
209 bool negate=sameSignEdge(left, right);
210 Edge lpos=getNonNeg(left);
211 Edge rpos=getNonNeg(right);
214 if (equalsEdge(lpos, rpos)) {
216 } else if (ltEdge(lpos, rpos)) {
217 Edge edges[]={lpos, rpos};
218 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
220 Edge edges[]={rpos, lpos};
221 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
224 e=constraintNegate(e);
228 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
229 if (isNegEdge(cond)) {
230 cond=constraintNegate(cond);
236 bool negate = isNegEdge(thenedge);
238 thenedge=constraintNegate(thenedge);
239 elseedge=constraintNegate(elseedge);
243 if (equalsEdge(cond, E_True)) {
245 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
246 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
247 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
248 result=constraintIMPLIES(cnf, cond, thenedge);
249 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
250 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
251 } else if (equalsEdge(thenedge, elseedge)) {
253 } else if (sameNodeOppSign(thenedge, elseedge)) {
254 if (ltEdge(cond, thenedge)) {
255 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
257 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
260 Edge edges[]={cond, thenedge, elseedge};
261 result=createNode(cnf, NodeType_ITE, 3, edges);
264 result=constraintNegate(result);
268 void addConstraint(CNF *cnf, Edge constraint) {
269 pushVectorEdge(&cnf->constraints, constraint);
272 Edge constraintNewVar(CNF *cnf) {
273 uint varnum=cnf->varcount++;
274 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
278 void countPass(CNF *cnf) {
279 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
280 VectorEdge *ve=allocDefVectorEdge();
281 for(uint i=0; i<numConstraints;i++) {
282 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
284 deleteVectorEdge(ve);
287 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
288 //Skip constants and variables...
289 if (edgeIsVarConst(e))
292 clearVectorEdge(stack);pushVectorEdge(stack, e);
294 bool isMatching=cnf->enableMatching;
296 while(getSizeVectorEdge(stack) != 0) {
297 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
298 bool polarity=isNegEdge(e);
299 Node *n=getNodePtrFromEdge(e);
300 if (getExpanded(n, polarity)) {
301 if (n->flags.type == NodeType_IFF ||
302 n->flags.type == NodeType_ITE) {
303 Edge pExp={n->ptrAnnot[polarity]};
304 getNodePtrFromEdge(pExp)->intAnnot[0]++;
306 n->intAnnot[polarity]++;
309 setExpanded(n, polarity); n->intAnnot[polarity]=1;
311 if (n->flags.type == NodeType_ITE||
312 n->flags.type == NodeType_IFF) {
313 n->intAnnot[polarity]=0;
314 Edge cond=n->edges[0];
315 Edge thenedge=n->edges[1];
316 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
317 thenedge=constraintNegateIf(thenedge, !polarity);
318 elseedge=constraintNegateIf(elseedge, !polarity);
319 thenedge=constraintAND2(cnf, cond, thenedge);
320 cond=constraintNegate(cond);
321 elseedge=constraintAND2(cnf, cond, elseedge);
322 thenedge=constraintNegate(thenedge);
323 elseedge=constraintNegate(elseedge);
324 cnf->enableMatching=false;
325 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
326 n->ptrAnnot[polarity]=succ1.node_ptr;
327 cnf->enableMatching=isMatching;
328 pushVectorEdge(stack, succ1);
329 if (getExpanded(n, !polarity)) {
330 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
331 Node *n1=getNodePtrFromEdge(succ1);
332 Node *n2=getNodePtrFromEdge(succ2);
333 n1->ptrAnnot[0]=succ2.node_ptr;
334 n2->ptrAnnot[0]=succ1.node_ptr;
335 n1->ptrAnnot[1]=succ2.node_ptr;
336 n2->ptrAnnot[1]=succ1.node_ptr;
339 for (uint i=0;i<n->numEdges;i++) {
340 Edge succ=n->edges[i];
341 succ=constraintNegateIf(succ, polarity);
342 if(!edgeIsVarConst(succ)) {
343 pushVectorEdge(stack, succ);
351 void convertPass(CNF *cnf, bool backtrackLit) {
352 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
353 VectorEdge *ve=allocDefVectorEdge();
354 for(uint i=0; i<numConstraints;i++) {
355 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
357 deleteVectorEdge(ve);
360 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
361 Node *nroot=getNodePtrFromEdge(root);
363 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
364 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
367 if (edgeIsConst(root)) {
368 if (isNegEdge(root)) {
370 Edge newvar=constraintNewVar(cnf);
371 Literal var=getEdgeVar(newvar);
372 Literal clause[] = {var, -var};
373 addArrayClauseLiteral(cnf->solver, 2, clause);
379 } else if (edgeIsVarConst(root)) {
380 Literal clause[] = { getEdgeVar(root)};
381 addArrayClauseLiteral(cnf->solver, 1, clause);
385 clearVectorEdge(stack);pushVectorEdge(stack, root);
386 while(getSizeVectorEdge(stack)!=0) {
387 Edge e=lastVectorEdge(stack);
388 Node *n=getNodePtrFromEdge(e);
390 if (edgeIsVarConst(e)) {
391 popVectorEdge(stack);
393 } else if (n->flags.type==NodeType_ITE ||
394 n->flags.type==NodeType_IFF) {
395 popVectorEdge(stack);
396 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
397 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
401 bool needPos = (n->intAnnot[0] > 0);
402 bool needNeg = (n->intAnnot[1] > 0);
403 if ((!needPos || n->flags.cnfVisitedUp & 1) ||
404 (!needNeg || n->flags.cnfVisitedUp & 2)) {
405 popVectorEdge(stack);
406 } else if ((needPos && !n->flags.cnfVisitedDown & 1) ||
407 (needNeg && !n->flags.cnfVisitedDown & 2)) {
409 n->flags.cnfVisitedDown|=1;
411 n->flags.cnfVisitedDown|=2;
412 for(uint i=0; i<n->numEdges; i++) {
413 Edge arg=n->edges[i];
414 arg=constraintNegateIf(arg, isNegEdge(e));
415 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
418 popVectorEdge(stack);
422 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
423 if (isProxy(cnfExp)) {
424 //solver.add(getProxy(cnfExp))
425 } else if (backtrackLit) {
426 //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
428 //solver.add(*cnfExp);
431 if (!((intptr_t) cnfExp & 1)) {
433 nroot->ptrAnnot[isNegEdge(root)] = NULL;
438 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
440 Node * n = getNodePtrFromEdge(e);
442 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
443 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
444 if (isProxy(otherExp))
445 l = -getProxy(otherExp);
447 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
448 Node * nsemNeg=getNodePtrFromEdge(semNeg);
449 if (nsemNeg != NULL) {
450 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
451 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
452 if (isProxy(otherExp))
453 l = -getProxy(otherExp);
454 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
455 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
456 if (isProxy(otherExp))
457 l = getProxy(otherExp);
463 Edge newvar = constraintNewVar(cnf);
464 l = getEdgeVar(newvar);
466 // Output the constraints on the auxiliary variable
467 constrainCNF(cnf, l, exp);
470 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
476 void produceCNF(CNF * cnf, Edge e) {
477 CNFExpr* expPos = NULL;
478 CNFExpr* expNeg = NULL;
479 Node *n = getNodePtrFromEdge(e);
481 if (n->intAnnot[0] > 0) {
482 expPos = produceConjunction(cnf, e);
485 if (n->intAnnot[1] > 0) {
486 expNeg = produceDisjunction(cnf, e);
489 /// @todo Propagate constants across semantic negations (this can
490 /// be done similarly to the calls to propagate shown below). The
491 /// trick here is that we need to figure out how to get the
492 /// semantic negation pointers, and ensure that they can have CNF
493 /// produced for them at the right point
495 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
497 // propagate from positive to negative, negative to positive
498 propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
500 // The polarity heuristic entails visiting the discovery polarity first
502 saveCNF(cnf, expPos, e, false);
503 saveCNF(cnf, expNeg, e, true);
505 saveCNF(cnf, expNeg, e, true);
506 saveCNF(cnf, expPos, e, false);
510 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
511 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
513 dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
514 } else if (isProxy(dest)) {
515 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
517 Literal clause[] = {getProxy(dest)};
518 addArrayClauseLiteral(cnf->solver, 1, clause);
520 Literal clause[] = {-getProxy(dest)};
521 addArrayClauseLiteral(cnf->solver, 1, clause);
524 dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
526 clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
533 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
534 Node *n=getNodePtrFromEdge(e);
535 n->flags.cnfVisitedUp |= (1 << sign);
536 if (exp == NULL || isProxy(exp)) return;
538 if (exp->litSize == 1) {
539 Literal l = getLiteralLitVector(&exp->singletons, 0);
541 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
542 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
543 introProxy(cnf, e, exp, sign);
545 n->ptrAnnot[sign] = exp;
549 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
550 if (alwaysTrueCNF(expr)) {
552 } else if (alwaysFalseCNF(expr)) {
553 Literal clause[] = {-lcond};
554 addArrayClauseLiteral(cnf->solver, 1, clause);
558 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
559 Literal l=getLiteralLitVector(&expr->singletons,i);
560 Literal clause[] = {-lcond, l};
561 addArrayClauseLiteral(cnf->solver, 1, clause);
563 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
564 LitVector *lv=getVectorLitVector(&expr->clauses,i);
565 addClauseLiteral(cnf->solver, -lcond); //Add first literal
566 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
570 void outputCNF(CNF *cnf, CNFExpr *expr) {
571 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
572 Literal l=getLiteralLitVector(&expr->singletons,i);
573 Literal clause[] = {l};
574 addArrayClauseLiteral(cnf->solver, 1, clause);
576 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
577 LitVector *lv=getVectorLitVector(&expr->clauses,i);
578 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
582 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
583 clearVectorEdge(&cnf->args);
585 *largestEdge = (Edge) {(Node*) NULL};
586 CNFExpr* largest = NULL;
587 Node *n=getNodePtrFromEdge(e);
590 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
591 Node * narg = getNodePtrFromEdge(arg);
593 if (edgeIsVarConst(arg)) {
594 pushVectorEdge(&cnf->args, arg);
598 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
599 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
602 if (narg->intAnnot[isNegEdge(arg)] == 1) {
603 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
604 if (!isProxy(argExp)) {
605 if (largest == NULL) {
609 } else if (argExp->litSize > largest->litSize) {
610 pushVectorEdge(&cnf->args, *largestEdge);
617 pushVectorEdge(&cnf->args, arg);
620 if (largest != NULL) {
621 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
622 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
629 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
632 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
633 if (accum == NULL) accum = allocCNFExprBool(true);
635 int i = getSizeVectorEdge(&cnf->args);
637 Edge arg = getVectorEdge(&cnf->args, --i);
638 if (edgeIsVarConst(arg)) {
639 conjoinCNFLit(accum, getEdgeVar(arg));
641 Node *narg=getNodePtrFromEdge(arg);
642 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
644 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
645 if (isProxy(argExp)) { // variable has been introduced
646 conjoinCNFLit(accum, getProxy(argExp));
648 conjoinCNFExpr(accum, argExp, destroy);
649 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
659 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
661 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
663 accum = allocCNFExprBool(false);
665 // This is necessary to check to make sure that we don't start out
666 // with an accumulator that is "too large".
668 /// @todo Strictly speaking, introProxy doesn't *need* to free
669 /// memory, then this wouldn't have to reallocate CNFExpr
671 /// @todo When this call to introProxy is made, the semantic
672 /// negation pointer will have been destroyed. Thus, it will not
673 /// be possible to use the correct proxy. That should be fixed.
675 // at this point, we will either have NULL, or a destructible expression
676 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
677 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
679 int i = getSizeVectorEdge(&cnf->args);
681 Edge arg=getVectorEdge(&cnf->args, --i);
682 Node *narg=getNodePtrFromEdge(arg);
683 if (edgeIsVarConst(arg)) {
684 disjoinCNFLit(accum, getEdgeVar(arg));
686 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
688 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
689 if (isProxy(argExp)) { // variable has been introduced
690 disjoinCNFLit(accum, getProxy(argExp));
691 } else if (argExp->litSize == 0) {
692 disjoinCNFExpr(accum, argExp, destroy);
694 // check to see if we should introduce a proxy
695 int aL = accum->litSize; // lits in accum
696 int eL = argExp->litSize; // lits in argument
697 int aC = getClauseSizeCNF(accum); // clauses in accum
698 int eC = getClauseSizeCNF(argExp); // clauses in argument
700 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
701 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
703 disjoinCNFExpr(accum, argExp, destroy);
704 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;