pushVectorBooleanOrder(&order->constraints, this);
}
-BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) : Boolean(PREDICATEOP), predicate(_predicate), undefStatus(_undefinedStatus) {
- initArrayInitElement(&inputs, _inputs, _numInputs);
-
+BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, Boolean *_undefinedStatus) :
+ Boolean(PREDICATEOP),
+ predicate(_predicate),
+ inputs(_inputs, _numInputs),
+ undefStatus(_undefinedStatus) {
for (uint i = 0; i < _numInputs; i++) {
pushVectorASTNode(GETELEMENTPARENTS(_inputs[i]), this);
}
initPredicateEncoding(&encoding, this);
}
-BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) : Boolean(LOGICOP), op(_op) {
- initArrayInitBoolean(&inputs, array, asize);
+BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize) :
+ Boolean(LOGICOP),
+ op(_op),
+ inputs(array, asize) {
pushVectorBoolean(solver->allBooleans, (Boolean *) this);
}
}
BooleanPredicate::~BooleanPredicate() {
- deleteInlineArrayElement(&inputs );
deleteFunctionEncoding(&encoding);
}
-
-BooleanLogic::~BooleanLogic() {
- deleteInlineArrayBoolean(&inputs);
-}
~BooleanPredicate();
Predicate *predicate;
FunctionEncoding encoding;
- ArrayElement inputs;
+ Array<Element *> inputs;
Boolean *undefStatus;
FunctionEncoding * getFunctionEncoding() {return &encoding;}
MEMALLOC;
class BooleanLogic : public Boolean {
public:
BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize);
- ~BooleanLogic();
LogicOp op;
- ArrayBoolean inputs;
+ Array<Boolean *> inputs;
MEMALLOC;
};
#endif
ElementSet::ElementSet(Set *s) : Element(ELEMSET), set(s) {
}
-ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : Element(ELEMFUNCRETURN), function(_function), overflowstatus(_overflowstatus) {
- initArrayInitElement(&inputs, array, numArrays);
+ElementFunction::ElementFunction(Function *_function, Element **array, uint numArrays, Boolean *_overflowstatus) : Element(ELEMFUNCRETURN), function(_function), inputs(array, numArrays), overflowstatus(_overflowstatus) {
for (uint i = 0; i < numArrays; i++)
pushVectorASTNode(GETELEMENTPARENTS(array[i]), this);
initFunctionEncoding(&functionencoding, this);
}
ElementFunction::~ElementFunction() {
- deleteInlineArrayElement(&inputs);
deleteFunctionEncoding(&functionencoding);
}
ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus);
~ElementFunction();
Function *function;
- ArrayElement inputs;
+ Array<Element *> inputs;
Boolean *overflowstatus;
FunctionEncoding functionencoding;
MEMALLOC;
#include "set.h"
-FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : Function(OPERATORFUNC), op(_op), range(_range), overflowbehavior(_overflowbehavior) {
- initArrayInitSet(&domains, domain, numDomain);
+FunctionOperator::FunctionOperator(ArithOp _op, Set **domain, uint numDomain, Set *_range, OverFlowBehavior _overflowbehavior) : Function(OPERATORFUNC), op(_op), domains(domain, numDomain), range(_range), overflowbehavior(_overflowbehavior) {
}
FunctionTable::FunctionTable (Table *_table, UndefinedBehavior _undefBehavior) : Function(TABLEFUNC), table(_table), undefBehavior(_undefBehavior) {
return range->exists(val);
}
-FunctionOperator::~FunctionOperator() {
- deleteInlineArraySet(&domains);
-}
class FunctionOperator : public Function {
public:
ArithOp op;
- ArraySet domains;
+ Array<Set *> 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;
};
#include "set.h"
#include "table.h"
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op) {
- initArrayInitSet(&domains, domain, numDomain);
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED) , op(_op), domains(domain, numDomain) {
}
PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {
}
-PredicateOperator::~PredicateOperator() {
- deleteInlineArraySet(&domains);
-}
-
bool PredicateOperator::evalPredicateOperator(uint64_t *inputs) {
switch (op) {
case EQUALS:
class PredicateOperator : public Predicate {
public:
PredicateOperator(CompOp op, Set **domain, uint numDomain);
- ~PredicateOperator();
bool evalPredicateOperator(uint64_t *inputs);
CompOp op;
- ArraySet domains;
+ Array<Set *> domains;
MEMALLOC;
};
Boolean *parent = getVectorBoolean(&oldb->parents, i);
BooleanLogic *logicop = (BooleanLogic *) parent;
- uint parentsize = getSizeArrayBoolean(&logicop->inputs);
+ uint parentsize = logicop->inputs.getSize();
for (uint j = 0; j < parentsize; j++) {
- Boolean *b = getArrayBoolean(&logicop->inputs, i);
+ Boolean *b = logicop->inputs.get(i);
if (b == oldb) {
- setArrayBoolean(&logicop->inputs, i, newb);
+ logicop->inputs.set(i, newb);
pushVectorBoolean(&newb->parents, parent);
}
}
}
void handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
- Boolean *b = getArrayBoolean(&bexpr->inputs, 0);
+ uint size = bexpr->inputs.getSize();
+ Boolean *b = bexpr->inputs.get(0);
uint childindex = (b == child) ? 0 : 1;
- removeElementArrayBoolean(&bexpr->inputs, childindex);
+ bexpr->inputs.remove(childindex);
bexpr->op = L_NOT;
}
void handleXORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
- Boolean *b = getArrayBoolean(&bexpr->inputs, 0);
+ uint size = bexpr->inputs.getSize();
+ Boolean *b = bexpr->inputs.get(0);
uint otherindex = (b == child) ? 1 : 0;
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, getArrayBoolean(&bexpr->inputs, otherindex));
+ replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(otherindex));
}
void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
- Boolean *b = getArrayBoolean(&bexpr->inputs, 0);
+ uint size = bexpr->inputs.getSize();
+ Boolean *b = bexpr->inputs.get(0);
if (b == child) {
//Replace with other term
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, getArrayBoolean(&bexpr->inputs, 1));
+ replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(1));
} else {
//Statement is true...
replaceBooleanWithTrue(This, (Boolean *)bexpr);
}
void handleIMPLIESFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
- Boolean *b = getArrayBoolean(&bexpr->inputs, 0);
+ uint size = bexpr->inputs.getSize();
+ Boolean *b = bexpr->inputs.get(0);
if (b == child) {
//Statement is true...
replaceBooleanWithTrue(This, (Boolean *)bexpr);
} else {
//Make into negation of first term
- removeElementArrayBoolean(&bexpr->inputs, 1);
+ bexpr->inputs.get(1);
bexpr->op = L_NOT;
}
}
void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
+ uint size = bexpr->inputs.getSize();
if (size == 1) {
replaceBooleanWithTrue(This, (Boolean *)bexpr);
}
for (uint i = 0; i < size; i++) {
- Boolean *b = getArrayBoolean(&bexpr->inputs, i);
+ Boolean *b = bexpr->inputs.get(i);
if (b == child) {
- removeElementArrayBoolean(&bexpr->inputs, i);
+ bexpr->inputs.remove(i);
}
}
if (size == 2) {
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, getArrayBoolean(&bexpr->inputs, 0));
+ replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
}
}
void handleORFalse(CSolver * This, BooleanLogic *bexpr, Boolean *child) {
- uint size = getSizeArrayBoolean(&bexpr->inputs);
+ uint size = bexpr->inputs.getSize();
if (size == 1) {
replaceBooleanWithFalse(This, (Boolean *) bexpr);
}
for (uint i = 0; i < size; i++) {
- Boolean *b = getArrayBoolean(&bexpr->inputs, i);
+ Boolean *b = bexpr->inputs.get(i);
if (b == child) {
- removeElementArrayBoolean(&bexpr->inputs, i);
+ bexpr->inputs.remove(i);
}
}
if (size == 2) {
- replaceBooleanWithBoolean(This, (Boolean *)bexpr, getArrayBoolean(&bexpr->inputs, 0));
+ replaceBooleanWithBoolean(This, (Boolean *)bexpr, bexpr->inputs.get(0));
}
}
#include "set.h"
#include "mutableset.h"
-Table::Table(Set **_domains, uint numDomain, Set *_range) : range(_range) {
- initArrayInitSet(&domains, _domains, numDomain);
+Table::Table(Set **_domains, uint numDomain, Set *_range) :
+ domains(_domains, numDomain),
+ range(_range) {
entries = allocHashSetTableEntry(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
}
}
Table::~Table() {
- deleteInlineArraySet(&domains);
HSIteratorTableEntry *iterator = iteratorTableEntry(entries);
while (hasNextTableEntry(iterator)) {
deleteTableEntry(nextTableEntry(iterator));
void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result);
TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
~Table();
- ArraySet domains;
+ Array<Set *> domains;
Set *range;
HashSetTableEntry *entries;
MEMALLOC;
void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
computeLogicOpBooleanValue(This);
computeLogicOpPolarity(This);
- uint size = getSizeArrayBoolean(&This->inputs);
+ uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
+ computePolarityAndBooleanValue(This->inputs.get(i));
}
}
switch (This->op) {
case L_AND:
case L_OR: {
- uint size = getSizeArrayBoolean(&This->inputs);
+ uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- Boolean *tmp = getArrayBoolean(&This->inputs, i);
+ Boolean *tmp = This->inputs.get(i);
updatePolarity(tmp, parentpolarity);
}
break;
}
case L_NOT: {
- Boolean *tmp = getArrayBoolean(&This->inputs, 0);
+ Boolean *tmp = This->inputs.get(0);
updatePolarity(tmp, negatePolarity(parentpolarity));
break;
}
case L_XOR: {
- updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
- updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
+ updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
+ updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
break;
}
case L_IMPLIES: {
- Boolean *left = getArrayBoolean(&This->inputs, 0);
+ Boolean *left = This->inputs.get(0);
updatePolarity(left, negatePolarity( parentpolarity));
- Boolean *right = getArrayBoolean(&This->inputs, 1);
+ Boolean *right = This->inputs.get(1);
updatePolarity(right, parentpolarity);
break;
}
switch (This->op) {
case L_AND: {
if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
+ uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+ updateMustValue(This->inputs.get(i), parentbv);
}
}
return;
}
case L_OR: {
if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
+ uint size = This->inputs.getSize();
for (uint i = 0; i < size; i++) {
- updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+ updateMustValue(This->inputs.get(i), parentbv);
}
}
return;
}
case L_NOT:
- updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+ updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
return;
case L_IMPLIES:
//implies is really an or with the first term negated
if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
- updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
- updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
+ uint size = This->inputs.getSize();
+ updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
+ updateMustValue(This->inputs.get(1), parentbv);
}
return;
case L_XOR:
}
Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
- Edge array[getSizeArrayBoolean(&constraint->inputs)];
- for (uint i = 0; i < getSizeArrayBoolean(&constraint->inputs); i++)
- array[i] = encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
+ Edge array[constraint->inputs.getSize()];
+ for (uint i = 0; i < constraint->inputs.getSize(); i++)
+ array[i] = encodeConstraintSATEncoder(This, constraint->inputs.get(i));
switch (constraint->op) {
case L_AND:
- return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
+ return constraintAND(This->cnf, constraint->inputs.getSize(), array);
case L_OR:
- return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
+ return constraintOR(This->cnf, constraint->inputs.getSize(), array);
case L_NOT:
- ASSERT( getSizeArrayBoolean(&constraint->inputs) == 1);
return constraintNegate(array[0]);
case L_XOR:
- ASSERT( getSizeArrayBoolean(&constraint->inputs) == 2);
return constraintXOR(This->cnf, array[0], array[1]);
case L_IMPLIES:
- ASSERT( getSizeArrayBoolean( &constraint->inputs) == 2);
return constraintIMPLIES(This->cnf, array[0], array[1]);
default:
model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *)constraint->predicate;
- uint numDomains = getSizeArraySet(&predicate->domains);
+ uint numDomains = predicate->domains.getSize();
FunctionEncodingType encType = constraint->encoding.type;
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement( &constraint->inputs, i);
+ Element *elem = constraint->inputs.get(i);
encodeElementSATEncoder(This, elem);
}
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getArraySet(&predicate->domains, i);
+ Set *set = predicate->domains.get(i);
vals[i] = set->getElement(indices[i]);
}
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);
+ Element *elem = constraint->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
Edge term = constraintAND(This->cnf, numDomains, carray);
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getArraySet(&predicate->domains, i);
+ Set *set = predicate->domains.get(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
model_print("Operator Function ...\n");
#endif
FunctionOperator *function = (FunctionOperator *) func->function;
- uint numDomains = getSizeArrayElement(&func->inputs);
+ uint numDomains = func->inputs.getSize();
/* Call base encoders for children */
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement( &func->inputs, i);
+ Element *elem = func->inputs.get(i);
encodeElementSATEncoder(This, elem);
}
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
+ Set *set = getElementSet(func->inputs.get(i));
vals[i] = set->getElement(indices[i]);
}
if (needClause) {
//Include this in the set of terms
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&func->inputs, i);
+ Element *elem = func->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
if (isInRange) {
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getElementSet(getArrayElement(&func->inputs, i));
+ Set *set = getElementSet(func->inputs.get(i));
if (index < set->getSize()) {
vals[i] = set->getElement(index);
Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
- ASSERT(getSizeArraySet(&predicate->domains) == 2);
- Element *elem0 = getArrayElement( &constraint->inputs, 0);
+ Element *elem0 = constraint->inputs.get(0);
encodeElementSATEncoder(This, elem0);
- Element *elem1 = getArrayElement( &constraint->inputs, 1);
+ Element *elem1 = constraint->inputs.get(1);
encodeElementSATEncoder(This, elem1);
ElementEncoding *ee0 = getElementEncoding(elem0);
ElementEncoding *ee1 = getElementEncoding(elem1);
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
Table *table = ((PredicateTable *)constraint->predicate)->table;
FunctionEncodingType encType = constraint->encoding.type;
- ArrayElement *inputs = &constraint->inputs;
- uint inputNum = getSizeArrayElement(inputs);
+ Array<Element*> * inputs = &constraint->inputs;
+ uint inputNum = inputs->getSize();
uint size = getSizeHashSetTableEntry(table->entries);
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge constraints[size];
}
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
- Element *el = getArrayElement(inputs, j);
+ Element *el = inputs->get(j);
carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
printCNF(carray[j]);
model_print("\n");
#endif
ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
//First encode children
- ArrayElement *inputs = &constraint->inputs;
- uint inputNum = getSizeArrayElement(inputs);
+ Array<Element *> *inputs = &constraint->inputs;
+ uint inputNum = inputs->getSize();
//Encode all the inputs first ...
for (uint i = 0; i < inputNum; i++) {
- encodeElementSATEncoder(This, getArrayElement(inputs, i));
+ encodeElementSATEncoder(This, inputs->get(i));
}
PredicateTable *predicate = (PredicateTable *)constraint->predicate;
switch (predicate->undefinedbehavior) {
break;
}
bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
- uint numDomains = getSizeArraySet(&predicate->table->domains);
+ uint numDomains = predicate->table->domains.getSize();
VectorEdge *clauses = allocDefVectorEdge();
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getArraySet(&predicate->table->domains, i);
+ Set *set = predicate->table->domains.get(i);
vals[i] = set->getElement(indices[i]);
}
bool hasOverflow = false;
}
Edge clause;
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&constraint->inputs, i);
+ Element *elem = constraint->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getArraySet(&predicate->table->domains, i);
+ Set *set = predicate->table->domains.get(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) {
UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior;
ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
- ArrayElement *elements = &func->inputs;
+ Array<Element *> *elements = &func->inputs;
Table *table = ((FunctionTable *) (func->function))->table;
uint size = getSizeHashSetTableEntry(table->entries);
Edge constraints[size];
while (hasNextTableEntry(iterator)) {
TableEntry *entry = nextTableEntry(iterator);
ASSERT(entry != NULL);
- uint inputNum = getSizeArrayElement(elements);
+ uint inputNum = elements->getSize();
Edge carray[inputNum];
for (uint j = 0; j < inputNum; j++) {
- Element *el = getArrayElement(elements, j);
+ Element *el = elements->get(j);
carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
}
Edge output = getElementValueConstraint(This, (Element *)func, entry->output);
#endif
ASSERT(GETFUNCTIONTYPE(elemFunc->function) == TABLEFUNC);
//First encode children
- ArrayElement *elements = &elemFunc->inputs;
- for (uint i = 0; i < getSizeArrayElement(elements); i++) {
- Element *elem = getArrayElement( elements, i);
+ Array<Element *> *elements = &elemFunc->inputs;
+ for (uint i = 0; i < elements->getSize(); i++) {
+ Element *elem = elements->get(i);
encodeElementSATEncoder(This, elem);
}
break;
}
- uint numDomains = getSizeArraySet(&function->table->domains);
+ uint numDomains = function->table->domains.getSize();
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
uint64_t vals[numDomains];//setup value array
for (uint i = 0; i < numDomains; i++) {
- Set *set = getArraySet(&function->table->domains, i);
+ Set *set = function->table->domains.get(i);
vals[i] = set->getElement(indices[i]);
}
bool isInRange = tableEntry != NULL;
ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
for (uint i = 0; i < numDomains; i++) {
- Element *elem = getArrayElement(&elemFunc->inputs, i);
+ Element *elem = elemFunc->inputs.get(i);
carray[i] = getElementValueConstraint(This, elem, vals[i]);
}
if (isInRange) {
notfinished = false;
for (uint i = 0; i < numDomains; i++) {
uint index = ++indices[i];
- Set *set = getArraySet(&function->table->domains, i);
+ Set *set = function->table->domains.get(i);
if (index < set->getSize()) {
vals[i] = set->getElement(index);
#ifndef ARRAY_H
#define ARRAY_H
-#define ArrayDef(name, type) \
- struct Array ## name { \
- type *array; \
- uint size; \
- }; \
- typedef struct Array ## name Array ## name; \
- static inline Array ## name *allocArray ## name(uint size) { \
- Array ## name * tmp = (Array ## name *)ourmalloc(sizeof(type)); \
- tmp->size = size; \
- tmp->array = (type *) ourcalloc(1, sizeof(type) * size); \
- return tmp; \
- } \
- static inline Array ## name *allocArrayInit ## name(type * array, uint size) { \
- Array ## name * tmp = allocArray ## name(size); \
- memcpy(tmp->array, array, size * sizeof(type)); \
- return tmp; \
- } \
- static inline void removeElementArray ## name(Array ## name * This, uint index) { \
- This->size--; \
- for (; index < This->size; index++) { \
- This->array[index] = This->array[index + 1]; \
- } \
- } \
- static inline type getArray ## name(Array ## name * This, uint index) { \
- return This->array[index]; \
- } \
- static inline void setArray ## name(Array ## name * This, uint index, type item) { \
- This->array[index] = item; \
- } \
- static inline uint getSizeArray ## name(Array ## name * This) { \
- return This->size; \
- } \
- static inline void deleteArray ## name(Array ## name * This) { \
- ourfree(This->array); \
- ourfree(This); \
- } \
- static inline type *exposeCArray ## name(Array ## name * This) { \
- return This->array; \
- } \
- static inline void deleteInlineArray ## name(Array ## name * This) { \
- ourfree(This->array); \
- } \
- static inline void initArray ## name(Array ## name * This, uint size) { \
- This->size = size; \
- This->array = (type *) ourcalloc(1, sizeof(type) * size); \
- } \
- static inline void initArrayInit ## name(Array ## name * This, type * array, uint size) { \
- initArray ## name(This, size); \
- memcpy(This->array, array, size * sizeof(type)); \
- }
+template<typename type>
+class Array {
+ public:
+ Array(uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
+ size(_size)
+ {
+ }
+
+ Array(type * _array, uint _size) :
+ array((type *)ourcalloc(1, sizeof(type) * _size)),
+ size(_size) {
+ memcpy(array, _array, _size * sizeof(type));
+ }
+
+ ~Array() {
+ ourfree(array);
+ }
+
+ void remove(uint index) {
+ size--;
+ for (; index < size; index++) {
+ array[index] = array[index + 1];
+ }
+ }
+
+ type get(uint index) {
+ return array[index];
+ }
+
+ void set(uint index, type item) {
+ array[index] = item;
+ }
+
+ uint getSize() {
+ return size;
+ }
+
+ type *expose() {
+ return array;
+ }
+
+ private:
+ type *array;
+ uint size;
+};
+
#endif
#include "classlist.h"
#include "array.h"
-ArrayDef(Element, Element *);
-ArrayDef(Boolean, Boolean *);
-ArrayDef(Set, Set *);
-
VectorDef(Table, Table *);
VectorDef(Set, Set *);
VectorDef(Boolean, Boolean *);
}
void naiveEncodingLogicOp(BooleanLogic *This) {
- for (uint i = 0; i < getSizeArrayBoolean(&This->inputs); i++) {
- naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
+ for (uint i = 0; i < This->inputs.getSize(); i++) {
+ naiveEncodingConstraint(This->inputs.get(i));
}
}
if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS);
- for (uint i = 0; i < getSizeArrayElement(&This->inputs); i++) {
- Element *element = getArrayElement(&This->inputs, i);
+ for (uint i = 0; i < This->inputs.getSize(); i++) {
+ Element *element = This->inputs.get(i);
naiveEncodingElement(element);
}
}
if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
ElementFunction *function = (ElementFunction *) This;
- for (uint i = 0; i < getSizeArrayElement(&function->inputs); i++) {
- Element *element = getArrayElement(&function->inputs, i);
+ for (uint i = 0; i < function->inputs.getSize(); i++) {
+ Element *element = function->inputs.get(i);
naiveEncodingElement(element);
}
FunctionEncoding *encoding = getElementFunctionEncoding(function);