From 974a00584da88dce9c638bd5fd981f2164176e2c Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 3 Jul 2019 17:05:35 -0700 Subject: [PATCH] Add a configuration for disabling the optimizations --- src/SatuneJavaAPI.java | 5 ++++ src/ccsolver.cc | 4 +++ src/ccsolver.h | 1 + src/csolver.cc | 55 ++++++++++++++++++++----------------- src/csolver.h | 4 +++ src/pycsolver.py | 2 ++ src/satune_SatuneJavaAPI.cc | 11 ++++++++ src/satune_SatuneJavaAPI.h | 8 ++++++ 8 files changed, 65 insertions(+), 25 deletions(-) diff --git a/src/SatuneJavaAPI.java b/src/SatuneJavaAPI.java index 2b6baea..a5e71d3 100644 --- a/src/SatuneJavaAPI.java +++ b/src/SatuneJavaAPI.java @@ -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); diff --git a/src/ccsolver.cc b/src/ccsolver.cc index ca20617..7707b74 100644 --- a/src/ccsolver.cc +++ b/src/ccsolver.cc @@ -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(); diff --git a/src/ccsolver.h b/src/ccsolver.h index 091303f..8e708b8 100644 --- 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); +void turnoffOptimizations(void *solver); 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 d1c6d33..3798586 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -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(); diff --git a/src/csolver.h b/src/csolver.h index 6996e42..49438b6 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -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; }; diff --git a/src/pycsolver.py b/src/pycsolver.py index 905d1d7..a3e0f11 100644 --- 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.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] diff --git a/src/satune_SatuneJavaAPI.cc b/src/satune_SatuneJavaAPI.cc index d1397ee..e337590 100644 --- a/src/satune_SatuneJavaAPI.cc +++ b/src/satune_SatuneJavaAPI.cc @@ -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 diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h index 7b301f9..e606b44 100644 --- 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); +/* + * Class: satune_SatuneJavaAPI + * Method: turnoffOptimizations + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations + (JNIEnv *, jobject, jlong); + /* * Class: satune_SatuneJavaAPI * Method: serialize -- 2.34.1