From: Hamed Gorjiara Date: Thu, 1 Feb 2018 03:57:39 +0000 (-0800) Subject: edit X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c081050838e3612c758d5ed4e59b71a9f5d89abb edit --- diff --git a/src/AST/element.cc b/src/AST/element.cc index ffe7acc..7dc02a2 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -133,6 +133,10 @@ void ElementFunction::serialize(Serializer *serializer) { void ElementFunction::print() { model_print("{ElementFunction<%p>:\n", this); function->print(); + model_print("OverFlow Boolean Flag:\n"); + overflowstatus.getBoolean()->print(); + model_print("Range:\n"); + getRange()->print(); model_print("Elements:\n"); uint size = inputs.getSize(); for (uint i = 0; i < size; i++) { diff --git a/src/AST/set.cc b/src/AST/set.cc index 585ae6d..9342484 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -69,14 +69,6 @@ uint Set::getSize() { } } -uint64_t Set::getMemberAt(uint index) { - if (isRange) { - return low + index; - } else { - return members->get(index); - } -} - Set::~Set() { if (!isRange) delete members; @@ -155,7 +147,7 @@ void Set::serialize(Serializer *serializer) { } void Set::print() { - model_print("{Set<%p>:", this); + model_print("{Set(%lu)<%p>:", type, this); if (isRange) { model_print("Range: low=%lu, high=%lu}", low, high); } else { diff --git a/src/AST/set.h b/src/AST/set.h index 34784d3..aaa8f38 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -22,7 +22,6 @@ public: uint getSize(); VarType getType() {return type;} uint64_t getNewUniqueItem() {return low++;} - uint64_t getMemberAt(uint index); uint64_t getElement(uint index); uint getUnionSize(Set *s); virtual bool isMutableSet() {return false;} diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 56614fa..9982039 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -124,13 +124,13 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) { Set *set = order->set; uint size = order->set->getSize(); for (uint i = 0; i < size; i++) { - uint64_t valueI = set->getMemberAt(i); + uint64_t valueI = set->getElement(i); for (uint j = i + 1; j < size; j++) { - uint64_t valueJ = set->getMemberAt(j); + uint64_t valueJ = set->getElement(j); OrderPair pairIJ(valueI, valueJ, E_NULL); Edge constIJ = getPairConstraint(order, &pairIJ); for (uint k = j + 1; k < size; k++) { - uint64_t valueK = set->getMemberAt(k); + uint64_t valueK = set->getElement(k); OrderPair pairJK(valueJ, valueK, E_NULL); OrderPair pairIK(valueI, valueK, E_NULL); Edge constIK = getPairConstraint(order, &pairIK); @@ -230,15 +230,15 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) { Set *set = order->set; uint size = order->set->getSize(); for (uint i = 0; i < size; i++) { - uint64_t valueI = set->getMemberAt(i); + uint64_t valueI = set->getElement(i); for (uint j = i + 1; j < size; j++) { - uint64_t valueJ = set->getMemberAt(j); + uint64_t valueJ = set->getElement(j); OrderPair pairIJ(valueI, valueJ, E_NULL); OrderPair pairJI(valueJ, valueI, E_NULL); Edge constIJ = getPartialPairConstraint(order, &pairIJ); Edge constJI = getPartialPairConstraint(order, &pairJI); for (uint k = j + 1; k < size; k++) { - uint64_t valueK = set->getMemberAt(k); + uint64_t valueK = set->getElement(k); OrderPair pairJK(valueJ, valueK, E_NULL); OrderPair pairIK(valueI, valueK, E_NULL); Edge constIK = getPartialPairConstraint(order, &pairIK); diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc index 031b98f..02d4898 100644 --- a/src/Encoders/elementencoding.cc +++ b/src/Encoders/elementencoding.cc @@ -54,7 +54,7 @@ void ElementEncoding::encodingArrayInitialization() { allocEncodingArrayElement(encSize); allocInUseArrayElement(encSize); for (uint i = 0; i < size; i++) { - encodingArray[i] = set->getMemberAt(i); + encodingArray[i] = set->getElement(i); setInUseElement(i); } } diff --git a/src/csolver.cc b/src/csolver.cc index 5d4f56d..be65781 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -26,6 +26,7 @@ #include "orderedge.h" #include "orderanalysis.h" #include +#include CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -582,14 +583,15 @@ int CSolver::solve() { } delete orderit; } - + model_print("*****************Before any modifications:************\n"); + printConstraints(); computePolarities(this); long long time2 = getTimeNano(); model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC); - Preprocess pp(this); - pp.doTransform(); +// Preprocess pp(this); +// pp.doTransform(); long long time3 = getTimeNano(); - model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC); +// model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC); DecomposeOrderTransform dot(this); dot.doTransform(); @@ -615,6 +617,8 @@ int CSolver::solve() { model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC); model_print("Is problem UNSAT after encoding: %d\n", unsat); + model_print("########## After all modifications: #############\n"); + printConstraints(); int result = unsat ? IS_UNSAT : satEncoder->solve(); model_print("Result Computed in CSolver: %d\n", result); @@ -681,3 +685,21 @@ void CSolver::autoTune(uint budget) { autotuner->tune(); delete autotuner; } + +//Set* CSolver::addItemsToRange(Element* element, uint num, ...){ +// va_list args; +// va_start(args, num); +// element->getRange() +// uint setSize = set->getSize(); +// uint newSize = setSize+ num; +// uint64_t members[newSize]; +// for(uint i=0; igetElement(i); +// } +// for( uint i=0; i< num; i++){ +// uint64_t arg = va_arg(args, uint64_t); +// members[setSize+i] = arg; +// } +// va_end(args); +// return createSet(set->getType(), members, newSize); +//} \ No newline at end of file diff --git a/src/csolver.h b/src/csolver.h index e254abb..b84d324 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -157,6 +157,7 @@ public: void replaceBooleanWithFalse(BooleanEdge bexpr); void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb); CSolver *clone(); +// Set* addItemsToRange(Element* element, uint num, ...); void serialize(); static CSolver *deserialize(const char *file); void autoTune(uint budget);