Fixing integerencoding memory leaks ...

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index ab88f2065be16dd226cceaf9bd9ae9d0eacc5fa2..b52ccf84921cb5cafe16d314cea7c7deed4bb002 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -10,11 +10,9 @@
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
        : Transform(_solver)
 {
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
        : Transform(_solver)
 {

-       orderIntEncoding = new HashTableOrderIntEncoding();

 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 IntegerEncodingTransform::~IntegerEncodingTransform() {

-       orderIntEncoding->resetanddelete();

 }
 
 void IntegerEncodingTransform::doTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {


@@ -30,26 +28,19 @@ void IntegerEncodingTransform::doTransform() {
 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {
 }
 
 void IntegerEncodingTransform::integerEncode(Order *currOrder) {

-       IntegerEncodingRecord *encodingRecord = NULL;
-       if (!orderIntEncoding->contains(currOrder)) {
-               encodingRecord = new IntegerEncodingRecord(
-                       solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
-               orderIntEncoding->put(currOrder, encodingRecord);
-               currOrder->setOrderEncodingType( INTEGERENCODING );
-       } else {
-               encodingRecord = orderIntEncoding->get(currOrder);
-       }
+       IntegerEncodingRecord *encodingRecord =  new IntegerEncodingRecord(
+               solver->createRangeSet(currOrder->set->getType(), 0, (uint64_t) currOrder->set->getSize() - 1));
+       currOrder->setOrderEncodingType( INTEGERENCODING );

        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {

-               orderIntegerEncodingSATEncoder(currOrder, currOrder->constraints.get(i));
+               orderIntegerEncodingSATEncoder(currOrder->constraints.get(i), encodingRecord);

        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
        solver->getActiveOrders()->remove(currOrder);
 }
 
 
        }
        currOrder->setOrderResolver(new IntegerEncOrderResolver(solver, encodingRecord));
        solver->getActiveOrders()->remove(currOrder);
 }
 
 

-void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder) {
-       IntegerEncodingRecord *ierec = orderIntEncoding->get(currOrder);
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder, IntegerEncodingRecord *ierec) {

        //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
        //getting two elements and using LT predicate ...
        Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
        Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);

diff --git a/src/ASTTransform/integerencoding.h b/src/ASTTransform/integerencoding.h
index 8066c2acf678924b7b7ffb8fe3306cc6b0f9ca10..805ed0bf22b2704932160abe9f888048d3363c40 100644 (file)
--- a/src/ASTTransform/integerencoding.h
+++ b/src/ASTTransform/integerencoding.h
@@ -14,14 +14,12 @@
 class IntegerEncodingTransform : public Transform {
 public:
        IntegerEncodingTransform(CSolver *solver);
 class IntegerEncodingTransform : public Transform {
 public:
        IntegerEncodingTransform(CSolver *solver);

-       void orderIntegerEncodingSATEncoder(Order * currOrder, BooleanOrder *boolOrder);
+       void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder, IntegerEncodingRecord *ierec);

        void doTransform();
        void integerEncode(Order *currOrder);
 
        virtual ~IntegerEncodingTransform();
 private:
        void doTransform();
        void integerEncode(Order *currOrder);
 
        virtual ~IntegerEncodingTransform();
 private:

-       //FIXME:We can remove it, because we don't need it for translating anymore... -HG
-       HashTableOrderIntEncoding *orderIntEncoding;

 };
 
 
 };
 
 

diff --git a/src/ASTTransform/integerencodingrecord.cc b/src/ASTTransform/integerencodingrecord.cc
index f8690d73e53aef5c8cda6aecdd25a728c04a9833..6c8ba2fff73f0daf7afd1ba648d715dbfa634586 100644 (file)
--- a/src/ASTTransform/integerencodingrecord.cc
+++ b/src/ASTTransform/integerencodingrecord.cc
@@ -12,22 +12,26 @@
 IntegerEncodingRecord::IntegerEncodingRecord(Set *_set) :
        secondarySet(_set)
 {
 IntegerEncodingRecord::IntegerEncodingRecord(Set *_set) :
        secondarySet(_set)
 {

-       elementTable = new HashsetOrderElement();
+       elementSet = new HashsetOrderElement();

 }
 
 IntegerEncodingRecord::~IntegerEncodingRecord() {
 }
 
 IntegerEncodingRecord::~IntegerEncodingRecord() {

-       if (elementTable != NULL) {
-               delete elementTable;
+       SetIteratorOrderElement *oiterator = elementSet->iterator();
+       while (oiterator->hasNext()) {
+               OrderElement *oe = oiterator->next();
+               delete oe;

        }
        }

+       delete oiterator;
+       delete elementSet;

 }
 
 Element *IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
        OrderElement oelement(item, NULL);
 }
 
 Element *IntegerEncodingRecord::getOrderIntegerElement(CSolver *This, uint64_t item, bool create) {
        OrderElement oelement(item, NULL);

-       if ( elementTable->contains(&oelement)) {
-               return elementTable->get(&oelement)->getElement();
+       if ( elementSet->contains(&oelement)) {
+               return elementSet->get(&oelement)->getElement();

        } else if (create) {
                Element *elem = This->getElementVar(secondarySet);
        } else if (create) {
                Element *elem = This->getElementVar(secondarySet);

-               elementTable->add(new OrderElement(item, elem));
+               elementSet->add(new OrderElement(item, elem));

                return elem;
        }
        return NULL;
                return elem;
        }
        return NULL;

diff --git a/src/ASTTransform/integerencodingrecord.h b/src/ASTTransform/integerencodingrecord.h
index 556e6c5be1db7733bd8039acbbb1ff2682b66f63..39c54ed9dc7476bbc8863a90ca0e6284303d08a3 100644 (file)
--- a/src/ASTTransform/integerencodingrecord.h
+++ b/src/ASTTransform/integerencodingrecord.h
@@ -21,7 +21,7 @@ public:
 
 private:
        Set *secondarySet;
 
 private:
        Set *secondarySet;

-       HashsetOrderElement *elementTable;
+       HashsetOrderElement *elementSet;

 };
 
 #endif/* INTEGERENCODINGRECORD_H */
 };
 
 #endif/* INTEGERENCODINGRECORD_H */

diff --git a/src/Encoders/orderencoding.cc b/src/Encoders/orderencoding.cc
index 5e81f14cd6ab262b523df65ca7756eb6e6e4c176..556554e8d7d3f06f55aab5cf1f42f57ed2277ff3 100644 (file)
--- a/src/Encoders/orderencoding.cc
+++ b/src/Encoders/orderencoding.cc
@@ -1,6 +1,15 @@
 #include "orderencoding.h"
 #include "orderencoding.h"

+#include "orderresolver.h"

 
 OrderEncoding::OrderEncoding(Order *_order) :
 
 OrderEncoding::OrderEncoding(Order *_order) :

+       resolver(NULL),

        type(ORDER_UNASSIGNED),
        type(ORDER_UNASSIGNED),

-       order(_order) {
+       order(_order)
+{
+}
+
+OrderEncoding::~OrderEncoding(){
+       if(resolver!= NULL){
+               delete resolver;
+       }

 }
 }

diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
index 0792d4aebabb0294b559b87cd9854381aae4b66a..4b0915a92fe18f74551f2ec46d7ee66c032cd831 100644 (file)
--- a/src/Encoders/orderencoding.h
+++ b/src/Encoders/orderencoding.h
@@ -11,7 +11,7 @@ typedef enum OrderEncodingType OrderEncodingType;
 class OrderEncoding {
 public:
        OrderEncoding(Order *order);
 class OrderEncoding {
 public:
        OrderEncoding(Order *order);

-
+       virtual ~OrderEncoding();

        OrderResolver *resolver;
        OrderEncodingType type;
        Order *order;
        OrderResolver *resolver;
        OrderEncodingType type;
        Order *order;

diff --git a/src/Translator/integerencorderresolver.cc b/src/Translator/integerencorderresolver.cc
index a9fb25c3b365117fd0ab4a4206aa67dbc9a18532..eaf4e476953f720f27cf2473642d5f5f471c903b 100644 (file)
--- a/src/Translator/integerencorderresolver.cc
+++ b/src/Translator/integerencorderresolver.cc
@@ -17,6 +17,7 @@ IntegerEncOrderResolver::IntegerEncOrderResolver(CSolver *_solver, IntegerEncodi
 }
 
 IntegerEncOrderResolver::~IntegerEncOrderResolver() {
 }
 
 IntegerEncOrderResolver::~IntegerEncOrderResolver() {

+       delete ierecord;

 }
 
 
 }
 
 

diff --git a/src/csolver.cc b/src/csolver.cc
index f52c4eb655a518a75d8fb843da27e7e7cf13846f..d94ddfce66ffed8a98b4e849c129ae8751b3c678 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -400,8 +400,8 @@ int CSolver::solve() {
        long long startTime = getTimeNano();
        computePolarities(this);
 
        long long startTime = getTimeNano();
        computePolarities(this);
 

-//     DecomposeOrderTransform dot(this);
-//     dot.doTransform();
+       DecomposeOrderTransform dot(this);
+       dot.doTransform();

 
        IntegerEncodingTransform iet(this);
        iet.doTransform();
 
        IntegerEncodingTransform iet(this);
        iet.doTransform();