Merge branch 'master' into brian
authorbdemsky <bdemsky@uci.edu>
Tue, 11 Jul 2017 06:07:48 +0000 (23:07 -0700)
committerbdemsky <bdemsky@uci.edu>
Tue, 11 Jul 2017 06:07:48 +0000 (23:07 -0700)
44 files changed:
.gitignore
papers/10.1007-978-3-642-12002-2_10.pdf [new file with mode: 0644]
papers/428811198-MIT.pdf [new file with mode: 0644]
papers/CNF_unobservable.pdf [new file with mode: 0644]
papers/date09.pdf [new file with mode: 0644]
papers/sat-cnf.pdf [new file with mode: 0644]
papers/sat04-bc-conv.pdf [new file with mode: 0644]
papers/tech08_sat.pdf [new file with mode: 0644]
src/AST/boolean.c
src/AST/boolean.h
src/AST/function.c
src/AST/function.h
src/AST/order.c
src/AST/order.h
src/AST/set.c
src/AST/set.h
src/AST/table.c
src/Backend/cnfexpr.c [new file with mode: 0644]
src/Backend/cnfexpr.h [new file with mode: 0644]
src/Backend/constraint.c
src/Backend/constraint.h
src/Backend/inc_solver.c
src/Backend/inc_solver.h
src/Backend/nodeedge.c [deleted file]
src/Backend/nodeedge.h [deleted file]
src/Backend/orderpair.c
src/Backend/orderpair.h
src/Backend/satencoder.c
src/Backend/satencoder.h
src/Collections/hashtable.h
src/Collections/structs.c
src/Collections/structs.h
src/Collections/vector.h
src/Encoders/elementencoding.c
src/Encoders/elementencoding.h
src/Test/Makefile
src/Test/buildconstraints.c
src/Test/run.sh
src/Test/testcnf.c [new file with mode: 0644]
src/classlist.h
src/common.c [new file with mode: 0644]
src/config.h
src/csolver.c
src/csolver.h

index c6f1f57..2d1b9f1 100644 (file)
@@ -1,9 +1,11 @@
 #Ignoring netbeans configs
 nbproject/
+sat_solver
+setup.sh
 
 #Ignoring binary files
 src/bin/
 src/lib_cons_comp.so
 /src/mymemory.cc
 .*
-*.dSYM
\ No newline at end of file
+*.dSYM
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
index 0000000..a9af157
Binary files /dev/null and b/papers/tech08_sat.pdf differ
index 3166c5d..4fd2c86 100644 (file)
@@ -8,7 +8,7 @@ Boolean* allocBoolean(VarType t) {
        BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
        GETBOOLEANTYPE(tmp)=BOOLEANVAR;
        tmp->vtype=t;
-       tmp->var=NULL;
+       tmp->var=E_NULL;
        allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp));
        return & tmp->base;
 }
index a59aff1..7382908 100644 (file)
@@ -6,6 +6,7 @@
 #include "structs.h"
 #include "astnode.h"
 #include "functionencoding.h"
+#include "constraint.h"
 
 /**
     This is a little sketchy, but apparently legit.
@@ -29,7 +30,7 @@ struct BooleanOrder {
 struct BooleanVar {
        Boolean base;
        VarType vtype;
-       Constraint * var;
+       Edge var;
 };
 
 struct BooleanLogic {
index 43adc25..61e413b 100644 (file)
@@ -20,6 +20,22 @@ Function* allocFunctionTable (Table* table){
        return &This->base;
 }
 
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange){
+       uint64_t result = 0;
+       switch( func->op){
+               case ADD:
+                       result = var1+ var2;
+                       break;
+               case SUB:
+                       result = var1 - var2;
+                       break;
+               default:
+                       ASSERT(0);
+       }
+       *isInRange = existsInSet(func->range, result);
+       return result;
+}
+
 void deleteFunction(Function* This){
        switch(GETFUNCTIONTYPE(This)){
        case TABLEFUNC:
index 2e04320..158a55c 100644 (file)
@@ -26,6 +26,7 @@ struct FunctionTable {
 
 Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior);
 Function* allocFunctionTable (Table* table);
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInrange);
 void deleteFunction(Function* This);
 
 #endif
index 19b1c6e..b1b52e3 100644 (file)
@@ -10,10 +10,14 @@ Order* allocOrder(OrderType type, Set * set){
        allocInlineDefVectorBoolean(& order->constraints);
        order->type=type;
        allocOrderEncoding(& order->order, order);
-       order->boolsToConstraints = allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       order->boolsToConstraints = NULL;
        return order;
 }
 
+void initializeOrderHashTable(Order* order){
+       order->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+}
+
 void addOrderConstraint(Order* order, BooleanOrder* constraint){
        pushVectorBoolean( &order->constraints, (Boolean*) constraint);
 }
@@ -25,6 +29,9 @@ void setOrderEncodingType(Order* order, OrderEncodingType type){
 void deleteOrder(Order* order){
        deleteVectorArrayBoolean(& order->constraints);
        deleteOrderEncoding(& order->order);
-       deleteHashTableBoolConst(order->boolsToConstraints);
+       if(order->boolsToConstraints!= NULL) {
+               resetAndDeleteHashTableBoolConst(order->boolsToConstraints);
+               deleteHashTableBoolConst(order->boolsToConstraints);
+       }
        ourfree(order);
 }
index 933d831..67f0d99 100644 (file)
@@ -16,6 +16,7 @@ struct Order {
 };
 
 Order* allocOrder(OrderType type, Set * set);
+void initializeOrderHashTable(Order * order);
 void addOrderConstraint(Order* order, BooleanOrder* constraint);
 void setOrderEncodingType(Order* order, OrderEncodingType type);
 void deleteOrder(Order* order);
index afe26ec..f72bbc3 100644 (file)
@@ -21,6 +21,19 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) {
        return tmp;
 }
 
+bool existsInSet(Set* set, uint64_t element){
+       if(set->isRange){
+               return element >= set->low && element <= set->high;
+       }else {
+               uint size = getSizeVectorInt(set->members);
+               for(uint i=0; i< size; i++){
+                       if(element == getVectorInt(set->members, i))
+                               return true;
+               }
+               return false;
+       }
+}
+
 uint getSetSize(Set* set){
        if(set->isRange){
                return set->high- set->low+1;
index 55fb57c..badb28c 100644 (file)
@@ -23,6 +23,7 @@ struct Set {
 
 Set *allocSet(VarType t, uint64_t * elements, uint num);
 Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);
+bool existsInSet(Set* set, uint64_t element);
 uint getSetSize(Set* set);
 void deleteSet(Set *set);
 #endif/* SET_H */
index a0b1e6f..2780aca 100644 (file)
@@ -15,7 +15,7 @@ Table * allocTable(Set **domains, uint numDomain, Set * range){
 }
 
 void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result){
-       ASSERT(getSizeArrayElement( &table->domains) == inputSize);
+       ASSERT(getSizeArraySet( &table->domains) == inputSize);
        pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result));
 }
 
diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
new file mode 100644 (file)
index 0000000..dbbd93f
--- /dev/null
@@ -0,0 +1,465 @@
+#include "cnfexpr.h"
+#include <stdio.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;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)
+               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;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) {
+                       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;i<getSizeLitVector(&expr->singletons);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;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;
+}
+
+#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(iThis<thisSize && iExpr<exprSize) {
+               if (thisAbs<exprAbs) {
+                       merged->literals[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;i<getSizeLitVector(&This->singletons);i++) {
+               Literal lThis=getLiteralLitVector(&This->singletons, i);
+               for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);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;i<getSizeLitVector(&expr->singletons);i++) {
+               Literal lExpr=getLiteralLitVector(&expr->singletons, i);
+               for(uint j=0;j<getSizeVectorLitVector(&This->clauses);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;i<getSizeVectorLitVector(&This->clauses);i++) {
+               LitVector * lThis=getVectorLitVector(&This->clauses, i);
+               for(uint j=0;j<getSizeVectorLitVector(&expr->clauses);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;i<getSizeLitVector(&This->singletons);i++) {
+               Literal lThis=getLiteralLitVector(&This->singletons, i);
+                       for(uint j=0;j<getSizeLitVector(&expr->singletons);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);
+}
+
+void printCNFExpr(CNFExpr *This) {
+       for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+               if (i!=0)
+                       printf(" ^ ");
+               Literal l=getLiteralLitVector(&This->singletons,i);
+               printf ("%d",l);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+               LitVector *lv=getVectorLitVector(&This->clauses,i);
+               printf(" ^ (");
+               for(uint j=0;j<getSizeLitVector(lv);j++) {
+                       if (j!=0)
+                               printf(" v ");
+                       printf("%d", getLiteralLitVector(lv, j));
+               }
+               printf(")");
+       }
+}
diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
new file mode 100644 (file)
index 0000000..1b64528
--- /dev/null
@@ -0,0 +1,58 @@
+#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 printCNFExpr(CNFExpr *This);
+
+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
index b491ca3..7f65364 100644 (file)
-/*      Copyright (c) 2015 Regents of the University of California
- *
- *      Author: Brian Demsky <bdemsky@uci.edu>
- *
- *      This program is free software; you can redistribute it and/or
- *      modify it under the terms of the GNU General Public License
- *      version 2 as published by the Free Software Foundation.
- */
-
 #include "constraint.h"
-#include "mymemory.h"
+#include <string.h>
+#include <stdlib.h>
 #include "inc_solver.h"
+#include "cnfexpr.h"
 
-Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
-Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};
-
-Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) {
-       Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
-       This->type=t;
-       This->numoperandsorvar=2;
-       This->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *));
-       This->neg=NULL;
-       ASSERT(l!=NULL);
-       //if (type==IMPLIES) {
-       //type=OR;
-       //      operands[0]=l->negate();
-       //      } else {
-       This->operands[0]=l;
-       //      }
-       This->operands[1]=r;
-       return This;
-}
-
-Constraint * allocUnaryConstraint(CType t, Constraint *l) {
-       Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
-       This->type=t;
-       This->numoperandsorvar=1;
-       This->operands=(Constraint **) ourmalloc(sizeof(Constraint *));
-       This->neg=NULL;
-       This->operands[0]=l;
-       return This;
-}
-
-Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) {
-       Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
-       This->type=t;
-       This->numoperandsorvar=num;
-       This->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *));
-       This->neg=NULL;
-       memcpy(This->operands, array, num*sizeof(Constraint *));
-       return This;
-}
-
-Constraint * allocVarConstraint(CType t, uint v) {
-       Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
-       This->type=t;
-       This->numoperandsorvar=v;
-       This->operands=NULL;
-       This->neg=NULL;
-       return This;
-}
-
-void deleteConstraint(Constraint *This) {
-       if (This->operands!=NULL)
-               ourfree(This->operands);
-}
-
-void dumpConstraint(Constraint * This, IncrementalSolver *solver) {
-       if (This->type==VAR) {
-               addClauseLiteral(solver, This->numoperandsorvar);
-               addClauseLiteral(solver, 0);
-       } else if (This->type==NOTVAR) {
-               addClauseLiteral(solver, -This->numoperandsorvar);
-               addClauseLiteral(solver, 0);
-       } else {
-               ASSERT(This->type==OR);
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       Constraint *c=This->operands[i];
-                       if (c->type==VAR) {
-                               addClauseLiteral(solver, c->numoperandsorvar);
-                       } else if (c->type==NOTVAR) {
-                               addClauseLiteral(solver, -c->numoperandsorvar);
-                       } else ASSERT(0);
-               }
-               addClauseLiteral(solver, 0);
+/* 
+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)
+Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
+Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
+Edge E_BOGUS={(Node *)0x12345673};
+Edge E_NULL={(Node *)NULL};
+
+
+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;i<cnf->capacity;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 internalfreeConstraint(Constraint * This) {
-       switch(This->type) {
-       case TRUE:
-       case FALSE:
-       case NOTVAR:
-       case VAR:
-               return;
-       case BOGUS:
-               ASSERT(0);
-       default:
-               This->type=BOGUS;
-               ourfree(This);
+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;
 }
 
-void freerecConstraint(Constraint *This) {
-       switch(This->type) {
-       case TRUE:
-       case FALSE:
-       case NOTVAR:
-       case VAR:
-               return;
-       case BOGUS:
-               ASSERT(0);
-       default:
-               if (This->operands!=NULL) {
-                       for(uint i=0;i<This->numoperandsorvar;i++)
-                               freerecConstraint(This->operands[i]);
+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;
                }
-               This->type=BOGUS;
-               deleteConstraint(This);
        }
+       *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) ((uintptr_t) edges[i].node_ptr);
+               hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
+       }
+       return (uint) hashvalue;
+}
 
-void printConstraint(Constraint * This) {
-       switch(This->type) {
-       case TRUE:
-               model_print("true");
-               break;
-       case FALSE:
-               model_print("false");
-               break;
-       case IMPLIES:
-               model_print("(");
-               printConstraint(This->operands[0]);
-               model_print(")");
-               model_print("=>");
-               model_print("(");
-               printConstraint(This->operands[1]);
-               model_print(")");
-               break;
-       case AND:
-       case OR:
-               model_print("(");
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       if (i!=0) {
-                               if (This->type==AND)
-                                       model_print(" ^ ");
-                               else
-                                       model_print(" v ");
+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, lneg, rneg);
+       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;
                        }
-                       printConstraint(This->operands[i]);
+               } else
+                       edges[++lowindex]=edges[initindex];
+       }
+       lowindex++; //Make lowindex look like size
+       
+       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]));
                }
-               model_print(")");
-               break;
-       case VAR:
-               model_print("t%u",This->numoperandsorvar);
-               break;
-       case NOTVAR:
-               model_print("!t%u",This->numoperandsorvar);
-               break;
-       default:
-               ASSERT(0);
-       }
-}
-
-Constraint * cloneConstraint(Constraint * This) {
-       switch(This->type) {
-       case TRUE:
-       case FALSE:
-       case VAR:
-       case NOTVAR:
-               return This;
-       case IMPLIES:
-               return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1]));
-       case AND:
-       case OR: {
-               Constraint *array[This->numoperandsorvar];
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       array[i]=cloneConstraint(This->operands[i]);
+       }
+
+       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});
                }
-               return allocArrayConstraint(This->type, This->numoperandsorvar, array);
+       } else {
+               Edge edges[]={cond, thenedge, elseedge};
+               result=createNode(cnf, NodeType_ITE, 3, edges);
        }
-       default:
-               ASSERT(0);
-               return NULL;
+       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;
+}
+
+int solveCNF(CNF *cnf) {
+       countPass(cnf);
+       convertPass(cnf, false);
+       finishedClauses(cnf->solver);
+       return solve(cnf->solver);
+}
+
+bool getValueCNF(CNF *cnf, Edge var) {
+       Literal l=getEdgeVar(var);
+       bool isneg=(l<0);
+       l=abs(l);
+       return isneg ^ getValueSolver(cnf->solver, l);
+}
+
+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);
 }
 
-Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) {
-       Constraint *carray[numvars];
-       for(uint j=0;j<numvars;j++) {
-               carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
-               value=value>>1;
+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;i<n->numEdges;i++) {
+                                       Edge succ=n->edges[i];
+                                       if(!edgeIsVarConst(succ)) {
+                                               succ=constraintNegateIf(succ, polarity);
+                                               pushVectorEdge(stack, succ);
+                                       }
+                               }
+                       }
+               }
        }
+}
 
-       return allocArrayConstraint(AND, numvars, carray);
+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);
 }
 
-/** Generates a constraint to ensure that all encodings are less than value */
-Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) {
-       Constraint *orarray[numvars];
-       Constraint *andarray[numvars];
-       uint andi=0;
+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);
 
-       while(true) {
-               uint val=value;
-               uint ori=0;
-               for(uint j=0;j<numvars;j++) {
-                       if ((val&1)==1)
-                               orarray[ori++]=negateConstraint(vars[j]);
-                       val=val>>1;
+               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;
                }
-               //no ones to flip, so bail now...
-               if (ori==0) {
-                       return allocArrayConstraint(AND, andi, andarray);
+
+               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);
                }
-               andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
+       }
+       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);
+       }
 
-               value=value+(1<<(__builtin_ctz(value)));
-               //flip the last one
+       if (!((intptr_t) cnfExp & 1)) {
+               deleteCNFExpr(cnfExp);
+               nroot->ptrAnnot[isNegEdge(root)] = NULL;
        }
 }
 
-Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
-       if (numvars==0)
-               return &ctrue;
-       Constraint *array[numvars*2];
-       for(uint i=0;i<numvars;i++) {
-               array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
-               array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
+
+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);
        }
-       return allocArrayConstraint(AND, numvars*2, array);
+       // Output the constraints on the auxiliary variable
+       constrainCNF(cnf, l, exp);
+       deleteCNFExpr(exp);
+  
+       n->ptrAnnot[isNeg] = (void*) ((intptr_t) (l << 1) | 1);
+       
+       return l;
 }
 
-Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
-       Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
-       Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
+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);
+       }
 
-       return allocConstraint(AND, imp1, imp2);
+       /// @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 mergeandfree(VectorConstraint * to, VectorConstraint * from) {
-       for(uint i=0;i<getSizeVectorConstraint(from);i++) {
-               Constraint *c=getVectorConstraint(from, i);
-               if (c->type==TRUE)
-                       continue;
-               if (c->type==FALSE) {
-                       for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
-                               freerecConstraint(getVectorConstraint(from,j));
-                       for(uint j=0;j<getSizeVectorConstraint(to);j++)
-                               freerecConstraint(getVectorConstraint(to, j));
-                       clearVectorConstraint(to);
-                       pushVectorConstraint(to, &ctrue);
-                       deleteVectorConstraint(from);
-                       return true;
+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));
                }
-               pushVectorConstraint(to, c);
+               return true;
        }
-       deleteVectorConstraint(from);
        return false;
 }
 
-VectorConstraint * simplifyConstraint(Constraint * This) {
-       switch(This->type) {
-       case TRUE:
-       case VAR:
-       case NOTVAR:
-       case FALSE: {
-               VectorConstraint * vec=allocDefVectorConstraint();
-               pushVectorConstraint(vec, This);
-               return vec;
-       }
-       case AND: {
-               VectorConstraint *vec=allocDefVectorConstraint();
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
-                       if (mergeandfree(vec, subvec)) {
-                               for(uint j=i+1;j<This->numoperandsorvar;j++) {
-                                       freerecConstraint(This->operands[j]);
-                               }
-                               internalfreeConstraint(This);
-                               return vec;
-                       }
+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;i<getSizeLitVector(&expr->singletons);i++) {
+               Literal l=getLiteralLitVector(&expr->singletons,i);
+               Literal clause[] = {-lcond, l};
+               addArrayClauseLiteral(cnf->solver, 2, clause);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);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;i<getSizeLitVector(&expr->singletons);i++) {
+               Literal l=getLiteralLitVector(&expr->singletons,i);
+               Literal clause[] = {l};
+               addArrayClauseLiteral(cnf->solver, 1, clause);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&expr->clauses);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;
                }
-               internalfreeConstraint(This);
-               return vec;
-       }
-       case OR: {
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       Constraint *c=This->operands[i];
-                       switch(c->type) {
-                       case TRUE: {
-                               VectorConstraint * vec=allocDefVectorConstraint();
-                               pushVectorConstraint(vec, c);
-                               freerecConstraint(This);
-                               return vec;
-                       }
-                       case FALSE: {
-                               Constraint *array[This->numoperandsorvar-1];
-                               uint index=0;
-                               for(uint j=0;j<This->numoperandsorvar;j++) {
-                                       if (j!=i)
-                                               array[index++]=This->operands[j];
+               
+               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;
                                }
-                               Constraint *cn=allocArrayConstraint(OR, index, array);
-                               VectorConstraint *vec=simplifyConstraint(cn);
-                               internalfreeConstraint(This);
-                               return vec;
                        }
-                       case VAR:
-                       case NOTVAR:
-                               break;
-                       case OR: {
-                               uint nsize=This->numoperandsorvar+c->numoperandsorvar-1;
-                               Constraint *array[nsize];
-                               uint index=0;
-                               for(uint j=0;j<This->numoperandsorvar;j++)
-                                       if (j!=i)
-                                               array[index++]=This->operands[j];
-                               for(uint j=0;j<c->numoperandsorvar;j++)
-                                       array[index++]=c->operands[j];
-                               Constraint *cn=allocArrayConstraint(OR, nsize, array);
-                               VectorConstraint *vec=simplifyConstraint(cn);
-                               internalfreeConstraint(This);
-                               internalfreeConstraint(c);
-                               return vec;
-                       }
-                       case IMPLIES: {
-                               uint nsize=This->numoperandsorvar+1;
-                               Constraint *array[nsize];
-                               uint index=0;
-                               for(uint j=0;j<This->numoperandsorvar;j++)
-                                       if (j!=i)
-                                               array[index++]=This->operands[j];
-                               array[index++]=negateConstraint(c->operands[0]);
-                               array[index++]=c->operands[1];
-                               Constraint *cn=allocArrayConstraint(OR, nsize, array);
-                               VectorConstraint *vec=simplifyConstraint(cn);
-                               internalfreeConstraint(This);
-                               internalfreeConstraint(c);
-                               return vec;
+               }
+               pushVectorEdge(&cnf->args, arg);
+       }
+       
+       if (largest != NULL) {
+               Node *nlargestEdge=getNodePtrFromEdge(*largestEdge);
+               nlargestEdge->ptrAnnot[isNegEdge(*largestEdge)] = NULL;
+       }
+       
+       return largest;
+}
+
+void printCNF(Edge e) {
+       if (edgeIsVarConst(e)) {
+               Literal l=getEdgeVar(e);
+               printf ("%d", l);
+               return;
+       }
+       bool isNeg=isNegEdge(e);
+       if (edgeIsConst(e)) {
+               if (isNeg)
+                       printf("T");
+               else
+                       printf("F");
+               return;
+       }
+       Node *n=getNodePtrFromEdge(e);
+       if (isNeg)
+               printf("!");
+       switch(getNodeType(e)) {
+       case NodeType_AND:
+               printf("and");
+               break;
+       case NodeType_ITE:
+               printf("ite");
+               break;
+       case NodeType_IFF:
+               printf("iff");
+               break;
+       }
+       printf("(");
+       for(uint i=0;i<n->numEdges;i++) {
+               Edge e=n->edges[i];
+               if (i!=0)
+                       printf(" ");
+               printCNF(e);
+       }
+       printf(")");
+}
+
+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;
                        }
-                       case AND: {
-                               Constraint *array[This->numoperandsorvar];
-
-                               VectorConstraint *vec=allocDefVectorConstraint();
-                               for(uint j=0;j<c->numoperandsorvar;j++) {
-                                       //copy other elements
-                                       for(uint k=0;k<This->numoperandsorvar;k++) {
-                                               if (k!=i) {
-                                                       array[k]=cloneConstraint(This->operands[k]);
-                                               }
-                                       }
+               }
+       }
+       
+       return accum;
+}
 
-                                       array[i]=cloneConstraint(c->operands[j]);
-                                       Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array);
-                                       VectorConstraint * newvec=simplifyConstraint(cn);
-                                       if (mergeandfree(vec, newvec)) {
-                                               freerecConstraint(This);
-                                               return vec;
-                                       }
+#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;
                                }
-                               freerecConstraint(This);
-                               return vec;
-                       }
-                       default:
-                               ASSERT(0);
                        }
-                       //continue on to next item
                }
-               VectorConstraint * vec=allocDefVectorConstraint();
-               if (This->numoperandsorvar==1) {
-                       Constraint *c=This->operands[0];
-                       freerecConstraint(This);
-                       pushVectorConstraint(vec, c);
-               } else
-                       pushVectorConstraint(vec, This);
-               return vec;
-       }
-       case IMPLIES: {
-               Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]);
-               VectorConstraint * vec=simplifyConstraint(cn);
-               internalfreeConstraint(This);
-               return vec;
-       }
-       default:
-               ASSERT(0);
-               return NULL;
-       }
-}
-
-Constraint * negateConstraint(Constraint * This) {
-       switch(This->type) {
-       case TRUE:
-               return &cfalse;
-       case FALSE:
-               return &ctrue;
-       case NOTVAR:
-       case VAR:
-               return This->neg;
-       case IMPLIES: {
-               Constraint *l=This->operands[0];
-               Constraint *r=This->operands[1];
-               This->operands[0]=r;
-               This->operands[1]=l;
-               return This;
-       }
-       case AND:
-       case OR: {
-               for(uint i=0;i<This->numoperandsorvar;i++) {
-                       This->operands[i]=negateConstraint(This->operands[i]);
+       }
+  
+       return accum;
+}
+
+Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
+       Edge carray[numvars];
+       for(uint j=0;j<numvars;j++) {
+               carray[j]=((value&1)==1) ? vars[j] : constraintNegate(vars[j]);
+               value=value>>1;
+       }
+       
+       return constraintAND(cnf, numvars, carray);
+}
+/** Generates a constraint to ensure that all encodings are less than value */
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value) {
+       Edge orarray[numvars];
+       Edge andarray[numvars];
+       uint andi=0;
+  
+       while(true) {
+               uint val=value;
+               uint ori=0;
+               for(uint j=0;j<numvars;j++) {
+                       if ((val&1)==1)
+                               orarray[ori++]=constraintNegate(vars[j]);
+                       val=val>>1;
+               }
+               //no ones to flip, so bail now...
+               if (ori==0) {
+                       return constraintAND(cnf, andi, andarray);
                }
-               This->type=(This->type==AND) ? OR : AND;
-               return This;
+               andarray[andi++]=constraintOR(cnf, ori, orarray);
+               
+               value=value+(1<<(__builtin_ctz(value)));
+               //flip the last one
        }
-       default:
-               ASSERT(0);
-               return NULL;
+}
+  
+Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
+       if (numvars==0)
+               return E_True;
+       Edge array[numvars];
+       for(uint i=0;i<numvars;i++) {
+               array[i]=constraintIFF(cnf, var1[i], var2[i]);
        }
+       return constraintAND(cnf, numvars, array);
 }
index e1b21d3..ae22fdb 100644 (file)
-/*      Copyright (c) 2015 Regents of the University of California
- *
- *      Author: Brian Demsky <bdemsky@uci.edu>
- *
- *      This program is free software; you can redistribute it and/or
- *      modify it under the terms of the GNU General Public License
- *      version 2 as published by the Free Software Foundation.
- */
-
 #ifndef CONSTRAINT_H
 #define CONSTRAINT_H
 #include "classlist.h"
-#include "structs.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;
 
-enum ConstraintType {
-       TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS
+struct NodeFlags {
+       NodeType type:2;
+       int varForced:1;
+       int wasExpanded:2;
+       int cnfVisitedDown:2;
+       int cnfVisitedUp:2;
 };
 
-typedef enum ConstraintType CType;
+typedef struct NodeFlags NodeFlags;
 
-struct Constraint {
-       CType type;
-       uint numoperandsorvar;
-       Constraint ** operands;
-       Constraint *neg;
+struct Node {
+       NodeFlags flags;
+       uint numEdges;
+       uint hashCode;
+       uint intAnnot[2];
+       void * ptrAnnot[2];
+       Edge edges[];
 };
 
-Constraint * allocConstraint(CType t, Constraint *l, Constraint *r);
-Constraint * allocUnaryConstraint(CType t, Constraint *l);
-Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array);
-Constraint * allocVarConstraint(CType t, uint var);
-
-void deleteConstraint(Constraint *);
-void printConstraint(Constraint * c);
-void dumpConstraint(Constraint * c, IncrementalSolver *solver);
-static inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
-VectorConstraint * simplify(Constraint * c);
-static inline CType getType(Constraint * c) {return c->type;}
-static inline bool isFalse(Constraint * c) {return c->type==FALSE;}
-static inline bool isTrue(Constraint * c) {return c->type==TRUE;}
-void internalfreeConstraint(Constraint * c);
-void freerecConstraint(Constraint * c);
-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;
-
-Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value);
-Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value);
-Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2);
-Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2);
+#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 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);
+static inline Edge constraintXOR(CNF *cnf, Edge left, Edge right) {return constraintNegate(constraintIFF(cnf, left,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);
+int solveCNF(CNF *cnf);
+bool getValueCNF(CNF *cnf, Edge var);
+void printCNF(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);
+Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);
+void outputCNF(CNF *cnf, CNFExpr *expr);
+
+Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge * vars, uint value);
+Edge generateLTConstraint(CNF *cnf, uint numvars, Edge * vars, uint value);
+Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2);
+
+extern Edge E_True;
+extern Edge E_False;
+extern Edge E_BOGUS;
+extern Edge E_NULL;
 #endif
index 5e1ed54..43113ff 100644 (file)
@@ -11,6 +11,7 @@
 #define SATSOLVER "sat_solver"
 #include <fcntl.h>
 #include "common.h"
+#include <string.h>
 
 IncrementalSolver * allocIncrementalSolver() {
        IncrementalSolver *This=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver));
@@ -27,6 +28,7 @@ void deleteIncrementalSolver(IncrementalSolver * This) {
        ourfree(This->buffer);
        if (This->solution != NULL)
                ourfree(This->solution);
+       ourfree(This);
 }
 
 void resetSolver(IncrementalSolver * This) {
@@ -42,6 +44,28 @@ void addClauseLiteral(IncrementalSolver * This, int literal) {
        }
 }
 
+void addArrayClauseLiteral(IncrementalSolver * This, uint numliterals, int * literals) {
+       uint index=0;
+       while(true) {
+               uint bufferspace=IS_BUFFERSIZE-This->offset;
+               uint numtowrite=numliterals-index;
+               if (bufferspace > numtowrite) {
+                       memcpy(&This->buffer[This->offset], &literals[index], numtowrite*sizeof(int));
+                       This->offset+=numtowrite;
+                       This->buffer[This->offset++]=0; //have one extra spot always
+                       if (This->offset==IS_BUFFERSIZE) {//Check if full
+                               flushBufferSolver(This);
+                       }
+                       return;
+               } else {
+                       memcpy(&This->buffer[This->offset], &literals[index], bufferspace*sizeof(int));
+                       This->offset+=bufferspace;
+                       index+=bufferspace;
+                       flushBufferSolver(This);
+               }
+       }
+}
+
 void finishedClauses(IncrementalSolver * This) {
        addClauseLiteral(This, 0);
 }
@@ -148,10 +172,24 @@ void killSolver(IncrementalSolver * This) {
                waitpid(This->solver_pid, &status, 0);
        }
 }
+bool first=true;
 
 void flushBufferSolver(IncrementalSolver * This) {
        ssize_t bytestowrite=sizeof(int)*This->offset;
        ssize_t byteswritten=0;
+       for(uint i=0;i<This->offset;i++) {
+               if (first)
+                       printf("(");
+               if (This->buffer[i]==0) {
+                       printf(")\n");
+                       first=true;
+               } else {
+                       if (!first)
+                               printf(" + ");
+                       first=false;
+                       printf("%d", This->buffer[i]);
+               }
+       }
        do {
                ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
                if (n == -1) {
index 15e5def..9b3e2ab 100644 (file)
@@ -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
deleted file mode 100644 (file)
index deb63d3..0000000
+++ /dev/null
@@ -1,256 +0,0 @@
-#include "nodeedge.h"
-#include <string.h>
-#include <stdlib.h>
-
-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);
-       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);
-       }
-       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->numEdges=numEdges;
-       n->flags.type=type;
-       n->hashCode=hashcode;
-       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 (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;
-}
-
-Edge constraintNewVar(CNF *cnf) {
-       uint varnum=cnf->varcount++;
-       Edge e={(Node *) ((((uintptr_t)varnum) << VAR_SHIFT) | EDGE_IS_VAR_CONSTANT) };
-       return e;
-}
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
deleted file mode 100644 (file)
index a83983d..0000000
+++ /dev/null
@@ -1,136 +0,0 @@
-#ifndef NODEEDGE_H
-#define NODEEDGE_H
-#include "classlist.h"
-
-#define NEGATE_EDGE 1
-#define EDGE_IS_VAR_CONSTANT 2
-#define VAR_SHIFT 2
-#define EDGE_MASK (NEGATE_EDGE | EDGE_IS_VAR_CONSTANT)
-
-struct Edge;
-typedef struct Edge Edge;
-
-struct Node;
-typedef struct Node Node;
-
-struct Edge {
-       Node * node_ptr;
-};
-
-enum NodeType {
-       NodeType_AND,
-       NodeType_ITE,
-       NodeType_IFF
-};
-
-typedef enum NodeType NodeType;
-
-struct NodeFlags {
-       NodeType type:2;
-};
-
-typedef struct NodeFlags NodeFlags;
-
-struct Node {
-       NodeFlags flags;
-       uint numEdges;
-       uint hashCode;
-       Edge edges[];
-};
-
-#define DEFAULT_CNF_ARRAY_SIZE 256
-#define LOAD_FACTOR 0.25
-#define enableMatching 1
-
-struct CNF {
-       uint varcount;
-       uint capacity;
-       uint size;
-       uint mask;
-       uint maxsize;
-       Node ** node_array;
-};
-
-typedef struct CNF CNF;
-
-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 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;
-}
-
-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);
-
-Edge E_True={(Node *)(uintptr_t) EDGE_IS_VAR_CONSTANT};
-Edge E_False={(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
-#endif
index 2290b36..4db56ca 100644 (file)
@@ -1,12 +1,14 @@
 #include "orderpair.h"
 
 
-OrderPair* allocOrderPair(uint64_t first, uint64_t second){
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint){
        OrderPair* pair = (OrderPair*) ourmalloc(sizeof(OrderPair));
        pair->first = first;
        pair->second = second;
+       pair->constraint = constraint;
        return pair;
 }
+
 void deleteOrderPair(OrderPair* pair){
        ourfree(pair);
-}
\ No newline at end of file
+}
index 21bddd7..05c8ffa 100644 (file)
 
 #include "classlist.h"
 #include "mymemory.h"
+#include "constraint.h"
 
 struct OrderPair{
        uint64_t first;
        uint64_t second;
+       Edge constraint;
 }; 
 
-OrderPair* allocOrderPair(uint64_t first, uint64_t second);
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Edge constraint);
 void deleteOrderPair(OrderPair* pair);
 
 #endif /* ORDERPAIR_H */
index dc557b5..8d943c4 100644 (file)
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
        This->varcount=1;
+       This->cnf=createCNF();
        return This;
 }
 
 void deleteSATEncoder(SATEncoder *This) {
+       deleteCNF(This->cnf);
        ourfree(This);
 }
 
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
-       /** We really should not walk the free list to generate constraint
-                       variables...walk the constraint tree instead.  Or even better
-                       yet, just do this as you need to during the encodeAllSATEncoder
-                       walk.  */
-
-//     FIXME!!!!(); // Make sure Hamed sees comment above
-
-       uint size = getSizeVectorElement(csolver->allElements);
-       for(uint i=0; i<size; i++){
-               Element* element = getVectorElement(csolver->allElements, i);
-               generateElementEncodingVariables(This,getElementEncoding(element));
-       }
-}
-
-
-Constraint * getElementValueConstraint(Element* This, uint64_t value) {
-       switch(getElementEncoding(This)->type){
+Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
+       generateElementEncodingVariables(This, getElementEncoding(elem));
+       switch(getElementEncoding(elem)->type){
                case ONEHOT:
+                       //FIXME
                        ASSERT(0);
                        break;
                case UNARY:
                        ASSERT(0);
                        break;
                case BINARYINDEX:
-                       ASSERT(0);
+                       return getElementValueBinaryIndexConstraint(This, elem, value);
                        break;
                case ONEHOTBINARY:
-                       return getElementValueBinaryIndexConstraint(This, value);
+                       ASSERT(0);
                        break;
                case BINARYVAL:
                        ASSERT(0);
@@ -60,19 +48,19 @@ Constraint * getElementValueConstraint(Element* This, uint64_t value) {
                        ASSERT(0);
                        break;
        }
-       return NULL;
+       return E_BOGUS;
 }
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
-       ASTNodeType type = GETELEMENTTYPE(This);
+
+Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
+       ASTNodeType type = GETELEMENTTYPE(elem);
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
-       ElementEncoding* elemEnc = getElementEncoding(This);
+       ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
                if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
-                       return generateBinaryConstraint(elemEnc->numVars,
-                               elemEnc->variables, i);
+                       return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
                }
        }
-       return NULL;
+       return E_BOGUS;
 }
 
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
@@ -80,26 +68,14 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        uint size=getSizeVectorBoolean(constraints);
        for(uint i=0;i<size;i++) {
                Boolean *constraint=getVectorBoolean(constraints, i);
-               encodeConstraintSATEncoder(This, constraint);
+               Edge c= encodeConstraintSATEncoder(This, constraint);
+               printCNF(c);
+               printf("\n");
+               addConstraint(This->cnf, c);
        }
-       
-//     FIXME: Following line for element!
-//     size = getSizeVectorElement(csolver->allElements);
-//     for(uint i=0; i<size; i++){
-//             Element* element = getVectorElement(csolver->allElements, i);
-//             switch(GETELEMENTTYPE(element)){
-//                     case ELEMFUNCRETURN: 
-//                             encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
-//                             break;
-//                     default:        
-//                             continue;
-//                             //ElementSets that aren't used in any constraints/functions
-//                             //will be eliminated.
-//             }
-//     }
 }
 
-Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
        switch(GETBOOLEANTYPE(constraint)) {
        case ORDERCONST:
                return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
@@ -115,50 +91,41 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
        }
 }
 
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) {
        for(uint i=0;i<num;i++)
                carray[i]=getNewVarSATEncoder(encoder);
 }
 
-Constraint * getNewVarSATEncoder(SATEncoder *This) {
-       Constraint * var=allocVarConstraint(VAR, This->varcount);
-       Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
-       setNegConstraint(var, varneg);
-       setNegConstraint(varneg, var);
-       return var;
+Edge getNewVarSATEncoder(SATEncoder *This) {
+       return constraintNewVar(This->cnf);
 }
 
-Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
-       if (constraint->var == NULL) {
+Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
+       if (edgeIsNull(constraint->var)) {
                constraint->var=getNewVarSATEncoder(This);
        }
        return constraint->var;
 }
 
-Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
-       Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
+Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
+       Edge array[getSizeArrayBoolean(&constraint->inputs)];
        for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
                array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 
        switch(constraint->op) {
        case L_AND:
-               return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
+               return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
        case L_OR:
-               return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
+               return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
        case L_NOT:
-               ASSERT(constraint->numArray==1);
-               return negateConstraint(array[0]);
-       case L_XOR: {
-               ASSERT(constraint->numArray==2);
-               Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
-               Constraint * nright=negateConstraint(cloneConstraint(array[1]));
-               return allocConstraint(OR,
-                                                                                                        allocConstraint(AND, array[0], nright),
-                                                                                                        allocConstraint(AND, nleft, array[1]));
-       }
+               ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
+               return constraintNegate(array[0]);
+       case L_XOR:
+               ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
+               return constraintXOR(This->cnf, array[0], array[1]);
        case L_IMPLIES:
-               ASSERT(constraint->numArray==2);
-               return allocConstraint(IMPLIES, array[0], array[1]);
+               ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
+               return constraintIMPLIES(This->cnf, array[0], array[1]);
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);
@@ -166,7 +133,7 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint)
 }
 
 
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
+Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
        switch( constraint->order->type){
                case PARTIAL:
                        return encodePartialOrderSATEncoder(This, constraint);
@@ -175,19 +142,41 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
+Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+       bool negate = false;
+       OrderPair flipped;
+       if (pair->first > pair->second) {
+               negate=true;
+               flipped.first=pair->second;
+               flipped.second=pair->first;
+               pair = &flipped;        //FIXME: accessing a local variable from outside of the function?
+       }
+       Edge constraint;
+       if (!containsBoolConst(table, pair)) {
+               constraint = getNewVarSATEncoder(This);
+               OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
+               putBoolConst(table, paircopy, paircopy);
+       } else
+               constraint = getBoolConst(table, pair)->constraint;
+       if (negate)
+               return constraintNegate(constraint);
+       else
+               return constraint;
+       
+}
 
-Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
        ASSERT(boolOrder->order->type == TOTAL);
-       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-       OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second);
-       if( !containsBoolConst(boolToConsts, pair) ){
+       if(boolOrder->order->boolsToConstraints == NULL){
+               initializeOrderHashTable(boolOrder->order);
                createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
-       Constraint* constraint = getOrderConstraint(boolToConsts, pair);
-       deleteOrderPair(pair);
+       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+       OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
+       Edge constraint = getPairConstraint(This, boolToConsts, & pair);
        return constraint;
 }
 
@@ -196,63 +185,53 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        VectorInt* mems = order->set->members;
        HashTableBoolConst* table = order->boolsToConstraints;
        uint size = getSizeVectorInt(mems);
+       uint csize =0;
        for(uint i=0; i<size; i++){
                uint64_t valueI = getVectorInt(mems, i);
                for(uint j=i+1; j<size;j++){
                        uint64_t valueJ = getVectorInt(mems, j);
-                       OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
-                       ASSERT(!containsBoolConst(table, pairIJ));
-                       Constraint* constIJ = getNewVarSATEncoder(This);
-                       putBoolConst(table, pairIJ, constIJ);
+                       OrderPair pairIJ = {valueI, valueJ};
+                       Edge constIJ=getPairConstraint(This, table, & pairIJ);
                        for(uint k=j+1; k<size; k++){
                                uint64_t valueK = getVectorInt(mems, k);
-                               OrderPair* pairJK = allocOrderPair(valueJ, valueK);
-                               OrderPair* pairIK = allocOrderPair(valueI, valueK);
-                               Constraint* constJK, *constIK;
-                               if(!containsBoolConst(table, pairJK)){
-                                       constJK = getNewVarSATEncoder(This);
-                                       putBoolConst(table, pairJK, constJK);
-                               }
-                               if(!containsBoolConst(table, pairIK)){
-                                       constIK = getNewVarSATEncoder(This);
-                                       putBoolConst(table, pairIK, constIK);
-                               }
-                               generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
+                               OrderPair pairJK = {valueJ, valueK};
+                               OrderPair pairIK = {valueI, valueK};
+                               Edge constIK = getPairConstraint(This, table, & pairIK);
+                               Edge constJK = getPairConstraint(This, table, & pairJK);
+                               addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); 
                        }
                }
        }
 }
 
-Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       Constraint* constraint= getBoolConst(table, pair);
-       ASSERT(constraint!= NULL);
+       Edge constraint = getBoolConst(table, pair)->constraint;
        if(pair->first > pair->second)
                return constraint;
        else
-               return negateConstraint(constraint);
+               return constraintNegate(constraint);
 }
 
-Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
-       //FIXME: first we should add the the constraint to the satsolver!
-       Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
-       Constraint * loop1= allocArrayConstraint(OR, 3, carray);
-       Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
-       Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
-       return allocConstraint(AND, loop1, loop2);
+Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
+       Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
+       Edge loop1= constraintOR(This->cnf, 3, carray);
+       Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
+       Edge loop2= constraintOR(This->cnf, 3, carray2 );
+       return constraintAND2(This->cnf, loop1, loop2);
 }
 
-Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
+Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
        // FIXME: we can have this implementation for partial order. Basically,
        // we compute the transitivity between two order constraints specified by the client! (also can be used
        // when client specify sparse constraints for the total order!)
-       ASSERT(boolOrder->order->type == PARTIAL);
+       ASSERT(constraint->order->type == PARTIAL);
 /*
        HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
        if( containsBoolConst(boolToConsts, boolOrder) ){
                return getBoolConst(boolToConsts, boolOrder);
        } else {
-               Constraint* constraint = getNewVarSATEncoder(This); 
+               Edge constraint = getNewVarSATEncoder(This); 
                putBoolConst(boolToConsts,boolOrder, constraint);
                VectorBoolean* orderConstrs = &boolOrder->order->constraints;
                uint size= getSizeVectorBoolean(orderConstrs);
@@ -260,7 +239,7 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
                        ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
                        BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
                        BooleanOrder* newBool;
-                       Constraint* first, *second;
+                       Edge first, second;
                        if(tmp->second==boolOrder->first){
                                newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
                                first = encodeTotalOrderSATEncoder(This, tmp);
@@ -272,16 +251,16 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
                                second = encodeTotalOrderSATEncoder(This, tmp);
                        }else
                                continue;
-                       Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
+                       Edge transConstr= encodeTotalOrderSATEncoder(This, newBool);
                        generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
                }
                return constraint;
        }
 */     
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
        switch(GETPREDICATETYPE(constraint->predicate) ){
                case TABLEPRED:
                        return encodeTablePredicateSATEncoder(This, constraint);
@@ -290,10 +269,10 @@ Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        switch(constraint->encoding.type){
                case ENUMERATEIMPLICATIONS:
                case ENUMERATEIMPLICATIONSNEGATE:
@@ -304,14 +283,14 @@ Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
        FunctionEncodingType encType = constraint->encoding.type;
        uint size = getSizeVectorTableEntry(entries);
-       Constraint* constraints[size];
+       Edge constraints[size];
        for(uint i=0; i<size; i++){
                TableEntry* entry = getVectorTableEntry(entries, i);
                if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
@@ -320,19 +299,25 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
                        continue;
                ArrayElement* inputs = &constraint->inputs;
                uint inputNum =getSizeArrayElement(inputs);
-               Constraint* carray[inputNum];
-               Element* el = getArrayElement(inputs, i);
+               Edge carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                       carray[j] = getElementValueConstraint(el, entry->inputs[j]);
+                       Element* el = getArrayElement(inputs, j);
+                       Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
+                       if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
+                               Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
+                               carray[j] = constraintAND2(This->cnf, func, tmpc);
+                       } else {
+                               carray[j] = tmpc;
+                       }
                }
-               constraints[i]=allocArrayConstraint(AND, inputNum, carray);
+               constraints[i]=constraintAND(This->cnf, inputNum, carray);
        }
-       Constraint* result= allocArrayConstraint(OR, size, constraints);
+       Edge result=constraintOR(This->cnf, size, constraints);
        //FIXME: if it didn't match with any entry
-       return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
+       return encType==ENUMERATEIMPLICATIONS? result: constraintNegate(result);
 }
 
-Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
        switch(constraint->encoding.type){
                case ENUMERATEIMPLICATIONS:
                        return encodeEnumOperatorPredicateSATEncoder(This, constraint);
@@ -342,30 +327,40 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-       ASSERT(GETPREDICATETYPE(constraint)==OPERATORPRED);
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+       ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
        PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
        ASSERT(predicate->op == EQUALS); //For now, we just only support equals
        //getting maximum size of in common elements between two sets!
        uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
        uint64_t commonElements [size];
        getEqualitySetIntersection(predicate, &size, commonElements);
-       Constraint*  carray[size];
+       Edge  carray[size];
        Element* elem1 = getArrayElement( &constraint->inputs, 0);
+       Edge elemc1 = E_NULL, elemc2 = E_NULL;
+       if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
+               elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
        Element* elem2 = getArrayElement( &constraint->inputs, 1);
+       if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
+               elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
        for(uint i=0; i<size; i++){
-               
-               carray[i] =  allocConstraint(AND, getElementValueConstraint(elem1, commonElements[i]),
-                       getElementValueConstraint(elem2, commonElements[i]) );
+               Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
+               Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
+               carray[i] =  constraintAND2(This->cnf, arg1, arg2);
        }
        //FIXME: the case when there is no intersection ....
-       return allocArrayConstraint(OR, size, carray);
+       Edge result = constraintOR(This->cnf, size, carray);
+       if (!edgeIsNull(elemc1))
+               result = constraintAND2(This->cnf, result, elemc1);
+       if (!edgeIsNull(elemc2))
+               result = constraintAND2(This->cnf, result, elemc2);
+       return result;
 }
 
-Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
        switch(GETFUNCTIONTYPE(This->function)){
                case TABLEFUNC:
                        return encodeTableElementFunctionSATEncoder(encoder, This);
@@ -374,10 +369,10 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
        switch(getElementFunctionEncoding(This)->type){
                case ENUMERATEIMPLICATIONS:
                        return encodeEnumTableElemFunctionSATEncoder(encoder, This);
@@ -388,32 +383,98 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
                default:
                        ASSERT(0);
        }
-       return NULL;
+       return E_BOGUS;
 }
 
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-       //FIXME: for now it just adds/substracts inputs exhustively
-       return NULL;
+Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+       ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
+       ASSERT(getSizeArrayElement(&This->inputs)==2 );
+       ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
+       ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
+       Edge carray[elem1->encArraySize*elem2->encArraySize];
+       uint size=0;
+       Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
+       for(uint i=0; i<elem1->encArraySize; i++){
+               if(isinUseElement(elem1, i)){
+                       for( uint j=0; j<elem2->encArraySize; j++){
+                               if(isinUseElement(elem2, j)){
+                                       bool isInRange = false;
+                                       uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
+                                               elem2->encodingArray[j], &isInRange);
+                                       //FIXME: instead of getElementValueConstraint, it might be useful to have another function
+                                       // that doesn't iterate over encodingArray and treats more efficient ...
+                                       Edge valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
+                                       Edge valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
+                                       Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
+                                       if(edgeIsNull(valConstrOut))
+                                               continue; //FIXME:Should talk to brian about it!
+                                       Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
+                                       switch( ((FunctionOperator*)This->function)->overflowbehavior ){
+                                               case IGNORE:
+                                                       if(isInRange){
+                                                               carray[size++] = OpConstraint;
+                                                       }
+                                                       break;
+                                               case WRAPAROUND:
+                                                       carray[size++] = OpConstraint;
+                                                       break;
+                                               case FLAGFORCESOVERFLOW:
+                                                       if(isInRange){
+                                                               Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
+                                                               carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
+                                                       }
+                                                       break;
+                                               case OVERFLOWSETSFLAG:
+                                                       if(isInRange){
+                                                               carray[size++] = OpConstraint;
+                                                       } else{
+                                                               carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
+                                                       }
+                                                       break;
+                                               case FLAGIFFOVERFLOW:
+                                                       if(isInRange){
+                                                               Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
+                                                               carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
+                                                       } else {
+                                                               carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
+                                                       }
+                                                       break;
+                                               case NOOVERFLOW:
+                                                       if(!isInRange){
+                                                               ASSERT(0);
+                                                       }
+                                                       carray[size++] = OpConstraint;
+                                                       break;
+                                               default:
+                                                       ASSERT(0);
+                                       }
+                                       
+                               }
+                       }
+               }
+       }
+       return constraintAND(encoder->cnf, size, carray);
 }
 
-Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
        ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
        ArrayElement* elements= &This->inputs;
        Table* table = ((FunctionTable*) (This->function))->table;
        uint size = getSizeVectorTableEntry(&table->entries);
-       Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
-       for(uint i=0; i<size; i++){
+       Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
+       for(uint i=0; i<size; i++) {
                TableEntry* entry = getVectorTableEntry(&table->entries, i);
-               uint inputNum =getSizeArrayElement(elements);
-               Element* el= getArrayElement(elements, i);
-               Constraint* carray[inputNum];
+               uint inputNum = getSizeArrayElement(elements);
+               Edge carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                       carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+                       Element* el= getArrayElement(elements, j);
+                       carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
                }
-               Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
-                       getElementValueBinaryIndexConstraint((Element*)This, entry->output));
+               Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
+               Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
                constraints[i]=row;
        }
-       Constraint* result = allocArrayConstraint(OR, size, constraints);
+       Edge result = constraintOR(encoder->cnf, size, constraints);
        return result;
 }
+
index 6963fee..0d6999f 100644 (file)
@@ -3,37 +3,39 @@
 
 #include "classlist.h"
 #include "structs.h"
+#include "inc_solver.h"
+#include "constraint.h"
 
 struct SATEncoder {
        uint varcount;
+       CNF * cnf;
 };
 
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This);
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
-Constraint * getNewVarSATEncoder(SATEncoder *This);
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
-Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
+Edge getNewVarSATEncoder(SATEncoder *This);
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge*carray);
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
+Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order);
-Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
-Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK);
-Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
-Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
-Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
-Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
-Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
+Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ, Edge constJK, Edge constIK);
+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
+Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
+Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
+Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
+Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
-Constraint * getElementValueConstraint(Element* This, uint64_t value);
+Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* element, uint64_t value);
+Edge getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value);
 
-Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
-Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
-Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
+Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
+Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
 #endif
index b7c78d9..dbf61f9 100644 (file)
        bool contains ## Name(const HashTable ## Name * tab, _Key key);       \
        void resize ## Name(HashTable ## Name * tab, unsigned int newsize);   \
        double getLoadFactor ## Name(HashTable ## Name * tab);                \
-       unsigned int getCapacity ## Name(HashTable ## Name * tab);
+       unsigned int getCapacity ## Name(HashTable ## Name * tab);                                              \
+       void resetAndDeleteHashTable ## Name(HashTable ## Name * tab);
 
-#define HashTableImpl(Name, _Key, _Val, hash_function, equals) \
+#define HashTableImpl(Name, _Key, _Val, hash_function, equals, freefunction) \
        HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \
                HashTable ## Name * tab = (HashTable ## Name *)ourmalloc(sizeof(HashTable ## Name)); \
                tab->table = (struct hashlistnode ## Name *)ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \
                tab->size = 0;                                                      \
                return tab;                                                         \
        }                                                                     \
-                                                                        \
-       void deleteHashTable ## Name(HashTable ## Name * tab) {                 \
+                                                                                                                                                                                                                                                                                               \
+       void deleteHashTable ## Name(HashTable ## Name * tab) {                                                         \
                ourfree(tab->table);                                                \
                if (tab->zero)                                                      \
                        ourfree(tab->zero);                                               \
                ourfree(tab);                                                       \
        }                                                                     \
-                                                                        \
+                                                                                                                                                                                                                                                                                               \
+       void resetAndDeleteHashTable ## Name(HashTable ## Name * tab) {                         \
+               for(uint i=0;i<tab->capacity;i++) {                                                                                                                                     \
+                       struct hashlistnode ## Name * bin=&tab->table[i];                                                                       \
+                       if (bin->key!=NULL) {                                                                                                                                                                                   \
+                               bin->key=NULL;                                                                                                                                                                                                  \
+                               if (bin->val!=NULL) {                                                                                                                                                                           \
+                                       freefunction(bin->val);                                                                                                                                                         \
+                                       bin->val=NULL;                                                                                                                                                                                          \
+                               }                                                                                                                                                                                                                                                               \
+                       }                                                                                                                                                                                                                                                                       \
+               }                                                                                                                                                                                                                                                                               \
+               if (tab->zero)  {                                                                                                                                                                                                               \
+                       if (tab->zero->val != NULL)                                                                                                                                                             \
+                               freefunction(tab->zero->val);                                                                                                                                           \
+                       ourfree(tab->zero);                                                                                                                                                                                             \
+                       tab->zero=NULL;                                                                                                                                                                                                         \
+               }                                                                                                                                                                                                                                                                               \
+               tab->size=0;                                                                                                                                                                                                                            \
+       }                                                                                                                                                                                                                                                                                       \
+                                                                                                                                                                                                                                                                                               \
        void reset ## Name(HashTable ## Name * tab) {                         \
                memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \
                if (tab->zero) {                                                    \
index 58d3728..29c7abe 100644 (file)
@@ -5,7 +5,6 @@
 VectorImpl(Table, Table *, 4);
 VectorImpl(Set, Set *, 4);
 VectorImpl(Boolean, Boolean *, 4);
-VectorImpl(Constraint, Constraint *, 4);
 VectorImpl(Function, Function *, 4);
 VectorImpl(Predicate, Predicate *, 4);
 VectorImpl(Element, Element *, 4);
@@ -22,14 +21,12 @@ inline bool Ptr_equals(void * key1, void * key2) {
        return key1 == key2;
 }
 
-inline unsigned int order_pair_hash_Function(OrderPair* This){
-       uint64_t x=This->first^This->second;
-       uint64_t a=This->first&This->second;
-       return (uint)((x<<4)^(a));
+static inline unsigned int order_pair_hash_Function(OrderPair* This){
+       return (uint) (This->first << 2) ^ This->second;
 }
 
-inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
+static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
        return key1->first== key2->first && key1->second == key2->second;
 }
 
-HashTableImpl(BoolConst, OrderPair *, Constraint *, order_pair_hash_Function, order_pair_equals);
+HashTableImpl(BoolConst, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);
index a45eb13..86addfb 100644 (file)
@@ -10,23 +10,19 @@ 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(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 *);
+HashTableDef(BoolConst, OrderPair *, OrderPair *);
 
 HashSetDef(Void, void *);
 
index 76da387..e0ebebd 100644 (file)
@@ -2,7 +2,7 @@
 #define VECTOR_H
 #include <string.h>
 
-#define VectorDef(name, type, defcap)                                   \
+#define VectorDef(name, type)                                                                                                                                                                          \
        struct Vector ## name {                                               \
                uint size;                                                          \
                uint capacity;                                                      \
        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);                                                         \
@@ -32,7 +35,7 @@
                Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
                tmp->size = 0;                                                      \
                tmp->capacity = capacity;                                           \
-               tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity);          \
+               tmp->array = (type *) ourmalloc(sizeof(type) * capacity);                                               \
                return tmp;                                                         \
        }                                                                     \
        Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
                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->capacity=newcap;                                                                                                                                                                        \
                }                                                                   \
                vector->array[vector->size++] = item;                               \
        }                                                                     \
@@ -73,7 +94,7 @@
        void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
                vector->size = 0;                                                      \
                vector->capacity = capacity;                                                                                                                                                                                    \
-               vector->array = (type *) ourcalloc(1, sizeof(type) * capacity);                 \
+               vector->array = (type *) ourmalloc(sizeof(type) * capacity);                            \
        }                                                                                                                                                                                                                                                                                       \
        void allocInlineDefVector ## name(Vector ## name * vector) {                                    \
                allocInlineVector ## name(vector, defcap);                                                                                                      \
index 08eb2e8..2989b3b 100644 (file)
@@ -29,12 +29,13 @@ void allocEncodingArrayElement(ElementEncoding *This, uint size) {
 }
 
 void allocInUseArrayElement(ElementEncoding *This, uint size) {
-       This->inUseArray=ourcalloc(1, size >> 6);
+       uint bytes = ((size + ((1 << 9)-1)) >> 6)&~7;//Depends on size of inUseArray
+       This->inUseArray=ourcalloc(1, bytes);
 }
 
 void allocElementConstraintVariables(ElementEncoding* This, uint numVars){
        This->numVars = numVars;
-       This->variables = ourmalloc(sizeof(Constraint*) * numVars);
+       This->variables = ourmalloc(sizeof(Edge) * numVars);
 }
 
 void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
@@ -49,7 +50,8 @@ void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This)
 
 void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){
        ASSERT(This->type!=ELEM_UNASSIGNED);
-       ASSERT(This->variables==NULL);
+       if(This->variables!=NULL)
+               return;
        switch(This->type){
                case BINARYINDEX:
                        generateBinaryIndexEncodingVars(encoder, This);
index 1528245..797f301 100644 (file)
@@ -2,6 +2,7 @@
 #define ELEMENTENCODING_H
 #include "classlist.h"
 #include "naiveencoder.h"
+#include "constraint.h"
 
 enum ElementEncodingType {
        ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
@@ -12,7 +13,7 @@ typedef enum ElementEncodingType ElementEncodingType;
 struct ElementEncoding {
        ElementEncodingType type;
        Element * element;
-       Constraint ** variables;/* List Variables Used To Encode Element */
+       Edge * variables;/* List Variables Used To Encode Element */
        uint64_t * encodingArray;       /* List the Variables in the appropriate order */
        uint64_t * inUseArray;/* Bitmap to track variables in use */
        uint encArraySize;
@@ -24,8 +25,6 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
-//FIXME
-//uint addNewVariableToEncodingArray(ElementEncoding* This, uint64_t var);
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
        return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
 }
index b3b7cb3..be27d60 100644 (file)
@@ -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
 
index caa8a92..222d4a1 100644 (file)
@@ -14,5 +14,31 @@ int main(int numargs, char ** argv) {
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
        addBoolean(solver, oc);
+               
+       uint64_t set2[] = {2, 3};
+       Set* rangef1 = createSet(solver, 1, set2, 2);
+       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
+       
+       Table* table = createTable(solver, domain, 2, s);
+       uint64_t row1[] = {0, 1};
+       uint64_t row2[] = {1, 1};
+       uint64_t row3[] = {2, 1};
+       uint64_t row4[] = {1, 2};
+       addTableEntry(solver, table, row1, 2, 0);
+       addTableEntry(solver, table, row2, 2, 1);
+       addTableEntry(solver, table, row3, 2, 2);
+       addTableEntry(solver, table, row4, 2, 2);
+       Function * f2 = completeTable(solver, table); //its range would be as same as s
+       
+       Boolean* overflow = getBooleanVar(solver , 2);
+       Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
+       Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
+       Set* domain2[] = {s,rangef1};
+       Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
+       Element* inputs2 [] = {e4, e3};
+       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
+       addBoolean(solver, pred);
+       
+       startEncoding(solver);
        deleteSolver(solver);
 }
index 9741fe0..e74b557 100755 (executable)
@@ -3,5 +3,7 @@
 export LD_LIBRARY_PATH=../bin
 # For Mac OSX
 export DYLD_LIBRARY_PATH=../bin
+# For sat_solver
+export PATH=.:$PATH
 
 $@
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
new file mode 100644 (file)
index 0000000..ebd79f5
--- /dev/null
@@ -0,0 +1,35 @@
+#include "constraint.h"
+#include <stdio.h>
+
+int main(int numargs, char ** argv) {
+       CNF *cnf=createCNF();
+       Edge v1=constraintNewVar(cnf);
+       Edge v2=constraintNewVar(cnf);
+       Edge v3=constraintNewVar(cnf);
+       Edge v4=constraintNewVar(cnf);
+       Edge v5=constraintNewVar(cnf);
+
+       Edge nv1=constraintNegate(v1);
+       Edge nv2=constraintNegate(v2);
+       Edge nv3=constraintNegate(v3);
+       Edge nv4=constraintNegate(v4);
+
+       Edge c1=constraintAND2(cnf, v1, nv2);
+       Edge c2=constraintAND2(cnf, v3, nv4);
+       Edge c3=constraintAND2(cnf, nv1, v2);
+       Edge c4=constraintAND2(cnf, nv3, v4);
+       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), v5);
+       printCNF(cor);
+       printf("\n");
+       addConstraint(cnf, cor);
+       int value=solveCNF(cnf);
+       if (value==1) {
+               bool v1v=getValueCNF(cnf, v1);
+               bool v2v=getValueCNF(cnf, v2);
+               bool v3v=getValueCNF(cnf, v3);
+               bool v4v=getValueCNF(cnf, v4);
+               printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v);
+       } else
+               printf("%d\n",value);
+       deleteCNF(cnf);
+}
index c02268d..4f44aff 100644 (file)
@@ -21,10 +21,6 @@ typedef struct CSolver CSolver;
 struct SATEncoder;
 typedef struct SATEncoder SATEncoder;
 
-
-struct Constraint;
-typedef struct Constraint Constraint;
-
 typedef struct BooleanOrder BooleanOrder;
 typedef struct BooleanVar BooleanVar;
 typedef struct BooleanLogic BooleanLogic;
diff --git a/src/common.c b/src/common.c
new file mode 100644 (file)
index 0000000..660472f
--- /dev/null
@@ -0,0 +1,6 @@
+#include "common.h"
+
+void assert_hook(void)
+{
+       model_print("Add breakpoint to line %u in file %s.\n", __LINE__, __FILE__);
+}
\ No newline at end of file
index b83cc1f..bd998c0 100644 (file)
@@ -20,7 +20,7 @@
 #endif
 
 #ifndef CONFIG_ASSERT
-//#define CONFIG_ASSERT
+#define CONFIG_ASSERT
 #endif
 
 #endif
index 6024099..d903044 100644 (file)
@@ -171,12 +171,13 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
        return constraint;
 }
 
-void encode(CSolver* solver){
+void startEncoding(CSolver* solver){
        naiveEncodingDecision(solver);
        SATEncoder* satEncoder = allocSATEncoder();
-       initializeConstraintVars(solver, satEncoder);
        encodeAllSATEncoder(solver, satEncoder);
+       int result= solveCNF(satEncoder->cnf);
+       model_print("sat_solver's result:%d\n", result);
        //For now, let's just delete it, and in future for doing queries 
        //we may need it.
        deleteSATEncoder(satEncoder);
-}
\ No newline at end of file
+}
index fd807ae..bd90bf3 100644 (file)
@@ -113,5 +113,5 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
 
 /** When everything is done, the client calls this function and then csolver starts to encode*/
-void encode(CSolver*);
+void startEncoding(CSolver*);
 #endif