Switch array struct to class

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index b349c9a5468a67f35c20335a5a585516ce5fe779..08af722b1c2e406f1559450b6aca3f7b5cedaaec 100644 (file)
--- 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 12996bd42a7c30c2d11ba770b47a1deb207f1017..80dc004c7583d3b5640568619a6aa56f11148eb3 100644 (file)
--- 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<Element *> 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<Boolean *> inputs;
        MEMALLOC;
 };
 #endif

diff --git a/src/AST/element.cc b/src/AST/element.cc
index e4d06fcfb75eb609ac53e04122c2c807957d5f6d..b2007c124c17d4ab87ef23e5f954836adee78023 100644 (file)
--- 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 df3cf62a0edd415658445714e962af2ad07fb9bd..3385d41bdd24f0e9225f0ef9f4680912965ae710 100644 (file)
--- 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<Element *> inputs;
        Boolean *overflowstatus;
        FunctionEncoding functionencoding;
        MEMALLOC;

diff --git a/src/AST/function.cc b/src/AST/function.cc
index c63becf15adc54eada5b26105ebedbd923a8a897..50f8715db77a7485e423894cdae8f00d2c4c20e3 100644 (file)
--- 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 914c43991926482ffb48886e5b2215625a236e9c..afa713f0e800cd9c3838336b4c1b970643b50c42 100644 (file)
--- 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<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;
 };
 

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index 7b7e9bdd51a6d52b0f3b8b7551246a5443ad24c9..feff67a946f7cb807b6f8970df3f4f024213c94d 100644 (file)
--- 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 f52ea6f6d1e07a07d0c460da3174ac8ac0cc2fe0..c59a6a6078bdc8f1838fe215cb2f290014731da4 100644 (file)
--- 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<Set *> domains;
        MEMALLOC;
 };
 

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 5e240514930bd2904f2c2e362ee3923d821637eb..386eba038e995d4fc25f4122ad50affcc602ef6a 100644 (file)
--- 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 3e8832784803ac64223d57421138eeb2bb53a259..b7d550c5aee6bbfb1cf66aadca78898c25ff9fbd 100644 (file)
--- 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 240eb29ab4da0ee0cbf8a7af85512e214aff7fe1..f232615a848b63c327a3074659aab0b556282fe5 100644 (file)
--- 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<Set *> domains;
        Set *range;
        HashSetTableEntry *entries;
        MEMALLOC;

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index bf787ea3960b33d16fb90a01aa46fb16e1eed468..909195ba5a86d4affb2a420d5026a37cc8293f05 100644 (file)
--- 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 73998a64aa0060ccd1994af572c4fb172dbe78da..b95e0b1c5217982c2d90f233e69aac547e7dc4f5 100644 (file)
--- 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 bdfc60e9eed0a2d718edaae25764bf75f780d8ec..9394899951b4898949e91563ccdeec9354d5568d 100644 (file)
--- 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 132d6e3ed7bdd29eb419545fa058a28a8ef81a7c..f8ceebe28a78bd49b3e01ff7d5b52c1e1969738e 100644 (file)
--- 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<Element*> * 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<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) {
@@ -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<Element *> *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<Element *> *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 d211759470591a2f84990db2d02ac4f7a4716c11..6197de71968b351d30d22a732e425e680793e3b1 100644 (file)
--- 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<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

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 4ee55494ff4247e4937577970de23f42a0e189fb..83b47b0168115f0d8e2c5562bdbd16bd53b3938f 100644 (file)
--- 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 f078b8fc3f122e755e3df2d1a283eeac7fa199fa..959662823fe58c0f11299222e2936100de7bb8e7 100644 (file)
--- 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);