From: Hamed Date: Mon, 10 Jul 2017 20:56:45 +0000 (-0700) Subject: Merge branch 'brian' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=67de286d5d94420d14a9f7910b78e7271a65a842;hp=c0e5beecb1d6ca75881cb4972642305ce607699f;p=satune.git Merge branch 'brian' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into hamed Because of memory bugs that vector had --- diff --git a/papers/10.1007-978-3-642-12002-2_10.pdf b/papers/10.1007-978-3-642-12002-2_10.pdf new file mode 100644 index 0000000..a5a6a9a Binary files /dev/null and b/papers/10.1007-978-3-642-12002-2_10.pdf differ diff --git a/papers/428811198-MIT.pdf b/papers/428811198-MIT.pdf new file mode 100644 index 0000000..1ac8c61 Binary files /dev/null and b/papers/428811198-MIT.pdf differ diff --git a/papers/CNF_unobservable.pdf b/papers/CNF_unobservable.pdf new file mode 100644 index 0000000..18e57f0 Binary files /dev/null and b/papers/CNF_unobservable.pdf differ diff --git a/papers/date09.pdf b/papers/date09.pdf new file mode 100644 index 0000000..a86110b Binary files /dev/null and b/papers/date09.pdf differ diff --git a/papers/sat-cnf.pdf b/papers/sat-cnf.pdf new file mode 100644 index 0000000..fe4ebec Binary files /dev/null and b/papers/sat-cnf.pdf differ diff --git a/papers/sat04-bc-conv.pdf b/papers/sat04-bc-conv.pdf new file mode 100644 index 0000000..85daef6 Binary files /dev/null and b/papers/sat04-bc-conv.pdf differ diff --git a/papers/tech08_sat.pdf b/papers/tech08_sat.pdf new file mode 100644 index 0000000..a9af157 Binary files /dev/null and b/papers/tech08_sat.pdf differ diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c new file mode 100644 index 0000000..6bbbbfc --- /dev/null +++ b/src/Backend/cnfexpr.c @@ -0,0 +1,449 @@ +#include "cnfexpr.h" + +/* +V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios, +Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon. + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be +included in all copies or substantial portions of the Software. If +you download or use the software, send email to Pete Manolios +(pete@ccs.neu.edu) with your name, contact information, and a short +note describing what you want to use BAT for. For any reuse or +distribution, you must make clear to others the license terms of this +work. + +Contact Pete Manolios if you want any of these conditions waived. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +*/ + +/* +C port of CNF SAT Conversion Copyright Brian Demsky 2017. +*/ + +#define LITCAPACITY 4 +#define MERGESIZE 5 + +VectorImpl(LitVector, LitVector *, 4) + +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 setLiteralLitVector(LitVector *This, uint index, Literal l) { + This->literals[index]=l; +} + +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;iclauses);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;iclauses);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) + clearCNFExpr(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;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + addLiteralLitVector(&This->singletons, l); + } + for(uint i=0;iclauses);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) { + clearCNFExpr(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;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + addLiteralLitVector(&This->singletons, l); + if (getSizeLitVector(&This->singletons)==0) { + //Found conflict... + clearCNFExpr(This, false); + if (destroy) { + deleteCNFExpr(expr); + } + return; + } + } + litSize+=getSizeLitVector(&expr->singletons); + if (destroy) { + for(uint i=0;iclauses);i++) { + LitVector *lv=getVectorLitVector(&expr->clauses,i); + litSize+=getSizeLitVector(lv); + pushVectorLitVector(&This->clauses, lv); + } + clearVectorLitVector(&expr->clauses); + deleteCNFExpr(expr); + } else { + for(uint i=0;iclauses);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;iclauses);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;isingletons);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; +} + +#define MERGETHRESHOLD 2 +LitVector * mergeLitVectors(LitVector *This, LitVector *expr) { + uint maxsize=This->size+expr->size+MERGETHRESHOLD; + LitVector *merged=ourmalloc(sizeof(LitVector)); + merged->literals=ourmalloc(sizeof(Literal)*maxsize); + merged->capacity=maxsize; + uint thisSize=boundedSize(This->size); + uint exprSize=boundedSize(expr->size); + uint iThis=0, iExpr=0, iMerge=0; + Literal lThis=This->literals[iThis]; + Literal lExpr=expr->literals[iExpr]; + Literal thisAbs=abs(lThis); + Literal exprAbs=abs(lExpr); + + while(iThisliterals[iMerge++]=lThis; + lThis=This->literals[++iThis]; + thisAbs=abs(lThis); + } else if(thisAbs>exprAbs) { + merged->literals[iMerge++]=lExpr; + lExpr=expr->literals[++iExpr]; + exprAbs=abs(lExpr); + } else if(lThis==lExpr) { + merged->literals[iMerge++]=lExpr; + lExpr=expr->literals[++iExpr]; + exprAbs=abs(lExpr); + lThis=This->literals[++iThis]; + thisAbs=abs(lThis); + } else if(lThis==-lExpr) { + merged->size=0; + return merged; + } + } + if (iThis < thisSize) { + memcpy(&merged->literals[iMerge], &This->literals[iThis], (thisSize-iThis) * sizeof(Literal)); + iMerge += (thisSize-iThis); + } + if (iExpr < exprSize) { + memcpy(&merged->literals[iMerge], &expr->literals[iExpr], (exprSize-iExpr) * sizeof(Literal)); + iMerge += (exprSize-iExpr); + } + merged->size=iMerge; + return merged; +} + +LitVector * mergeLitVectorLiteral(LitVector *This, Literal l) { + LitVector *copy=cloneLitVector(This); + addLiteralLitVector(copy, l); + return copy; +} + +void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) { + /** Handle the special cases */ + if (expr->litSize == 0) { + if (expr->isTrue) { + clearCNFExpr(This, true); + } + if (destroy) { + deleteCNFExpr(expr); + } + return; + } else if (This->litSize == 0) { + if (!This->isTrue) { + copyCNF(This, expr, destroy); + } else if (destroy) { + deleteCNFExpr(expr); + } + return; + } else if (expr->litSize == 1) { + disjoinCNFLit(This, getLiteralLitVector(&expr->singletons,0)); + if (destroy) { + deleteCNFExpr(expr); + } + return; + } else if (destroy && This->litSize == 1) { + Literal l=getLiteralLitVector(&This->singletons,0); + copyCNF(This, expr, true); + disjoinCNFLit(This, l); + return; + } + + /** Handle the full cross product */ + uint mergeIndex=0; + uint newCapacity=getClauseSizeCNF(This)*getClauseSizeCNF(expr); + LitVector ** mergeArray=ourmalloc(newCapacity*sizeof(LitVector*)); + uint singleIndex=0; + /** First do the singleton, clause pairs */ + for(uint i=0;isingletons);i++) { + Literal lThis=getLiteralLitVector(&This->singletons, i); + for(uint j=0;jclauses);j++) { + LitVector * lExpr=getVectorLitVector(&expr->clauses, j); + LitVector * copy=cloneLitVector(lExpr); + addLiteralLitVector(copy, lThis); + if (getSizeLitVector(copy)==0) { + deleteLitVector(copy); + } else { + mergeArray[mergeIndex++]=copy; + } + } + } + + /** Next do the clause, singleton pairs */ + for(uint i=0;isingletons);i++) { + Literal lExpr=getLiteralLitVector(&expr->singletons, i); + for(uint j=0;jclauses);j++) { + LitVector * lThis=getVectorLitVector(&This->clauses, j); + LitVector * copy=cloneLitVector(lThis); + addLiteralLitVector(copy, lExpr); + if (getSizeLitVector(copy)==0) { + deleteLitVector(copy); + } else { + mergeArray[mergeIndex++]=copy; + } + } + } + + /** Next do the clause, clause pairs */ + for(uint i=0;iclauses);i++) { + LitVector * lThis=getVectorLitVector(&This->clauses, i); + for(uint j=0;jclauses);j++) { + LitVector * lExpr=getVectorLitVector(&expr->clauses, j); + LitVector * merge=mergeLitVectors(lThis, lExpr); + if (getSizeLitVector(merge)==0) { + deleteLitVector(merge); + } else { + mergeArray[mergeIndex++]=merge; + } + } + deleteLitVector(lThis);//Done with this litVector + } + + /** Finally do the singleton, singleton pairs */ + for(uint i=0;isingletons);i++) { + Literal lThis=getLiteralLitVector(&This->singletons, i); + for(uint j=0;jsingletons);j++) { + Literal lExpr=getLiteralLitVector(&expr->singletons, j); + if (lThis==lExpr) { + //We have a singleton still in the final result + setLiteralLitVector(&This->singletons, singleIndex++, lThis); + } else if (lThis!=-lExpr) { + LitVector *mergeLV=allocLitVector(); + addLiteralLitVector(mergeLV, lThis); + addLiteralLitVector(mergeLV, lExpr); + mergeArray[mergeIndex++]=mergeLV; + } + } + } + + ourfree(This->clauses.array); + setSizeLitVector(&This->singletons, singleIndex); + This->clauses.capacity=newCapacity; + This->clauses.array=mergeArray; + This->clauses.size=mergeIndex; + if (destroy) + deleteCNFExpr(expr); +} + + + diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h new file mode 100644 index 0000000..5f1f907 --- /dev/null +++ b/src/Backend/cnfexpr.h @@ -0,0 +1,57 @@ +#ifndef CNFEXPR_H +#define CNFEXPR_H +#include "classlist.h" +#include "vector.h" + +typedef int Literal; + + +struct LitVector { + uint size; + uint capacity; + Literal *literals; +}; +typedef struct LitVector LitVector; + +VectorDef(LitVector, LitVector *) + +struct CNFExpr { + uint litSize; + bool isTrue; + VectorLitVector clauses; + LitVector singletons; +}; + +typedef struct CNFExpr CNFExpr; + +LitVector * allocLitVector(); +void initLitVector(LitVector *This); +void clearLitVector(LitVector *This); +void freeLitVector(LitVector *This); +LitVector *cloneLitVector(LitVector *orig); +void deleteLitVector(LitVector *This); +void addLiteralLitVector(LitVector *This, Literal l); +Literal getLiteralLitVector(LitVector *This, uint index); +void setLiteralLitVector(LitVector *This, uint index, Literal l); +LitVector * mergeLitVectorLiteral(LitVector *This, Literal l); +LitVector * mergeLitVectors(LitVector *This, LitVector *expr); + +static inline uint getSizeLitVector(LitVector *This) {return This->size;} +static inline void setSizeLitVector(LitVector *This, uint size) {This->size=size;} + +CNFExpr * allocCNFExprBool(bool isTrue); +CNFExpr * allocCNFExprLiteral(Literal l); +void deleteCNFExpr(CNFExpr *This); +void clearCNFExpr(CNFExpr *This, bool isTrue); + +void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy); +static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;} +static inline bool alwaysFalseCNF(CNFExpr * This) {return (This->litSize==0) && !This->isTrue;} +static inline uint getLitSizeCNF(CNFExpr * This) {return This->litSize;} +static inline uint getClauseSizeCNF(CNFExpr * This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);} +void conjoinCNFLit(CNFExpr *This, Literal l); +void disjoinCNFLit(CNFExpr *This, Literal l); +void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy); +void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy); + +#endif diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 964c697..cf66791 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -44,6 +44,7 @@ Constraint * cloneConstraint(Constraint * c); static inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;} Constraint *negateConstraint(Constraint * c); + extern Constraint ctrue; extern Constraint cfalse; @@ -51,4 +52,6 @@ Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint val Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); + + #endif diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c index 5e1ed54..4e0649a 100644 --- a/src/Backend/inc_solver.c +++ b/src/Backend/inc_solver.c @@ -42,6 +42,19 @@ void addClauseLiteral(IncrementalSolver * This, int literal) { } } +void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) { + for(uint i=0;ibuffer[This->offset++]=literals[i]; + if (This->offset==IS_BUFFERSIZE) { + flushBufferSolver(This); + } + } + This->buffer[This->offset++]=0; + if (This->offset==IS_BUFFERSIZE) { + flushBufferSolver(This); + } +} + void finishedClauses(IncrementalSolver * This) { addClauseLiteral(This, 0); } diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h index 15e5def..9b3e2ab 100644 --- a/src/Backend/inc_solver.h +++ b/src/Backend/inc_solver.h @@ -31,6 +31,7 @@ struct IncrementalSolver { IncrementalSolver * allocIncrementalSolver(); void deleteIncrementalSolver(IncrementalSolver * This); void addClauseLiteral(IncrementalSolver * This, int literal); +void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals); void finishedClauses(IncrementalSolver * This); void freeze(IncrementalSolver * This, int variable); int solve(IncrementalSolver * This); diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c new file mode 100644 index 0000000..6349453 --- /dev/null +++ b/src/Backend/nodeedge.c @@ -0,0 +1,767 @@ +#include "nodeedge.h" +#include +#include +#include "inc_solver.h" +#include "cnfexpr.h" + +/* +V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios, +Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon. + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be +included in all copies or substantial portions of the Software. If +you download or use the software, send email to Pete Manolios +(pete@ccs.neu.edu) with your name, contact information, and a short +note describing what you want to use BAT for. For any reuse or +distribution, you must make clear to others the license terms of this +work. + +Contact Pete Manolios if you want any of these conditions waived. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +*/ + +/* +C port of CNF SAT Conversion Copyright Brian Demsky 2017. +*/ + + +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); + cnf->solver=allocIncrementalSolver(); + return cnf; +} + +void deleteCNF(CNF * cnf) { + for(uint i=0;icapacity;i++) { + Node *n=cnf->node_array[i]; + if (n!=NULL) + ourfree(n); + } + deleteVectorArrayEdge(& cnf->constraints); + deleteVectorArrayEdge(& cnf->args); + deleteIncrementalSolver(cnf->solver); + 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;ihashCode; + 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->flags.varForced=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> 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;inode_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(initindexenableMatching && 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, lowindex, 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 solveCNF(CNF *cnf) { + countPass(cnf); + convertPass(cnf, false); + finishedClauses(cnf->solver); + solve(cnf->solver); +} + + +void countPass(CNF *cnf) { + uint numConstraints=getSizeVectorEdge(&cnf->constraints); + VectorEdge *ve=allocDefVectorEdge(); + for(uint i=0; iconstraints, i)); + } + deleteVectorEdge(ve); +} + +void countConstraint(CNF *cnf, VectorEdge *stack, Edge eroot) { + //Skip constants and variables... + if (edgeIsVarConst(eroot)) + return; + + clearVectorEdge(stack);pushVectorEdge(stack, eroot); + + 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); + + 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 { + n->intAnnot[polarity]=1; + for (uint i=0;inumEdges;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; iconstraints, 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}; + addArrayClauseLiteral(cnf->solver, 1, clause); + clause[0]=-var; + addArrayClauseLiteral(cnf->solver, 1, clause); + return; + } else { + //trivially true + return; + } + } else if (edgeIsVarConst(root)) { + Literal clause[] = { getEdgeVar(root)}; + addArrayClauseLiteral(cnf->solver, 1, 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); + if (n->ptrAnnot[0]!=NULL) + pushVectorEdge(stack, (Edge) {(Node *)n->ptrAnnot[0]}); + if (n->ptrAnnot[1]!=NULL) + 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; inumEdges; 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)) { + Literal l=getProxy(cnfExp); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } else if (backtrackLit) { + Literal l=introProxy(cnf, root, cnfExp, isNegEdge(root)); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } else { + outputCNF(cnf, cnfExp); + } + + if (!((intptr_t) cnfExp & 1)) { + deleteCNFExpr(cnfExp); + 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<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; +} + +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 + if (!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)}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } else { + Literal clause[] = {-getProxy(*dest)}; + addArrayClauseLiteral(cnf->solver, 1, 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 lcond, CNFExpr *expr) { + if (alwaysTrueCNF(expr)) { + return; + } else if (alwaysFalseCNF(expr)) { + Literal clause[] = {-lcond}; + addArrayClauseLiteral(cnf->solver, 1, clause); + return; + } + + for(uint i=0;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + Literal clause[] = {-lcond, l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } + for(uint i=0;iclauses);i++) { + LitVector *lv=getVectorLitVector(&expr->clauses,i); + addClauseLiteral(cnf->solver, -lcond); //Add first literal + addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); //Add rest + } +} + +void outputCNF(CNF *cnf, CNFExpr *expr) { + for(uint i=0;isingletons);i++) { + Literal l=getLiteralLitVector(&expr->singletons,i); + Literal clause[] = {l}; + addArrayClauseLiteral(cnf->solver, 1, clause); + } + for(uint i=0;iclauses);i++) { + LitVector *lv=getVectorLitVector(&expr->clauses,i); + addArrayClauseLiteral(cnf->solver, getSizeLitVector(lv), lv->literals); + } +} + +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; +} diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h new file mode 100644 index 0000000..95ee530 --- /dev/null +++ b/src/Backend/nodeedge.h @@ -0,0 +1,211 @@ +#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<flags.wasExpanded |= (1<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 edgeIsNull(Edge e) { + return e.node_ptr == NULL; +} + +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); +} + +CNF * createCNF(); +void deleteCNF(CNF * cnf); + +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 addConstraint(CNF *cnf, Edge constraint); +void solveCNF(CNF *cnf); + + +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); +Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg); +void outputCNF(CNF *cnf, CNFExpr *expr); + +Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT}; +Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)}; +#endif diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 5936bbd..6b274ce 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -10,18 +10,17 @@ ArrayDef(Element, Element *); ArrayDef(Boolean, Boolean *); ArrayDef(Set, Set *); - -VectorDef(Table, Table *, 4); -VectorDef(Set, Set *, 4); -VectorDef(Boolean, Boolean *, 4); -VectorDef(Constraint, Constraint *, 4); -VectorDef(Function, Function *, 4); -VectorDef(Predicate, Predicate *, 4); -VectorDef(Element, Element *, 4); -VectorDef(Order, Order *, 4); -VectorDef(TableEntry, TableEntry *, 4); -VectorDef(ASTNode, ASTNode *, 4); -VectorDef(Int, uint64_t, 4); +VectorDef(Table, Table *); +VectorDef(Set, Set *); +VectorDef(Boolean, Boolean *); +VectorDef(Constraint, Constraint *); +VectorDef(Function, Function *); +VectorDef(Predicate, Predicate *); +VectorDef(Element, Element *); +VectorDef(Order, Order *); +VectorDef(TableEntry, TableEntry *); +VectorDef(ASTNode, ASTNode *); +VectorDef(Int, uint64_t); HashTableDef(Void, void *, void *); HashTableDef(BoolConst, OrderPair *, Constraint *); diff --git a/src/Collections/vector.h b/src/Collections/vector.h index 76da387..5b638e9 100644 --- a/src/Collections/vector.h +++ b/src/Collections/vector.h @@ -2,7 +2,7 @@ #define VECTOR_H #include -#define VectorDef(name, type, defcap) \ +#define VectorDef(name, type) \ struct Vector ## name { \ uint size; \ uint capacity; \ @@ -13,9 +13,12 @@ Vector ## name * allocDefVector ## name(); \ Vector ## name * allocVectorArray ## name(uint capacity, type * array); \ void pushVector ## name(Vector ## name *vector, type item); \ - type getVector ## name(Vector ## name *vector, uint index); \ + type lastVector ## name(Vector ## name *vector); \ + void popVector ## name(Vector ## name *vector); \ + type getVector ## name(Vector ## name *vector, uint index); \ void setVector ## name(Vector ## name *vector, uint index, type item); \ uint getSizeVector ## name(Vector ## name *vector); \ + void setSizeVector ## name(Vector ## name *vector, uint size); \ void deleteVector ## name(Vector ## name *vector); \ void clearVector ## name(Vector ## name *vector); \ void deleteVectorArray ## name(Vector ## name *vector); \ @@ -41,10 +44,27 @@ memcpy(tmp->array, array, capacity * sizeof(type)); \ return tmp; \ } \ - void pushVector ## name(Vector ## name *vector, type item) { \ - if (vector->size >= vector->capacity) { \ - uint newcap=vector->capacity * 2; \ - vector->array=(type *)ourrealloc(vector->array, newcap); \ + void popVector ## name(Vector ## name *vector) { \ + vector->size--; \ + } \ + type lastVector ## name(Vector ## name *vector) { \ + return vector->array[vector->size-1]; \ + } \ + void setSizeVector ## name(Vector ## name *vector, uint size) { \ + if (size <= vector->size) { \ + vector->size=size; \ + return; \ + } else if (size > vector->capacity) { \ + vector->array=(type *)ourrealloc(vector->array, size * sizeof(type)); \ + vector->capacity=size; \ + } \ + bzero(&vector->array[vector->size], (size-vector->size)*sizeof(type)); \ + vector->size=size; \ + } \ + void pushVector ## name(Vector ## name *vector, type item) { \ + if (vector->size >= vector->capacity) { \ + uint newcap=vector->capacity << 1; \ + vector->array=(type *)ourrealloc(vector->array, newcap * sizeof(type)); \ } \ vector->array[vector->size++] = item; \ } \ diff --git a/src/Test/Makefile b/src/Test/Makefile index b3b7cb3..be27d60 100644 --- a/src/Test/Makefile +++ b/src/Test/Makefile @@ -6,7 +6,7 @@ include $(BASE)/common.mk DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS)))) -CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections +CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend all: $(OBJECTS) ../bin/run.sh diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c new file mode 100644 index 0000000..9405009 --- /dev/null +++ b/src/Test/testcnf.c @@ -0,0 +1,18 @@ +#include "nodeedge.h" + +int main(int numargs, char ** argv) { + CNF *cnf=createCNF(); + Edge v1=constraintNewVar(cnf); + Edge v2=constraintNewVar(cnf); + Edge v3=constraintNewVar(cnf); + Edge nv1=constraintNegate(v1); + Edge nv2=constraintNegate(v2); + Edge iff1=constraintIFF(cnf, nv1, v2); + Edge iff2=constraintIFF(cnf, nv2, v3); + // Edge iff3=constraintIFF(cnf, v3, nv1); + //Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3}); + Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2}); + addConstraint(cnf, cand); + solveCNF(cnf); + deleteCNF(cnf); +}