Adding checks to avoid further processing on UNSAT Problems
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Mar 2019 01:09:47 +0000 (18:09 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Mar 2019 01:09:47 +0000 (18:09 -0700)
13 files changed:
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Polarity/polarityassignment.cc
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/elementopt.cc
src/ASTTransform/integerencoding.cc
src/ASTTransform/preprocess.cc
src/ASTTransform/varorderingopt.cc
src/Backend/satencoder.cc
src/Encoders/naiveencoder.cc
src/Test/deserializersolveprintopt.cc
src/common.mk
src/csolver.cc
src/csolver.h

index 66d8606..84166a8 100644 (file)
@@ -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();
index 4a772ee..b8b01d0 100644 (file)
@@ -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();
index 62b0828..eaf8141 100644 (file)
@@ -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()) {
index 96ca8f6..899f659 100644 (file)
@@ -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.
index 6be73ea..2a7b901 100644 (file)
@@ -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()) {
index c0e3571..ca2a655 100644 (file)
@@ -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);
index 890afd9..9fd8c60 100644 (file)
@@ -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;
index 62adb2f..618b8c1 100644 (file)
@@ -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();
index 63ec82f..ac20be5 100644 (file)
@@ -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();
index 0c707ce..d5f5c2e 100644 (file)
@@ -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;
        }
index b99e2db..1533d5f 100644 (file)
@@ -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
 
index 1eba56d..cd2ec55 100644 (file)
@@ -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();
 
index d7ccdb5..54012de 100644 (file)
@@ -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);