Reduce unnecessary vector alloc/free

[satune.git] / src / Backend / satfuncopencoder.cc

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 41b687ec17aa2d6cac9d10511c91ea33c9af52c9..f4eda5240d69c401d2a47ec0cd0474199103c837 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -34,7 +34,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                Element *elem = constraint->inputs.get(i);
                encodeElementSATEncoder(elem);
        }
-       VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
+       VectorEdge *clauses = vector;
 
        uint indices[numDomains];       //setup indices
        bzero(indices, sizeof(uint) * numDomains);
@@ -75,11 +75,11 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
                }
        }
        if (getSizeVectorEdge(clauses) == 0) {
-               deleteVectorEdge(clauses);
+               clearVectorEdge(clauses);
                return E_False;
        }
        Edge cor = constraintOR(cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-       deleteVectorEdge(clauses);
+       clearVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;
 }
 
@@ -88,7 +88,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 #ifdef TRACE_DEBUG
        model_print("Operator Function ...\n");
 #endif
-       FunctionOperator *function = (FunctionOperator *) func->function;
+       FunctionOperator *function = (FunctionOperator *) func->getFunction();
        uint numDomains = func->inputs.getSize();
 
        /* Call base encoders for children */
@@ -104,18 +104,18 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = getElementSet(func->inputs.get(i));
+               Set *set = func->inputs.get(i)->getRange();
                vals[i] = set->getElement(indices[i]);
        }
 
-       Edge overFlowConstraint = ((BooleanVar *) func->overflowstatus)->var;
+       Edge overFlowConstraint = encodeConstraintSATEncoder(func->overflowstatus);
 
        bool notfinished = true;
        while (notfinished) {
                Edge carray[numDomains + 1];
 
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
-               bool isInRange = ((FunctionOperator *)func->function)->isInRangeFunction(result);
+               bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
                bool needClause = isInRange;
                if (function->overflowbehavior == SATC_OVERFLOWSETSFLAG || function->overflowbehavior == SATC_FLAGIFFOVERFLOW) {
                        needClause = true;
@@ -173,7 +173,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = getElementSet(func->inputs.get(i));
+                       Set *set = func->inputs.get(i)->getRange();
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
@@ -200,11 +200,11 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        encodeElementSATEncoder(elem0);
        Element *elem1 = constraint->inputs.get(1);
        encodeElementSATEncoder(elem1);
-       ElementEncoding *ee0 = getElementEncoding(elem0);
-       ElementEncoding *ee1 = getElementEncoding(elem1);
+       ElementEncoding *ee0 = elem0->getElementEncoding();
+       ElementEncoding *ee1 = elem1->getElementEncoding();
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       switch (predicate->op) {
+       switch (predicate->getOp()) {
        case SATC_EQUALS:
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case SATC_LT: