Adding checks to avoid further processing on UNSAT Problems
[satune.git] / src / csolver.cc
index 1eba56d..cd2ec55 100644 (file)
@@ -605,6 +605,9 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
 }
 
 int CSolver::solve() {
+       if(isUnSAT()){
+               return IS_UNSAT;
+       }
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -660,7 +663,7 @@ int CSolver::solve() {
 
                time2 = getTimeNano();
                model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 
                time2 = getTimeNano();
                model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+               
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
 
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();