From cbd921ee35b6a29934fd7cecccde7f160228af17 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Mon, 18 Mar 2019 18:09:47 -0700 Subject: [PATCH] Adding checks to avoid further processing on UNSAT Problems --- src/ASTAnalyses/Encoding/encodinggraph.cc | 2 +- src/ASTAnalyses/Polarity/polarityassignment.cc | 3 +++ src/ASTTransform/decomposeordertransform.cc | 2 ++ src/ASTTransform/elementopt.cc | 2 +- src/ASTTransform/integerencoding.cc | 3 +++ src/ASTTransform/preprocess.cc | 2 +- src/ASTTransform/varorderingopt.cc | 3 +++ src/Backend/satencoder.cc | 3 +++ src/Encoders/naiveencoder.cc | 3 +++ src/Test/deserializersolveprintopt.cc | 2 +- src/common.mk | 2 +- src/csolver.cc | 5 ++++- src/csolver.h | 2 +- 13 files changed, 27 insertions(+), 7 deletions(-) diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc index 66d8606..84166a8 100644 --- 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 4a772ee..b8b01d0 100644 --- 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 62b0828..eaf8141 100644 --- 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 96ca8f6..899f659 100644 --- 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 6be73ea..2a7b901 100644 --- 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 c0e3571..ca2a655 100644 --- 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 890afd9..9fd8c60 100644 --- 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 62adb2f..618b8c1 100644 --- 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 63ec82f..ac20be5 100644 --- a/src/Encoders/naiveencoder.cc +++ b/src/Encoders/naiveencoder.cc @@ -15,6 +15,9 @@ #include 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 0c707ce..d5f5c2e 100644 --- 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 b99e2db..1533d5f 100644 --- 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 1eba56d..cd2ec55 100644 --- 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 d7ccdb5..54012de 100644 --- 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); -- 2.34.1