From 918b2bcc43064f8557738e13c2fcc98b96736836 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 21:36:05 -0700 Subject: [PATCH] Switch array struct to class --- src/AST/boolean.cc | 19 +++--- src/AST/boolean.h | 5 +- src/AST/element.cc | 4 +- src/AST/element.h | 2 +- src/AST/function.cc | 6 +- src/AST/function.h | 3 +- src/AST/predicate.cc | 7 +- src/AST/predicate.h | 3 +- src/AST/rewriter.cc | 46 ++++++------- src/AST/table.cc | 6 +- src/AST/table.h | 2 +- src/ASTAnalyses/polarityassignment.cc | 34 +++++----- src/Backend/satencoder.cc | 13 ++-- src/Backend/satfuncopencoder.cc | 25 ++++--- src/Backend/satfunctableencoder.cc | 40 +++++------ src/Collections/array.h | 97 +++++++++++++-------------- src/Collections/structs.h | 4 -- src/Encoders/naiveencoder.cc | 12 ++-- 18 files changed, 151 insertions(+), 177 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index b349c9a..08af722 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -15,17 +15,21 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : B 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); } @@ -34,10 +38,5 @@ Boolean::~Boolean() { } BooleanPredicate::~BooleanPredicate() { - deleteInlineArrayElement(&inputs ); deleteFunctionEncoding(&encoding); } - -BooleanLogic::~BooleanLogic() { - deleteInlineArrayBoolean(&inputs); -} diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 12996bd..80dc004 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -50,7 +50,7 @@ class BooleanPredicate : public Boolean { ~BooleanPredicate(); Predicate *predicate; FunctionEncoding encoding; - ArrayElement inputs; + Array inputs; Boolean *undefStatus; FunctionEncoding * getFunctionEncoding() {return &encoding;} MEMALLOC; @@ -59,9 +59,8 @@ class BooleanPredicate : public Boolean { class BooleanLogic : public Boolean { public: BooleanLogic(CSolver *solver, LogicOp _op, Boolean **array, uint asize); - ~BooleanLogic(); LogicOp op; - ArrayBoolean inputs; + Array inputs; MEMALLOC; }; #endif diff --git a/src/AST/element.cc b/src/AST/element.cc index e4d06fc..b2007c1 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -13,8 +13,7 @@ Element::Element(ASTNodeType _type) : ASTNode(_type) { 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); @@ -50,7 +49,6 @@ Set *getElementSet(Element *This) { } ElementFunction::~ElementFunction() { - deleteInlineArrayElement(&inputs); deleteFunctionEncoding(&functionencoding); } diff --git a/src/AST/element.h b/src/AST/element.h index df3cf62..3385d41 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -40,7 +40,7 @@ class ElementFunction : public Element { ElementFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus); ~ElementFunction(); Function *function; - ArrayElement inputs; + Array inputs; Boolean *overflowstatus; FunctionEncoding functionencoding; MEMALLOC; diff --git a/src/AST/function.cc b/src/AST/function.cc index c63becf..50f8715 100644 --- a/src/AST/function.cc +++ b/src/AST/function.cc @@ -3,8 +3,7 @@ #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) { @@ -28,6 +27,3 @@ bool FunctionOperator::isInRangeFunction(uint64_t val) { return range->exists(val); } -FunctionOperator::~FunctionOperator() { - deleteInlineArraySet(&domains); -} diff --git a/src/AST/function.h b/src/AST/function.h index 914c439..afa713f 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -17,13 +17,12 @@ class Function { class FunctionOperator : public Function { public: ArithOp op; - ArraySet domains; + Array 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; }; diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index 7b7e9bd..feff67a 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -3,17 +3,12 @@ #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: diff --git a/src/AST/predicate.h b/src/AST/predicate.h index f52ea6f..c59a6a6 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -17,10 +17,9 @@ class Predicate { class PredicateOperator : public Predicate { public: PredicateOperator(CompOp op, Set **domain, uint numDomain); - ~PredicateOperator(); bool evalPredicateOperator(uint64_t *inputs); CompOp op; - ArraySet domains; + Array domains; MEMALLOC; }; diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index 5e24051..386eba0 100644 --- a/src/AST/rewriter.cc +++ b/src/AST/rewriter.cc @@ -42,12 +42,12 @@ void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) { 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); } } @@ -55,26 +55,26 @@ void replaceBooleanWithBoolean(CSolver * This, Boolean *oldb, Boolean *newb) { } 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); @@ -82,20 +82,20 @@ void handleIMPLIESTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) { } 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); @@ -103,33 +103,33 @@ void handleANDTrue(CSolver * This, BooleanLogic *bexpr, Boolean *child) { } 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)); } } diff --git a/src/AST/table.cc b/src/AST/table.cc index 3e88327..b7d550c 100644 --- a/src/AST/table.cc +++ b/src/AST/table.cc @@ -5,8 +5,9 @@ #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); } @@ -28,7 +29,6 @@ TableEntry * Table::getTableEntry(uint64_t *inputs, uint inputSize) { } Table::~Table() { - deleteInlineArraySet(&domains); HSIteratorTableEntry *iterator = iteratorTableEntry(entries); while (hasNextTableEntry(iterator)) { deleteTableEntry(nextTableEntry(iterator)); diff --git a/src/AST/table.h b/src/AST/table.h index 240eb29..f232615 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -10,7 +10,7 @@ class Table { void addNewTableEntry(uint64_t *inputs, uint inputSize, uint64_t result); TableEntry *getTableEntry(uint64_t *inputs, uint inputSize); ~Table(); - ArraySet domains; + Array domains; Set *range; HashSetTableEntry *entries; MEMALLOC; diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc index bf787ea..909195b 100644 --- a/src/ASTAnalyses/polarityassignment.cc +++ b/src/ASTAnalyses/polarityassignment.cc @@ -44,9 +44,9 @@ void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) { 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)); } } @@ -83,27 +83,27 @@ void computeLogicOpPolarity(BooleanLogic *This) { 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; } @@ -117,31 +117,31 @@ void computeLogicOpBooleanValue(BooleanLogic *This) { 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: diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 73998a6..b95e0b1 100644 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -73,23 +73,20 @@ Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) { } 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); diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc index bdfc60e..9394899 100644 --- a/src/Backend/satfuncopencoder.cc +++ b/src/Backend/satfuncopencoder.cc @@ -25,14 +25,14 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *const 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 @@ -42,7 +42,7 @@ 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); + Set *set = predicate->domains.get(i); vals[i] = set->getElement(indices[i]); } @@ -53,7 +53,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c 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); @@ -63,7 +63,7 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder *This, BooleanPredicate *c 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); @@ -90,11 +90,11 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * 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); } @@ -105,7 +105,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)); + Set *set = getElementSet(func->inputs.get(i)); vals[i] = set->getElement(indices[i]); } @@ -125,7 +125,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * 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) { @@ -174,7 +174,7 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * 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); @@ -197,10 +197,9 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder *This, ElementFunction * 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); diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc index 132d6e3..f8ceebe 100644 --- a/src/Backend/satfunctableencoder.cc +++ b/src/Backend/satfunctableencoder.cc @@ -16,8 +16,8 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat 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 * inputs = &constraint->inputs; + uint inputNum = inputs->getSize(); uint size = getSizeHashSetTableEntry(table->entries); bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; Edge constraints[size]; @@ -34,7 +34,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder *This, BooleanPredicat } 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"); @@ -73,11 +73,11 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons #endif ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED); //First encode children - ArrayElement *inputs = &constraint->inputs; - uint inputNum = getSizeArrayElement(inputs); + Array *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) { @@ -88,7 +88,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons break; } bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE; - uint numDomains = getSizeArraySet(&predicate->table->domains); + uint numDomains = predicate->table->domains.getSize(); VectorEdge *clauses = allocDefVectorEdge(); @@ -97,7 +97,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); + Set *set = predicate->table->domains.get(i); vals[i] = set->getElement(indices[i]); } bool hasOverflow = false; @@ -113,7 +113,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons } 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]); } @@ -150,7 +150,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons 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); @@ -179,7 +179,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *cons void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction *func) { UndefinedBehavior undefStatus = ((FunctionTable *) func->function)->undefBehavior; ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); - ArrayElement *elements = &func->inputs; + Array *elements = &func->inputs; Table *table = ((FunctionTable *) (func->function))->table; uint size = getSizeHashSetTableEntry(table->entries); Edge constraints[size]; @@ -188,10 +188,10 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder *This, ElementFunction 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); @@ -222,9 +222,9 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el #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 *elements = &elemFunc->inputs; + for (uint i = 0; i < elements->getSize(); i++) { + Element *elem = elements->get(i); encodeElementSATEncoder(This, elem); } @@ -237,7 +237,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el break; } - uint numDomains = getSizeArraySet(&function->table->domains); + uint numDomains = function->table->domains.getSize(); VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses @@ -246,7 +246,7 @@ 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); + Set *set = function->table->domains.get(i); vals[i] = set->getElement(indices[i]); } @@ -258,7 +258,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el 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) { @@ -300,7 +300,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder *This, ElementFunction *el 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); diff --git a/src/Collections/array.h b/src/Collections/array.h index d211759..6197de7 100644 --- a/src/Collections/array.h +++ b/src/Collections/array.h @@ -1,55 +1,52 @@ #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 +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 diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 4ee5549..83b47b0 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -6,10 +6,6 @@ #include "classlist.h" #include "array.h" -ArrayDef(Element, Element *); -ArrayDef(Boolean, Boolean *); -ArrayDef(Set, Set *); - VectorDef(Table, Table *); VectorDef(Set, Set *); VectorDef(Boolean, Boolean *); diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc index f078b8f..9596628 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -45,8 +45,8 @@ void naiveEncodingConstraint(Boolean *This) { } 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)); } } @@ -55,8 +55,8 @@ void naiveEncodingPredicate(BooleanPredicate *This) { 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); } } @@ -70,8 +70,8 @@ void naiveEncodingElement(Element *This) { 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); -- 2.34.1