edits

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index db1bd7df788be614f8292e93874ba952b0b23a48..12996bd42a7c30c2d11ba770b47a1deb207f1017 100644 (file)
--- 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 3b0f6e40464a271415836cc3d5f5e9bac298b9d8..e4d06fcfb75eb609ac53e04122c2c807957d5f6d 100644 (file)
--- 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 3a32139a03f1edb5acc1ab8fd8e4252968291d7f..c63becf15adc54eada5b26105ebedbd923a8a897 100644 (file)
--- 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 37e13762c512076905270524a37b533470bc48d0..914c43991926482ffb48886e5b2215625a236e9c 100644 (file)
--- 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 92bb55795004b90c97f0e2fd967e7ee9533494f0..f797d9b029d7e176c9503cb26119987bff415385 100644 (file)
--- 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 a4a7621d96bb794a6e5a90f035ce2b674fe0a6d5..65ff8fc180829b76543df89765cefb9c0e0a154d 100644 (file)
--- 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 dfc8596b6425e63a474725f5143939ca80266335..7b7e9bdd51a6d52b0f3b8b7551246a5443ad24c9 100644 (file)
--- 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 ff4ee8ce48e9abb1bc179c9eb4c2dbcc5992f0e0..f52ea6f6d1e07a07d0c460da3174ac8ac0cc2fe0 100644 (file)
--- 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 003379e003edb9ed64bb9aea0a4840f87a8e70ea..c9e64ffb035a60b8cf6c6f8777b1400efad8ba92 100644 (file)
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -1,56 +1,42 @@
 #include "set.h"
 #include <stddef.h>
 
-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 16fde20057370fc70cf9f4e5e265bb83f474971c..172f0a7abfb8bb28aa37111e0e1948d20667fc30 100644 (file)
--- 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 b903744dac3b9062495c224a7f2b1b80607d1bfb..3e8832784803ac64223d57421138eeb2bb53a259 100644 (file)
--- 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 d9a0c185f32d685d316f796f8306740d788dc36c..240eb29ab4da0ee0cbf8a7af85512e214aff7fe1 100644 (file)
--- 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 8e66c9b16b06ab040abd616f04865c6506f1da25..bdfc60e9eed0a2d718edaae25764bf75f780d8ec 100644 (file)
--- 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 44bbc3236a7b05ab2c3427482b4418c18c1039d9..132d6e3ed7bdd29eb419545fa058a28a8ef81a7c 100644 (file)
--- 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 cfa97fd6f4ee9da9c14d9ac1475a4a58cc1f10fe..a22f31add710430d00ad8c6325ba8c578bca154e 100644 (file)
--- 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 ca0fdaeccda4aeb69dcc1c5bfaa2f43b92832304..0be125611bbd258402e5ce5156e5ee5179c5f08c 100644 (file)
--- 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 71dc582cba636090189f7f097894ed390cbbaa8b..f078b8fc3f122e755e3df2d1a283eeac7fa199fa 100644 (file)
--- 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 9a5a42f684bdc2e5e9f6f94d1e6b609cce69b0df..42ac5aa07b027cff094e3b60a2b9cdd062af6aeb 100644 (file)
--- 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 a6728d65ffecb484547b70595a5b822c25b2c60e..0871a414d450f5a2906dd86d80f3f9f586e1a491 100644 (file)
--- 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 8baae7a27304f84a7718d83683505a6a2eae0722..5d748a699b40a047d451ab254fbd2097469fe0a9 100644 (file)
--- 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 51d8c7fb0c991f0e9e31bddd690be33e91b67119..918d484f5363256965da43d1f257885eced40828 100644 (file)
--- 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;
 }