bug fixes for cloning and encodinggraph
authorHamed Gorjiara <hgorjiar@uci.edu>
Mon, 30 Apr 2018 00:47:17 +0000 (17:47 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Mon, 30 Apr 2018 00:47:17 +0000 (17:47 -0700)
src/AST/boolean.cc
src/AST/element.cc
src/ASTAnalyses/Encoding/encodinggraph.cc
src/Test/clonetest.cc [new file with mode: 0644]
src/Test/deserializersolvetest.cc

index c576268..46e277a 100644 (file)
@@ -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() {
index 7dc02a2..54a5c41 100644 (file)
@@ -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;
 }
 
index ce695e2..6bd28e2 100644 (file)
@@ -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
@@ -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;
+}
index b003226..2d7a852 100644 (file)
@@ -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();