edit
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 1 Feb 2018 03:57:39 +0000 (19:57 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 1 Feb 2018 03:57:39 +0000 (19:57 -0800)
src/AST/element.cc
src/AST/set.cc
src/AST/set.h
src/Backend/satorderencoder.cc
src/Encoders/elementencoding.cc
src/csolver.cc
src/csolver.h

index ffe7acc..7dc02a2 100644 (file)
@@ -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++) {
index 585ae6d..9342484 100644 (file)
@@ -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 {
index 34784d3..aaa8f38 100644 (file)
@@ -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;}
index 56614fa..9982039 100644 (file)
@@ -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);
index 031b98f..02d4898 100644 (file)
@@ -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);
        }
 }
index 5d4f56d..be65781 100644 (file)
@@ -26,6 +26,7 @@
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include <time.h>
+#include <stdarg.h>
 
 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; 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
index e254abb..b84d324 100644 (file)
@@ -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);