Reduce unnecessary vector alloc/free

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

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 1fe98ce398af1bf4e54b854b410448b72552914d..44e3e63795103d06574a3aa645b6c2eb71a95bcd 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -14,11 +14,18 @@
 
 SATEncoder::SATEncoder(CSolver *_solver) :
        cnf(createCNF()),
-       solver(_solver) {
+       solver(_solver),
+  vector(allocDefVectorEdge()) {
 }
 
 SATEncoder::~SATEncoder() {
        deleteCNF(cnf);
+       deleteVectorEdge(vector);
+}
+
+void SATEncoder::resetSATEncoder() {
+       resetCNF(cnf);
+       booledgeMap.reset();
 }
 
 int SATEncoder::solve() {
@@ -37,7 +44,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 
 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
        Edge result;
-       Boolean * constraint = c.getBoolean();
+       Boolean *constraint = c.getBoolean();
 
        if (booledgeMap.contains(constraint)) {
                Edge e = {(Node *) booledgeMap.get(constraint)};
@@ -96,7 +103,7 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
        case SATC_OR:
        case SATC_XOR:
        case SATC_IMPLIES:
-               //Don't handle, translate these away...
+       //Don't handle, translate these away...
        default:
                model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
                exit(-1);
@@ -131,7 +138,7 @@ Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 
 void SATEncoder::encodeElementSATEncoder(Element *element) {
        /* Check to see if we have already encoded this element. */
-       if (getElementEncoding(element)->variables != NULL)
+       if (element->getElementEncoding()->variables != NULL)
                return;
 
        /* Need to encode. */
@@ -164,7 +171,7 @@ void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 }
 
 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
-       switch (getElementFunctionEncoding(function)->type) {
+       switch (function->getElementFunctionEncoding()->type) {
        case ENUMERATEIMPLICATIONS:
                encodeEnumTableElemFunctionSATEncoder(function);
                break;