Adding checks to avoid further processing on UNSAT Problems

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 66d86062aa2d5a7c08513a80001b25a582b73f66..84166a88ddf6dd51773c04765f0e0107053e0a9b 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -113,7 +113,7 @@ void EncodingGraph::validate() {
 
 
 void EncodingGraph::encode() {
-       if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+       if (solver->isUnSAT() || solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
                return;
        buildGraph();
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();

diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index 4a772ee87839187cca95aa9e1acd4bf6c1f03d04..b8b01d0e6a4b99f769a4df47d7fa734c044a5f10 100644 (file)
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -2,6 +2,9 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
+       if(This->isUnSAT()){
+               return;
+       }
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge boolean = iterator->next();

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 62b08284cbcd446fccb6677e01b49d26b53d563b..eaf81415bdb74a31771ad9c541761d1f78187606 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -28,6 +28,8 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
+       if(solver->isUnSAT())
+               return;
        HashsetOrder *orders = solver->getActiveOrders()->copy();
        SetIteratorOrder *orderit = orders->iterator();
        while (orderit->hasNext()) {

diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 96ca8f65cb408c14400fae975dff4d65160b5de0..899f6591c2b4ce4a7eed0f18e8e1134d73895b4f 100644 (file)
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -17,7 +17,7 @@ ElementOpt::~ElementOpt() {
 }
 
 void ElementOpt::doTransform() {
-       if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
+       if (solver->isUnSAT() || solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
                return;
 
        //Set once we know we are going to use it.

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 6be73ea9bfbf648d7e2eac98e8610a98c6c8aff6..2a7b9012f74eae6272ef4a97d23545060028a67a 100644 (file)
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -17,6 +17,9 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {
+       if(solver->isUnSAT()){
+               return;
+       }
        HashsetOrder *orders = solver->getActiveOrders()->copy();
        SetIteratorOrder *orderit = orders->iterator();
        while (orderit->hasNext()) {

diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
index c0e357173d3d815d10bd08887850cb228ef5e140..ca2a655987b6395b286e045bb72e281c995d4f82 100644 (file)
--- a/src/ASTTransform/preprocess.cc
+++ b/src/ASTTransform/preprocess.cc
@@ -13,7 +13,7 @@ Preprocess::~Preprocess() {
 }
 
 void Preprocess::doTransform() {
-       if (!solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+       if (solver->isUnSAT() || !solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
                return;
 
        BooleanIterator bit(solver);

diff --git a/src/ASTTransform/varorderingopt.cc b/src/ASTTransform/varorderingopt.cc
index 890afd97009d0efa11a865e288ad902fe8a0d84d..9fd8c60eed3cb96512e55c56b9d78138c588fe91 100644 (file)
--- a/src/ASTTransform/varorderingopt.cc
+++ b/src/ASTTransform/varorderingopt.cc
@@ -26,6 +26,9 @@ VarOrderingOpt::~VarOrderingOpt() {
 }
 
 void VarOrderingOpt::doTransform() {
+       if(solver->isUnSAT()){
+               return;
+       }
        BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
        if ( direction == CONSTRAINTORDERING ) {
                return;

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 62adb2fa9a635fbdde70862b5d2f75c3c4eac304..618b8c17c22114177393754313dda6a3c1d8aa5c 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -35,6 +35,9 @@ int SATEncoder::solve(long timeout) {
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+       if(csolver->isUnSAT()){
+               return;
+       }
        SetIteratorBooleanEdge *iterator = csolver->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge constraint = iterator->next();

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index 63ec82f66d4d55488a60869067c11d1383bd1524..ac20be5ce06e28572ba61a331f3094fa24a6202e 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -15,6 +15,9 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
+       if(This->isUnSAT()){
+               return;
+       }
        SetIteratorBooleanEdge *iterator = This->getConstraints();
        while (iterator->hasNext()) {
                BooleanEdge b = iterator->next();

diff --git a/src/Test/deserializersolveprintopt.cc b/src/Test/deserializersolveprintopt.cc
index 0c707ce8c2577f063d609e203664fe96df90d032..d5f5c2e3bace826873a3e57e4e24809bc43a8eeb 100644 (file)
--- a/src/Test/deserializersolveprintopt.cc
+++ b/src/Test/deserializersolveprintopt.cc
@@ -8,13 +8,13 @@ int main(int argc, char **argv) {
        }
        for (int i = 1; i < argc; i++) {
                CSolver *solver = CSolver::deserialize(argv[i]);
+               solver->printConstraints();
                int value = solver->solve();
                if (value == 1) {
                        printf("%s is SAT\n", argv[i]);
                } else {
                        printf("%s is UNSAT\n", argv[i]);
                }
-               solver->printConstraints();
 
                delete solver;
        }

diff --git a/src/common.mk b/src/common.mk
index b99e2db7c69a602ee44dd4d9581e2d80a3693db5..1533d5f81cb96ff8e7412a094041bb5da178cf09 100644 (file)
--- a/src/common.mk
+++ b/src/common.mk
@@ -5,7 +5,7 @@ CXX := g++
 JAVAC := javac
 
 UNAME := $(shell uname)
-JAVA_INC := /usr/lib/jvm/java-1.8.0-openjdk-amd64/include/
+JAVA_INC := /usr/lib/jvm/default-java/include/
 LIB_NAME := cons_comp
 LIB_SO := lib_$(LIB_NAME).so
 

diff --git a/src/csolver.cc b/src/csolver.cc
index 1eba56d4bd46afdfa886a9e7b5efbfaa361360a2..cd2ec550aae443580cc9fac82b0d9f918aa0b174 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -605,6 +605,9 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
+       if(isUnSAT()){
+               return IS_UNSAT;
+       }
        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);
-
+               
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
 

diff --git a/src/csolver.h b/src/csolver.h
index d7ccdb53ee3bd58f46857b7ceb496fa7440b1923..54012dee4ae3adf9deafd7b172dd573d539777c0 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -126,7 +126,7 @@ public:
 
        /** When everything is done, the client calls this function and then csolver starts to encode*/
        int solve();
-
+       
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);