From 835bbfff70365c1b2116dec6f82b9f6e9f1806dd Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Sun, 29 Apr 2018 17:47:17 -0700 Subject: [PATCH] bug fixes for cloning and encodinggraph --- src/AST/boolean.cc | 21 ++++++++-- src/AST/element.cc | 15 +++++-- src/ASTAnalyses/Encoding/encodinggraph.cc | 4 +- src/Test/clonetest.cc | 51 +++++++++++++++++++++++ src/Test/deserializersolvetest.cc | 2 +- 5 files changed, 85 insertions(+), 8 deletions(-) create mode 100644 src/Test/clonetest.cc diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index c576268..46e277a 100644 --- 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 7dc02a2..54a5c41 100644 --- 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 ce695e2..6bd28e2 100644 --- 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 index 0000000..43954bd --- /dev/null +++ b/src/Test/clonetest.cc @@ -0,0 +1,51 @@ +#include "csolver.h" +#include +#include + +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 b003226..2d7a852 100644 --- 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(); -- 2.34.1