Add a configuration for disabling the optimizations
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 4 Jul 2019 00:05:35 +0000 (17:05 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 4 Jul 2019 00:05:35 +0000 (17:05 -0700)
src/SatuneJavaAPI.java
src/ccsolver.cc
src/ccsolver.h
src/csolver.cc
src/csolver.h
src/pycsolver.py
src/satune_SatuneJavaAPI.cc
src/satune_SatuneJavaAPI.h

index 2b6baea..a5e71d3 100644 (file)
@@ -43,6 +43,10 @@ public class SatuneJavaAPI{
             printConstraints(satune);
         }
        
+        public void turnoffOptimizations(){
+            turnoffOptimizations(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 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);
index ca20617..7707b74 100644 (file)
@@ -170,6 +170,10 @@ void printConstraints(void *solver) {
        CCSOLVER(solver)->printConstraints();
 }
 
+void turnoffOptimizations(void *solver) {
+       CCSOLVER(solver)->turnoffOptimizations();
+}
+
 
 void serialize(void *solver) {
        CCSOLVER(solver)->serialize();
index 091303f..8e708b8 100644 (file)
@@ -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);
+void turnoffOptimizations(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
 void setInterpreter(void *solver, unsigned int type);
index d1c6d33..3798586 100644 (file)
@@ -40,6 +40,7 @@ CSolver::CSolver() :
        unsat(false),
        booleanVarUsed(false),
        incrementalMode(false),
+       optimizationsOff(false),
        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) {
-       if (!useInterpreter()) {
+       if (!useInterpreter() && !optimizationsOff) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
@@ -650,8 +651,9 @@ int CSolver::solveIncremental() {
        }
        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);
@@ -733,36 +735,39 @@ int CSolver::solve() {
                        }
                        delete orderit;
                }
+               long long time1, time2;
+               
                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();
-               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();
-
-               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();
index 6996e42..49438b6 100644 (file)
@@ -142,6 +142,8 @@ public:
 
        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);
 
@@ -237,10 +239,12 @@ private:
        bool unsat;
        bool booleanVarUsed;
        bool incrementalMode;
+       bool optimizationsOff;
        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
        Interpreter *interpreter;
+       bool noOptimization;
        friend class ElementOpt;
        friend class VarOrderingOpt;
 };
index 905d1d7..a3e0f11 100644 (file)
@@ -115,6 +115,8 @@ def loadCSolver():
        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]
index d1397ee..e337590 100644 (file)
@@ -457,6 +457,17 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
        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
index 7b301f9..e606b44 100644 (file)
@@ -329,6 +329,14 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
 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