#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;
+ allocInlineDefVectorBoolean(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);
+ allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+ return & This -> base;
}
Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs){
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);
#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;
+ allocInlineDefVectorASTNode(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;
+ allocInlineArrayInitElement(&This->inputs, array, numArrays);
+ allocInlineDefVectorASTNode(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;
break;
}
default:
- ;
+ ASSERT(0);
}
deleteVectorArrayASTNode(GETELEMENTPARENTS(This));
-
ourfree(This);
}
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:
return NULL;
}
-
static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func){
return &func->functionencoding;
}
-
#endif
#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);
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;
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:
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
#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) {
#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;
+ allocInlineDefVectorBoolean(& This->constraints);
+ This->type=type;
+ allocOrderEncoding(& This->order, This);
+ This->boolsToConstraints = NULL;
+ return This;
}
-void initializeOrderHashTable(Order* order){
- order->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+void initializeOrderHashTable(Order* This){
+ This->boolsToConstraints= allocHashTableBoolConst(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->boolsToConstraints!= NULL) {
+ resetAndDeleteHashTableBoolConst(This->boolsToConstraints);
+ deleteHashTableBoolConst(This->boolsToConstraints);
}
- ourfree(order);
+ ourfree(This);
}
};
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
#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;
+ allocInlineArrayInitSet(&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
}
}
}
-
}
-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;
}
}
}
//need to handle freeing array...
- ourfree(predicate);
+ ourfree(This);
}
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
#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);
}
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 */
#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));
+ allocInlineArrayInitSet(&This->domains, domains, numDomain);
+ allocInlineDefVectorTableEntry(&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);
}
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
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]);
}
Boolean * getBooleanVar(CSolver *solver, VarType type) {
- Boolean* boolean= allocBoolean(type);
+ Boolean* boolean= allocBooleanVar(type);
pushVectorBoolean(solver->allBooleans, boolean);
return boolean;
}