Merge branch 'hamed' into brian

diff --git a/.gitignore b/.gitignore
index c6f1f57..2d1b9f1 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -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/src/AST/order.c b/src/AST/order.c
index 2f3de74..b1b52e3 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -29,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);
 }

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index b491ca3..46c8c5e 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -63,6 +63,7 @@ Constraint * allocVarConstraint(CType t, uint v) {
 void deleteConstraint(Constraint *This) {
        if (This->operands!=NULL)
                ourfree(This->operands);
+       ourfree(This);
 }
 
 void dumpConstraint(Constraint * This, IncrementalSolver *solver) {
@@ -97,7 +98,7 @@ void internalfreeConstraint(Constraint * This) {
                ASSERT(0);
        default:
                This->type=BOGUS;
-               ourfree(This);
+               deleteConstraint(This);
        }
 }
 
@@ -159,6 +160,7 @@ void printConstraint(Constraint * This) {
                model_print("!t%u",This->numoperandsorvar);
                break;
        default:
+               model_print("In printingConstraint: %d", This->type);
                ASSERT(0);
        }
 }

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 0d254c8..cf66791 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -34,7 +34,7 @@ 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);
+VectorConstraint * simplifyConstraint(Constraint * This);
 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;}

diff --git a/src/Backend/orderpair.c b/src/Backend/orderpair.c
index 2290b36..109fc53 100644 (file)
--- a/src/Backend/orderpair.c
+++ b/src/Backend/orderpair.c
@@ -1,12 +1,14 @@
 #include "orderpair.h"
 
 
-OrderPair* allocOrderPair(uint64_t first, uint64_t second){
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Constraint * 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
+}

diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h
index 21bddd7..bdffb15 100644 (file)
--- a/src/Backend/orderpair.h
+++ b/src/Backend/orderpair.h
@@ -14,9 +14,10 @@
 struct OrderPair{
        uint64_t first;
        uint64_t second;
+       Constraint *constraint;
 }; 
 
-OrderPair* allocOrderPair(uint64_t first, uint64_t second);
+OrderPair* allocOrderPair(uint64_t first, uint64_t second, Constraint * constraint);
 void deleteOrderPair(OrderPair* pair);
 
 #endif /* ORDERPAIR_H */

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index e78cb3f..fa1d513 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -16,10 +16,12 @@
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
        This->varcount=1;
+       This->satSolver = allocIncrementalSolver();
        return This;
 }
 
 void deleteSATEncoder(SATEncoder *This) {
+       deleteIncrementalSolver(This->satSolver);
        ourfree(This);
 }
 
@@ -27,6 +29,7 @@ Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64
        generateElementEncodingVariables(encoder, getElementEncoding(This));
        switch(getElementEncoding(This)->type){
                case ONEHOT:
+                       //FIXME
                        ASSERT(0);
                        break;
                case UNARY:
@@ -60,6 +63,20 @@ Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value)
        return NULL;
 }
 
+void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver) {
+       VectorConstraint* simplified = simplifyConstraint(c);
+       uint size = getSizeVectorConstraint(simplified);
+       for(uint i=0; i<size; i++) {
+               Constraint *simp=getVectorConstraint(simplified, i);
+               if (simp->type==TRUE)
+                       continue;
+               ASSERT(simp->type!=FALSE);
+               dumpConstraint(simp, satSolver);
+               freerecConstraint(simp);
+       }
+       deleteVectorConstraint(simplified);
+}
+
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        VectorBoolean *constraints=csolver->constraints;
        uint size=getSizeVectorBoolean(constraints);
@@ -68,6 +85,9 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
                Constraint* c= encodeConstraintSATEncoder(This, constraint);
                printConstraint(c);
                model_print("\n\n");
+               addConstraintToSATSolver(c, This->satSolver);
+               //FIXME: When do we want to delete constraints? Should we keep an array of them
+               // and delete them later, or it would be better to just delete them right away?
        }
 }
 
@@ -162,10 +182,10 @@ Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, Ord
        Constraint * constraint;
        if (!containsBoolConst(table, pair)) {
                constraint = getNewVarSATEncoder(This);
-               OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
-               putBoolConst(table, paircopy, constraint);
+               OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
+               putBoolConst(table, paircopy, paircopy);
        } else
-               constraint = getBoolConst(table, pair);
+               constraint = getBoolConst(table, pair)->constraint;
        if (negate)
                return negateConstraint(constraint);
        else
@@ -180,9 +200,8 @@ Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrd
                return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
        HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-       OrderPair pair={boolOrder->first, boolOrder->second};
-       Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
-       ASSERT(constraint != NULL);
+       OrderPair pair={boolOrder->first, boolOrder->second, NULL};
+       Constraint *constraint = getPairConstraint(This, boolToConsts, & pair);
        return constraint;
 }
 
@@ -215,8 +234,7 @@ Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* or
 
 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       Constraint* constraint= getBoolConst(table, pair);
-       ASSERT(constraint!= NULL);
+       Constraint* constraint= getBoolConst(table, pair)->constraint;
        if(pair->first > pair->second)
                return constraint;
        else

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 36cbc77..0ada52b 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -3,9 +3,11 @@
 
 #include "classlist.h"
 #include "structs.h"
+#include "inc_solver.h"
 
 struct SATEncoder {
        uint varcount;
+       IncrementalSolver* satSolver;
 };
 
 SATEncoder * allocSATEncoder();
@@ -35,4 +37,5 @@ Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
+void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver);
 #endif

diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h
index b7c78d9..dbf61f9 100644 (file)
--- a/src/Collections/hashtable.h
+++ b/src/Collections/hashtable.h
@@ -62,9 +62,10 @@
        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)); \
@@ -77,14 +78,34 @@
                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) {                                                    \

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index f5f8f68..0453231 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -30,4 +30,4 @@ 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);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 6b274ce..8700459 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -23,7 +23,7 @@ VectorDef(ASTNode, ASTNode *);
 VectorDef(Int, uint64_t);
 
 HashTableDef(Void, void *, void *);
-HashTableDef(BoolConst, OrderPair *, Constraint *);
+HashTableDef(BoolConst, OrderPair *, OrderPair *);
 
 HashSetDef(Void, void *);
 

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 6ed38c2..a5158ab 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -29,7 +29,8 @@ 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){

diff --git a/src/Test/run.sh b/src/Test/run.sh
index 9741fe0..e74b557 100755 (executable)
--- a/src/Test/run.sh
+++ b/src/Test/run.sh
@@ -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/csolver.c b/src/csolver.c
index d63c266..1d31e42 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,9 +174,11 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
 void startEncoding(CSolver* solver){
        naiveEncodingDecision(solver);
        SATEncoder* satEncoder = allocSATEncoder();
-//     initializeConstraintVars(solver, satEncoder);
        encodeAllSATEncoder(solver, satEncoder);
+       finishedClauses(satEncoder->satSolver);
+       int result= solve(satEncoder->satSolver);
+       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
+}