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 void solveCNF(CNF *cnf) {
319 convertPass(cnf, false);
324 void countPass(CNF *cnf) {
325 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
326 VectorEdge *ve=allocDefVectorEdge();
327 for(uint i=0; i<numConstraints;i++) {
328 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
330 deleteVectorEdge(ve);
333 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
334 //Skip constants and variables...
335 if (edgeIsVarConst(eroot))
338 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
340 bool isMatching=cnf->enableMatching;
342 while(getSizeVectorEdge(stack) != 0) {
343 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
344 bool polarity=isNegEdge(e);
345 Node *n=getNodePtrFromEdge(e);
346 if (getExpanded(n, polarity)) {
347 if (n->flags.type == NodeType_IFF ||
348 n->flags.type == NodeType_ITE) {
349 Edge pExp={n->ptrAnnot[polarity]};
350 getNodePtrFromEdge(pExp)->intAnnot[0]++;
352 n->intAnnot[polarity]++;
355 setExpanded(n, polarity);
357 if (n->flags.type == NodeType_ITE||
358 n->flags.type == NodeType_IFF) {
359 n->intAnnot[polarity]=0;
360 Edge cond=n->edges[0];
361 Edge thenedge=n->edges[1];
362 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
363 thenedge=constraintNegateIf(thenedge, !polarity);
364 elseedge=constraintNegateIf(elseedge, !polarity);
365 thenedge=constraintAND2(cnf, cond, thenedge);
366 cond=constraintNegate(cond);
367 elseedge=constraintAND2(cnf, cond, elseedge);
368 thenedge=constraintNegate(thenedge);
369 elseedge=constraintNegate(elseedge);
370 cnf->enableMatching=false;
371 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
372 n->ptrAnnot[polarity]=succ1.node_ptr;
373 cnf->enableMatching=isMatching;
374 pushVectorEdge(stack, succ1);
375 if (getExpanded(n, !polarity)) {
376 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
377 Node *n1=getNodePtrFromEdge(succ1);
378 Node *n2=getNodePtrFromEdge(succ2);
379 n1->ptrAnnot[0]=succ2.node_ptr;
380 n2->ptrAnnot[0]=succ1.node_ptr;
381 n1->ptrAnnot[1]=succ2.node_ptr;
382 n2->ptrAnnot[1]=succ1.node_ptr;
385 n->intAnnot[polarity]=1;
386 for (uint i=0;i<n->numEdges;i++) {
387 Edge succ=n->edges[i];
388 succ=constraintNegateIf(succ, polarity);
389 if(!edgeIsVarConst(succ)) {
390 pushVectorEdge(stack, succ);
398 void convertPass(CNF *cnf, bool backtrackLit) {
399 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
400 VectorEdge *ve=allocDefVectorEdge();
401 for(uint i=0; i<numConstraints;i++) {
402 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
404 deleteVectorEdge(ve);
407 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
408 Node *nroot=getNodePtrFromEdge(root);
410 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
411 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
414 if (edgeIsConst(root)) {
415 if (isNegEdge(root)) {
417 Edge newvar=constraintNewVar(cnf);
418 Literal var=getEdgeVar(newvar);
419 Literal clause[] = {var};
420 addArrayClauseLiteral(cnf->solver, 1, clause);
422 addArrayClauseLiteral(cnf->solver, 1, clause);
428 } else if (edgeIsVarConst(root)) {
429 Literal clause[] = { getEdgeVar(root)};
430 addArrayClauseLiteral(cnf->solver, 1, clause);
434 clearVectorEdge(stack);pushVectorEdge(stack, root);
435 while(getSizeVectorEdge(stack)!=0) {
436 Edge e=lastVectorEdge(stack);
437 Node *n=getNodePtrFromEdge(e);
439 if (edgeIsVarConst(e)) {
440 popVectorEdge(stack);
442 } else if (n->flags.type==NodeType_ITE ||
443 n->flags.type==NodeType_IFF) {
444 popVectorEdge(stack);
445 if (n->ptrAnnot[0]!=NULL)
446 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
447 if (n->ptrAnnot[1]!=NULL)
448 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
452 bool needPos = (n->intAnnot[0] > 0);
453 bool needNeg = (n->intAnnot[1] > 0);
454 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
455 (!needNeg || n->flags.cnfVisitedUp & 2)) {
456 popVectorEdge(stack);
457 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
458 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
460 n->flags.cnfVisitedDown|=1;
462 n->flags.cnfVisitedDown|=2;
463 for(uint i=0; i<n->numEdges; i++) {
464 Edge arg=n->edges[i];
465 arg=constraintNegateIf(arg, isNegEdge(e));
466 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
469 popVectorEdge(stack);
473 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
474 if (isProxy(cnfExp)) {
475 Literal l=getProxy(cnfExp);
476 Literal clause[] = {l};
477 addArrayClauseLiteral(cnf->solver, 1, clause);
478 } else if (backtrackLit) {
479 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
480 Literal clause[] = {l};
481 addArrayClauseLiteral(cnf->solver, 1, clause);
483 outputCNF(cnf, cnfExp);
486 if (!((intptr_t) cnfExp & 1)) {
487 deleteCNFExpr(cnfExp);
488 nroot->ptrAnnot[isNegEdge(root)] = NULL;
493 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
495 Node * n = getNodePtrFromEdge(e);
497 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
498 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
499 if (isProxy(otherExp))
500 l = -getProxy(otherExp);
502 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
503 Node * nsemNeg=getNodePtrFromEdge(semNeg);
504 if (nsemNeg != NULL) {
505 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
506 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
507 if (isProxy(otherExp))
508 l = -getProxy(otherExp);
509 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
510 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
511 if (isProxy(otherExp))
512 l = getProxy(otherExp);
518 Edge newvar = constraintNewVar(cnf);
519 l = getEdgeVar(newvar);
521 // Output the constraints on the auxiliary variable
522 constrainCNF(cnf, l, exp);
525 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
530 void produceCNF(CNF * cnf, Edge e) {
531 CNFExpr* expPos = NULL;
532 CNFExpr* expNeg = NULL;
533 Node *n = getNodePtrFromEdge(e);
535 if (n->intAnnot[0] > 0) {
536 expPos = produceConjunction(cnf, e);
539 if (n->intAnnot[1] > 0) {
540 expNeg = produceDisjunction(cnf, e);
543 /// @todo Propagate constants across semantic negations (this can
544 /// be done similarly to the calls to propagate shown below). The
545 /// trick here is that we need to figure out how to get the
546 /// semantic negation pointers, and ensure that they can have CNF
547 /// produced for them at the right point
549 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
551 // propagate from positive to negative, negative to positive
552 if (!propagate(cnf, & expPos, expNeg, true))
553 propagate(cnf, & expNeg, expPos, true);
555 // The polarity heuristic entails visiting the discovery polarity first
557 saveCNF(cnf, expPos, e, false);
558 saveCNF(cnf, expNeg, e, true);
560 saveCNF(cnf, expNeg, e, true);
561 saveCNF(cnf, expPos, e, false);
565 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
566 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
568 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
569 } else if (isProxy(*dest)) {
570 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
572 Literal clause[] = {getProxy(*dest)};
573 addArrayClauseLiteral(cnf->solver, 1, clause);
575 Literal clause[] = {-getProxy(*dest)};
576 addArrayClauseLiteral(cnf->solver, 1, clause);
579 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
581 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
588 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
589 Node *n=getNodePtrFromEdge(e);
590 n->flags.cnfVisitedUp |= (1 << sign);
591 if (exp == NULL || isProxy(exp)) return;
593 if (exp->litSize == 1) {
594 Literal l = getLiteralLitVector(&exp->singletons, 0);
596 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
597 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
598 introProxy(cnf, e, exp, sign);
600 n->ptrAnnot[sign] = exp;
604 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
605 if (alwaysTrueCNF(expr)) {
607 } else if (alwaysFalseCNF(expr)) {
608 Literal clause[] = {-lcond};
609 addArrayClauseLiteral(cnf->solver, 1, clause);
613 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
614 Literal l=getLiteralLitVector(&expr->singletons,i);
615 Literal clause[] = {-lcond, l};
616 addArrayClauseLiteral(cnf->solver, 1, clause);
618 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
619 LitVector *lv=getVectorLitVector(&expr->clauses,i);
620 addClauseLiteral(cnf->solver, -lcond); //Add first literal
621 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
625 void outputCNF(CNF *cnf, CNFExpr *expr) {
626 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
627 Literal l=getLiteralLitVector(&expr->singletons,i);
628 Literal clause[] = {l};
629 addArrayClauseLiteral(cnf->solver, 1, clause);
631 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
632 LitVector *lv=getVectorLitVector(&expr->clauses,i);
633 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
637 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
638 clearVectorEdge(&cnf->args);
640 *largestEdge = (Edge) {(Node*) NULL};
641 CNFExpr* largest = NULL;
642 Node *n=getNodePtrFromEdge(e);
645 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
646 Node * narg = getNodePtrFromEdge(arg);
648 if (edgeIsVarConst(arg)) {
649 pushVectorEdge(&cnf->args, arg);
653 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
654 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
657 if (narg->intAnnot[isNegEdge(arg)] == 1) {
658 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
659 if (!isProxy(argExp)) {
660 if (largest == NULL) {
664 } else if (argExp->litSize > largest->litSize) {
665 pushVectorEdge(&cnf->args, *largestEdge);
672 pushVectorEdge(&cnf->args, arg);
675 if (largest != NULL) {
676 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
677 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
684 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
687 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
688 if (accum == NULL) accum = allocCNFExprBool(true);
690 int i = getSizeVectorEdge(&cnf->args);
692 Edge arg = getVectorEdge(&cnf->args, --i);
693 if (edgeIsVarConst(arg)) {
694 conjoinCNFLit(accum, getEdgeVar(arg));
696 Node *narg=getNodePtrFromEdge(arg);
697 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
699 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
700 if (isProxy(argExp)) { // variable has been introduced
701 conjoinCNFLit(accum, getProxy(argExp));
703 conjoinCNFExpr(accum, argExp, destroy);
704 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
714 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
716 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
718 accum = allocCNFExprBool(false);
720 // This is necessary to check to make sure that we don't start out
721 // with an accumulator that is "too large".
723 /// @todo Strictly speaking, introProxy doesn't *need* to free
724 /// memory, then this wouldn't have to reallocate CNFExpr
726 /// @todo When this call to introProxy is made, the semantic
727 /// negation pointer will have been destroyed. Thus, it will not
728 /// be possible to use the correct proxy. That should be fixed.
730 // at this point, we will either have NULL, or a destructible expression
731 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
732 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
734 int i = getSizeVectorEdge(&cnf->args);
736 Edge arg=getVectorEdge(&cnf->args, --i);
737 Node *narg=getNodePtrFromEdge(arg);
738 if (edgeIsVarConst(arg)) {
739 disjoinCNFLit(accum, getEdgeVar(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 disjoinCNFLit(accum, getProxy(argExp));
746 } else if (argExp->litSize == 0) {
747 disjoinCNFExpr(accum, argExp, destroy);
749 // check to see if we should introduce a proxy
750 int aL = accum->litSize; // lits in accum
751 int eL = argExp->litSize; // lits in argument
752 int aC = getClauseSizeCNF(accum); // clauses in accum
753 int eC = getClauseSizeCNF(argExp); // clauses in argument
755 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
756 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
758 disjoinCNFExpr(accum, argExp, destroy);
759 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;