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);
320 finishedClauses(cnf->solver);
325 void countPass(CNF *cnf) {
326 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
327 VectorEdge *ve=allocDefVectorEdge();
328 for(uint i=0; i<numConstraints;i++) {
329 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
331 deleteVectorEdge(ve);
334 void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) {
335 //Skip constants and variables...
336 if (edgeIsVarConst(eroot))
339 clearVectorEdge(stack);pushVectorEdge(stack, eroot);
341 bool isMatching=cnf->enableMatching;
343 while(getSizeVectorEdge(stack) != 0) {
344 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
345 bool polarity=isNegEdge(e);
346 Node *n=getNodePtrFromEdge(e);
347 if (getExpanded(n, polarity)) {
348 if (n->flags.type == NodeType_IFF ||
349 n->flags.type == NodeType_ITE) {
350 Edge pExp={n->ptrAnnot[polarity]};
351 getNodePtrFromEdge(pExp)->intAnnot[0]++;
353 n->intAnnot[polarity]++;
356 setExpanded(n, polarity);
358 if (n->flags.type == NodeType_ITE||
359 n->flags.type == NodeType_IFF) {
360 n->intAnnot[polarity]=0;
361 Edge cond=n->edges[0];
362 Edge thenedge=n->edges[1];
363 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
364 thenedge=constraintNegateIf(thenedge, !polarity);
365 elseedge=constraintNegateIf(elseedge, !polarity);
366 thenedge=constraintAND2(cnf, cond, thenedge);
367 cond=constraintNegate(cond);
368 elseedge=constraintAND2(cnf, cond, elseedge);
369 thenedge=constraintNegate(thenedge);
370 elseedge=constraintNegate(elseedge);
371 cnf->enableMatching=false;
372 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
373 n->ptrAnnot[polarity]=succ1.node_ptr;
374 cnf->enableMatching=isMatching;
375 pushVectorEdge(stack, succ1);
376 if (getExpanded(n, !polarity)) {
377 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
378 Node *n1=getNodePtrFromEdge(succ1);
379 Node *n2=getNodePtrFromEdge(succ2);
380 n1->ptrAnnot[0]=succ2.node_ptr;
381 n2->ptrAnnot[0]=succ1.node_ptr;
382 n1->ptrAnnot[1]=succ2.node_ptr;
383 n2->ptrAnnot[1]=succ1.node_ptr;
386 n->intAnnot[polarity]=1;
387 for (uint i=0;i<n->numEdges;i++) {
388 Edge succ=n->edges[i];
389 succ=constraintNegateIf(succ, polarity);
390 if(!edgeIsVarConst(succ)) {
391 pushVectorEdge(stack, succ);
399 void convertPass(CNF *cnf, bool backtrackLit) {
400 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
401 VectorEdge *ve=allocDefVectorEdge();
402 for(uint i=0; i<numConstraints;i++) {
403 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
405 deleteVectorEdge(ve);
408 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
409 Node *nroot=getNodePtrFromEdge(root);
411 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
412 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
415 if (edgeIsConst(root)) {
416 if (isNegEdge(root)) {
418 Edge newvar=constraintNewVar(cnf);
419 Literal var=getEdgeVar(newvar);
420 Literal clause[] = {var};
421 addArrayClauseLiteral(cnf->solver, 1, clause);
423 addArrayClauseLiteral(cnf->solver, 1, clause);
429 } else if (edgeIsVarConst(root)) {
430 Literal clause[] = { getEdgeVar(root)};
431 addArrayClauseLiteral(cnf->solver, 1, clause);
435 clearVectorEdge(stack);pushVectorEdge(stack, root);
436 while(getSizeVectorEdge(stack)!=0) {
437 Edge e=lastVectorEdge(stack);
438 Node *n=getNodePtrFromEdge(e);
440 if (edgeIsVarConst(e)) {
441 popVectorEdge(stack);
443 } else if (n->flags.type==NodeType_ITE ||
444 n->flags.type==NodeType_IFF) {
445 popVectorEdge(stack);
446 if (n->ptrAnnot[0]!=NULL)
447 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
448 if (n->ptrAnnot[1]!=NULL)
449 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
453 bool needPos = (n->intAnnot[0] > 0);
454 bool needNeg = (n->intAnnot[1] > 0);
455 if ((!needPos || n->flags.cnfVisitedUp & 1) &&
456 (!needNeg || n->flags.cnfVisitedUp & 2)) {
457 popVectorEdge(stack);
458 } else if ((needPos && !(n->flags.cnfVisitedDown & 1)) ||
459 (needNeg && !(n->flags.cnfVisitedDown & 2))) {
461 n->flags.cnfVisitedDown|=1;
463 n->flags.cnfVisitedDown|=2;
464 for(uint i=0; i<n->numEdges; i++) {
465 Edge arg=n->edges[i];
466 arg=constraintNegateIf(arg, isNegEdge(e));
467 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
470 popVectorEdge(stack);
474 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
475 if (isProxy(cnfExp)) {
476 Literal l=getProxy(cnfExp);
477 Literal clause[] = {l};
478 addArrayClauseLiteral(cnf->solver, 1, clause);
479 } else if (backtrackLit) {
480 Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root));
481 Literal clause[] = {l};
482 addArrayClauseLiteral(cnf->solver, 1, clause);
484 outputCNF(cnf, cnfExp);
487 if (!((intptr_t) cnfExp & 1)) {
488 deleteCNFExpr(cnfExp);
489 nroot->ptrAnnot[isNegEdge(root)] = NULL;
494 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
496 Node * n = getNodePtrFromEdge(e);
498 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
499 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
500 if (isProxy(otherExp))
501 l = -getProxy(otherExp);
503 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
504 Node * nsemNeg=getNodePtrFromEdge(semNeg);
505 if (nsemNeg != NULL) {
506 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
507 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
508 if (isProxy(otherExp))
509 l = -getProxy(otherExp);
510 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
511 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
512 if (isProxy(otherExp))
513 l = getProxy(otherExp);
519 Edge newvar = constraintNewVar(cnf);
520 l = getEdgeVar(newvar);
522 // Output the constraints on the auxiliary variable
523 constrainCNF(cnf, l, exp);
526 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
531 void produceCNF(CNF * cnf, Edge e) {
532 CNFExpr* expPos = NULL;
533 CNFExpr* expNeg = NULL;
534 Node *n = getNodePtrFromEdge(e);
536 if (n->intAnnot[0] > 0) {
537 expPos = produceConjunction(cnf, e);
540 if (n->intAnnot[1] > 0) {
541 expNeg = produceDisjunction(cnf, e);
544 /// @todo Propagate constants across semantic negations (this can
545 /// be done similarly to the calls to propagate shown below). The
546 /// trick here is that we need to figure out how to get the
547 /// semantic negation pointers, and ensure that they can have CNF
548 /// produced for them at the right point
550 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
552 // propagate from positive to negative, negative to positive
553 if (!propagate(cnf, & expPos, expNeg, true))
554 propagate(cnf, & expNeg, expPos, true);
556 // The polarity heuristic entails visiting the discovery polarity first
558 saveCNF(cnf, expPos, e, false);
559 saveCNF(cnf, expNeg, e, true);
561 saveCNF(cnf, expNeg, e, true);
562 saveCNF(cnf, expPos, e, false);
566 bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
567 if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
569 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
570 } else if (isProxy(*dest)) {
571 bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
573 Literal clause[] = {getProxy(*dest)};
574 addArrayClauseLiteral(cnf->solver, 1, clause);
576 Literal clause[] = {-getProxy(*dest)};
577 addArrayClauseLiteral(cnf->solver, 1, clause);
580 *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
582 clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
589 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
590 Node *n=getNodePtrFromEdge(e);
591 n->flags.cnfVisitedUp |= (1 << sign);
592 if (exp == NULL || isProxy(exp)) return;
594 if (exp->litSize == 1) {
595 Literal l = getLiteralLitVector(&exp->singletons, 0);
597 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
598 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
599 introProxy(cnf, e, exp, sign);
601 n->ptrAnnot[sign] = exp;
605 void constrainCNF(CNF * cnf, Literal lcond, CNFExpr *expr) {
606 if (alwaysTrueCNF(expr)) {
608 } else if (alwaysFalseCNF(expr)) {
609 Literal clause[] = {-lcond};
610 addArrayClauseLiteral(cnf->solver, 1, clause);
614 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
615 Literal l=getLiteralLitVector(&expr->singletons,i);
616 Literal clause[] = {-lcond, l};
617 addArrayClauseLiteral(cnf->solver, 1, clause);
619 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
620 LitVector *lv=getVectorLitVector(&expr->clauses,i);
621 addClauseLiteral(cnf->solver, -lcond); //Add first literal
622 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest
626 void outputCNF(CNF *cnf, CNFExpr *expr) {
627 for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
628 Literal l=getLiteralLitVector(&expr->singletons,i);
629 Literal clause[] = {l};
630 addArrayClauseLiteral(cnf->solver, 1, clause);
632 for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
633 LitVector *lv=getVectorLitVector(&expr->clauses,i);
634 addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals);
638 CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
639 clearVectorEdge(&cnf->args);
641 *largestEdge = (Edge) {(Node*) NULL};
642 CNFExpr* largest = NULL;
643 Node *n=getNodePtrFromEdge(e);
646 Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
647 Node * narg = getNodePtrFromEdge(arg);
649 if (edgeIsVarConst(arg)) {
650 pushVectorEdge(&cnf->args, arg);
654 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
655 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
658 if (narg->intAnnot[isNegEdge(arg)] == 1) {
659 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
660 if (!isProxy(argExp)) {
661 if (largest == NULL) {
665 } else if (argExp->litSize > largest->litSize) {
666 pushVectorEdge(&cnf->args, *largestEdge);
673 pushVectorEdge(&cnf->args, arg);
676 if (largest != NULL) {
677 Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
678 nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
685 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
688 CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
689 if (accum == NULL) accum = allocCNFExprBool(true);
691 int i = getSizeVectorEdge(&cnf->args);
693 Edge arg = getVectorEdge(&cnf->args, --i);
694 if (edgeIsVarConst(arg)) {
695 conjoinCNFLit(accum, getEdgeVar(arg));
697 Node *narg=getNodePtrFromEdge(arg);
698 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
700 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
701 if (isProxy(argExp)) { // variable has been introduced
702 conjoinCNFLit(accum, getProxy(argExp));
704 conjoinCNFExpr(accum, argExp, destroy);
705 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
715 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
717 CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
719 accum = allocCNFExprBool(false);
721 // This is necessary to check to make sure that we don't start out
722 // with an accumulator that is "too large".
724 /// @todo Strictly speaking, introProxy doesn't *need* to free
725 /// memory, then this wouldn't have to reallocate CNFExpr
727 /// @todo When this call to introProxy is made, the semantic
728 /// negation pointer will have been destroyed. Thus, it will not
729 /// be possible to use the correct proxy. That should be fixed.
731 // at this point, we will either have NULL, or a destructible expression
732 if (getClauseSizeCNF(accum) > CLAUSE_MAX)
733 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
735 int i = getSizeVectorEdge(&cnf->args);
737 Edge arg=getVectorEdge(&cnf->args, --i);
738 Node *narg=getNodePtrFromEdge(arg);
739 if (edgeIsVarConst(arg)) {
740 disjoinCNFLit(accum, getEdgeVar(arg));
742 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
744 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
745 if (isProxy(argExp)) { // variable has been introduced
746 disjoinCNFLit(accum, getProxy(argExp));
747 } else if (argExp->litSize == 0) {
748 disjoinCNFExpr(accum, argExp, destroy);
750 // check to see if we should introduce a proxy
751 int aL = accum->litSize; // lits in accum
752 int eL = argExp->litSize; // lits in argument
753 int aC = getClauseSizeCNF(accum); // clauses in accum
754 int eC = getClauseSizeCNF(argExp); // clauses in argument
756 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
757 disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
759 disjoinCNFExpr(accum, argExp, destroy);
760 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;