edit

diff --git a/src/AST/element.cc b/src/AST/element.cc
index ffe7acc929bfa534e15596a037ae7b90ee5ee92a..7dc02a21cdc7dc6843e20c6d5a112b87d2db019e 100644 (file)
--- 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();
 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++) {
        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 585ae6d1068a109cadf9891d555db7548972b44c..9342484a21a81ce61e73cd14fae87a9148d9902c 100644 (file)
--- 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;
 Set::~Set() {
        if (!isRange)
                delete members;


@@ -155,7 +147,7 @@ void Set::serialize(Serializer *serializer) {
 }
 
 void Set::print() {
 }
 
 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 {
        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 34784d3ce44bd89c5c9bd475317ff68cba5c7f0f..aaa8f3819a28a23daa21155308ca783b9f752b11 100644 (file)
--- 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++;}
        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;}
        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 56614fabe78a4e953ebebee916c16ae0442b6fce..9982039333a6da897c17afc6e5ff54d3d303c7cd 100644 (file)
--- 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++) {
        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++) {
                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++) {
                        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);
                                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++) {
        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++) {
                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++) {
                        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);
                                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 031b98f5b434e2552c4219bbe33ca80bd2ff73af..02d4898e3515959b969e869494ff2f4d23a27aa8 100644 (file)
--- 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++) {
        allocEncodingArrayElement(encSize);
        allocInUseArrayElement(encSize);
        for (uint i = 0; i < size; i++) {

-               encodingArray[i] = set->getMemberAt(i);
+               encodingArray[i] = set->getElement(i);

                setInUseElement(i);
        }
 }
                setInUseElement(i);
        }
 }

diff --git a/src/csolver.cc b/src/csolver.cc
index 5d4f56d2e1897b6311e629835e533b54f07891b6..be657815fe789f4f50324ba23f07bb0a893845d6 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -26,6 +26,7 @@
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include <time.h>
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include <time.h>

+#include <stdarg.h>

 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),


@@ -582,14 +583,15 @@ int CSolver::solve() {
                }
                delete orderit;
        }
                }
                delete orderit;
        }

-
+        model_print("*****************Before any modifications:************\n");
+        printConstraints();

        computePolarities(this);
        long long time2 = getTimeNano();
        model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
        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();
        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();
 
        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("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);
 
        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;
 }
        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; i<setSize; i++){
+//                members[i] = set->getElement(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 e254abbc29c8026ddc274166f4b9de23c167c89d..b84d3245801d801e1524876841d9d378c26e4f81 100644 (file)
--- 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();
        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);
        void serialize();
        static CSolver *deserialize(const char *file);
        void autoTune(uint budget);