Add a configuration for disabling the optimizations

diff --git a/src/SatuneJavaAPI.java b/src/SatuneJavaAPI.java
index 2b6baeaf6a05840123a9761e9ca69211ee74ca70..a5e71d3c39e21baba983758d35ac8db990dfbfc0 100644 (file)
--- a/src/SatuneJavaAPI.java
+++ b/src/SatuneJavaAPI.java
@@ -43,6 +43,10 @@ public class SatuneJavaAPI{
             printConstraints(satune);
         }
        
             printConstraints(satune);
         }
        

+        public void turnoffOptimizations(){
+            turnoffOptimizations(satune);
+        }
+       

         public int solve(){
             return solve(satune);
         }
         public int solve(){
             return solve(satune);
         }


@@ -81,6 +85,7 @@ public class SatuneJavaAPI{
        private native int getBooleanValue(long solver,long bool);
        private native int getOrderConstraintValue(long solver,long order, long first, long second);
        private native void printConstraints(long solver);
        private native int getBooleanValue(long solver,long bool);
        private native int getOrderConstraintValue(long solver,long order, long first, long second);
        private native void printConstraints(long solver);

+       private native void turnoffOptimizations(long solver);

        private native void serialize(long solver);
        private native void mustHaveValue(long solver, long element);
        private native void setInterpreter(long solver, int type);
        private native void serialize(long solver);
        private native void mustHaveValue(long solver, long element);
        private native void setInterpreter(long solver, int type);

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index ca206174148a35bccd80682a8231b015176036cb..7707b74babcd70149011e1af8b9dea1f624c7398 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -170,6 +170,10 @@ void printConstraints(void *solver) {
        CCSOLVER(solver)->printConstraints();
 }
 
        CCSOLVER(solver)->printConstraints();
 }
 

+void turnoffOptimizations(void *solver) {
+       CCSOLVER(solver)->turnoffOptimizations();
+}
+

 
 void serialize(void *solver) {
        CCSOLVER(solver)->serialize();
 
 void serialize(void *solver) {
        CCSOLVER(solver)->serialize();

diff --git a/src/ccsolver.h b/src/ccsolver.h
index 091303fb18540a420da62aaac0c8ad1f632489e3..8e708b833e407aa2a4aed5205fd501cfd0919fb7 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -46,6 +46,7 @@ void freezeElement(void *solver,void *element);
 int getBooleanValue(void *solver,void *boolean);
 int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);
 int getBooleanValue(void *solver,void *boolean);
 int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);

+void turnoffOptimizations(void *solver);

 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
 void setInterpreter(void *solver, unsigned int type);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
 void setInterpreter(void *solver, unsigned int type);

diff --git a/src/csolver.cc b/src/csolver.cc
index d1c6d33f202826cdb41807586c441efca6543c86..379858685235b90dd9514b4519417696d4bae906 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -40,6 +40,7 @@ CSolver::CSolver() :
        unsat(false),
        booleanVarUsed(false),
        incrementalMode(false),
        unsat(false),
        booleanVarUsed(false),
        incrementalMode(false),

+       optimizationsOff(false),

        tuner(NULL),
        elapsedTime(0),
        satsolverTimeout(NOTIMEOUT),
        tuner(NULL),
        elapsedTime(0),
        satsolverTimeout(NOTIMEOUT),


@@ -566,7 +567,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {

-       if (!useInterpreter()) {
+       if (!useInterpreter() && !optimizationsOff) {

                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {


@@ -650,8 +651,9 @@ int CSolver::solveIncremental() {
        }
        int result = IS_INDETER;
        ASSERT (!useInterpreter());
        }
        int result = IS_INDETER;
        ASSERT (!useInterpreter());

-       
-       computePolarities(this);
+       if(!optimizationsOff){
+               computePolarities(this);
+       }

 //     long long time1 = getTimeNano();
 //     model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 //     Preprocess pp(this);
 //     long long time1 = getTimeNano();
 //     model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 //     Preprocess pp(this);


@@ -733,36 +735,39 @@ int CSolver::solve() {
                        }
                        delete orderit;
                }
                        }
                        delete orderit;
                }

+               long long time1, time2;
+               

                computePolarities(this);
                computePolarities(this);

-               long long time1 = getTimeNano();
-               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
-               Preprocess pp(this);
-               pp.doTransform();
-               long long time2 = getTimeNano();
-               model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
-
-               DecomposeOrderTransform dot(this);
-               dot.doTransform();

                time1 = getTimeNano();
                time1 = getTimeNano();

-               model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+               if(!optimizationsOff){
+                       Preprocess pp(this);
+                       pp.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);

 
 

-               IntegerEncodingTransform iet(this);
-               iet.doTransform();
+                       DecomposeOrderTransform dot(this);
+                       dot.doTransform();
+                       time1 = getTimeNano();
+                       model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);

 
 

-               ElementOpt eop(this);
-               eop.doTransform();
+                       IntegerEncodingTransform iet(this);
+                       iet.doTransform();

 
 

-               EncodingGraph eg(this);
-               eg.encode();
+                       ElementOpt eop(this);
+                       eop.doTransform();

 
 

+                       EncodingGraph eg(this);
+                       eg.encode();
+               }

                naiveEncodingDecision(this);
                //      eg.validate();
                naiveEncodingDecision(this);
                //      eg.validate();

-
-               VarOrderingOpt bor(this, satEncoder);
-               bor.doTransform();
-
-               time2 = getTimeNano();
-               model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               if(!optimizationsOff){
+                       VarOrderingOpt bor(this, satEncoder);
+                       bor.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               }

 
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
 
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();

diff --git a/src/csolver.h b/src/csolver.h
index 6996e4229c9376f78b5d4258ee7d2669f334b858..49438b697b1235287cba1a437ec4b17aa63c9f7f 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -142,6 +142,8 @@ public:
 
        void freezeElement(Element *e);
        
 
        void freezeElement(Element *e);
        

+       void turnoffOptimizations(){optimizationsOff = true;}
+       

        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 
        /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
        bool getBooleanValue(BooleanEdge boolean);
 


@@ -237,10 +239,12 @@ private:
        bool unsat;
        bool booleanVarUsed;
        bool incrementalMode;
        bool unsat;
        bool booleanVarUsed;
        bool incrementalMode;

+       bool optimizationsOff;

        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;
        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;

+       bool noOptimization;

        friend class ElementOpt;
        friend class VarOrderingOpt;
 };
        friend class ElementOpt;
        friend class VarOrderingOpt;
 };

diff --git a/src/pycsolver.py b/src/pycsolver.py
index 905d1d775a8fd25b99a947e77d67b8d8d010b66d..a3e0f11b3c5ed981997a84b2a44b006a86f8f352 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -115,6 +115,8 @@ def loadCSolver():
        csolverlb.getOrderConstraintValue.restype = c_int
        csolverlb.printConstraints.argtypes = [c_void_p]
        csolverlb.printConstraints.restype = None
        csolverlb.getOrderConstraintValue.restype = c_int
        csolverlb.printConstraints.argtypes = [c_void_p]
        csolverlb.printConstraints.restype = None

+       csolverlb.turnoffOptimizations.argtypes = [c_void_p]
+       csolverlb.turnoffOptimizations.restype = None

         csolverlb.clone.argtypes = [c_void_p]
        csolverlb.clone.restype = c_void_p
        csolverlb.serialize.argtypes = [c_void_p]
         csolverlb.clone.argtypes = [c_void_p]
        csolverlb.clone.restype = c_void_p
        csolverlb.serialize.argtypes = [c_void_p]

diff --git a/src/satune_SatuneJavaAPI.cc b/src/satune_SatuneJavaAPI.cc
index d1397ee88e7ebe7be39cb2a98260c30bff990eb6..e337590fa92b409cb9272beb9e65a26ea8cfad77 100644 (file)
--- a/src/satune_SatuneJavaAPI.cc
+++ b/src/satune_SatuneJavaAPI.cc
@@ -457,6 +457,17 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        printConstraints((void *)solver);
 }
 
        printConstraints((void *)solver);
 }
 

+/*
+ * Class:     SatuneJavaAPI
+ * Method:    turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+       (JNIEnv *env, jobject obj, jlong solver)
+{
+       turnoffOptimizations((void *)solver);
+}
+

 /*
  * Class:     SatuneJavaAPI
  * Method:    serialize
 /*
  * Class:     SatuneJavaAPI
  * Method:    serialize

diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h
index 7b301f96ba3c7b2703b6017ee08a8e9e1c98a7b8..e606b44a74388e8cbb322e2f86b44019a83cce8b 100644 (file)
--- a/src/satune_SatuneJavaAPI.h
+++ b/src/satune_SatuneJavaAPI.h
@@ -329,6 +329,14 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        (JNIEnv *, jobject, jlong);
 
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        (JNIEnv *, jobject, jlong);
 

+/*
+ * Class:     satune_SatuneJavaAPI
+ * Method:    turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+       (JNIEnv *, jobject, jlong);
+

 /*
  * Class:     satune_SatuneJavaAPI
  * Method:    serialize
 /*
  * Class:     satune_SatuneJavaAPI
  * Method:    serialize