Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...

Getting new updates

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 4fd2c8615be473a2b3499fd28ee555514c340fad..622c8a338ca83df1c21eee3eaec19bb4dccfc8bf 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -4,35 +4,32 @@
 #include "element.h"
 #include "order.h"
 
-Boolean* allocBoolean(VarType t) {
-       BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
-       GETBOOLEANTYPE(tmp)=BOOLEANVAR;
-       tmp->vtype=t;
-       tmp->var=E_NULL;
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp));
-       return & tmp->base;
+Boolean* allocBooleanVar(VarType t) {
+       BooleanVar* This=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
+       GETBOOLEANTYPE(This)=BOOLEANVAR;
+       This->vtype=t;
+       This->var=E_NULL;
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
+       return & This->base;
 }
 
 Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
-       BooleanOrder* tmp=(BooleanOrder *) ourmalloc(sizeof (BooleanOrder));
-       GETBOOLEANTYPE(tmp)=ORDERCONST;
-       tmp->order=order;
-       tmp->first=first;
-       tmp->second=second;
-       //FIXME: what if client calls this function with the same arguments?
-       //Instead of vector we should keep a hashtable from PAIR->BOOLEANOrder with
-       //asymmetric hash function.  
-       pushVectorBoolean(&order->constraints, &tmp->base);
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(tmp));
-       return & tmp -> base;
+       BooleanOrder* This=(BooleanOrder *) ourmalloc(sizeof (BooleanOrder));
+       GETBOOLEANTYPE(This)=ORDERCONST;
+       This->order=order;
+       This->first=first;
+       This->second=second;
+       pushVectorBoolean(&order->constraints, &This->base);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
+       return & This -> base;
 }
 
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs){
        BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
        GETBOOLEANTYPE(This)= PREDICATEOP;
        This->predicate=predicate;
-       allocInlineArrayInitElement(&This->inputs, inputs, numInputs);
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initArrayInitElement(&This->inputs, inputs, numInputs);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
 
        for(uint i=0;i<numInputs;i++) {
                pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
@@ -44,8 +41,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
        BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
-       allocInlineArrayInitBoolean(&This->inputs, array, asize);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initArrayInitBoolean(&This->inputs, array, asize);
        pushVectorBoolean(solver->allBooleans, (Boolean *) This);
        return & This->base;
 }

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 7382908c3075f30eb730f563ce5d56ea22ec300e..928ba41bc78fec2d252e5bb0b6da2cb559752dba 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -46,7 +46,7 @@ struct BooleanPredicate {
        ArrayElement inputs;
 };
 
-Boolean * allocBoolean(VarType t);
+Boolean * allocBooleanVar(VarType t);
 Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
 Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs);
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);

diff --git a/src/AST/element.c b/src/AST/element.c
index 9fc426c1fb686f544f7d20608b258ac8becad41c..f9b7579a2cc8d1693f6c51bb8228ad0943ba3412 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -6,45 +6,45 @@
 #include "table.h"
 
 Element *allocElementSet(Set * s) {
-       ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet));
-       GETELEMENTTYPE(tmp)= ELEMSET;
-       tmp->set=s;
-       allocInlineDefVectorASTNode(GETELEMENTPARENTS(tmp));
-       initElementEncoding(&tmp->encoding, (Element *) tmp);
-       return &tmp->base;
+       ElementSet * This=(ElementSet *)ourmalloc(sizeof(ElementSet));
+       GETELEMENTTYPE(This)= ELEMSET;
+       This->set=s;
+       initDefVectorASTNode(GETELEMENTPARENTS(This));
+       initElementEncoding(&This->encoding, (Element *) This);
+       return &This->base;
 }
 
 Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus){
-       ElementFunction* tmp = (ElementFunction*) ourmalloc(sizeof(ElementFunction));
-       GETELEMENTTYPE(tmp)= ELEMFUNCRETURN;
-       tmp->function=function;
-       tmp->overflowstatus = overflowstatus;
-       allocInlineArrayInitElement(&tmp->inputs, array, numArrays);
-       allocInlineDefVectorASTNode(GETELEMENTPARENTS(tmp));
+       ElementFunction* This = (ElementFunction*) ourmalloc(sizeof(ElementFunction));
+       GETELEMENTTYPE(This)= ELEMFUNCRETURN;
+       This->function=function;
+       This->overflowstatus = overflowstatus;
+       initArrayInitElement(&This->inputs, array, numArrays);
+       initDefVectorASTNode(GETELEMENTPARENTS(This));
        for(uint i=0;i<numArrays;i++)
-               pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) tmp);
-       initElementEncoding(&tmp->domainencoding, (Element *) tmp);
-       initFunctionEncoding(&tmp->functionencoding, (Element *) tmp);
-       return &tmp->base;
+               pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) This);
+       initElementEncoding(&This->domainencoding, (Element *) This);
+       initFunctionEncoding(&This->functionencoding, (Element *) This);
+       return &This->base;
 }
 
 Set* getElementSet(Element* This){
        switch(GETELEMENTTYPE(This)){
-               case ELEMSET:
-                       return ((ElementSet*)This)->set;
-               case ELEMFUNCRETURN:
-                       ;//Nope is needed for label assignment. i.e. next instruction isn't a statement 
-                       Function* func = ((ElementFunction*)This)->function;
-                       switch(GETFUNCTIONTYPE(func)){
-                               case TABLEFUNC:
-                                       return ((FunctionTable*)func)->table->range;
-                               case OPERATORFUNC:
-                                       return ((FunctionOperator*)func)->range;
-                               default:
-                                       ASSERT(0);
-                       }
+       case ELEMSET:
+               return ((ElementSet*)This)->set;
+       case ELEMFUNCRETURN: {
+               Function* func = ((ElementFunction*)This)->function;
+               switch(GETFUNCTIONTYPE(func)){
+               case TABLEFUNC:
+                       return ((FunctionTable*)func)->table->range;
+               case OPERATORFUNC:
+                       return ((FunctionOperator*)func)->range;
                default:
                        ASSERT(0);
+               }
+       }
+       default:
+               ASSERT(0);
        }
        ASSERT(0);
        return NULL;
@@ -65,9 +65,8 @@ void deleteElement(Element *This) {
                break;
        }
        default:
-               ;
+               ASSERT(0);
        }
        deleteVectorArrayASTNode(GETELEMENTPARENTS(This));
-
        ourfree(This);
 }

diff --git a/src/AST/element.h b/src/AST/element.h
index 509ee8c3d34566c21faf9f4e8d78d2fca84f6e4d..bce0073f3826a84d14ccf6907ae0dba506171aa9 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -34,6 +34,7 @@ Element * allocElementSet(Set *s);
 Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus);
 void deleteElement(Element *This);
 Set* getElementSet(Element* This);
+
 static inline ElementEncoding* getElementEncoding(Element* This){
        switch(GETELEMENTTYPE(This)){
                case ELEMSET:
@@ -46,9 +47,7 @@ static inline ElementEncoding* getElementEncoding(Element* This){
        return NULL;
 }
 
-
 static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func){
        return &func->functionencoding;
 }
-
 #endif

diff --git a/src/AST/function.c b/src/AST/function.c
index 61e413b88ebdf1ce42553288b4a1a0495bdc5c29..1aba4b78050a23b0c588a2d27df8b4da470434f6 100644 (file)
--- a/src/AST/function.c
+++ b/src/AST/function.c
@@ -3,10 +3,10 @@
 #include "set.h"
 
 
-Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior){
+Function* allocFunctionOperator(ArithOp op, Set ** domain, uint numDomain, Set * range, OverFlowBehavior overflowbehavior) {
        FunctionOperator* This = (FunctionOperator*) ourmalloc(sizeof(FunctionOperator));
        GETFUNCTIONTYPE(This)=OPERATORFUNC;
-       allocInlineArrayInitSet(&This->domains, domain, numDomain);
+       initArrayInitSet(&This->domains, domain, numDomain);
        This->op=op;
        This->overflowbehavior = overflowbehavior;
        This->range=range;
@@ -20,9 +20,9 @@ Function* allocFunctionTable (Table* table){
        return &This->base;
 }
 
-uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange){
+uint64_t applyFunctionOperator(FunctionOperator* This, uint64_t var1, uint64_t var2) {
        uint64_t result = 0;
-       switch( func->op){
+       switch(This->op){
                case ADD:
                        result = var1+ var2;
                        break;
@@ -32,10 +32,13 @@ uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t v
                default:
                        ASSERT(0);
        }
-       *isInRange = existsInSet(func->range, result);
        return result;
 }
 
+bool isInRangeFunction(FunctionOperator *This, uint64_t val) {
+       return existsInSet(This->range, val);
+}
+
 void deleteFunction(Function* This){
        switch(GETFUNCTIONTYPE(This)){
        case TABLEFUNC:

diff --git a/src/AST/function.h b/src/AST/function.h
index 158a55c9059f0650b2dbab700af63434781ea844..17a32112d0f636cee89a41205c0e79ea2cd42639 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -24,9 +24,10 @@ struct FunctionTable {
        Table* table;
 };
 
-Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior);
+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);
+uint64_t applyFunctionOperator(FunctionOperator* This, uint64_t var1, uint64_t var2);
+bool isInRangeFunction(FunctionOperator *This, uint64_t val);
 void deleteFunction(Function* This);
 
 #endif

diff --git a/src/AST/mutableset.c b/src/AST/mutableset.c
index 18f038b420548738fffcc945d1f8eb50305dbf5a..1c893a394aa9a83b1b46277232969de0fc6bab90 100644 (file)
--- a/src/AST/mutableset.c
+++ b/src/AST/mutableset.c
@@ -1,13 +1,13 @@
 #include "mutableset.h"
 
 MutableSet * allocMutableSet(VarType t) {
-       MutableSet * tmp=(MutableSet *)ourmalloc(sizeof(MutableSet));
-       tmp->type=t;
-       tmp->isRange=false;
-       tmp->low=0;
-       tmp->high=0;
-       tmp->members=allocDefVectorInt();
-       return tmp;
+       MutableSet * This=(MutableSet *)ourmalloc(sizeof(MutableSet));
+       This->type=t;
+       This->isRange=false;
+       This->low=0;
+       This->high=0;
+       This->members=allocDefVectorInt();
+       return This;
 }
 
 void addElementMSet(MutableSet * set, uint64_t element) {

diff --git a/src/AST/order.c b/src/AST/order.c
index b1b52e3e82df9fc52b4e5099a5f646a041eecec3..92c52ae64069a575a64d538284333fa924fd4c9c 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -3,35 +3,34 @@
 #include "set.h"
 #include "boolean.h"
 
-
 Order* allocOrder(OrderType type, Set * set){
-       Order* order = (Order*)ourmalloc(sizeof(Order));
-       order->set=set;
-       allocInlineDefVectorBoolean(& order->constraints);
-       order->type=type;
-       allocOrderEncoding(& order->order, order);
-       order->boolsToConstraints = NULL;
-       return order;
+       Order* This = (Order*)ourmalloc(sizeof(Order));
+       This->set=set;
+       initDefVectorBoolean(& This->constraints);
+       This->type=type;
+       initOrderEncoding(& This->order, This);
+       This->orderPairTable = NULL;
+       return This;
 }
 
-void initializeOrderHashTable(Order* order){
-       order->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+void initializeOrderHashTable(Order* This){
+       This->orderPairTable=allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
 }
 
-void addOrderConstraint(Order* order, BooleanOrder* constraint){
-       pushVectorBoolean( &order->constraints, (Boolean*) constraint);
+void addOrderConstraint(Order* This, BooleanOrder* constraint){
+       pushVectorBoolean( &This->constraints, (Boolean*) constraint);
 }
 
-void setOrderEncodingType(Order* order, OrderEncodingType type){
-       order->order.type = type;
+void setOrderEncodingType(Order* This, OrderEncodingType type){
+       This->order.type = type;
 }
 
-void deleteOrder(Order* order){
-       deleteVectorArrayBoolean(& order->constraints);
-       deleteOrderEncoding(& order->order);
-       if(order->boolsToConstraints!= NULL) {
-               resetAndDeleteHashTableBoolConst(order->boolsToConstraints);
-               deleteHashTableBoolConst(order->boolsToConstraints);
+void deleteOrder(Order* This){
+       deleteVectorArrayBoolean(& This->constraints);
+       deleteOrderEncoding(& This->order);
+       if(This->orderPairTable != NULL) {
+               resetAndDeleteHashTableOrderPair(This->orderPairTable);
+               deleteHashTableOrderPair(This->orderPairTable);
        }
-       ourfree(order);
+       ourfree(This);
 }

diff --git a/src/AST/order.h b/src/AST/order.h
index 67f0d9928b5406e0df0b2bbd0fcf21e4b169f3c1..bb35603069b3bb857da0a46223cb24d7e890baa0 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -10,14 +10,14 @@
 struct Order {
        OrderType type;
        Set * set;
-       HashTableBoolConst* boolsToConstraints;
+       HashTableOrderPair * orderPairTable;
        VectorBoolean constraints;
        OrderEncoding 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);
+void initializeOrderHashTable(Order * This);
+void addOrderConstraint(Order * This, BooleanOrder * constraint);
+void setOrderEncodingType(Order * This, OrderEncodingType type);
+void deleteOrder(Order * This);
 #endif

diff --git a/src/AST/predicate.c b/src/AST/predicate.c
index 116f152673cd3a2d23239a09d46c497b512a9c91..19e159760ddc897931494f1782826c64319489c3 100644 (file)
--- a/src/AST/predicate.c
+++ b/src/AST/predicate.c
@@ -3,29 +3,30 @@
 #include "set.h"
 
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){
-       PredicateOperator* predicate = ourmalloc(sizeof(PredicateOperator));
-       GETPREDICATETYPE(predicate)=OPERATORPRED;
-       allocInlineArrayInitSet(&predicate->domains, domain, numDomain);
-       predicate->op=op;
-       return &predicate->base;
+       PredicateOperator* This = ourmalloc(sizeof(PredicateOperator));
+       GETPREDICATETYPE(This)=OPERATORPRED;
+       initArrayInitSet(&This->domains, domain, numDomain);
+       This->op=op;
+       return &This->base;
 }
 
 Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){
-       PredicateTable* predicate = ourmalloc(sizeof(PredicateTable));
-       GETPREDICATETYPE(predicate) = TABLEPRED;
-       predicate->table=table;
-       predicate->undefinedbehavior=undefBehavior;
-       return &predicate->base;
+       PredicateTable* This = ourmalloc(sizeof(PredicateTable));
+       GETPREDICATETYPE(This) = TABLEPRED;
+       This->table=table;
+       This->undefinedbehavior=undefBehavior;
+       return &This->base;
 }
 
-void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64_t* result){
-       ASSERT( predicate->op == EQUALS);
+// BRIAN: REVISIT
+void getEqualitySetIntersection(PredicateOperator* This, uint* size, uint64_t* result){
+       ASSERT( This->op == EQUALS);
        //make sure equality has 2 operands
-       ASSERT(getSizeArraySet( &predicate->domains) == 2);
+       ASSERT(getSizeArraySet( &This->domains) == 2);
        *size=0;
-       VectorInt* mems1 = getArraySet(&predicate->domains, 0)->members; 
+       VectorInt* mems1 = getArraySet(&This->domains, 0)->members; 
        uint size1 = getSizeVectorInt(mems1);
-       VectorInt* mems2 = getArraySet(&predicate->domains, 1)->members;
+       VectorInt* mems2 = getArraySet(&This->domains, 1)->members;
        uint size2 = getSizeVectorInt(mems2);
        //FIXME:This isn't efficient, if we a hashset datastructure for Set, we
        // can reduce it to O(n), but for now .... HG
@@ -38,13 +39,12 @@ void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64
                        }
                }
        }
-       
 }
 
-void deletePredicate(Predicate* predicate){
-       switch(GETPREDICATETYPE(predicate)) {
+void deletePredicate(Predicate* This){
+       switch(GETPREDICATETYPE(This)) {
        case OPERATORPRED: {
-               PredicateOperator * operpred=(PredicateOperator *) predicate;
+               PredicateOperator * operpred=(PredicateOperator *) This;
                deleteInlineArraySet(&operpred->domains);
                break;
        }
@@ -53,6 +53,6 @@ void deletePredicate(Predicate* predicate){
        }
        }
        //need to handle freeing array...
-       ourfree(predicate);
+       ourfree(This);
 }
 

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 22f33d0e2e4bacaac23a6f22ac608e475d36c72c..6aaacce08de5c292ac5c363dd91b46ec40fa57e3 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -23,10 +23,9 @@ struct PredicateTable {
        UndefinedBehavior undefinedbehavior;
 };
 
-
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain);
 Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior);
 // size and result will be modified by this function!
-void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64_t* result);
-void deletePredicate(Predicate* predicate);
+void getEqualitySetIntersection(PredicateOperator* This, uint* size, uint64_t* result);
+void deletePredicate(Predicate* This);
 #endif

diff --git a/src/AST/set.c b/src/AST/set.c
index f72bbc33fbce11e11d9b1f317bc3c001e794614f..05aaf910e3cca2343b66895689da59db1432138c 100644 (file)
--- a/src/AST/set.c
+++ b/src/AST/set.c
@@ -2,48 +2,48 @@
 #include <stddef.h>
 
 Set * allocSet(VarType t, uint64_t* elements, uint num) {
-       Set * tmp=(Set *)ourmalloc(sizeof(Set));
-       tmp->type=t;
-       tmp->isRange=false;
-       tmp->low=0;
-       tmp->high=0;
-       tmp->members=allocVectorArrayInt(num, elements);
-       return tmp;
+       Set * This=(Set *)ourmalloc(sizeof(Set));
+       This->type=t;
+       This->isRange=false;
+       This->low=0;
+       This->high=0;
+       This->members=allocVectorArrayInt(num, elements);
+       return This;
 }
 
 Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) {
-       Set * tmp=(Set *)ourmalloc(sizeof(Set));
-       tmp->type=t;
-       tmp->isRange=true;
-       tmp->low=lowrange;
-       tmp->high=highrange;
-       tmp->members=NULL;
-       return tmp;
+       Set * This=(Set *)ourmalloc(sizeof(Set));
+       This->type=t;
+       This->isRange=true;
+       This->low=lowrange;
+       This->high=highrange;
+       This->members=NULL;
+       return This;
 }
 
-bool existsInSet(Set* set, uint64_t element){
-       if(set->isRange){
-               return element >= set->low && element <= set->high;
+bool existsInSet(Set* This, uint64_t element){
+       if(This->isRange){
+               return element >= This->low && element <= This->high;
        }else {
-               uint size = getSizeVectorInt(set->members);
+               uint size = getSizeVectorInt(This->members);
                for(uint i=0; i< size; i++){
-                       if(element == getVectorInt(set->members, i))
+                       if(element == getVectorInt(This->members, i))
                                return true;
                }
                return false;
        }
 }
 
-uint getSetSize(Set* set){
-       if(set->isRange){
-               return set->high- set->low+1;
+uint getSetSize(Set* This){
+       if(This->isRange){
+               return This->high- This->low+1;
        }else{
-               return getSizeVectorInt(set->members);
+               return getSizeVectorInt(This->members);
        }
 }
 
-void deleteSet(Set * set) {
-       if (!set->isRange)
-               deleteVectorInt(set->members);
-       ourfree(set);
+void deleteSet(Set * This) {
+       if (!This->isRange)
+               deleteVectorInt(This->members);
+       ourfree(This);
 }

diff --git a/src/AST/set.h b/src/AST/set.h
index badb28c4b6a165ce2e048fd7b4618ad41a3a4e5c..5139927e690e759592ab18ab5d326f090e0fffca 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -20,11 +20,10 @@ struct Set {
        VectorInt * members;
 };
 
-
-Set *allocSet(VarType t, uint64_t * elements, uint num);
+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);
+bool existsInSet(Set * This, uint64_t element);
+uint getSetSize(Set * This);
+void deleteSet(Set * This);
 #endif/* SET_H */
 

diff --git a/src/AST/table.c b/src/AST/table.c
index 2780aca127e2725a5bb5d9f37fdbde224d376e0f..72d23ddf7f1f9b8d06427f072e9ae7dcaec8fe56 100644 (file)
--- a/src/AST/table.c
+++ b/src/AST/table.c
@@ -5,27 +5,26 @@
 #include "set.h"
 #include "mutableset.h"
 
-
 Table * allocTable(Set **domains, uint numDomain, Set * range){
-       Table* table = (Table*) ourmalloc(sizeof(Table));
-       allocInlineArrayInitSet(&table->domains, domains, numDomain);
-       allocInlineDefVectorTableEntry(&table->entries);
-       table->range =range;
-       return table;
+       Table* This = (Table*) ourmalloc(sizeof(Table));
+       initArrayInitSet(&This->domains, domains, numDomain);
+       initDefVectorTableEntry(&This->entries);
+       This->range =range;
+       return This;
 }
 
-void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result){
-       ASSERT(getSizeArraySet( &table->domains) == inputSize);
-       pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result));
+void addNewTableEntry(Table* This, uint64_t* inputs, uint inputSize, uint64_t result){
+       ASSERT(getSizeArraySet( &This->domains) == inputSize);
+       pushVectorTableEntry(&This->entries, allocTableEntry(inputs, inputSize, result));
 }
 
-void deleteTable(Table* table){
-  deleteInlineArraySet(&table->domains);
-  uint size = getSizeVectorTableEntry(&table->entries);
+void deleteTable(Table* This){
+  deleteInlineArraySet(&This->domains);
+  uint size = getSizeVectorTableEntry(&This->entries);
   for(uint i=0; i<size; i++){
-    deleteTableEntry(getVectorTableEntry(&table->entries, i));
+    deleteTableEntry(getVectorTableEntry(&This->entries, i));
   }
-  deleteVectorArrayTableEntry(&table->entries);
-  ourfree(table);
+  deleteVectorArrayTableEntry(&This->entries);
+  ourfree(This);
 }
 

diff --git a/src/AST/table.h b/src/AST/table.h
index 90f50015071d9c701c9c76310602ee0da1813de4..d2df3a4d62b132aa0c54762b955562b53a5d7825 100644 (file)
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -10,7 +10,7 @@ struct Table {
        VectorTableEntry entries;
 };
 
-Table * allocTable(Set **domains, uint numDomain, Set * range);
-void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result);
-void deleteTable(Table* table);
+Table * allocTable(Set ** domains, uint numDomain, Set * range);
+void addNewTableEntry(Table * This, uint64_t * inputs, uint inputSize, uint64_t result);
+void deleteTable(Table * This);
 #endif

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index dbbd93f53d51e6143db4a1bdbda6bf1102c2f4df..c2a5bc9f9d3769c8592419e7069c358ab1f6e2db 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -117,7 +117,7 @@ CNFExpr * allocCNFExprBool(bool isTrue) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=0;
        This->isTrue=isTrue;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        return This;
 }
@@ -126,7 +126,7 @@ CNFExpr * allocCNFExprLiteral(Literal l) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=1;
        This->isTrue=false;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        addLiteralLitVector(&This->singletons, l);
        return This;

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 7f65364f357945557178915547e194ede587a797..e9f9aa0f35f1eecf72f5e42f60801fb7b145cc64 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -56,8 +56,8 @@ CNF * createCNF() {
        cnf->size=0;
        cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
        cnf->enableMatching=true;
-       allocInlineDefVectorEdge(& cnf->constraints);
-       allocInlineDefVectorEdge(& cnf->args);
+       initDefVectorEdge(& cnf->constraints);
+       initDefVectorEdge(& cnf->args);
        cnf->solver=allocIncrementalSolver();
        return cnf;
 }
@@ -309,7 +309,7 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge) {
        return result;
 }
 
-void addConstraint(CNF *cnf, Edge constraint) {
+void addConstraintCNF(CNF *cnf, Edge constraint) {
        pushVectorEdge(&cnf->constraints, constraint);
 }
 

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index ae22fdb4b53cebbdff9e3c937f067b2ee06016d1..2693455a0ba0f85da0c731709482c5b2de67d152 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -191,7 +191,7 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
-void addConstraint(CNF *cnf, Edge constraint);
+void addConstraintCNF(CNF *cnf, Edge constraint);
 int solveCNF(CNF *cnf);
 bool getValueCNF(CNF *cnf, Edge var);
 void printCNF(Edge e);

diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c
index 0754fd94b8b4ca0f8e0d31ff7fa5d69c294dfec5..8a37343935e4df02cefcb38c35bbece9bd940c8b 100644 (file)
--- a/src/Backend/inc_solver.c
+++ b/src/Backend/inc_solver.c
@@ -81,7 +81,6 @@ int solve(IncrementalSolver * This) {
        return getSolution(This);
 }
 
-
 void startSolve(IncrementalSolver *This) {
        addClauseLiteral(This, IS_RUNSOLVER);
        flushBufferSolver(This);
@@ -173,11 +172,15 @@ void killSolver(IncrementalSolver * This) {
                waitpid(This->solver_pid, &status, 0);
        }
 }
+
+//DEBUGGING CODE STARTS
 bool first=true;
+//DEBUGGING CODE ENDS
 
 void flushBufferSolver(IncrementalSolver * This) {
        ssize_t bytestowrite=sizeof(int)*This->offset;
        ssize_t byteswritten=0;
+       //DEBUGGING CODE STARTS
        for(uint i=0;i<This->offset;i++) {
                if (first)
                        printf("(");
@@ -191,6 +194,7 @@ void flushBufferSolver(IncrementalSolver * This) {
                        printf("%d", This->buffer[i]);
                }
        }
+       //DEBUGGING CODE ENDS
        do {
                ssize_t n=write(This->to_solver_fd, &((char *)This->buffer)[byteswritten], bytestowrite);
                if (n == -1) {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 838827de2f6613b49cc91aa74b78182d03554111..4b7d4474fed603db72fb2985febfeb7d645eac1f 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -71,7 +71,7 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
                Edge c= encodeConstraintSATEncoder(This, constraint);
                printCNF(c);
                printf("\n\n");
-               addConstraint(This->cnf, c);
+               addConstraintCNF(This->cnf, c);
        }
 }
 
@@ -145,22 +145,22 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
        return E_BOGUS;
 }
 
-Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
+Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * 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?
+               pair = &flipped;
        }
        Edge constraint;
-       if (!containsBoolConst(table, pair)) {
+       if (!containsOrderPair(table, pair)) {
                constraint = getNewVarSATEncoder(This);
                OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
-               putBoolConst(table, paircopy, paircopy);
+               putOrderPair(table, paircopy, paircopy);
        } else
-               constraint = getBoolConst(table, pair)->constraint;
+               constraint = getOrderPair(table, pair)->constraint;
        if (negate)
                return constraintNegate(constraint);
        else
@@ -170,20 +170,20 @@ Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair *
 
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
        ASSERT(boolOrder->order->type == TOTAL);
-       if(boolOrder->order->boolsToConstraints == NULL){
+       if(boolOrder->order->orderPairTable == NULL){
                initializeOrderHashTable(boolOrder->order);
                createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
-       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+       HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable;
        OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
-       Edge constraint = getPairConstraint(This, boolToConsts, & pair);
+       Edge constraint = getPairConstraint(This, orderPairTable, & pair);
        return constraint;
 }
 
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        ASSERT(order->type == TOTAL);
        VectorInt* mems = order->set->members;
-       HashTableBoolConst* table = order->boolsToConstraints;
+       HashTableOrderPair* table = order->orderPairTable;
        uint size = getSizeVectorInt(mems);
        uint csize =0;
        for(uint i=0; i<size; i++){
@@ -198,15 +198,15 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
                                OrderPair pairIK = {valueI, valueK};
                                Edge constIK = getPairConstraint(This, table, & pairIK);
                                Edge constJK = getPairConstraint(This, table, & pairJK);
-                               addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); 
+                               addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); 
                        }
                }
        }
 }
 
-Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        ASSERT(pair->first!= pair->second);
-       Edge constraint = getBoolConst(table, pair)->constraint;
+       Edge constraint = getOrderPair(table, pair)->constraint;
        if(pair->first > pair->second)
                return constraint;
        else
@@ -227,12 +227,12 @@ Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
        // when client specify sparse constraints for the total order!)
        ASSERT(constraint->order->type == PARTIAL);
 /*
-       HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-       if( containsBoolConst(boolToConsts, boolOrder) ){
-               return getBoolConst(boolToConsts, boolOrder);
+       HashTableOrderPair* boolToConsts = boolOrder->order->boolsToConstraints;
+       if( containsOrderPair(boolToConsts, boolOrder) ){
+               return getOrderPair(boolToConsts, boolOrder);
        } else {
                Edge constraint = getNewVarSATEncoder(This); 
-               putBoolConst(boolToConsts,boolOrder, constraint);
+               putOrderPair(boolToConsts,boolOrder, constraint);
                VectorBoolean* orderConstrs = &boolOrder->order->constraints;
                uint size= getSizeVectorBoolean(orderConstrs);
                for(uint i=0; i<size; i++){
@@ -409,9 +409,10 @@ Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunctio
                if(isinUseElement(elemEnc1, i)){
                        for( uint j=0; j<elemEnc2->encArraySize; j++){
                                if(isinUseElement(elemEnc2, j)){
-                                       bool isInRange = false;
                                        uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
-                                               elemEnc2->encodingArray[j], &isInRange);
+                                               elemEnc2->encodingArray[j]);
+                                       bool isInRange = isInRangeFunction((FunctionOperator*)This->function, result);
+
                                        //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, elemEnc1->element, elemEnc1->encodingArray[i]);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index c2705b410c7f81cef0adc6667a52ea0627c08c37..22b1b2edd1002932e1af7a206027177034b9e6d6 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -19,7 +19,7 @@ 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);
-Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
+Edge getOrderConstraint(HashTableOrderPair *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);

diff --git a/src/Collections/array.h b/src/Collections/array.h
index 73d0c32124a7cb873724179c2001aeeaa90103e4..19a22b3cdb7c947a70204f05623dfd53aa9a8212 100644 (file)
--- a/src/Collections/array.h
+++ b/src/Collections/array.h
@@ -37,12 +37,12 @@
        static inline void deleteInlineArray ## name(Array ## name *This) {                                     \
                ourfree(This->array);                                                                                                                                                                                           \
        }                                                                                                                                                                                                                                                                                       \
-       static inline void allocInlineArray ## name(Array ## name * This, uint size) {                  \
+       static inline void initArray ## name(Array ## name * This, uint size) {                 \
                This->size = size;                                                                                                                                                                                                      \
                This->array = (type *) ourcalloc(1, sizeof(type) * size);                                               \
        }                                                                                                                                                                                                                                                                                       \
-       static inline void allocInlineArrayInit ## name(Array ## name * This, type *array, uint size) { \
-               allocInlineArray ##name(This, size);                                                                                                                            \
+       static inline void initArrayInit ## name(Array ## name * This, type *array, uint size) { \
+               initArray ##name(This, size);                                                                                                                                                           \
                memcpy(This->array, array, size * sizeof(type));                                                                                \
        }
 

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 29c7abe0d5e7ba0809e6dfe40f12978f62b52c58..64821c9513a5020bee96da921ebae4c01953cf7e 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -29,4 +29,4 @@ static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
        return key1->first== key2->first && key1->second == key2->second;
 }
 
-HashTableImpl(BoolConst, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);
+HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 86addfbe03c21704998f0c06049c63e2d8689cde..3a4e81a8a0e26e477d6ec4c67cb1427bcc9ca196 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -22,7 +22,7 @@ VectorDef(ASTNode, ASTNode *);
 VectorDef(Int, uint64_t);
 
 HashTableDef(Void, void *, void *);
-HashTableDef(BoolConst, OrderPair *, OrderPair *);
+HashTableDef(OrderPair, OrderPair *, OrderPair *);
 
 HashSetDef(Void, void *);
 

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index e0ebebd035ac76afe61573a902f184109a8d69c6..650f33dc8352b3cea81983de89eb53af0a0054e7 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -23,9 +23,9 @@
        void clearVector ## name(Vector ## name *vector);                     \
        void deleteVectorArray ## name(Vector ## name *vector);                                                         \
        type * exposeArray ## name(Vector ## name * vector);                                                                    \
-       void allocInlineVector ## name(Vector ## name * vector, uint capacity); \
-       void allocInlineDefVector ## name(Vector ## name * vector);                                             \
-       void allocInlineVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
+       void initVector ## name(Vector ## name * vector, uint capacity); \
+       void initDefVector ## name(Vector ## name * vector);                                            \
+       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
 #define VectorImpl(name, type, defcap)                                  \
        Vector ## name * allocDefVector ## name() {                           \
@@ -91,16 +91,16 @@
        void deleteVectorArray ## name(Vector ## name *vector) {                                                        \
                ourfree(vector->array);                                             \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
+       void initVector ## name(Vector ## name * vector, uint capacity) { \
                vector->size = 0;                                                      \
                vector->capacity = capacity;                                                                                                                                                                                    \
                vector->array = (type *) ourmalloc(sizeof(type) * capacity);                            \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineDefVector ## name(Vector ## name * vector) {                                    \
-               allocInlineVector ## name(vector, defcap);                                                                                                      \
+       void initDefVector ## name(Vector ## name * vector) {                                   \
+               initVector ## name(vector, defcap);                                                                                                     \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {     \
-               allocInlineVector ##name(vector, capacity);                                                                                                     \
+       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {    \
+               initVector ##name(vector, capacity);                                                                                                    \
                vector->size=capacity;                                                                                                                                                                                  \
                memcpy(vector->array, array, capacity * sizeof(type));  \
        }

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 797f301c6ca3d67284d5b6d0d356045a374e703f..af9696f691e06ead7be9555bfce0e0e6bb3c95e8 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -25,6 +25,9 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
+void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
+void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
+
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
        return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
 }
@@ -33,7 +36,4 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
        This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
-void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
-
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 5b38732e6382e337f83b08bdcbb17d2138a3c874..5560526c2e5f9aec00d64b445722bc44ffca38ef 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -13,7 +13,7 @@
 #include "order.h"
 #include <strings.h>
 
-
+//BRIAN: MAKE FOLLOW TREE STRUCTURE
 void naiveEncodingDecision(CSolver* csolver){
        uint size = getSizeVectorElement(csolver->allElements);
        for(uint i=0; i<size; i++){
@@ -57,5 +57,3 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) {
                setInUseElement(This, i);
        }
 }
-
-

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 182e3da1027742255ebfd91755c77c51a75ff9bd..2b9fb87516c302ea1214f1c2a8958dea5a4e7ce8 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -3,11 +3,8 @@
 #include "classlist.h"
 #include "structs.h"
 
-
-
 /**
- *For now, This function just simply goes through elements/functions and 
- *assigns a predefined Encoding to each of them 
+ * The NaiveEncoder assigns a predefined Encoding to each Element and Function.
  * @param csolver
  * @param encoder
  */

diff --git a/src/Encoders/orderencoding.c b/src/Encoders/orderencoding.c
index 161704b5228978808eface4698b65af763afa742..1f1d93f514b8bc133f7ef12a855449a809fba402 100644 (file)
--- a/src/Encoders/orderencoding.c
+++ b/src/Encoders/orderencoding.c
@@ -1,6 +1,6 @@
 #include "orderencoding.h"
 
-void allocOrderEncoding(OrderEncoding * This, Order *order) {
+void initOrderEncoding(OrderEncoding * This, Order *order) {
        This->type=ORDER_UNASSIGNED;
        This->order=order;
 }

diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
index a101ea105699fa2571fe7e0cdb53d41b18b1ee7f..f408d665dd405b208ff0f3be4e4e39e2b6e30fcc 100644 (file)
--- a/src/Encoders/orderencoding.h
+++ b/src/Encoders/orderencoding.h
@@ -13,7 +13,7 @@ struct OrderEncoding {
        Order *order;
 };
 
-void allocOrderEncoding(OrderEncoding * This, Order *order);
+void initOrderEncoding(OrderEncoding * This, Order *order);
 void deleteOrderEncoding(OrderEncoding *This);
 
 #endif

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 222d4a11c74aec994f48ca90dc3e512d4c196656..c4440a7aade9bf54036b1c1dd8392e6cf687f45b 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -10,10 +10,10 @@ int main(int numargs, char ** argv) {
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
        Boolean * b=applyPredicate(solver, equals, inputs, 2);
-       addBoolean(solver, b);
+       addConstraint(solver, b);
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
-       addBoolean(solver, oc);
+       addConstraint(solver, oc);
                
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
@@ -37,7 +37,7 @@ int main(int numargs, char ** argv) {
        Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
        Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
-       addBoolean(solver, pred);
+       addConstraint(solver, pred);
        
        startEncoding(solver);
        deleteSolver(solver);

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index ebd79f52f9a788a460d0119e879eec4c8f3a75af..6740543ffaeef71821e83a5f0721310e1866295c 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -7,7 +7,6 @@ int main(int numargs, char ** argv) {
        Edge v2=constraintNewVar(cnf);
        Edge v3=constraintNewVar(cnf);
        Edge v4=constraintNewVar(cnf);
-       Edge v5=constraintNewVar(cnf);
 
        Edge nv1=constraintNegate(v1);
        Edge nv2=constraintNegate(v2);
@@ -18,10 +17,10 @@ int main(int numargs, char ** argv) {
        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);
+       Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4));
        printCNF(cor);
        printf("\n");
-       addConstraint(cnf, cor);
+       addConstraintCNF(cnf, cor);
        int value=solveCNF(cnf);
        if (value==1) {
                bool v1v=getValueCNF(cnf, v1);

diff --git a/src/csolver.c b/src/csolver.c
index 8c4f22e079a4a651d7806e46d72a4a807d792c93..40490d535c4ddc7723fa99cd6e7470b029e7cc8a 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -10,16 +10,16 @@
 #include "satencoder.h"
 
 CSolver * allocCSolver() {
-       CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver));
-       tmp->constraints=allocDefVectorBoolean();
-       tmp->allBooleans=allocDefVectorBoolean();
-       tmp->allSets=allocDefVectorSet();
-       tmp->allElements=allocDefVectorElement();
-       tmp->allPredicates = allocDefVectorPredicate();
-       tmp->allTables = allocDefVectorTable();
-       tmp->allOrders = allocDefVectorOrder();
-       tmp->allFunctions = allocDefVectorFunction();
-       return tmp;
+       CSolver * This=(CSolver *) ourmalloc(sizeof(CSolver));
+       This->constraints=allocDefVectorBoolean();
+       This->allBooleans=allocDefVectorBoolean();
+       This->allSets=allocDefVectorSet();
+       This->allElements=allocDefVectorElement();
+       This->allPredicates = allocDefVectorPredicate();
+       This->allTables = allocDefVectorTable();
+       This->allOrders = allocDefVectorOrder();
+       This->allFunctions = allocDefVectorFunction();
+       return This;
 }
 
 /** This function tears down the solver and the entire AST */
@@ -89,11 +89,11 @@ MutableSet * createMutableSet(CSolver * This, VarType type) {
        return set;
 }
 
-void addItem(CSolver *solver, MutableSet * set, uint64_t element) {
+void addItem(CSolver *This, MutableSet * set, uint64_t element) {
        addElementMSet(set, element);
 }
 
-uint64_t createUniqueItem(CSolver *solver, MutableSet * set) {
+uint64_t createUniqueItem(CSolver *This, MutableSet * set) {
        uint64_t element=set->low++;
        addElementMSet(set, element);
        return element;
@@ -105,76 +105,76 @@ Element * getElementVar(CSolver *This, Set * set) {
        return element;
 }
 
-Boolean * getBooleanVar(CSolver *solver, VarType type) {
-       Boolean* boolean= allocBoolean(type);
-       pushVectorBoolean(solver->allBooleans, boolean);
+Boolean * getBooleanVar(CSolver *This, VarType type) {
+       Boolean* boolean= allocBooleanVar(type);
+       pushVectorBoolean(This->allBooleans, boolean);
        return boolean;
 }
 
-Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior) {
+Function * createFunctionOperator(CSolver *This, ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior) {
        Function* function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
-       pushVectorFunction(solver->allFunctions, function);
+       pushVectorFunction(This->allFunctions, function);
        return function;
 }
 
-Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) {
+Predicate * createPredicateOperator(CSolver *This, CompOp op, Set ** domain, uint numDomain) {
        Predicate* predicate= allocPredicateOperator(op, domain,numDomain);
-       pushVectorPredicate(solver->allPredicates, predicate);
+       pushVectorPredicate(This->allPredicates, predicate);
        return predicate;
 }
 
-Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) {
+Table * createTable(CSolver *This, Set **domains, uint numDomain, Set * range) {
        Table* table= allocTable(domains,numDomain,range);
-       pushVectorTable(solver->allTables, table);
+       pushVectorTable(This->allTables, table);
        return table;
 }
 
-void addTableEntry(CSolver *solver, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) {
+void addTableEntry(CSolver *This, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) {
        addNewTableEntry(table,inputs, inputSize,result);
 }
 
-Function * completeTable(CSolver *solver, Table * table) {
+Function * completeTable(CSolver *This, Table * table) {
        Function* function = allocFunctionTable(table);
-       pushVectorFunction(solver->allFunctions,function);
+       pushVectorFunction(This->allFunctions,function);
        return function;
 }
 
-Element * applyFunction(CSolver *solver, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
+Element * applyFunction(CSolver *This, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
        Element* element= allocElementFunction(function,array,numArrays,overflowstatus);
-       pushVectorElement(solver->allElements, element);
+       pushVectorElement(This->allElements, element);
        return element;
 }
 
-Boolean * applyPredicate(CSolver *solver, Predicate * predicate, Element ** inputs, uint numInputs) {
+Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs) {
        Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
-       pushVectorBoolean(solver->allBooleans, boolean);
+       pushVectorBoolean(This->allBooleans, boolean);
        return boolean;
 }
 
-Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array, uint asize) {
-       return allocBooleanLogicArray(solver, op, array, asize);
+Boolean * applyLogicalOperation(CSolver *This, LogicOp op, Boolean ** array, uint asize) {
+       return allocBooleanLogicArray(This, op, array, asize);
 }
 
-void addBoolean(CSolver *This, Boolean * constraint) {
+void addConstraint(CSolver *This, Boolean * constraint) {
        pushVectorBoolean(This->constraints, constraint);
 }
 
-Order * createOrder(CSolver *solver, OrderType type, Set * set) {
+Order * createOrder(CSolver *This, OrderType type, Set * set) {
        Order* order = allocOrder(type, set);
-       pushVectorOrder(solver->allOrders, order);
+       pushVectorOrder(This->allOrders, order);
        return order;
 }
 
-Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64_t second) {
+Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t second) {
        Boolean* constraint = allocBooleanOrder(order, first, second);
-       pushVectorBoolean(solver->allBooleans,constraint);
+       pushVectorBoolean(This->allBooleans,constraint);
        return constraint;
 }
 
-void startEncoding(CSolver* solver){
-       naiveEncodingDecision(solver);
+void startEncoding(CSolver* This){
+       naiveEncodingDecision(This);
        SATEncoder* satEncoder = allocSATEncoder();
-       encodeAllSATEncoder(solver, satEncoder);
+       encodeAllSATEncoder(This, satEncoder);
        int result= solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
        for(uint i=1; i<=satEncoder->cnf->solver->solutionsize; i++){

diff --git a/src/csolver.h b/src/csolver.h
index bd90bf3054a5cbf85e4b506097391c2786e51d7d..827609c94abe3094f0d70c93add5e89949f44ec7 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -104,7 +104,7 @@ Boolean * applyLogicalOperation(CSolver *, LogicOp op, Boolean ** array, uint as
 /** This function adds a boolean constraint to the set of constraints
     to be satisfied */
 
-void addBoolean(CSolver *, Boolean * constraint);
+void addConstraint(CSolver *, Boolean * constraint);
 
 /** This function instantiates an order of type type over the set set. */
 Order * createOrder(CSolver *, OrderType type, Set * set);