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);
24 void deleteCNF(CNF * cnf) {
25 for(uint i=0;i<cnf->capacity;i++) {
26 Node *n=cnf->node_array[i];
30 deleteVectorArrayEdge(& cnf->constraints);
31 ourfree(cnf->node_array);
35 void resizeCNF(CNF *cnf, uint newCapacity) {
36 Node **old_array=cnf->node_array;
37 Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
38 uint oldCapacity=cnf->capacity;
39 uint newMask=newCapacity-1;
40 for(uint i=0;i<oldCapacity;i++) {
42 uint hashCode=n->hashCode;
43 uint newindex=hashCode & newMask;
44 for(;;newindex=(newindex+1) & newMask) {
45 if (new_array[newindex] == NULL) {
46 new_array[newindex]=n;
52 cnf->node_array=new_array;
53 cnf->capacity=newCapacity;
54 cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
58 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
59 Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
60 memcpy(n->edges, edges, sizeof(Edge)*numEdges);
62 n->flags.wasExpanded=0;
63 n->flags.cnfVisitedDown=0;
64 n->flags.cnfVisitedUp=0;
67 n->intAnnot[0]=0;n->intAnnot[1]=0;
68 n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
72 Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
73 if (cnf->size > cnf->maxsize) {
74 resizeCNF(cnf, cnf->capacity << 1);
76 uint hashvalue=hashNode(type, numEdges, edges);
78 uint index=hashvalue & mask;
80 for(;;index=(index+1)&mask) {
81 n_ptr=&cnf->node_array[index];
83 if ((*n_ptr)->hashCode==hashvalue) {
84 if (compareNodes(*n_ptr, type, numEdges, edges)) {
93 *n_ptr=allocNode(type, numEdges, edges, hashvalue);
98 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
99 uint hashvalue=type ^ numEdges;
100 for(uint i=0;i<numEdges;i++) {
101 hashvalue ^= (uint) edges[i].node_ptr;
102 hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
104 return (uint) hashvalue;
107 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
108 if (node->flags.type!=type || node->numEdges != numEdges)
110 Edge *nodeedges=node->edges;
111 for(uint i=0;i<numEdges;i++) {
112 if (!equalsEdge(nodeedges[i], edges[i]))
118 Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
119 Edge edgearray[numEdges];
121 for(uint i=0; i<numEdges; i++) {
122 edgearray[i]=constraintNegate(edges[i]);
124 Edge eand=constraintAND(cnf, numEdges, edgearray);
125 return constraintNegate(eand);
128 Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
129 Edge lneg=constraintNegate(left);
130 Edge rneg=constraintNegate(right);
131 Edge eand=constraintAND2(cnf, left, right);
132 return constraintNegate(eand);
135 int comparefunction(const Edge * e1, const Edge * e2) {
136 return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
139 Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
140 qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
142 while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
145 uint remainSize=numEdges-initindex;
149 else if (remainSize == 1)
150 return edges[initindex];
151 else if (equalsEdge(edges[initindex], E_False))
154 /** De-duplicate array */
156 edges[lowindex++]=edges[initindex++];
158 for(;initindex<numEdges;initindex++) {
159 Edge e1=edges[lowindex];
160 Edge e2=edges[initindex];
161 if (sameNodeVarEdge(e1, e2)) {
162 if (!sameSignEdge(e1, e2)) {
166 edges[lowindex++]=edges[initindex];
171 if (cnf->enableMatching && lowindex==2 &&
172 isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
173 getNodeType(edges[0]) == NodeType_AND &&
174 getNodeType(edges[1]) == NodeType_AND &&
175 getNodeSize(edges[0]) == 2 &&
176 getNodeSize(edges[1]) == 2) {
177 Edge * e0edges=getEdgeArray(edges[0]);
178 Edge * e1edges=getEdgeArray(edges[1]);
179 if (sameNodeOppSign(e0edges[0], e1edges[0])) {
180 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
181 } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
182 return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
183 } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
184 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
185 } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
186 return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
190 return createNode(cnf, NodeType_AND, numEdges, edges);
193 Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
194 Edge edges[2]={left, right};
195 return constraintAND(cnf, 2, edges);
198 Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
201 array[1]=constraintNegate(right);
202 Edge eand=constraintAND(cnf, 2, array);
203 return constraintNegate(eand);
206 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
207 bool negate=sameSignEdge(left, right);
208 Edge lpos=getNonNeg(left);
209 Edge rpos=getNonNeg(right);
212 if (equalsEdge(lpos, rpos)) {
214 } else if (ltEdge(lpos, rpos)) {
215 Edge edges[]={lpos, rpos};
216 e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
218 Edge edges[]={rpos, lpos};
219 e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
222 e=constraintNegate(e);
226 Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
227 if (isNegEdge(cond)) {
228 cond=constraintNegate(cond);
234 bool negate = isNegEdge(thenedge);
236 thenedge=constraintNegate(thenedge);
237 elseedge=constraintNegate(elseedge);
241 if (equalsEdge(cond, E_True)) {
243 } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
244 result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
245 } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
246 result=constraintIMPLIES(cnf, cond, thenedge);
247 } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
248 result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
249 } else if (equalsEdge(thenedge, elseedge)) {
251 } else if (sameNodeOppSign(thenedge, elseedge)) {
252 if (ltEdge(cond, thenedge)) {
253 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
255 result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
258 Edge edges[]={cond, thenedge, elseedge};
259 result=createNode(cnf, NodeType_ITE, 3, edges);
262 result=constraintNegate(result);
266 void addConstraint(CNF *cnf, Edge constraint) {
267 pushVectorEdge(&cnf->constraints, constraint);
270 Edge constraintNewVar(CNF *cnf) {
271 uint varnum=cnf->varcount++;
272 Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
276 void countPass(CNF *cnf) {
277 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
278 VectorEdge *ve=allocDefVectorEdge();
279 for(uint i=0; i<numConstraints;i++) {
280 countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
282 deleteVectorEdge(ve);
285 void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
286 //Skip constants and variables...
287 if (edgeIsVarConst(e))
290 clearVectorEdge(stack);pushVectorEdge(stack, e);
292 bool isMatching=cnf->enableMatching;
294 while(getSizeVectorEdge(stack) != 0) {
295 Edge e=lastVectorEdge(stack); popVectorEdge(stack);
296 bool polarity=isNegEdge(e);
297 Node *n=getNodePtrFromEdge(e);
298 if (getExpanded(n, polarity)) {
299 if (n->flags.type == NodeType_IFF ||
300 n->flags.type == NodeType_ITE) {
301 Edge pExp={n->ptrAnnot[polarity]};
302 getNodePtrFromEdge(pExp)->intAnnot[0]++;
304 n->intAnnot[polarity]++;
307 setExpanded(n, polarity); n->intAnnot[polarity]=1;
309 if (n->flags.type == NodeType_ITE||
310 n->flags.type == NodeType_IFF) {
311 n->intAnnot[polarity]=0;
312 Edge cond=n->edges[0];
313 Edge thenedge=n->edges[1];
314 Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
315 thenedge=constraintNegateIf(thenedge, !polarity);
316 elseedge=constraintNegateIf(elseedge, !polarity);
317 thenedge=constraintAND2(cnf, cond, thenedge);
318 cond=constraintNegate(cond);
319 elseedge=constraintAND2(cnf, cond, elseedge);
320 thenedge=constraintNegate(thenedge);
321 elseedge=constraintNegate(elseedge);
322 cnf->enableMatching=false;
323 Edge succ1=constraintAND2(cnf, thenedge, elseedge);
324 n->ptrAnnot[polarity]=succ1.node_ptr;
325 cnf->enableMatching=isMatching;
326 pushVectorEdge(stack, succ1);
327 if (getExpanded(n, !polarity)) {
328 Edge succ2={(Node *)n->ptrAnnot[!polarity]};
329 Node *n1=getNodePtrFromEdge(succ1);
330 Node *n2=getNodePtrFromEdge(succ2);
331 n1->ptrAnnot[0]=succ2.node_ptr;
332 n2->ptrAnnot[0]=succ1.node_ptr;
333 n1->ptrAnnot[1]=succ2.node_ptr;
334 n2->ptrAnnot[1]=succ1.node_ptr;
337 for (uint i=0;i<n->numEdges;i++) {
338 Edge succ=n->edges[i];
339 succ=constraintNegateIf(succ, polarity);
340 if(!edgeIsVarConst(succ)) {
341 pushVectorEdge(stack, succ);
349 void convertPass(CNF *cnf, bool backtrackLit) {
350 uint numConstraints=getSizeVectorEdge(&cnf->constraints);
351 VectorEdge *ve=allocDefVectorEdge();
352 for(uint i=0; i<numConstraints;i++) {
353 convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
355 deleteVectorEdge(ve);
358 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
359 Node *nroot=getNodePtrFromEdge(root);
361 if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
362 root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
365 if (edgeIsConst(root)) {
366 if (isNegEdge(root)) {
368 Edge newvar=constraintNewVar(cnf);
369 Literal var=getEdgeVar(newvar);
370 Literal clause[] = {var, -var, 0};
371 addArrayClauseLiteral(cnf->solver, 3, clause);
377 } else if (edgeIsVarConst(root)) {
378 Literal clause[] = { getEdgeVar(root), 0};
379 addArrayClauseLiteral(cnf->solver, 2, clause);
383 clearVectorEdge(stack);pushVectorEdge(stack, root);
384 while(getSizeVectorEdge(stack)!=0) {
385 Edge e=lastVectorEdge(stack);
386 Node *n=getNodePtrFromEdge(e);
388 if (edgeIsVarConst(e)) {
389 popVectorEdge(stack);
391 } else if (n->flags.type==NodeType_ITE ||
392 n->flags.type==NodeType_IFF) {
393 popVectorEdge(stack);
394 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
395 pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
399 bool needPos = (n->intAnnot[0] > 0);
400 bool needNeg = (n->intAnnot[1] > 0);
401 if ((!needPos || n->flags.cnfVisitedUp & 1) ||
402 (!needNeg || n->flags.cnfVisitedUp & 2)) {
403 popVectorEdge(stack);
404 } else if ((needPos && !n->flags.cnfVisitedDown & 1) ||
405 (needNeg && !n->flags.cnfVisitedDown & 2)) {
407 n->flags.cnfVisitedDown|=1;
409 n->flags.cnfVisitedDown|=2;
410 for(uint i=0; i<n->numEdges; i++) {
411 Edge arg=n->edges[i];
412 arg=constraintNegateIf(arg, isNegEdge(e));
413 pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
416 popVectorEdge(stack);
420 CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
421 if (isProxy(cnfExp)) {
422 //solver.add(getProxy(cnfExp))
423 } else if (backtrackLit) {
424 //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
426 //solver.add(*cnfExp);
429 if (!((intptr_t) cnfExp & 1)) {
431 nroot->ptrAnnot[isNegEdge(root)] = NULL;
436 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
438 Node * n = getNodePtrFromEdge(e);
440 if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
441 CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
442 if (isProxy(otherExp))
443 l = -getProxy(otherExp);
445 Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
446 Node * nsemNeg=getNodePtrFromEdge(semNeg);
447 if (nsemNeg != NULL) {
448 if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
449 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
450 if (isProxy(otherExp))
451 l = -getProxy(otherExp);
452 } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
453 CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
454 if (isProxy(otherExp))
455 l = getProxy(otherExp);
461 Edge newvar = constraintNewVar(cnf);
462 l = getEdgeVar(newvar);
464 // Output the constraints on the auxiliary variable
465 constrainCNF(cnf, l, exp);
468 n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
474 void produceCNF(CNF * cnf, Edge e) {
475 CNFExpr* expPos = NULL;
476 CNFExpr* expNeg = NULL;
477 Node *n = getNodePtrFromEdge(e);
479 if (n->intAnnot[0] > 0) {
480 expPos = produceConjunction(cnf, e);
483 if (n->intAnnot[1] > 0) {
484 expNeg = produceDisjunction(cnf, e);
487 /// @todo Propagate constants across semantic negations (this can
488 /// be done similarly to the calls to propagate shown below). The
489 /// trick here is that we need to figure out how to get the
490 /// semantic negation pointers, and ensure that they can have CNF
491 /// produced for them at the right point
493 /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
495 // propagate from positive to negative, negative to positive
496 propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
498 // The polarity heuristic entails visiting the discovery polarity first
500 saveCNF(cnf, expPos, e, false);
501 saveCNF(cnf, expNeg, e, true);
503 saveCNF(cnf, expNeg, e, true);
504 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), 0};
518 addArrayClauseLiteral(cnf->solver, 2, clause);
520 Literal clause[] = {-getProxy(dest), 0};
521 addArrayClauseLiteral(cnf->solver, 2, clause);
524 dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
526 clearCNF(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 = exp->singletons()[0];
541 n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
542 } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->isVarForced())) {
543 introProxy(cnf, e, exp, sign);
545 n->ptrAnnot[sign] = exp;
549 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp) {
550 if (alwaysTrueCNF(exp)) {
552 } else if (alwaysFalseCNF(exp)) {
553 Literal clause[] = {-l, 0};
554 addArrayClauseLiteral(cnf->solver, 2, clause);
561 void outputCNF(CNF *cnf, CNFExpr *exp) {
565 CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
568 *largestEdge = (void*) NULL;
569 CNFExpr* largest = NULL;
572 Edge arg = (*e)[--i]; arg.negateIf(isNeg);
573 Node * narg = getNodePtrFromEdge(arg);
580 if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
581 arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
584 if (narg->intAnnot[isNegEdge(arg)] == 1) {
585 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
586 if (!isProxy(argExp)) {
587 if (largest == NULL) {
591 } else if (argExp->litSize > largest->litSize) {
592 args.push(* largestEdge);
602 if (largest != NULL) {
603 largestEdge->ptrAnnot(isNegEdge(*largestEdge)) = NULL;
610 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
612 CNFExpr* accum = fillArgs(e, false, largestEdge);
613 if (accum == NULL) accum = allocCNFExprBool(true);
615 int i = _args.size();
617 Edge arg(_args[--i]);
619 accum->conjoin(atomLit(arg));
621 CNFExpr* argExp = (CNFExpr*) arg->ptrAnnot(isNegEdge(arg));
623 bool destroy = (--arg->intAnnot(isNegEdge(arg)) == 0);
624 if (isProxy(argExp)) { // variable has been introduced
625 accum->conjoin(getProxy(argExp));
627 accum->conjoin(argExp, destroy);
628 if (destroy) arg->ptrAnnot(isNegEdge(arg)) = NULL;
638 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
640 CNFExpr* accum = fillArgs(e, true, largestEdge);
642 accum = allocCNFExprBool(false);
644 // This is necessary to check to make sure that we don't start out
645 // with an accumulator that is "too large".
647 /// @todo Strictly speaking, introProxy doesn't *need* to free
648 /// memory, then this wouldn't have to reallocate CNFExpr
650 /// @todo When this call to introProxy is made, the semantic
651 /// negation pointer will have been destroyed. Thus, it will not
652 /// be possible to use the correct proxy. That should be fixed.
654 // at this point, we will either have NULL, or a destructible expression
655 if (accum->clauseSize() > CLAUSE_MAX)
656 accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
658 int i = _args.size();
660 Edge arg(_args[--i]);
661 Node *narg=getNodePtrFromEdge(arg);
663 accum->disjoin(atomLit(arg));
665 CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
667 bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
668 if (isProxy(argExp)) { // variable has been introduced
669 accum->disjoin(getProxy(argExp));
670 } else if (argExp->litSize == 0) {
671 accum->disjoin(argExp, destroy);
673 // check to see if we should introduce a proxy
674 int aL = accum->litSize; // lits in accum
675 int eL = argExp->litSize; // lits in argument
676 int aC = getClauseSizeCNF(accum); // clauses in accum
677 int eC = getClauseSizeCNF(argExp); // clauses in argument
679 if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
680 accum->disjoin(introProxy(cnf, arg, argExp, isNegEdge(arg)));
682 accum->disjoin(argExp, destroy);
683 if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;