--- /dev/null
+#include "cnfexpr.h"
+
+#define LITCAPACITY 4
+#define MERGESIZE 5
+
+static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
+
+LitVector * allocLitVector() {
+ LitVector *This=ourmalloc(sizeof(LitVector));
+ initLitVector(This);
+ return This;
+}
+
+void initLitVector(LitVector *This) {
+ This->size=0;
+ This->capacity=LITCAPACITY;
+ This->literals=ourmalloc(This->capacity * sizeof(Literal));
+}
+
+LitVector *cloneLitVector(LitVector *orig) {
+ LitVector *This=ourmalloc(sizeof(LitVector));
+ This->size=orig->size;
+ This->capacity=orig->capacity;
+ This->literals=ourmalloc(This->capacity * sizeof(Literal));
+ memcpy(This->literals, orig->literals, sizeof(Literal) * This->size);
+ return This;
+}
+
+void clearLitVector(LitVector *This) {
+ This->size=0;
+}
+
+void freeLitVector(LitVector *This) {
+ ourfree(This->literals);
+}
+
+void deleteLitVector(LitVector *This) {
+ freeLitVector(This);
+ ourfree(This);
+}
+
+Literal getLiteralLitVector(LitVector *This, uint index) {
+ return This->literals[index];
+}
+
+void addLiteralLitVector(LitVector *This, Literal l) {
+ Literal labs = abs(l);
+ uint vec_size=This->size;
+ uint searchsize=boundedSize(vec_size);
+ uint i=0;
+ for (; i < searchsize; i++) {
+ Literal curr = This->literals[i];
+ Literal currabs = abs(curr);
+ if (currabs > labs)
+ break;
+ if (currabs == labs) {
+ if (curr == -l)
+ This->size = 0; //either true or false now depending on whether this is a conj or disj
+ return;
+ }
+ if ((++This->size) >= This->capacity) {
+ This->capacity <<= 1;
+ This->literals=ourrealloc(This->literals, This->capacity * sizeof(Literal));
+ }
+
+ if (vec_size < MERGESIZE) {
+ memmove(&This->literals[i+1], &This->literals[i], (vec_size-i) * sizeof(Literal));
+ This->literals[i]=l;
+ } else {
+ This->literals[vec_size]=l;
+ }
+ }
+}
+
+CNFExpr * allocCNFExprBool(bool isTrue) {
+ CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+ This->litSize=0;
+ This->isTrue=isTrue;
+ allocInlineVectorLitVector(&This->clauses, 2);
+ initLitVector(&This->singletons);
+ return This;
+}
+
+CNFExpr * allocCNFExprLiteral(Literal l) {
+ CNFExpr *This=ourmalloc(sizeof(CNFExpr));
+ This->litSize=1;
+ This->isTrue=false;
+ allocInlineVectorLitVector(&This->clauses, 2);
+ initLitVector(&This->singletons);
+ addLiteralLitVector(&This->singletons, l);
+ return This;
+}
+
+void clearCNFExpr(CNFExpr *This, bool isTrue) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
+ clearVectorLitVector(&This->clauses);
+ clearLitVector(&This->singletons);
+ This->litSize=0;
+ This->isTrue=isTrue;
+}
+
+void deleteCNFExpr(CNFExpr *This) {
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ deleteLitVector(getVectorLitVector(&This->clauses, i));
+ }
+ deleteVectorArrayLitVector(&This->clauses);
+ freeLitVector(&This->singletons);
+ ourfree(This);
+}
+
+void conjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0 && !This->isTrue) //Handle False
+ return;
+
+ This->litSize-=getSizeLitVector(&This->singletons);
+ addLiteralLitVector(&This->singletons, l);
+ uint newsize=getSizeLitVector(&This->singletons);
+ if (newsize==0)
+ clearCNF(This, false); //We found a conflict
+ else
+ This->litSize+=getSizeLitVector(&This->singletons);
+}
+
+void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ if (destroy) {
+ ourfree(This->singletons.literals);
+ ourfree(This->clauses.array);
+ This->litSize=expr->litSize;
+ This->singletons.literals=expr->singletons.literals;
+ This->singletons.capacity=expr->singletons.capacity;
+ This->clauses.size=expr->clauses.size;
+ This->clauses.array=expr->clauses.array;
+ This->clauses.capacity=expr->clauses.capacity;
+ ourfree(expr);
+ } else {
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ addLiteralLitVector(&This->singletons, l);
+ }
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+ }
+ This->litSize=expr->litSize;
+ }
+}
+
+void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ if (expr->litSize==0) {
+ if (!This->isTrue) {
+ clearCNF(This, false);
+ }
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ if (This->litSize==0) {
+ if (This->isTrue) {
+ copyCNF(This, expr, destroy);
+ } else if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ uint litSize=This->litSize;
+ litSize-=getSizeLitVector(&expr->singletons);
+ for(uint i=0;i<getSizeLitVector(&expr->singletons);i++) {
+ Literal l=getLiteralLitVector(&expr->singletons,i);
+ addLiteralLitVector(&This->singletons, l);
+ if (getSizeLitVector(&This->singletons)==0) {
+ //Found conflict...
+ clearCNF(This, false);
+ if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ }
+ litSize+=getSizeLitVector(&expr->singletons);
+ if (destroy) {
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ litSize+=getSizeLitVector(lv);
+ pushVectorLitVector(&This->clauses, lv);
+ }
+ clearVectorLitVector(&expr->clauses);
+ deleteCNFExpr(expr);
+ } else {
+ for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);i++) {
+ LitVector *lv=getVectorLitVector(&expr->clauses,i);
+ litSize+=getSizeLitVector(lv);
+ pushVectorLitVector(&This->clauses, cloneLitVector(lv));
+ }
+ }
+ This->litSize=litSize;
+}
+
+void disjoinCNFLit(CNFExpr *This, Literal l) {
+ if (This->litSize==0) {
+ if (!This->isTrue) {
+ This->litSize++;
+ addLiteralLitVector(&This->singletons, l);
+ }
+ return;
+ }
+
+ uint litSize=0;
+ uint newindex=0;
+ for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+ LitVector * lv=getVectorLitVector(&This->clauses, i);
+ addLiteralLitVector(lv, l);
+ uint newSize=getSizeLitVector(lv);
+ if (newSize!=0) {
+ setVectorLitVector(&This->clauses, newindex++, lv);
+ } else {
+ deleteLitVector(lv);
+ }
+ litSize+=newSize;
+ }
+ setSizeVectorLitVector(&This->clauses, newindex);
+
+ bool hasSameSingleton=false;
+ for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+ Literal lsing=getLiteralLitVector(&This->singletons, i);
+ if (lsing == l) {
+ hasSameSingleton=true;
+ } else if (lsing != -l) {
+ //Create new LitVector with both l and lsing
+ LitVector *newlitvec=allocLitVector();
+ addLiteralLitVector(newlitvec, l);
+ addLiteralLitVector(newlitvec, lsing);
+ litSize+=2;
+ pushVectorLitVector(&This->clauses, newlitvec);
+ }
+ }
+ clearLitVector(&This->singletons);
+ if (hasSameSingleton) {
+ addLiteralLitVector(&This->singletons, l);
+ litSize++;
+ } else if (litSize==0) {
+ This->isTrue=true;//we are true
+ }
+ This->litSize=litSize;
+}
+
+void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
+ if (expr->litSize == 0) {
+ if (expr->isTrue) {
+ clearCNF(This, true);
+ }
+ if (destroy)
+ deleteCNFExpr(expr);
+ return;
+ }
+ if (This->litSize == 0) {
+ if (!This->isTrue) {
+ copyCNF(This, expr, destroy);
+ } else if (destroy) {
+ deleteCNFExpr(expr);
+ }
+ return;
+ }
+ //Do big cross product computation
+ //FIXME
+
+
+}
+
+
+
--- /dev/null
+#include "nodeedge.h"
+#include <string.h>
+#include <stdlib.h>
+#include "inc_solver.h"
+#include "cnfexpr.h"
+
+/** Code ported from C++ BAT implementation of NICE-SAT */
+
+VectorImpl(Edge, Edge, 16)
+
+CNF * createCNF() {
+ CNF * cnf=ourmalloc(sizeof(CNF));
+ cnf->varcount=1;
+ cnf->capacity=DEFAULT_CNF_ARRAY_SIZE;
+ cnf->mask=cnf->capacity-1;
+ cnf->node_array=ourcalloc(1, sizeof(Node *)*cnf->capacity);
+ cnf->size=0;
+ cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
+ cnf->enableMatching=true;
+ allocInlineDefVectorEdge(& cnf->constraints);
+ allocInlineDefVectorEdge(& cnf->args);
+ return cnf;
+}
+
+void deleteCNF(CNF * cnf) {
+ for(uint i=0;i<cnf->capacity;i++) {
+ Node *n=cnf->node_array[i];
+ if (n!=NULL)
+ ourfree(n);
+ }
+ deleteVectorArrayEdge(& cnf->constraints);
+ deleteVectorArrayEdge(& cnf->args);
+ ourfree(cnf->node_array);
+ ourfree(cnf);
+}
+
+void resizeCNF(CNF *cnf, uint newCapacity) {
+ Node **old_array=cnf->node_array;
+ Node **new_array=ourcalloc(1, sizeof(Node *)*newCapacity);
+ uint oldCapacity=cnf->capacity;
+ uint newMask=newCapacity-1;
+ for(uint i=0;i<oldCapacity;i++) {
+ Node *n=old_array[i];
+ uint hashCode=n->hashCode;
+ uint newindex=hashCode & newMask;
+ for(;;newindex=(newindex+1) & newMask) {
+ if (new_array[newindex] == NULL) {
+ new_array[newindex]=n;
+ break;
+ }
+ }
+ }
+ ourfree(old_array);
+ cnf->node_array=new_array;
+ cnf->capacity=newCapacity;
+ cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
+ cnf->mask=newMask;
+}
+
+Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashcode) {
+ Node *n=(Node *)ourmalloc(sizeof(Node)+sizeof(Edge)*numEdges);
+ memcpy(n->edges, edges, sizeof(Edge)*numEdges);
+ n->flags.type=type;
+ n->flags.wasExpanded=0;
+ n->flags.cnfVisitedDown=0;
+ n->flags.cnfVisitedUp=0;
+ n->numEdges=numEdges;
+ n->hashCode=hashcode;
+ n->intAnnot[0]=0;n->intAnnot[1]=0;
+ n->ptrAnnot[0]=NULL;n->ptrAnnot[1]=NULL;
+ return n;
+}
+
+Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
+ if (cnf->size > cnf->maxsize) {
+ resizeCNF(cnf, cnf->capacity << 1);
+ }
+ uint hashvalue=hashNode(type, numEdges, edges);
+ uint mask=cnf->mask;
+ uint index=hashvalue & mask;
+ Node **n_ptr;
+ for(;;index=(index+1)&mask) {
+ n_ptr=&cnf->node_array[index];
+ if (*n_ptr!=NULL) {
+ if ((*n_ptr)->hashCode==hashvalue) {
+ if (compareNodes(*n_ptr, type, numEdges, edges)) {
+ Edge e={*n_ptr};
+ return e;
+ }
+ }
+ } else {
+ break;
+ }
+ }
+ *n_ptr=allocNode(type, numEdges, edges, hashvalue);
+ Edge e={*n_ptr};
+ return e;
+}
+
+uint hashNode(NodeType type, uint numEdges, Edge * edges) {
+ uint hashvalue=type ^ numEdges;
+ for(uint i=0;i<numEdges;i++) {
+ hashvalue ^= (uint) edges[i].node_ptr;
+ hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
+ }
+ return (uint) hashvalue;
+}
+
+bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges) {
+ if (node->flags.type!=type || node->numEdges != numEdges)
+ return false;
+ Edge *nodeedges=node->edges;
+ for(uint i=0;i<numEdges;i++) {
+ if (!equalsEdge(nodeedges[i], edges[i]))
+ return false;
+ }
+ return true;
+}
+
+Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges) {
+ Edge edgearray[numEdges];
+
+ for(uint i=0; i<numEdges; i++) {
+ edgearray[i]=constraintNegate(edges[i]);
+ }
+ Edge eand=constraintAND(cnf, numEdges, edgearray);
+ return constraintNegate(eand);
+}
+
+Edge constraintOR2(CNF * cnf, Edge left, Edge right) {
+ Edge lneg=constraintNegate(left);
+ Edge rneg=constraintNegate(right);
+ Edge eand=constraintAND2(cnf, left, right);
+ return constraintNegate(eand);
+}
+
+int comparefunction(const Edge * e1, const Edge * e2) {
+ return ((uintptr_t)e1->node_ptr)-((uintptr_t)e2->node_ptr);
+}
+
+Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges) {
+ qsort(edges, numEdges, sizeof(Edge), (int (*)(const void *, const void *)) comparefunction);
+ int initindex=0;
+ while(initindex<numEdges && equalsEdge(edges[initindex], E_True))
+ initindex++;
+
+ uint remainSize=numEdges-initindex;
+
+ if (remainSize == 0)
+ return E_True;
+ else if (remainSize == 1)
+ return edges[initindex];
+ else if (equalsEdge(edges[initindex], E_False))
+ return E_False;
+
+ /** De-duplicate array */
+ uint lowindex=0;
+ edges[lowindex++]=edges[initindex++];
+
+ for(;initindex<numEdges;initindex++) {
+ Edge e1=edges[lowindex];
+ Edge e2=edges[initindex];
+ if (sameNodeVarEdge(e1, e2)) {
+ if (!sameSignEdge(e1, e2)) {
+ return E_False;
+ }
+ } else
+ edges[lowindex++]=edges[initindex];
+ }
+ if (lowindex==1)
+ return edges[0];
+
+ if (cnf->enableMatching && lowindex==2 &&
+ isNegNodeEdge(edges[0]) && isNegNodeEdge(edges[1]) &&
+ getNodeType(edges[0]) == NodeType_AND &&
+ getNodeType(edges[1]) == NodeType_AND &&
+ getNodeSize(edges[0]) == 2 &&
+ getNodeSize(edges[1]) == 2) {
+ Edge * e0edges=getEdgeArray(edges[0]);
+ Edge * e1edges=getEdgeArray(edges[1]);
+ if (sameNodeOppSign(e0edges[0], e1edges[0])) {
+ return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+ } else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
+ return constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+ } else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
+ return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+ } else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
+ return constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+ }
+ }
+
+ return createNode(cnf, NodeType_AND, numEdges, edges);
+}
+
+Edge constraintAND2(CNF * cnf, Edge left, Edge right) {
+ Edge edges[2]={left, right};
+ return constraintAND(cnf, 2, edges);
+}
+
+Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
+ Edge array[2];
+ array[0]=left;
+ array[1]=constraintNegate(right);
+ Edge eand=constraintAND(cnf, 2, array);
+ return constraintNegate(eand);
+}
+
+Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
+ bool negate=sameSignEdge(left, right);
+ Edge lpos=getNonNeg(left);
+ Edge rpos=getNonNeg(right);
+
+ Edge e;
+ if (equalsEdge(lpos, rpos)) {
+ e=E_True;
+ } else if (ltEdge(lpos, rpos)) {
+ Edge edges[]={lpos, rpos};
+ e=(edgeIsConst(lpos)) ? rpos : createNode(cnf, NodeType_IFF, 2, edges);
+ } else {
+ Edge edges[]={rpos, lpos};
+ e=(edgeIsConst(rpos)) ? lpos : createNode(cnf, NodeType_IFF, 2, edges);
+ }
+ if (negate)
+ e=constraintNegate(e);
+ return e;
+}
+
+Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
+ if (isNegEdge(cond)) {
+ cond=constraintNegate(cond);
+ Edge tmp=thenedge;
+ thenedge=elseedge;
+ elseedge=tmp;
+ }
+
+ bool negate = isNegEdge(thenedge);
+ if (negate) {
+ thenedge=constraintNegate(thenedge);
+ elseedge=constraintNegate(elseedge);
+ }
+
+ Edge result;
+ if (equalsEdge(cond, E_True)) {
+ result=thenedge;
+ } else if (equalsEdge(thenedge, E_True) || equalsEdge(cond, thenedge)) {
+ result=constraintOR(cnf, 2, (Edge[]) {cond, elseedge});
+ } else if (equalsEdge(elseedge, E_True) || sameNodeOppSign(cond, elseedge)) {
+ result=constraintIMPLIES(cnf, cond, thenedge);
+ } else if (equalsEdge(thenedge, E_False) || equalsEdge(cond, elseedge)) {
+ result=constraintAND(cnf, 2, (Edge[]) {cond, thenedge});
+ } else if (equalsEdge(thenedge, elseedge)) {
+ result=thenedge;
+ } else if (sameNodeOppSign(thenedge, elseedge)) {
+ if (ltEdge(cond, thenedge)) {
+ result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {cond, thenedge});
+ } else {
+ result=createNode(cnf, NodeType_IFF, 2, (Edge[]) {thenedge, cond});
+ }
+ } else {
+ Edge edges[]={cond, thenedge, elseedge};
+ result=createNode(cnf, NodeType_ITE, 3, edges);
+ }
+ if (negate)
+ result=constraintNegate(result);
+ return result;
+}
+
+void addConstraint(CNF *cnf, Edge constraint) {
+ pushVectorEdge(&cnf->constraints, constraint);
+}
+
+Edge constraintNewVar(CNF *cnf) {
+ uint varnum=cnf->varcount++;
+ Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
+ return e;
+}
+
+void countPass(CNF *cnf) {
+ uint numConstraints=getSizeVectorEdge(&cnf->constraints);
+ VectorEdge *ve=allocDefVectorEdge();
+ for(uint i=0; i<numConstraints;i++) {
+ countConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i));
+ }
+ deleteVectorEdge(ve);
+}
+
+void countConstraint(CNF *cnf, VectorEdge *stack, Edge e) {
+ //Skip constants and variables...
+ if (edgeIsVarConst(e))
+ return;
+
+ clearVectorEdge(stack);pushVectorEdge(stack, e);
+
+ bool isMatching=cnf->enableMatching;
+
+ while(getSizeVectorEdge(stack) != 0) {
+ Edge e=lastVectorEdge(stack); popVectorEdge(stack);
+ bool polarity=isNegEdge(e);
+ Node *n=getNodePtrFromEdge(e);
+ if (getExpanded(n, polarity)) {
+ if (n->flags.type == NodeType_IFF ||
+ n->flags.type == NodeType_ITE) {
+ Edge pExp={n->ptrAnnot[polarity]};
+ getNodePtrFromEdge(pExp)->intAnnot[0]++;
+ } else {
+ n->intAnnot[polarity]++;
+ }
+ } else {
+ setExpanded(n, polarity); n->intAnnot[polarity]=1;
+
+ if (n->flags.type == NodeType_ITE||
+ n->flags.type == NodeType_IFF) {
+ n->intAnnot[polarity]=0;
+ Edge cond=n->edges[0];
+ Edge thenedge=n->edges[1];
+ Edge elseedge=n->flags.type == NodeType_IFF? constraintNegate(thenedge): n->edges[2];
+ thenedge=constraintNegateIf(thenedge, !polarity);
+ elseedge=constraintNegateIf(elseedge, !polarity);
+ thenedge=constraintAND2(cnf, cond, thenedge);
+ cond=constraintNegate(cond);
+ elseedge=constraintAND2(cnf, cond, elseedge);
+ thenedge=constraintNegate(thenedge);
+ elseedge=constraintNegate(elseedge);
+ cnf->enableMatching=false;
+ Edge succ1=constraintAND2(cnf, thenedge, elseedge);
+ n->ptrAnnot[polarity]=succ1.node_ptr;
+ cnf->enableMatching=isMatching;
+ pushVectorEdge(stack, succ1);
+ if (getExpanded(n, !polarity)) {
+ Edge succ2={(Node *)n->ptrAnnot[!polarity]};
+ Node *n1=getNodePtrFromEdge(succ1);
+ Node *n2=getNodePtrFromEdge(succ2);
+ n1->ptrAnnot[0]=succ2.node_ptr;
+ n2->ptrAnnot[0]=succ1.node_ptr;
+ n1->ptrAnnot[1]=succ2.node_ptr;
+ n2->ptrAnnot[1]=succ1.node_ptr;
+ }
+ } else {
+ for (uint i=0;i<n->numEdges;i++) {
+ Edge succ=n->edges[i];
+ succ=constraintNegateIf(succ, polarity);
+ if(!edgeIsVarConst(succ)) {
+ pushVectorEdge(stack, succ);
+ }
+ }
+ }
+ }
+ }
+}
+
+void convertPass(CNF *cnf, bool backtrackLit) {
+ uint numConstraints=getSizeVectorEdge(&cnf->constraints);
+ VectorEdge *ve=allocDefVectorEdge();
+ for(uint i=0; i<numConstraints;i++) {
+ convertConstraint(cnf, ve, getVectorEdge(&cnf->constraints, i), backtrackLit);
+ }
+ deleteVectorEdge(ve);
+}
+
+void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit) {
+ Node *nroot=getNodePtrFromEdge(root);
+
+ if (isNodeEdge(root) && (nroot->flags.type == NodeType_ITE || nroot->flags.type == NodeType_IFF)) {
+ root = (Edge) { (Node *) nroot->ptrAnnot[isNegEdge(root)]};
+ }
+
+ if (edgeIsConst(root)) {
+ if (isNegEdge(root)) {
+ //trivally unsat
+ Edge newvar=constraintNewVar(cnf);
+ Literal var=getEdgeVar(newvar);
+ Literal clause[] = {var, -var, 0};
+ addArrayClauseLiteral(cnf->solver, 3, clause);
+ return;
+ } else {
+ //trivially true
+ return;
+ }
+ } else if (edgeIsVarConst(root)) {
+ Literal clause[] = { getEdgeVar(root), 0};
+ addArrayClauseLiteral(cnf->solver, 2, clause);
+ return;
+ }
+
+ clearVectorEdge(stack);pushVectorEdge(stack, root);
+ while(getSizeVectorEdge(stack)!=0) {
+ Edge e=lastVectorEdge(stack);
+ Node *n=getNodePtrFromEdge(e);
+
+ if (edgeIsVarConst(e)) {
+ popVectorEdge(stack);
+ continue;
+ } else if (n->flags.type==NodeType_ITE ||
+ n->flags.type==NodeType_IFF) {
+ popVectorEdge(stack);
+ pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]});
+ pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[1]});
+ continue;
+ }
+
+ bool needPos = (n->intAnnot[0] > 0);
+ bool needNeg = (n->intAnnot[1] > 0);
+ if ((!needPos || n->flags.cnfVisitedUp & 1) ||
+ (!needNeg || n->flags.cnfVisitedUp & 2)) {
+ popVectorEdge(stack);
+ } else if ((needPos && !n->flags.cnfVisitedDown & 1) ||
+ (needNeg && !n->flags.cnfVisitedDown & 2)) {
+ if (needPos)
+ n->flags.cnfVisitedDown|=1;
+ if (needNeg)
+ n->flags.cnfVisitedDown|=2;
+ for(uint i=0; i<n->numEdges; i++) {
+ Edge arg=n->edges[i];
+ arg=constraintNegateIf(arg, isNegEdge(e));
+ pushVectorEdge(stack, arg); //WARNING, THIS LOOKS LIKE A BUG IN THE ORIGINAL CODE
+ }
+ } else {
+ popVectorEdge(stack);
+ produceCNF(cnf, e);
+ }
+ }
+ CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
+ if (isProxy(cnfExp)) {
+ //solver.add(getProxy(cnfExp))
+ } else if (backtrackLit) {
+ //solver.add(introProxy(solver, root, cnfExp, isNegEdge(root)));
+ } else {
+ //solver.add(*cnfExp);
+ }
+
+ if (!((intptr_t) cnfExp & 1)) {
+ //free rootExp
+ nroot->ptrAnnot[isNegEdge(root)] = NULL;
+ }
+}
+
+
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg) {
+ Literal l = 0;
+ Node * n = getNodePtrFromEdge(e);
+
+ if (n->flags.cnfVisitedUp & (1<<!isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) n->ptrAnnot[!isNeg];
+ if (isProxy(otherExp))
+ l = -getProxy(otherExp);
+ } else {
+ Edge semNeg={(Node *) n->ptrAnnot[isNeg]};
+ Node * nsemNeg=getNodePtrFromEdge(semNeg);
+ if (nsemNeg != NULL) {
+ if (nsemNeg->flags.cnfVisitedUp & (1 << isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[isNeg];
+ if (isProxy(otherExp))
+ l = -getProxy(otherExp);
+ } else if (nsemNeg->flags.cnfVisitedUp & (1<< !isNeg)) {
+ CNFExpr* otherExp = (CNFExpr*) nsemNeg->ptrAnnot[!isNeg];
+ if (isProxy(otherExp))
+ l = getProxy(otherExp);
+ }
+ }
+ }
+
+ if (l == 0) {
+ Edge newvar = constraintNewVar(cnf);
+ l = getEdgeVar(newvar);
+ }
+ // Output the constraints on the auxiliary variable
+ constrainCNF(cnf, l, exp);
+ deleteCNFExpr(exp);
+
+ n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
+
+ return l;
+}
+
+//DONE
+void produceCNF(CNF * cnf, Edge e) {
+ CNFExpr* expPos = NULL;
+ CNFExpr* expNeg = NULL;
+ Node *n = getNodePtrFromEdge(e);
+
+ if (n->intAnnot[0] > 0) {
+ expPos = produceConjunction(cnf, e);
+ }
+
+ if (n->intAnnot[1] > 0) {
+ expNeg = produceDisjunction(cnf, e);
+ }
+
+ /// @todo Propagate constants across semantic negations (this can
+ /// be done similarly to the calls to propagate shown below). The
+ /// trick here is that we need to figure out how to get the
+ /// semantic negation pointers, and ensure that they can have CNF
+ /// produced for them at the right point
+ ///
+ /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
+
+ // propagate from positive to negative, negative to positive
+ propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
+
+ // The polarity heuristic entails visiting the discovery polarity first
+ if (isPosEdge(e)) {
+ saveCNF(cnf, expPos, e, false);
+ saveCNF(cnf, expNeg, e, true);
+ } else {
+ saveCNF(cnf, expNeg, e, true);
+ saveCNF(cnf, expPos, e, false);
+ }
+}
+
+bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
+ if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
+ if (dest == NULL) {
+ dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ } else if (isProxy(dest)) {
+ bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ if (alwaysTrue) {
+ Literal clause[] = {getProxy(dest), 0};
+ addArrayClauseLiteral(cnf->solver, 2, clause);
+ } else {
+ Literal clause[] = {-getProxy(dest), 0};
+ addArrayClauseLiteral(cnf->solver, 2, clause);
+ }
+
+ dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ } else {
+ clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+ }
+ return true;
+ }
+ return false;
+}
+
+void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign) {
+ Node *n=getNodePtrFromEdge(e);
+ n->flags.cnfVisitedUp |= (1 << sign);
+ if (exp == NULL || isProxy(exp)) return;
+
+ if (exp->litSize == 1) {
+ Literal l = getLiteralLitVector(&exp->singletons, 0);
+ deleteCNFExpr(exp);
+ n->ptrAnnot[sign] = (void*) ((intptr_t) (l << 1) | 1);
+ } else if (exp->litSize != 0 && (n->intAnnot[sign] > 1 || n->flags.varForced)) {
+ introProxy(cnf, e, exp, sign);
+ } else {
+ n->ptrAnnot[sign] = exp;
+ }
+}
+
+void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp) {
+ if (alwaysTrueCNF(exp)) {
+ return;
+ } else if (alwaysFalseCNF(exp)) {
+ Literal clause[] = {-l, 0};
+ addArrayClauseLiteral(cnf->solver, 2, clause);
+ return;
+ }
+ //FIXME
+
+}
+
+void outputCNF(CNF *cnf, CNFExpr *exp) {
+
+}
+
+CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
+ clearVectorEdge(&cnf->args);
+
+ *largestEdge = (Edge) {(Node*) NULL};
+ CNFExpr* largest = NULL;
+ Node *n=getNodePtrFromEdge(e);
+ int i = n->numEdges;
+ while (i != 0) {
+ Edge arg = n->edges[--i]; arg=constraintNegateIf(arg, isNeg);
+ Node * narg = getNodePtrFromEdge(arg);
+
+ if (edgeIsVarConst(arg)) {
+ pushVectorEdge(&cnf->args, arg);
+ continue;
+ }
+
+ if (narg->flags.type == NodeType_ITE || narg->flags.type == NodeType_IFF) {
+ arg = (Edge) {(Node *) narg->ptrAnnot[isNegEdge(arg)]};
+ }
+
+ if (narg->intAnnot[isNegEdge(arg)] == 1) {
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+ if (!isProxy(argExp)) {
+ if (largest == NULL) {
+ largest = argExp;
+ * largestEdge = arg;
+ continue;
+ } else if (argExp->litSize > largest->litSize) {
+ pushVectorEdge(&cnf->args, *largestEdge);
+ largest = argExp;
+ * largestEdge = arg;
+ continue;
+ }
+ }
+ }
+ pushVectorEdge(&cnf->args, arg);
+ }
+
+ if (largest != NULL) {
+ Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
+ nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
+ }
+
+ return largest;
+}
+
+
+CNFExpr * produceConjunction(CNF * cnf, Edge e) {
+ Edge largestEdge;
+
+ CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
+ if (accum == NULL) accum = allocCNFExprBool(true);
+
+ int i = getSizeVectorEdge(&cnf->args);
+ while (i != 0) {
+ Edge arg = getVectorEdge(&cnf->args, --i);
+ if (edgeIsVarConst(arg)) {
+ conjoinCNFLit(accum, getEdgeVar(arg));
+ } else {
+ Node *narg=getNodePtrFromEdge(arg);
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
+ if (isProxy(argExp)) { // variable has been introduced
+ conjoinCNFLit(accum, getProxy(argExp));
+ } else {
+ conjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+ }
+ }
+ }
+
+ return accum;
+}
+
+#define CLAUSE_MAX 3
+
+CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
+ Edge largestEdge;
+ CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
+ if (accum == NULL)
+ accum = allocCNFExprBool(false);
+
+ // This is necessary to check to make sure that we don't start out
+ // with an accumulator that is "too large".
+
+ /// @todo Strictly speaking, introProxy doesn't *need* to free
+ /// memory, then this wouldn't have to reallocate CNFExpr
+
+ /// @todo When this call to introProxy is made, the semantic
+ /// negation pointer will have been destroyed. Thus, it will not
+ /// be possible to use the correct proxy. That should be fixed.
+
+ // at this point, we will either have NULL, or a destructible expression
+ if (getClauseSizeCNF(accum) > CLAUSE_MAX)
+ accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
+
+ int i = getSizeVectorEdge(&cnf->args);
+ while (i != 0) {
+ Edge arg=getVectorEdge(&cnf->args, --i);
+ Node *narg=getNodePtrFromEdge(arg);
+ if (edgeIsVarConst(arg)) {
+ disjoinCNFLit(accum, getEdgeVar(arg));
+ } else {
+ CNFExpr* argExp = (CNFExpr*) narg->ptrAnnot[isNegEdge(arg)];
+
+ bool destroy = (--narg->intAnnot[isNegEdge(arg)] == 0);
+ if (isProxy(argExp)) { // variable has been introduced
+ disjoinCNFLit(accum, getProxy(argExp));
+ } else if (argExp->litSize == 0) {
+ disjoinCNFExpr(accum, argExp, destroy);
+ } else {
+ // check to see if we should introduce a proxy
+ int aL = accum->litSize; // lits in accum
+ int eL = argExp->litSize; // lits in argument
+ int aC = getClauseSizeCNF(accum); // clauses in accum
+ int eC = getClauseSizeCNF(argExp); // clauses in argument
+
+ if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+ disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
+ } else {
+ disjoinCNFExpr(accum, argExp, destroy);
+ if (destroy) narg->ptrAnnot[isNegEdge(arg)] = NULL;
+ }
+ }
+ }
+ }
+
+ return accum;
+}
--- /dev/null
+#ifndef NODEEDGE_H
+#define NODEEDGE_H
+#include "classlist.h"
+#include "vector.h"
+
+#define NEGATE_EDGE 1
+#define EDGE_IS_VAR_CONSTANT 2
+#define VAR_SHIFT 2
+#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
+
+typedef int Literal;
+
+struct Edge;
+typedef struct Edge Edge;
+
+struct Node;
+typedef struct Node Node;
+
+struct Edge {
+ Node * node_ptr;
+};
+
+VectorDef(Edge, Edge)
+
+enum NodeType {
+ NodeType_AND,
+ NodeType_ITE,
+ NodeType_IFF
+};
+
+typedef enum NodeType NodeType;
+
+struct NodeFlags {
+ NodeType type:2;
+ int varForced:1;
+ int wasExpanded:2;
+ int cnfVisitedDown:2;
+ int cnfVisitedUp:2;
+};
+
+typedef struct NodeFlags NodeFlags;
+
+struct Node {
+ NodeFlags flags;
+ uint numEdges;
+ uint hashCode;
+ uint intAnnot[2];
+ void * ptrAnnot[2];
+ Edge edges[];
+};
+
+#define DEFAULT_CNF_ARRAY_SIZE 256
+#define LOAD_FACTOR 0.25
+
+struct CNF {
+ uint varcount;
+ uint capacity;
+ uint size;
+ uint mask;
+ uint maxsize;
+ bool enableMatching;
+ Node ** node_array;
+ IncrementalSolver * solver;
+ VectorEdge constraints;
+ VectorEdge args;
+};
+
+typedef struct CNF CNF;
+
+struct CNFExpr;
+typedef struct CNFExpr CNFExpr;
+
+static inline bool getExpanded(Node *n, int isNegated) {
+ return n->flags.wasExpanded & (1<<isNegated);
+}
+
+static inline void setExpanded(Node *n, int isNegated) {
+ n->flags.wasExpanded |= (1<<isNegated);
+}
+
+static inline Edge constraintNegate(Edge e) {
+ Edge enew = { (Node *) (((uintptr_t) e.node_ptr) ^ NEGATE_EDGE)};
+ return enew;
+}
+
+static inline bool sameNodeVarEdge(Edge e1, Edge e2) {
+ return ! (((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & (~ (uintptr_t) NEGATE_EDGE));
+}
+
+static inline bool sameSignEdge(Edge e1, Edge e2) {
+ return !(((uintptr_t) e1.node_ptr ^ (uintptr_t) e2.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool sameNodeOppSign(Edge e1, Edge e2) {
+ return (((uintptr_t) e1.node_ptr) ^ ((uintptr_t)e2.node_ptr)) == NEGATE_EDGE;
+}
+
+static inline bool isNegEdge(Edge e) {
+ return ((uintptr_t)e.node_ptr) & NEGATE_EDGE;
+}
+
+static inline bool isPosEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & NEGATE_EDGE);
+}
+
+static inline bool isNodeEdge(Edge e) {
+ return !(((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT);
+}
+
+static inline bool isNegNodeEdge(Edge e) {
+ return (((uintptr_t) e.node_ptr) & (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)) == NEGATE_EDGE;
+}
+
+static inline Node * getNodePtrFromEdge(Edge e) {
+ return (Node *) (((uintptr_t) e.node_ptr) & ~((uintptr_t) EDGE_MASK));
+}
+
+static inline NodeType getNodeType(Edge e) {
+ Node * n=getNodePtrFromEdge(e);
+ return n->flags.type;
+}
+
+static inline bool equalsEdge(Edge e1, Edge e2) {
+ return e1.node_ptr == e2.node_ptr;
+}
+
+static inline bool ltEdge(Edge e1, Edge e2) {
+ return (uintptr_t) e1.node_ptr < (uintptr_t) e2.node_ptr;
+}
+
+static inline uint getNodeSize(Edge e) {
+ Node * n=getNodePtrFromEdge(e);
+ return n->numEdges;
+}
+
+static inline Edge * getEdgeArray(Edge e) {
+ Node * n=getNodePtrFromEdge(e);
+ return n->edges;
+}
+
+static inline Edge getNonNeg(Edge e) {
+ Edge enew={(Node *)(((uintptr_t)e.node_ptr)&(~((uintptr_t)NEGATE_EDGE)))};
+ return enew;
+}
+
+static inline bool edgeIsConst(Edge e) {
+ return (((uintptr_t) e.node_ptr) & ~((uintptr_t)NEGATE_EDGE)) == EDGE_IS_VAR_CONSTANT;
+}
+
+static inline bool edgeIsVarConst(Edge e) {
+ return ((uintptr_t)e.node_ptr) & EDGE_IS_VAR_CONSTANT;
+}
+
+static inline Edge constraintNegateIf(Edge e, bool negate) {
+ Edge eret={(Node *)(((uintptr_t)e.node_ptr) ^ negate)};
+ return eret;
+}
+
+static inline Literal getEdgeVar(Edge e) {
+ int val = (int) (((uintptr_t) e.node_ptr) >> VAR_SHIFT);
+ return isNegEdge(e) ? -val : val;
+}
+
+static inline bool isProxy(CNFExpr *expr) {
+ return (bool) (((intptr_t) expr) & 1);
+}
+
+static inline Literal getProxy(CNFExpr *expr) {
+ return (Literal) (((intptr_t) expr) >> 1);
+}
+
+uint hashNode(NodeType type, uint numEdges, Edge * edges);
+Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
+bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
+Edge create(CNF *cnf, NodeType type, uint numEdges, Edge * edges);
+Edge constraintOR(CNF * cnf, uint numEdges, Edge *edges);
+Edge constraintAND(CNF * cnf, uint numEdges, Edge * edges);
+Edge constraintOR2(CNF * cnf, Edge left, Edge right);
+Edge constraintAND2(CNF * cnf, Edge left, Edge right);
+Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right);
+Edge constraintIFF(CNF * cnf, Edge left, Edge right);
+Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
+Edge constraintNewVar(CNF *cnf);
+void countPass(CNF *cnf);
+void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
+void convertPass(CNF *cnf, bool backtrackLit);
+void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
+void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
+void produceCNF(CNF * cnf, Edge e);
+CNFExpr * produceConjunction(CNF * cnf, Edge e);
+CNFExpr* produceDisjunction(CNF *cnf, Edge e);
+bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
+void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
+CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
+
+Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
+Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
+#endif
projects / satune.git / commitdiff