From 78450a264304838bdf91bbab742dd32dae643fca Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Thu, 24 Aug 2017 17:47:01 -0700 Subject: [PATCH] edits --- src/AST/boolean.h | 14 +------- src/AST/element.cc | 4 +-- src/AST/function.cc | 38 ++++++---------------- src/AST/function.h | 26 ++++++++------- src/AST/order.cc | 50 ++++++++++++---------------- src/AST/order.h | 16 +++++---- src/AST/predicate.cc | 35 ++++---------------- src/AST/predicate.h | 24 ++++++++------ src/AST/set.cc | 52 +++++++++++------------------- src/AST/set.h | 18 +++++++---- src/AST/table.cc | 32 ++++++++---------- src/AST/table.h | 12 ++++--- src/Backend/satfuncopencoder.cc | 22 ++++++------- src/Backend/satfunctableencoder.cc | 20 ++++++------ src/Backend/satorderencoder.cc | 12 +++---- src/Backend/sattranslator.cc | 2 +- src/Encoders/naiveencoder.cc | 6 ++-- src/Encoders/orderencoder.cc | 4 +-- src/Encoders/ordergraph.cc | 10 +++--- src/classlist.h | 32 ++++++------------ src/csolver.cc | 32 +++++++++--------- 21 files changed, 192 insertions(+), 269 deletions(-) diff --git a/src/AST/boolean.h b/src/AST/boolean.h index db1bd7d..12996bd 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -52,10 +52,10 @@ class BooleanPredicate : public Boolean { FunctionEncoding encoding; ArrayElement inputs; Boolean *undefStatus; + FunctionEncoding * getFunctionEncoding() {return &encoding;} MEMALLOC; }; - class BooleanLogic : public Boolean { public: BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize); @@ -64,16 +64,4 @@ class BooleanLogic : public Boolean { ArrayBoolean inputs; MEMALLOC; }; - - - -Boolean *allocBooleanVar(VarType t); -Boolean *allocBooleanOrder(Order *order, uint64_t first, uint64_t second); -Boolean *allocBooleanPredicate(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus); -Boolean *allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean **array, uint asize); -void deleteBoolean(Boolean *This); -static inline FunctionEncoding *getPredicateFunctionEncoding(BooleanPredicate *func) { - return &func->encoding; -} - #endif diff --git a/src/AST/element.cc b/src/AST/element.cc index 3b0f6e4..e4d06fc 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -22,7 +22,7 @@ ElementFunction::ElementFunction(Function *_function, Element **array, uint numA ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) { uint64_t array[]={value}; - set = allocSet(_type, array, 1); + set = new Set(_type, array, 1); } Set *getElementSet(Element *This) { @@ -55,7 +55,7 @@ ElementFunction::~ElementFunction() { } ElementConst::~ElementConst() { - deleteSet(set); + delete set; } Element::~Element() { diff --git a/src/AST/function.cc b/src/AST/function.cc index 3a32139..c63becf 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -3,27 +3,16 @@ #include "set.h" -Function *allocFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior) { - FunctionOperator *This = (FunctionOperator *) ourmalloc(sizeof(FunctionOperator)); - GETFUNCTIONTYPE(This) = OPERATORFUNC; - initArrayInitSet(&This->domains, domain, numDomain); - This->op = op; - This->overflowbehavior = overflowbehavior; - This->range = range; - return &This->base; +FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : Function(OPERATORFUNC), op(_op), range(_range), overflowbehavior(_overflowbehavior) { + initArrayInitSet(&domains, domain, numDomain); } -Function *allocFunctionTable (Table *table, UndefinedBehavior undefBehavior) { - FunctionTable *This = (FunctionTable *) ourmalloc(sizeof(FunctionTable)); - GETFUNCTIONTYPE(This) = TABLEFUNC; - This->table = table; - This->undefBehavior = undefBehavior; - return &This->base; +FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) : Function(TABLEFUNC), table(_table), undefBehavior(_undefBehavior) { } -uint64_t applyFunctionOperator(FunctionOperator *This, uint numVals, uint64_t *values) { +uint64_t FunctionOperator::applyFunctionOperator(uint numVals, uint64_t *values) { ASSERT(numVals == 2); - switch (This->op) { + switch (op) { case ADD: return values[0] + values[1]; break; @@ -35,19 +24,10 @@ uint64_t applyFunctionOperator(FunctionOperator *This, uint numVals, uint64_t *v } } -bool isInRangeFunction(FunctionOperator *This, uint64_t val) { - return existsInSet(This->range, val); +bool FunctionOperator::isInRangeFunction(uint64_t val) { + return range->exists(val); } -void deleteFunction(Function *This) { - switch (GETFUNCTIONTYPE(This)) { - case TABLEFUNC: - break; - case OPERATORFUNC: - deleteInlineArraySet(&((FunctionOperator *) This)->domains); - break; - default: - ASSERT(0); - } - ourfree(This); +FunctionOperator::~FunctionOperator() { + deleteInlineArraySet(&domains); } diff --git a/src/AST/function.h b/src/AST/function.h index 37e1376..914c439 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -7,28 +7,32 @@ #define GETFUNCTIONTYPE(o) (((Function *)o)->type) -struct Function { +class Function { + public: + Function(FunctionType _type) : type(_type) {} FunctionType type; + MEMALLOC; }; -struct FunctionOperator { - Function base; +class FunctionOperator : public Function { + public: ArithOp op; ArraySet domains; Set *range; OverFlowBehavior overflowbehavior; + FunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior); + uint64_t applyFunctionOperator(uint numVals, uint64_t *values); + bool isInRangeFunction(uint64_t val); + ~FunctionOperator(); + MEMALLOC; }; -struct FunctionTable { - Function base; +class FunctionTable : public Function { + public: Table *table; UndefinedBehavior undefBehavior; + FunctionTable (Table *table, UndefinedBehavior behavior); + MEMALLOC; }; -Function *allocFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range, OverFlowBehavior overflowbehavior); -Function *allocFunctionTable (Table *table, UndefinedBehavior behavior); -uint64_t applyFunctionOperator(FunctionOperator *This, uint numVals, uint64_t *values); -bool isInRangeFunction(FunctionOperator *This, uint64_t val); -void deleteFunction(Function *This); - #endif diff --git a/src/AST/order.cc b/src/AST/order.cc index 92bb557..f797d9b 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -4,46 +4,38 @@ #include "boolean.h" #include "ordergraph.h" -Order *allocOrder(OrderType type, Set *set) { - Order *This = (Order *)ourmalloc(sizeof(Order)); - This->set = set; - initDefVectorBooleanOrder(&This->constraints); - This->type = type; - initOrderEncoding(&This->order, This); - This->orderPairTable = NULL; - This->elementTable = NULL; - This->graph = NULL; - return This; +Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), elementTable(NULL), graph(NULL) { + initDefVectorBooleanOrder(&constraints); + initOrderEncoding(&order, this); } -void initializeOrderHashTable(Order *This) { - This->orderPairTable = allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); +void Order::initializeOrderHashTable() { + orderPairTable = allocHashTableOrderPair(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); } -void initializeOrderElementsHashTable(Order *This){ - This->elementTable = allocHashSetOrderElement(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); +void Order::initializeOrderElementsHashTable() { + elementTable = allocHashSetOrderElement(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); } -void addOrderConstraint(Order *This, BooleanOrder *constraint) { - pushVectorBooleanOrder( &This->constraints, constraint); +void Order::addOrderConstraint(BooleanOrder *constraint) { + pushVectorBooleanOrder(&constraints, constraint); } -void setOrderEncodingType(Order *This, OrderEncodingType type) { - This->order.type = type; +void Order::setOrderEncodingType(OrderEncodingType type) { + order.type = type; } -void deleteOrder(Order *This) { - deleteVectorArrayBooleanOrder(&This->constraints); - deleteOrderEncoding(&This->order); - if (This->orderPairTable != NULL) { - resetAndDeleteHashTableOrderPair(This->orderPairTable); - deleteHashTableOrderPair(This->orderPairTable); +Order::~Order() { + deleteVectorArrayBooleanOrder(&constraints); + deleteOrderEncoding(&order); + if (orderPairTable != NULL) { + resetAndDeleteHashTableOrderPair(orderPairTable); + deleteHashTableOrderPair(orderPairTable); } - if(This->elementTable != NULL){ - deleteHashSetOrderElement(This->elementTable); + if(elementTable != NULL){ + deleteHashSetOrderElement(elementTable); } - if (This->graph != NULL) { - deleteOrderGraph(This->graph); + if (graph != NULL) { + deleteOrderGraph(graph); } - ourfree(This); } diff --git a/src/AST/order.h b/src/AST/order.h index a4a7621..65ff8fc 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -7,7 +7,10 @@ #include "orderencoding.h" #include "boolean.h" -struct Order { +class Order { + public: + Order(OrderType type, Set *set); + ~Order(); OrderType type; Set *set; HashTableOrderPair *orderPairTable; @@ -15,12 +18,11 @@ struct Order { OrderGraph *graph; VectorBooleanOrder constraints; OrderEncoding order; + void initializeOrderHashTable(); + void initializeOrderElementsHashTable(); + void addOrderConstraint(BooleanOrder *constraint); + void setOrderEncodingType(OrderEncodingType type); + MEMALLOC; }; -Order *allocOrder(OrderType type, Set *set); -void initializeOrderHashTable(Order *This); -void initializeOrderElementsHashTable(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.cc b/src/AST/predicate.cc index dfc8596..7b7e9bd 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -3,40 +3,19 @@ #include "set.h" #include "table.h" -Predicate *allocPredicateOperator(CompOp op, Set **domain, uint numDomain) { - PredicateOperator *This = (PredicateOperator *)ourmalloc(sizeof(PredicateOperator)); - GETPREDICATETYPE(This) = OPERATORPRED; - initArrayInitSet(&This->domains, domain, numDomain); - This->op = op; - return &This->base; +PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op) { + initArrayInitSet(&domains, domain, numDomain); } -Predicate *allocPredicateTable(Table *table, UndefinedBehavior undefBehavior) { - ASSERT(table->range == NULL); - PredicateTable *This = (PredicateTable *) ourmalloc(sizeof(PredicateTable)); - GETPREDICATETYPE(This) = TABLEPRED; - This->table = table; - This->undefinedbehavior = undefBehavior; - return &This->base; +PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) { } -void deletePredicate(Predicate *This) { - switch (GETPREDICATETYPE(This)) { - case OPERATORPRED: { - PredicateOperator *operpred = (PredicateOperator *) This; - deleteInlineArraySet(&operpred->domains); - break; - } - case TABLEPRED: { - break; - } - } - //need to handle freeing array... - ourfree(This); +PredicateOperator::~PredicateOperator() { + deleteInlineArraySet(&domains); } -bool evalPredicateOperator(PredicateOperator *This, uint64_t *inputs) { - switch (This->op) { +bool PredicateOperator::evalPredicateOperator(uint64_t *inputs) { + switch (op) { case EQUALS: return inputs[0] == inputs[1]; case LT: diff --git a/src/AST/predicate.h b/src/AST/predicate.h index ff4ee8c..f52ea6f 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -7,24 +7,28 @@ #define GETPREDICATETYPE(o) (((Predicate *)(o))->type) -struct Predicate { +class Predicate { + public: + Predicate(PredicateType _type) : type(_type) {} PredicateType type; + MEMALLOC; }; -struct PredicateOperator { - Predicate base; +class PredicateOperator : public Predicate { + public: + PredicateOperator(CompOp op, Set **domain, uint numDomain); + ~PredicateOperator(); + bool evalPredicateOperator(uint64_t *inputs); CompOp op; ArraySet domains; + MEMALLOC; }; -struct PredicateTable { - Predicate base; +class PredicateTable : public Predicate { + public: + PredicateTable(Table *table, UndefinedBehavior undefBehavior); Table *table; UndefinedBehavior undefinedbehavior; + MEMALLOC; }; - -Predicate *allocPredicateOperator(CompOp op, Set **domain, uint numDomain); -Predicate *allocPredicateTable(Table *table, UndefinedBehavior undefBehavior); -bool evalPredicateOperator(PredicateOperator *This, uint64_t *inputs); -void deletePredicate(Predicate *This); #endif diff --git a/src/AST/set.cc b/src/AST/set.cc index 003379e..c9e64ff 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -1,56 +1,42 @@ #include "set.h" #include -Set *allocSet(VarType t, uint64_t *elements, uint num) { - 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::Set(VarType t, uint64_t *elements, uint num) : type(t), isRange(false), low(0), high(0) { + members = allocVectorArrayInt(num, elements); } -Set *allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { - Set *This = (Set *)ourmalloc(sizeof(Set)); - This->type = t; - This->isRange = true; - This->low = lowrange; - This->high = highrange; - This->members = NULL; - return This; +Set::Set(VarType t, uint64_t lowrange, uint64_t highrange) : type(t), isRange(true), low(lowrange), high(highrange), members(NULL) { } -bool existsInSet(Set *This, uint64_t element) { - if (This->isRange) { - return element >= This->low && element <= This->high; +bool Set::exists(uint64_t element) { + if (isRange) { + return element >= low && element <= high; } else { - uint size = getSizeVectorInt(This->members); + uint size = getSizeVectorInt(members); for (uint i = 0; i < size; i++) { - if (element == getVectorInt(This->members, i)) + if (element == getVectorInt(members, i)) return true; } return false; } } -uint64_t getSetElement(Set *This, uint index) { - if (This->isRange) - return This->low + index; +uint64_t Set::getElement(uint index) { + if (isRange) + return low + index; else - return getVectorInt(This->members, index); + return getVectorInt(members, index); } -uint getSetSize(Set *This) { - if (This->isRange) { - return This->high - This->low + 1; +uint Set::getSize() { + if (isRange) { + return high - low + 1; } else { - return getSizeVectorInt(This->members); + return getSizeVectorInt(members); } } -void deleteSet(Set *This) { - if (!This->isRange) - deleteVectorInt(This->members); - ourfree(This); +Set::~Set() { + if (!isRange) + deleteVectorInt(members); } diff --git a/src/AST/set.h b/src/AST/set.h index 16fde20..172f0a7 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -12,19 +12,23 @@ #include "structs.h" #include "mymemory.h" -struct Set { +class Set { + public: + Set(VarType t, uint64_t *elements, uint num); + Set(VarType t, uint64_t lowrange, uint64_t highrange); + ~Set(); + bool exists(uint64_t element); + uint getSize(); + uint64_t getElement(uint index); + VarType type; bool isRange; uint64_t low;//also used to count unique items uint64_t high; VectorInt *members; + MEMALLOC; }; -Set *allocSet(VarType t, uint64_t *elements, uint num); -Set *allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); -bool existsInSet(Set *This, uint64_t element); -uint getSetSize(Set *This); -uint64_t getSetElement(Set *This, uint index); -void deleteSet(Set *This); + #endif/* SET_H */ diff --git a/src/AST/table.cc b/src/AST/table.cc index b903744..3e88327 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -5,41 +5,35 @@ #include "set.h" #include "mutableset.h" -Table *allocTable(Set **domains, uint numDomain, Set *range) { - Table *This = (Table *) ourmalloc(sizeof(Table)); - initArrayInitSet(&This->domains, domains, numDomain); - This->entries = allocHashSetTableEntry(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); - This->range = range; - return This; +Table::Table(Set **_domains, uint numDomain, Set *_range) : range(_range) { + initArrayInitSet(&domains, _domains, numDomain); + entries = allocHashSetTableEntry(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); } -void addNewTableEntry(Table *This, uint64_t *inputs, uint inputSize, uint64_t result) { - ASSERT(getSizeArraySet( &This->domains) == inputSize); +void Table::addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result) { #ifdef CONFIG_ASSERT - if (This->range == NULL) + if (range == NULL) ASSERT(result == true || result == false); #endif TableEntry *tb = allocTableEntry(inputs, inputSize, result); - ASSERT(!containsHashSetTableEntry(This->entries, tb)); - bool status = addHashSetTableEntry(This->entries, tb); + bool status = addHashSetTableEntry(entries, tb); ASSERT(status); } -TableEntry *getTableEntryFromTable(Table *table, uint64_t *inputs, uint inputSize) { +TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) { TableEntry *temp = allocTableEntry(inputs, inputSize, -1); - TableEntry *result = getHashSetTableEntry(table->entries, temp); + TableEntry *result = getHashSetTableEntry(entries, temp); deleteTableEntry(temp); return result; } -void deleteTable(Table *This) { - deleteInlineArraySet(&This->domains); - HSIteratorTableEntry *iterator = iteratorTableEntry(This->entries); +Table::~Table() { + deleteInlineArraySet(&domains); + HSIteratorTableEntry *iterator = iteratorTableEntry(entries); while (hasNextTableEntry(iterator)) { - deleteTableEntry( nextTableEntry(iterator) ); + deleteTableEntry(nextTableEntry(iterator)); } deleteIterTableEntry(iterator); - deleteHashSetTableEntry(This->entries); - ourfree(This); + deleteHashSetTableEntry(entries); } diff --git a/src/AST/table.h b/src/AST/table.h index d9a0c18..240eb29 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -4,14 +4,16 @@ #include "mymemory.h" #include "structs.h" -struct Table { +class Table { + public: + Table(Set **domains, uint numDomain, Set *range); + void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result); + TableEntry *getTableEntry(uint64_t *inputs, uint inputSize); + ~Table(); ArraySet domains; Set *range; HashSetTableEntry *entries; + MEMALLOC; }; -Table *allocTable(Set **domains, uint numDomain, Set *range); -void addNewTableEntry(Table *This, uint64_t *inputs, uint inputSize, uint64_t result); -TableEntry *getTableEntryFromTable(Table *table, uint64_t *inputs, uint inputSize); -void deleteTable(Table *This); #endif diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index 8e66c9b..bdfc60e 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -43,14 +43,14 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c uint64_t vals[numDomains];//setup value array for (uint i = 0; i < numDomains; i++) { Set *set = getArraySet(&predicate->domains, i); - vals[i] = getSetElement(set, indices[i]); + vals[i] = set->getElement(indices[i]); } bool notfinished = true; while (notfinished) { Edge carray[numDomains]; - if (evalPredicateOperator(predicate, vals) ^ generateNegation) { + if (predicate->evalPredicateOperator(vals) ^ generateNegation) { //Include this in the set of terms for (uint i = 0; i < numDomains; i++) { Element *elem = getArrayElement(&constraint->inputs, i); @@ -65,13 +65,13 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c uint index = ++indices[i]; Set *set = getArraySet(&predicate->domains, i); - if (index < getSetSize(set)) { - vals[i] = getSetElement(set, index); + if (index < set->getSize()) { + vals[i] = set->getElement(index); notfinished = true; break; } else { indices[i] = 0; - vals[i] = getSetElement(set, 0); + vals[i] = set->getElement(0); } } } @@ -106,7 +106,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * uint64_t vals[numDomains];//setup value array for (uint i = 0; i < numDomains; i++) { Set *set = getElementSet(getArrayElement(&func->inputs, i)); - vals[i] = getSetElement(set, indices[i]); + vals[i] = set->getElement(indices[i]); } Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var; @@ -115,8 +115,8 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * while (notfinished) { Edge carray[numDomains + 1]; - uint64_t result = applyFunctionOperator(function, numDomains, vals); - bool isInRange = isInRangeFunction((FunctionOperator *)func->function, result); + uint64_t result = function->applyFunctionOperator(numDomains, vals); + bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result); bool needClause = isInRange; if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) { needClause = true; @@ -176,13 +176,13 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * uint index = ++indices[i]; Set *set = getElementSet(getArrayElement(&func->inputs, i)); - if (index < getSetSize(set)) { - vals[i] = getSetElement(set, index); + if (index < set->getSize()) { + vals[i] = set->getElement(index); notfinished = true; break; } else { indices[i] = 0; - vals[i] = getSetElement(set, 0); + vals[i] = set->getElement(0); } } } diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 44bbc32..132d6e3 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -98,7 +98,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons uint64_t vals[numDomains];//setup value array for (uint i = 0; i < numDomains; i++) { Set *set = getArraySet(&predicate->table->domains, i); - vals[i] = getSetElement(set, indices[i]); + vals[i] = set->getElement(indices[i]); } bool hasOverflow = false; Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus); @@ -106,7 +106,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons bool notfinished = true; while (notfinished) { Edge carray[numDomains]; - TableEntry *tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains); + TableEntry *tableEntry = predicate->table->getTableEntry(vals, numDomains); bool isInRange = tableEntry != NULL; if (!isInRange && !hasOverflow) { hasOverflow = true; @@ -152,13 +152,13 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons uint index = ++indices[i]; Set *set = getArraySet(&predicate->table->domains, i); - if (index < getSetSize(set)) { - vals[i] = getSetElement(set, index); + if (index < set->getSize()) { + vals[i] = set->getElement(index); notfinished = true; break; } else { indices[i] = 0; - vals[i] = getSetElement(set, 0); + vals[i] = set->getElement(0); } } } @@ -247,14 +247,14 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el uint64_t vals[numDomains];//setup value array for (uint i = 0; i < numDomains; i++) { Set *set = getArraySet(&function->table->domains, i); - vals[i] = getSetElement(set, indices[i]); + vals[i] = set->getElement(indices[i]); } Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus); bool notfinished = true; while (notfinished) { Edge carray[numDomains + 1]; - TableEntry *tableEntry = getTableEntryFromTable(function->table, vals, numDomains); + TableEntry *tableEntry = function->table->getTableEntry(vals, numDomains); bool isInRange = tableEntry != NULL; ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED); for (uint i = 0; i < numDomains; i++) { @@ -302,13 +302,13 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el uint index = ++indices[i]; Set *set = getArraySet(&function->table->domains, i); - if (index < getSetSize(set)) { - vals[i] = getSetElement(set, index); + if (index < set->getSize()) { + vals[i] = set->getElement(index); notfinished = true; break; } else { indices[i] = 0; - vals[i] = getSetElement(set, 0); + vals[i] = set->getElement(0); } } } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index cfa97fd..a22f31a 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -43,7 +43,7 @@ Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ return gvalue; if (boolOrder->order->elementTable == NULL) { - initializeOrderElementsHashTable(boolOrder->order); + boolOrder->order->initializeOrderElementsHashTable(); } //getting two elements and using LT predicate ... Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first); @@ -59,10 +59,10 @@ Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ encodingArrayInitialization(encoding); } Set * sarray[]={order->set, order->set}; - Predicate *predicate =allocPredicateOperator(LT, sarray, 2); + Predicate *predicate =new PredicateOperator(LT, sarray, 2); Element * parray[]={elem1, elem2}; - Boolean * boolean=allocBooleanPredicate(predicate, parray, 2, NULL); - setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT); + BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL); + setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT); {//Adding new elements and boolean/predicate to solver regarding memory management pushVectorBoolean(This->solver->allBooleans, boolean); pushVectorPredicate(This->solver->allPredicates, predicate); @@ -101,7 +101,7 @@ Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) { HashSetOrderElement* eset = order->elementTable; OrderElement oelement ={item, NULL}; if( !containsHashSetOrderElement(eset, &oelement)){ - Element* elem = allocElementSet(order->set); + Element* elem = new ElementSet(order->set); ElementEncoding* encoding = getElementEncoding(elem); setElementEncodingType(encoding, BINARYINDEX); encodingArrayInitialization(encoding); @@ -139,7 +139,7 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { ASSERT(boolOrder->order->type == TOTAL); if (boolOrder->order->orderPairTable == NULL) { - initializeOrderHashTable(boolOrder->order); + boolOrder->order->initializeOrderHashTable(); bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); if (doOptOrderStructure) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); diff --git a/src/Backend/sattranslator.cc b/src/Backend/sattranslator.cc index ca0fdae..0be1256 100644 --- a/src/Backend/sattranslator.cc +++ b/src/Backend/sattranslator.cc @@ -59,7 +59,7 @@ uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemE uint64_t getElementValueSATTranslator(CSolver *This, Element *element) { ElementEncoding *elemEnc = getElementEncoding(element); if (elemEnc->numVars == 0)//case when the set has only one item - return getSetElement(getElementSet(element), 0); + return getElementSet(element)->getElement(0); switch (elemEnc->type) { case ONEHOT: return getElementValueOneHotSATTranslator(This, elemEnc); diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index 71dc582..f078b8f 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -28,7 +28,7 @@ void naiveEncodingConstraint(Boolean *This) { return; } case ORDERCONST: { - setOrderEncodingType( ((BooleanOrder *)This)->order, PAIRWISE ); + ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE); return; } case LOGICOP: { @@ -51,9 +51,9 @@ void naiveEncodingLogicOp(BooleanLogic *This) { } void naiveEncodingPredicate(BooleanPredicate *This) { - FunctionEncoding *encoding = getPredicateFunctionEncoding(This); + FunctionEncoding *encoding = This->getFunctionEncoding(); if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED) - setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS); + setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS); for (uint i = 0; i < getSizeArrayElement(&This->inputs); i++) { Element *element = getArrayElement(&This->inputs, i); diff --git a/src/Encoders/orderencoder.cc b/src/Encoders/orderencoder.cc index 9a5a42f..42ac5aa 100644 --- a/src/Encoders/orderencoder.cc +++ b/src/Encoders/orderencoder.cc @@ -405,7 +405,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { neworder = getVectorOrder(&ordervec, from->sccNum); if (neworder == NULL) { Set *set = (Set *) allocMutableSet(order->set->type); - neworder = allocOrder(order->type, set); + neworder = new Order(order->type, set); pushVectorOrder(This->allOrders, neworder); setExpandVectorOrder(&ordervec, from->sccNum, neworder); if (order->type == PARTIAL) @@ -427,7 +427,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); } orderconstraint->order = neworder; - addOrderConstraint(neworder, orderconstraint); + neworder->addOrderConstraint(orderconstraint); } } diff --git a/src/Encoders/ordergraph.cc b/src/Encoders/ordergraph.cc index a6728d6..0871a41 100644 --- a/src/Encoders/ordergraph.cc +++ b/src/Encoders/ordergraph.cc @@ -33,8 +33,8 @@ OrderGraph *buildMustOrderGraph(Order *order) { } void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) { - Polarity polarity = constr->base.polarity; - BooleanValue mustval = constr->base.boolVal; + Polarity polarity = constr->polarity; + BooleanValue mustval = constr->boolVal; Order *order = graph->order; switch (polarity) { case P_BOTHTRUEFALSE: @@ -45,7 +45,7 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean _1to2->polPos = true; addNewOutgoingEdge(node1, _1to2); addNewIncomingEdge(node2, _1to2); - if (constr->base.polarity == P_TRUE) + if (constr->polarity == P_TRUE) break; } case P_FALSE: { @@ -73,7 +73,7 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean } void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) { - BooleanValue mustval = constr->base.boolVal; + BooleanValue mustval = constr->boolVal; Order *order = graph->order; switch (mustval) { case BV_UNSAT: @@ -83,7 +83,7 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo _1to2->polPos = true; addNewOutgoingEdge(node1, _1to2); addNewIncomingEdge(node2, _1to2); - if (constr->base.boolVal == BV_MUSTBETRUE) + if (constr->boolVal == BV_MUSTBETRUE) break; } case BV_MUSTBEFALSE: { diff --git a/src/classlist.h b/src/classlist.h index 8baae7a..5d748a6 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -31,35 +31,23 @@ class ASTNode; struct IncrementalSolver; typedef struct IncrementalSolver IncrementalSolver; -struct Set; -typedef struct Set Set; -typedef struct Set MutableSet; +class Set; +typedef class Set MutableSet; class ElementFunction; class ElementSet; class ElementConst; class Element; -typedef struct FunctionOperator FunctionOperator; -typedef struct FunctionTable FunctionTable; +class FunctionOperator; +class FunctionTable; +class Function; -struct Function; -typedef struct Function Function; - -struct Predicate; -typedef struct Predicate Predicate; - -struct PredicateTable; -typedef struct PredicateTable PredicateTable; - -struct PredicateOperator; -typedef struct PredicateOperator PredicateOperator; - -struct Table; -typedef struct Table Table; - -struct Order; -typedef struct Order Order; +class Predicate; +class PredicateTable; +class PredicateOperator; +class Table; +class Order; struct OrderPair; typedef struct OrderPair OrderPair; diff --git a/src/csolver.cc b/src/csolver.cc index 51d8c7f..918d484 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -36,13 +36,13 @@ void deleteSolver(CSolver *This) { uint size = getSizeVectorBoolean(This->allBooleans); for (uint i = 0; i < size; i++) { - deleteBoolean(getVectorBoolean(This->allBooleans, i)); + delete getVectorBoolean(This->allBooleans, i); } deleteVectorBoolean(This->allBooleans); size = getSizeVectorSet(This->allSets); for (uint i = 0; i < size; i++) { - deleteSet(getVectorSet(This->allSets, i)); + delete getVectorSet(This->allSets, i); } deleteVectorSet(This->allSets); @@ -54,25 +54,25 @@ void deleteSolver(CSolver *This) { size = getSizeVectorTable(This->allTables); for (uint i = 0; i < size; i++) { - deleteTable(getVectorTable(This->allTables, i)); + delete getVectorTable(This->allTables, i); } deleteVectorTable(This->allTables); size = getSizeVectorPredicate(This->allPredicates); for (uint i = 0; i < size; i++) { - deletePredicate(getVectorPredicate(This->allPredicates, i)); + delete getVectorPredicate(This->allPredicates, i); } deleteVectorPredicate(This->allPredicates); size = getSizeVectorOrder(This->allOrders); for (uint i = 0; i < size; i++) { - deleteOrder(getVectorOrder(This->allOrders, i)); + delete getVectorOrder(This->allOrders, i); } deleteVectorOrder(This->allOrders); size = getSizeVectorFunction(This->allFunctions); for (uint i = 0; i < size; i++) { - deleteFunction(getVectorFunction(This->allFunctions, i)); + delete getVectorFunction(This->allFunctions, i); } deleteVectorFunction(This->allFunctions); deleteSATEncoder(This->satEncoder); @@ -81,13 +81,13 @@ void deleteSolver(CSolver *This) { } Set *createSet(CSolver *This, VarType type, uint64_t *elements, uint numelements) { - Set *set = allocSet(type, elements, numelements); + Set *set = new Set(type, elements, numelements); pushVectorSet(This->allSets, set); return set; } Set *createRangeSet(CSolver *This, VarType type, uint64_t lowrange, uint64_t highrange) { - Set *set = allocSetRange(type, lowrange, highrange); + Set *set = new Set(type, lowrange, highrange); pushVectorSet(This->allSets, set); return set; } @@ -121,31 +121,31 @@ Element *getElementConst(CSolver *This, VarType type, uint64_t value) { } Boolean *getBooleanVar(CSolver *This, VarType type) { - Boolean *boolean = allocBooleanVar(type); + Boolean *boolean = new BooleanVar(type); pushVectorBoolean(This->allBooleans, boolean); return boolean; } Function *createFunctionOperator(CSolver *This, ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) { - Function *function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior); + Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior); pushVectorFunction(This->allFunctions, function); return function; } Predicate *createPredicateOperator(CSolver *This, CompOp op, Set **domain, uint numDomain) { - Predicate *predicate = allocPredicateOperator(op, domain,numDomain); + Predicate *predicate = new PredicateOperator(op, domain,numDomain); pushVectorPredicate(This->allPredicates, predicate); return predicate; } Predicate *createPredicateTable(CSolver *This, Table *table, UndefinedBehavior behavior) { - Predicate *predicate = allocPredicateTable(table, behavior); + Predicate *predicate = new PredicateTable(table, behavior); pushVectorPredicate(This->allPredicates, predicate); return predicate; } Table *createTable(CSolver *This, Set **domains, uint numDomain, Set *range) { - Table *table = allocTable(domains,numDomain,range); + Table *table = new Table(domains,numDomain,range); pushVectorTable(This->allTables, table); return table; } @@ -155,11 +155,11 @@ Table *createTableForPredicate(CSolver *solver, Set **domains, uint numDomain) { } void addTableEntry(CSolver *This, Table *table, uint64_t *inputs, uint inputSize, uint64_t result) { - addNewTableEntry(table,inputs, inputSize,result); + table->addNewTableEntry(inputs, inputSize,result); } Function *completeTable(CSolver *This, Table *table, UndefinedBehavior behavior) { - Function *function = allocFunctionTable(table, behavior); + Function *function = new FunctionTable(table, behavior); pushVectorFunction(This->allFunctions,function); return function; } @@ -188,7 +188,7 @@ void addConstraint(CSolver *This, Boolean *constraint) { } Order *createOrder(CSolver *This, OrderType type, Set *set) { - Order *order = allocOrder(type, set); + Order *order = new Order(type, set); pushVectorOrder(This->allOrders, order); return order; } -- 2.34.1