Merge branch 'hamed' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index b74df47f37c6c22cb20c2e5391b2c0d4e09533ea..7c13eae9c8bebe007000abf801f735522dd36d67 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -26,6 +26,7 @@
 #include "orderedge.h"
 #include "orderanalysis.h"
 #include <time.h>
+#include <stdarg.h>
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -182,6 +183,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
        return set;
 }
 
+bool CSolver::itemExistInSet(Set *set, uint64_t item){
+        return set->exists(item);
+}
+
 VarType CSolver::getSetVarType(Set *set) {
        return set->getType();
 }
@@ -217,6 +222,10 @@ Element *CSolver::getElementVar(Set *set) {
        return element;
 }
 
+void CSolver::mustHaveValue(Element *element){
+       element->getElementEncoding()->anyValue = true;
+}
+
 Set *CSolver::getElementRange (Element *element) {
        return element->getRange();
 }
@@ -342,9 +351,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
        return applyLogicalOperation(op, array, 1);
 }
 
-static int ptrcompares(const void *p1, const void *p2) {
-       uintptr_t b1 = *(uintptr_t const *) p1;
-       uintptr_t b2 = *(uintptr_t const *) p2;
+static int booleanEdgeCompares(const void *p1, const void *p2) {
+       BooleanEdge be1 = *(BooleanEdge const *) p1;
+       BooleanEdge be2 = *(BooleanEdge const *) p2;
+       uint64_t b1 = be1->id;
+       uint64_t b2 = be2->id;
        if (b1 < b2)
                return -1;
        else if (b1 == b2)
@@ -416,7 +427,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
                } else if (newindex == 1) {
                        return newarray[0];
                } else {
-                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
+                       bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
                        array = newarray;
                        asize = newindex;
                }
@@ -578,7 +589,6 @@ int CSolver::solve() {
                }
                delete orderit;
        }
-
        computePolarities(this);
        long long time2 = getTimeNano();
        model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
@@ -612,7 +622,7 @@ int CSolver::solve() {
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in CSolver: %d\n", result);
+       model_print("Result Computed in SAT solver: %d\n", result);
 
        if (deleteTuner) {
                delete tuner;
@@ -677,3 +687,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