bug fixes for cloning and encodinggraph

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index c576268058f3b5203687a2d6cef9e496a90bcf2e..46e277a390a5ec8ca35ab5fec34147d775e25af8 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -71,19 +71,32 @@ Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
 }
 
 Boolean *BooleanOrder::clone(CSolver *solver, CloneMap *map) {
+        Boolean *b = (Boolean *) map->get(this);
+       if (b != NULL)
+               return b;
        Order *ordercopy = order->clone(solver, map);
-       return solver->orderConstraint(ordercopy, first, second).getRaw();
+       b= solver->orderConstraint(ordercopy, first, second).getRaw();
+        map->put(this, b);
+        return b;
 }
 
 Boolean *BooleanLogic::clone(CSolver *solver, CloneMap *map) {
+        Boolean *b = (Boolean *) map->get(this);
+       if (b != NULL)
+               return b;
        BooleanEdge array[inputs.getSize()];
        for (uint i = 0; i < inputs.getSize(); i++) {
                array[i] = cloneEdge(solver, map, inputs.get(i));
        }
-       return solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw();
+       b= solver->applyLogicalOperation(op, array, inputs.getSize()).getRaw();
+        map->put(this, b);
+        return b;
 }
 
 Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
+        Boolean *b = (Boolean *) map->get(this);
+       if (b != NULL)
+               return b;
        Element *array[inputs.getSize()];
        for (uint i = 0; i < inputs.getSize(); i++) {
                array[i] = inputs.get(i)->clone(solver, map);
@@ -91,7 +104,9 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
        Predicate *pred = predicate->clone(solver, map);
        BooleanEdge defstatus = undefStatus ? cloneEdge(solver, map, undefStatus) : BooleanEdge();
 
-       return solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw();
+       b= solver->applyPredicateTable(pred, array, inputs.getSize(), defstatus).getRaw();
+        map->put(this, b);
+        return b;
 }
 
 void BooleanPredicate::updateParents() {

diff --git a/src/AST/element.cc b/src/AST/element.cc
index 7dc02a21cdc7dc6843e20c6d5a112b87d2db019e..54a5c4163780eb56a435d95f3aeb511f2476d83d 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -35,7 +35,12 @@ ElementConst::ElementConst(uint64_t _value, Set *_set) :
 }
 
 Element *ElementConst::clone(CSolver *solver, CloneMap *map) {
-       return solver->getElementConst(type, value);
+        Element *e = (Element *) map->get(this);
+       if (e != NULL)
+               return e;
+       e= solver->getElementConst(type, value);
+        map->put(this,e);
+        return e;
 }
 
 Element *ElementSet::clone(CSolver *solver, CloneMap *map) {
@@ -43,16 +48,20 @@ Element *ElementSet::clone(CSolver *solver, CloneMap *map) {
        if (e != NULL)
                return e;
        e = solver->getElementVar(set->clone(solver, map));
-       map->put(e, e);
+       map->put(this, e);
        return e;
 }
 
 Element *ElementFunction::clone(CSolver *solver, CloneMap *map) {
+        Element *e = (Element *) map->get(this);
+       if (e != NULL)
+               return e;
        Element *array[inputs.getSize()];
        for (uint i = 0; i < inputs.getSize(); i++) {
                array[i] = inputs.get(i)->clone(solver, map);
        }
-       Element *e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), overflowstatus->clone(solver, map));
+       e = solver->applyFunction(function->clone(solver, map), array, inputs.getSize(), overflowstatus->clone(solver, map));
+        map->put(this,e);
        return e;
 }
 

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index ce695e25560553ffc03156bc5eea48c5ec041877..6bd28e2075348cc0e1768eec4166039507185529 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -78,8 +78,10 @@ void EncodingGraph::encode() {
                                } else if (encodetype == BINARYINDEX) {
                                        EncodingSubGraph *subgraph = graphMap.get(n);
                                         DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
-                                       if (subgraph == NULL)
+                                       if (subgraph == NULL){
+                                                encoding->encodingArrayInitialization();
                                                continue;
+                                        }
                                        uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
                                        uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
                                        encoding->allocInUseArrayElement(paddedSize);

diff --git a/src/Test/clonetest.cc b/src/Test/clonetest.cc
new file mode 100644 (file)
index 0000000..43954bd
--- /dev/null
+++ b/src/Test/clonetest.cc
@@ -0,0 +1,51 @@
+#include "csolver.h"
+#include <unistd.h>
+#include <sys/types.h>
+
+int main(int argc, char **argv) {
+       if (argc < 2) {
+               printf("You should specify file names ...");
+               exit(-1);
+       }
+        //usleep(20000000);
+       for (int i = 1; i < argc; i++) {
+               CSolver *solver = CSolver::deserialize(argv[i]);
+               CSolver *copy = solver->clone();
+                CSolver *copy2 = solver->clone();
+                CSolver *copy3 = solver->clone();
+                CSolver *copy4 = solver->clone();
+                int value = copy->solve();
+                if (value == 1) {
+                       printf("Copy %s is SAT\n", argv[i]);
+               } else {
+                       printf("Copy %s is UNSAT\n", argv[i]);
+               }
+                value = copy2->solve();
+                if (value == 1) {
+                       printf("Copy2 %s is SAT\n", argv[i]);
+               } else {
+                       printf("Copy2 %s is UNSAT\n", argv[i]);
+               }
+                value = copy3->solve();
+                if (value == 1) {
+                       printf("Copy3 %s is SAT\n", argv[i]);
+               } else {
+                       printf("Copy3 %s is UNSAT\n", argv[i]);
+               }
+                value = copy4->solve();
+                if (value == 1) {
+                       printf("Copy4 %s is SAT\n", argv[i]);
+               } else {
+                       printf("Copy4 %s is UNSAT\n", argv[i]);
+               }
+                value = solver->solve();
+               if (value == 1) {
+                       printf("Original %s is SAT\n", argv[i]);
+               } else {
+                       printf("Original %s is UNSAT\n", argv[i]);
+               }
+                
+               delete solver;
+       }
+       return 1;
+}

diff --git a/src/Test/deserializersolvetest.cc b/src/Test/deserializersolvetest.cc
index b003226f67b0ecba33619581519db70e32098aaa..2d7a8521ff93ca3484f18fc1992e2f7a220aa8cf 100644 (file)
--- a/src/Test/deserializersolvetest.cc
+++ b/src/Test/deserializersolvetest.cc
@@ -7,7 +7,7 @@ int main(int argc, char **argv) {
                printf("You should specify file names ...");
                exit(-1);
        }
-        usleep(20000000);
+        //usleep(20000000);
        for (int i = 1; i < argc; i++) {
                CSolver *solver = CSolver::deserialize(argv[i]);
                int value = solver->solve();