edits
authorbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 08:54:32 +0000 (01:54 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 25 Aug 2017 08:54:32 +0000 (01:54 -0700)
15 files changed:
src/AST/boolean.cc
src/AST/element.cc
src/AST/order.cc
src/Backend/satelemencoder.cc
src/Backend/satorderencoder.cc
src/Backend/sattranslator.cc
src/Encoders/elementencoding.cc
src/Encoders/elementencoding.h
src/Encoders/functionencoding.cc
src/Encoders/functionencoding.h
src/Encoders/naiveencoder.cc
src/Encoders/naiveencoder.h
src/Encoders/orderencoding.cc
src/Encoders/orderencoding.h
src/classlist.h

index 3e05452019f17d6a576e68a610889ed2b81f4187..62f6bff6fc7c9e4c133aa10ce2f0abb04480761e 100644 (file)
@@ -28,12 +28,12 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
 BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) :
        Boolean(PREDICATEOP),
        predicate(_predicate),
+       encoding(this),
        inputs(_inputs, _numInputs),
        undefStatus(_undefinedStatus) {
        for (uint i = 0; i < _numInputs; i++) {
                GETELEMENTPARENTS(_inputs[i])->push(this);
        }
-       initPredicateEncoding(&encoding, this);
 }
 
 BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) :
@@ -44,5 +44,4 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint a
 }
 
 BooleanPredicate::~BooleanPredicate() {
-       deleteFunctionEncoding(&encoding);
 }
index fd9e470b696be28a953bcfdc57bd9cc673d19f2e..be4f77b5ffa50a13fe76cb938aa05e60b4b72ea4 100644 (file)
@@ -5,17 +5,24 @@
 #include "function.h"
 #include "table.h"
 
-Element::Element(ASTNodeType _type) : ASTNode(_type) {
-       initElementEncoding(&encoding, (Element *) this);
+Element::Element(ASTNodeType _type) :
+       ASTNode(_type),
+       encoding(this) {
 }
 
-ElementSet::ElementSet(Set *s) : Element(ELEMSET), set(s) {
+ElementSet::ElementSet(Set *s) :
+       Element(ELEMSET),
+       set(s) {
 }
 
-ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : Element(ELEMFUNCRETURN), function(_function), inputs(array, numArrays), overflowstatus(_overflowstatus) {
+ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) :
+       Element(ELEMFUNCRETURN),
+       function(_function),
+       inputs(array, numArrays),
+       overflowstatus(_overflowstatus),
+       functionencoding(this) {
        for (uint i = 0; i < numArrays; i++)
                GETELEMENTPARENTS(array[i])->push(this);
-       initFunctionEncoding(&functionencoding, this);
 }
 
 ElementConst::ElementConst(uint64_t _value, VarType _type) : Element(ELEMCONST), value(_value) {
@@ -48,7 +55,6 @@ Set *getElementSet(Element *This) {
 }
 
 ElementFunction::~ElementFunction() {
-       deleteFunctionEncoding(&functionencoding);
 }
 
 ElementConst::~ElementConst() {
@@ -56,5 +62,4 @@ ElementConst::~ElementConst() {
 }
 
 Element::~Element() {
-       deleteElementEncoding(&encoding);
 }
index 5d9fc4ebb1a9558371c6dc3cc3de2f531da1b3d8..5e16938fd04edd8b14b95be68eea09ac5270adef 100644 (file)
@@ -4,8 +4,13 @@
 #include "boolean.h"
 #include "ordergraph.h"
 
-Order::Order(OrderType _type, Set *_set) : type(_type), set(_set), orderPairTable(NULL), elementTable(NULL), graph(NULL) {
-       initOrderEncoding(&order, this);
+Order::Order(OrderType _type, Set *_set) :
+       type(_type),
+       set(_set),
+       orderPairTable(NULL),
+       elementTable(NULL),
+       graph(NULL),
+       order(this) {
 }
 
 void Order::initializeOrderHashTable() {
@@ -25,7 +30,6 @@ void Order::setOrderEncodingType(OrderEncodingType type) {
 }
 
 Order::~Order() {
-       deleteOrderEncoding(&order);
        if (orderPairTable != NULL) {
                orderPairTable->resetanddelete();
                delete orderPairTable;
index 5aaa162051cebf93fc54f6aa6a87662e815408b7..8513d924f5c50826598529d18dbe0049f9010ed7 100644 (file)
@@ -31,7 +31,7 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder *This, Element *elem, uint6
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
-               if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i] == value) {
+               if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        return (elemEnc->numVars == 0) ? E_True : generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
                }
        }
@@ -43,7 +43,7 @@ Edge getElementValueOneHotConstraint(SATEncoder *This, Element *elem, uint64_t v
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
-               if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i] == value) {
+               if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        return (elemEnc->numVars == 0) ? E_True : elemEnc->variables[i];
                }
        }
@@ -55,7 +55,7 @@ Edge getElementValueUnaryConstraint(SATEncoder *This, Element *elem, uint64_t va
        ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding *elemEnc = getElementEncoding(elem);
        for (uint i = 0; i < elemEnc->encArraySize; i++) {
-               if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i] == value) {
+               if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
                        if (elemEnc->numVars == 0)
                                return E_True;
                        if (i == 0)
index 4ca56e29b30181e37e599128a0b20d6ee6f4ab7c..e9c4824d459d9ccc8904fbf132ac23339e4be1f2 100644 (file)
@@ -48,21 +48,21 @@ Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
        //getting two elements and using LT predicate ...
        Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
        ElementEncoding *encoding = getElementEncoding(elem1);
-       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, BINARYINDEX);
-               encodingArrayInitialization(encoding);
+       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+               encoding->setElementEncodingType(BINARYINDEX);
+               encoding->encodingArrayInitialization();
        }
        Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
        encoding = getElementEncoding(elem2);
-       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, BINARYINDEX);
-               encodingArrayInitialization(encoding);
+       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+               encoding->setElementEncodingType(BINARYINDEX);
+               encoding->encodingArrayInitialization();
        }
        Set * sarray[]={order->set, order->set};
        Predicate *predicate =new PredicateOperator(LT, sarray, 2);
        Element * parray[]={elem1, elem2};
        BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL);
-       setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT);
+       boolean->getFunctionEncoding()->setFunctionEncodingType(CIRCUIT);
        {//Adding new elements and boolean/predicate to solver regarding memory management
                This->solver->allBooleans.push(boolean);
                This->solver->allPredicates.push(predicate);
@@ -103,8 +103,8 @@ Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
        if( !eset->contains(&oelement)){
                Element* elem = new ElementSet(order->set);
                ElementEncoding* encoding = getElementEncoding(elem);
-               setElementEncodingType(encoding, BINARYINDEX);
-               encodingArrayInitialization(encoding);
+               encoding->setElementEncodingType(BINARYINDEX);
+               encoding->encodingArrayInitialization();
                encodeElementSATEncoder(This, elem);
                eset->add(allocOrderElement(item, elem));
                return elem;
index b028bf86777bd24a69546db8a93d3c600b43070d..94f6e18cf15d1beab675ed38b0b3407b67d9e281 100644 (file)
@@ -13,8 +13,8 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
-       model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
-       ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
+       model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, elemEnc->isinUseElement(index));
+       ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
        return elemEnc->encodingArray[index];
 }
 
@@ -41,7 +41,7 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
-       ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
+       ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
        return elemEnc->encodingArray[index];
 }
 
index dde2692d6894c207e6fc541db5852e0848f9845f..69036a1f2a7baf210340db31711d0ecec9dd6862 100644 (file)
@@ -3,38 +3,50 @@
 #include "naiveencoder.h"
 #include "element.h"
 #include "satencoder.h"
+#include "set.h"
 
-void initElementEncoding(ElementEncoding *This, Element *element) {
-       This->element = element;
-       This->type = ELEM_UNASSIGNED;
-       This->variables = NULL;
-       This->encodingArray = NULL;
-       This->inUseArray = NULL;
-       This->numVars = 0;
-       This->encArraySize = 0;
+ElementEncoding::ElementEncoding(Element *_element) :
+       type(ELEM_UNASSIGNED),
+       element(_element),
+       variables(NULL),
+       encodingArray(NULL),
+       inUseArray(NULL),
+       encArraySize(0),
+       numVars(0) {
 }
 
-void deleteElementEncoding(ElementEncoding *This) {
-       if (This->variables != NULL)
-               ourfree(This->variables);
-       if (This->encodingArray != NULL)
-               ourfree(This->encodingArray);
-       if (This->inUseArray != NULL)
-               ourfree(This->inUseArray);
+ElementEncoding::~ElementEncoding() {
+       if (variables != NULL)
+               ourfree(variables);
+       if (encodingArray != NULL)
+               ourfree(encodingArray);
+       if (inUseArray != NULL)
+               ourfree(inUseArray);
 }
 
-void allocEncodingArrayElement(ElementEncoding *This, uint size) {
-       This->encodingArray = (uint64_t *) ourcalloc(1, sizeof(uint64_t) * size);
-       This->encArraySize = size;
+void ElementEncoding::allocEncodingArrayElement(uint size) {
+       encodingArray = (uint64_t *) ourcalloc(1, sizeof(uint64_t) * size);
+       encArraySize = size;
 }
 
-void allocInUseArrayElement(ElementEncoding *This, uint size) {
+void ElementEncoding::allocInUseArrayElement(uint size) {
        uint bytes = ((size + ((1 << 9) - 1)) >> 6) & ~7;//Depends on size of inUseArray
-       This->inUseArray = (uint64_t *) ourcalloc(1, bytes);
+       inUseArray = (uint64_t *) ourcalloc(1, bytes);
 }
 
-void setElementEncodingType(ElementEncoding *This, ElementEncodingType type) {
-       This->type = type;
+void ElementEncoding::setElementEncodingType(ElementEncodingType _type) {
+       type = _type;
 }
 
-
+void ElementEncoding::encodingArrayInitialization() {
+       Set *set = getElementSet(element);
+       ASSERT(!set->isRange);
+       uint size = set->members->getSize();
+       uint encSize = getSizeEncodingArray(size);
+       allocEncodingArrayElement(encSize);
+       allocInUseArrayElement(encSize);
+       for (uint i = 0; i < size; i++) {
+               encodingArray[i] = set->members->get(i);
+               setInUseElement(i);
+       }
+}
index c0f0d2d9e774270d30ee4c934fad0d23e91aa627..27ff2488fb16db80f6544f0a3ec9a36a26316685 100644 (file)
@@ -10,7 +10,33 @@ enum ElementEncodingType {
 
 typedef enum ElementEncodingType ElementEncodingType;
 
-struct ElementEncoding {
+class ElementEncoding {
+ public:
+       ElementEncoding(Element *element);
+       ElementEncodingType getElementEncodingType() {return type;}
+       ~ElementEncoding();
+       void setElementEncodingType(ElementEncodingType type);
+       void deleteElementEncoding();
+       void allocEncodingArrayElement(uint size);
+       void allocInUseArrayElement(uint size);
+       uint numEncodingVars() {return numVars;}
+       bool isinUseElement(uint offset) { return (inUseArray[(offset >> 6)] >> (offset & 63)) & 0x1;}
+       void setInUseElement(uint offset) {inUseArray[(offset >> 6)] |= 1 << (offset & 63);}
+       void encodingArrayInitialization();
+       uint getSizeEncodingArray(uint setSize) {
+               switch (type) {
+               case BINARYINDEX:
+                       return NEXTPOW2(setSize);
+               case ONEHOT:
+               case UNARY:
+                       return setSize;
+               default:
+                       ASSERT(0);
+               }
+               return -1;
+       }
+
+       
        ElementEncodingType type;
        Element *element;
        Edge *variables;/* List Variables Used To Encode Element */
@@ -29,22 +55,9 @@ struct ElementEncoding {
                };
        };
        uint numVars;   /* Number of variables */
+       MEMALLOC;
 };
 
-void initElementEncoding(ElementEncoding *This, Element *element);
-static inline ElementEncodingType getElementEncodingType(ElementEncoding *This) {return This->type;}
-void setElementEncodingType(ElementEncoding *This, ElementEncodingType type);
-void deleteElementEncoding(ElementEncoding *This);
-void allocEncodingArrayElement(ElementEncoding *This, uint size);
-void allocInUseArrayElement(ElementEncoding *This, uint size);
-static inline uint numEncodingVars(ElementEncoding *This) {return This->numVars;}
-
-static inline bool isinUseElement(ElementEncoding *This, uint offset) {
-       return (This->inUseArray[(offset >> 6)] >> (offset & 63)) & 0x1;
-}
 
-static inline void setInUseElement(ElementEncoding *This, uint offset) {
-       This->inUseArray[(offset >> 6)] |= 1 << (offset & 63);
-}
 
 #endif
index 75910cfe307c3a3648f6358748f9de64fdafe592..7086f5f75e7e30676bc28daefd509c58e6468314 100644 (file)
@@ -1,18 +1,17 @@
 #include "functionencoding.h"
 
-void initFunctionEncoding(FunctionEncoding *This, Element *function) {
-       This->op.function = function;
-       This->type = FUNC_UNASSIGNED;
+FunctionEncoding::FunctionEncoding(Element *function) :
+       type(FUNC_UNASSIGNED)
+{
+       op.function = function;
 }
 
-void initPredicateEncoding(FunctionEncoding *This,  Boolean *predicate) {
-       This->op.predicate = predicate;
-       This->type = FUNC_UNASSIGNED;
+FunctionEncoding::FunctionEncoding(Boolean *predicate) :
+       type(FUNC_UNASSIGNED)
+{
+       op.predicate = predicate;
 }
 
-void deleteFunctionEncoding(FunctionEncoding *This) {
-}
-
-void setFunctionEncodingType(FunctionEncoding *encoding, FunctionEncodingType type) {
-       encoding->type = type;
+void FunctionEncoding::setFunctionEncodingType(FunctionEncodingType _type) {
+       type = _type;
 }
index bc98cd3be44fcc7891b6c15b3d5a9358e4af9986..0919a9ea9b90bfe269dafe37ac652019971ae7ef 100644 (file)
@@ -15,16 +15,18 @@ union ElementPredicate {
 
 typedef union ElementPredicate ElementPredicate;
 
-struct FunctionEncoding {
+class FunctionEncoding {
+ public:
        FunctionEncodingType type;
        bool isFunction;//true for function, false for predicate
        ElementPredicate op;
+       FunctionEncoding(Element *function);
+       FunctionEncoding(Boolean *predicate);
+       void setFunctionEncodingType(FunctionEncodingType type);
+       FunctionEncodingType getFunctionEncodingType() {return type;}
+       MEMALLOC;
 };
 
-void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
-void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
-void setFunctionEncodingType(FunctionEncoding *encoding, FunctionEncodingType type);
-static inline FunctionEncodingType getFunctionEncodingType(FunctionEncoding *This) {return This->type;}
-void deleteFunctionEncoding(FunctionEncoding *This);
+
 
 #endif
index 5cd785cdd45cc447415f6d2111ab46fd97ce997f..826ba8f7bb5ecbb07fd6e141cad1c655043ceeb6 100644 (file)
@@ -52,8 +52,8 @@ void naiveEncodingLogicOp(BooleanLogic *This) {
 
 void naiveEncodingPredicate(BooleanPredicate *This) {
        FunctionEncoding *encoding = This->getFunctionEncoding();
-       if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
-               setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS);
+       if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+               This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
 
        for (uint i = 0; i < This->inputs.getSize(); i++) {
                Element *element = This->inputs.get(i);
@@ -63,9 +63,9 @@ void naiveEncodingPredicate(BooleanPredicate *This) {
 
 void naiveEncodingElement(Element *This) {
        ElementEncoding *encoding = getElementEncoding(This);
-       if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, BINARYINDEX);
-               encodingArrayInitialization(encoding);
+       if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+               encoding->setElementEncodingType(BINARYINDEX);
+               encoding->encodingArrayInitialization();
        }
 
        if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
@@ -75,34 +75,8 @@ void naiveEncodingElement(Element *This) {
                        naiveEncodingElement(element);
                }
                FunctionEncoding *encoding = getElementFunctionEncoding(function);
-               if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
-                       setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
+               if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
+                       getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
        }
 }
 
-uint getSizeEncodingArray(ElementEncoding *This, uint setSize) {
-       switch (This->type) {
-       case BINARYINDEX:
-               return NEXTPOW2(setSize);
-       case ONEHOT:
-       case UNARY:
-               return setSize;
-       default:
-               ASSERT(0);
-       }
-       return -1;
-}
-
-void encodingArrayInitialization(ElementEncoding *This) {
-       Element *element = This->element;
-       Set *set = getElementSet(element);
-       ASSERT(set->isRange == false);
-       uint size = set->members->getSize();
-       uint encSize = getSizeEncodingArray(This, size);
-       allocEncodingArrayElement(This, encSize);
-       allocInUseArrayElement(This, encSize);
-       for (uint i = 0; i < size; i++) {
-               This->encodingArray[i] = set->members->get(i);
-               setInUseElement(This, i);
-       }
-}
index c3260a050e92a99a0809c25a048b6395b5f54a6d..dbc9148d6199d72257498de94791381f3f5417d6 100644 (file)
@@ -14,7 +14,4 @@ void naiveEncodingConstraint(Boolean *This);
 void naiveEncodingLogicOp(BooleanLogic *This);
 void naiveEncodingPredicate(BooleanPredicate *This);
 void naiveEncodingElement(Element *This);
-void encodingArrayInitialization(ElementEncoding *This);
-uint getSizeEncodingArray(ElementEncoding *, uint setSize);
-
 #endif
index 51dddccc52b4263a7e1ea1bd9fc3b12b63a8b7df..5e81f14cd6ab262b523df65ca7756eb6e6e4c176 100644 (file)
@@ -1,9 +1,6 @@
 #include "orderencoding.h"
 
-void initOrderEncoding(OrderEncoding *This, Order *order) {
-       This->type = ORDER_UNASSIGNED;
-       This->order = order;
-}
-
-void deleteOrderEncoding(OrderEncoding *This) {
+OrderEncoding::OrderEncoding(Order *_order) :
+       type(ORDER_UNASSIGNED),
+       order(_order) {
 }
index 35ad5649afa8344a241a31a18f97b76bb07a6665..766245ee5b1418e9157ae32ed3d959b6fab7a757 100644 (file)
@@ -8,12 +8,13 @@ enum OrderEncodingType {
 
 typedef enum OrderEncodingType OrderEncodingType;
 
-struct OrderEncoding {
+class OrderEncoding {
+ public:
+       OrderEncoding(Order *order);
+
        OrderEncodingType type;
        Order *order;
+       MEMALLOC;
 };
 
-void initOrderEncoding(OrderEncoding *This, Order *order);
-void deleteOrderEncoding(OrderEncoding *This);
-
 #endif
index fe87c3b86dd98457cbf8e5030c63794a758a1526..92cc697f4f14c007e1c198337e06c578866f10f4 100644 (file)
@@ -50,14 +50,9 @@ typedef struct IncrementalSolver IncrementalSolver;
 struct OrderElement;
 typedef struct OrderElement OrderElement;
 
-struct ElementEncoding;
-typedef struct ElementEncoding ElementEncoding;
-
-struct FunctionEncoding;
-typedef struct FunctionEncoding FunctionEncoding;
-
-struct OrderEncoding;
-typedef struct OrderEncoding OrderEncoding;
+class ElementEncoding;
+class FunctionEncoding;
+class OrderEncoding;
 
 struct TableEntry;
 typedef struct TableEntry TableEntry;