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) :
}
BooleanPredicate::~BooleanPredicate() {
- deleteFunctionEncoding(&encoding);
}
#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) {
}
ElementFunction::~ElementFunction() {
- deleteFunctionEncoding(&functionencoding);
}
ElementConst::~ElementConst() {
}
Element::~Element() {
- deleteElementEncoding(&encoding);
}
#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() {
}
Order::~Order() {
- deleteOrderEncoding(&order);
if (orderPairTable != NULL) {
orderPairTable->resetanddelete();
delete orderPairTable;
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);
}
}
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];
}
}
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)
//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);
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;
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];
}
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];
}
#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);
+ }
+}
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 */
};
};
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
#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;
}
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
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);
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) {
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);
- }
-}
void naiveEncodingLogicOp(BooleanLogic *This);
void naiveEncodingPredicate(BooleanPredicate *This);
void naiveEncodingElement(Element *This);
-void encodingArrayInitialization(ElementEncoding *This);
-uint getSizeEncodingArray(ElementEncoding *, uint setSize);
-
#endif
#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) {
}
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
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;