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 be657815fe789f4f50324ba23f07bb0a893845d6..7c13eae9c8bebe007000abf801f735522dd36d67 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -222,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();
 }
@@ -347,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)
@@ -421,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;
                }
@@ -583,15 +589,13 @@ 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();
@@ -617,10 +621,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);
+       model_print("Result Computed in SAT solver: %d\n", result);
 
        if (deleteTuner) {
                delete tuner;