X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=d1c6d33f202826cdb41807586c441efca6543c86;hb=3a614d0deec343d2474efaabaa7220e7bcbed0d0;hp=14f902b85e846c5f7c6e0a7e1bc76eb03705a9a3;hpb=3267d387309bb4d2aa130a940f386b419652a956;p=satune.git diff --git a/src/csolver.cc b/src/csolver.cc index 14f902b..d1c6d33 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -29,13 +29,17 @@ #include "varorderingopt.h" #include #include -#include "alloyenc.h" +#include "alloyinterpreter.h" +#include "smtinterpreter.h" +#include "mathsatinterpreter.h" +#include "smtratinterpreter.h" CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), boolFalse(boolTrue.negate()), unsat(false), booleanVarUsed(false), + incrementalMode(false), tuner(NULL), elapsedTime(0), satsolverTimeout(NOTIMEOUT), @@ -82,8 +86,8 @@ CSolver::~CSolver() { for (uint i = 0; i < size; i++) { delete allFunctions.get(i); } - - if(interpreter != NULL){ + + if (interpreter != NULL) { delete interpreter; } @@ -136,6 +140,7 @@ void CSolver::resetSolver() { allOrders.clear(); allFunctions.clear(); constraints.reset(); + encodedConstraints.reset(); activeOrders.reset(); boolMap.reset(); elemMap.reset(); @@ -162,9 +167,9 @@ CSolver *CSolver::clone() { return copy; } -CSolver *CSolver::deserialize(const char *file, bool alloy) { +CSolver *CSolver::deserialize(const char *file, InterpreterType itype) { model_print("deserializing %s ...\n", file); - Deserializer deserializer(file, alloy); + Deserializer deserializer(file, itype); return deserializer.deserialize(); } @@ -237,6 +242,17 @@ void CSolver::mustHaveValue(Element *element) { element->anyValue = true; } +void CSolver::freezeElementsVariables() { + + for(uint i=0; i< allElements.getSize(); i++){ + Element *e = allElements.get(i); + if(e->frozen){ + satEncoder->freezeElementVariables(&e->encoding); + } + } +} + + Set *CSolver::getElementRange (Element *element) { return element->getRange(); } @@ -261,7 +277,6 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) { - ASSERT(numArrays == 2); Element *element = new ElementFunction(function,array,numArrays,overflowstatus); Element *e = elemMap.get(element); if (e == NULL) { @@ -316,7 +331,7 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) { BooleanEdge CSolver::getBooleanVar(VarType type) { Boolean *boolean = new BooleanVar(type); allBooleans.push(boolean); - if(!booleanVarUsed) + if (!booleanVarUsed) booleanVarUsed = true; return BooleanEdge(boolean); } @@ -393,8 +408,28 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin return applyLogicalOperation(op, newarray, asize); } +BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize){ + BooleanEdge newarray[asize + 1]; + + newarray[asize] = applyLogicalOperation(SATC_OR, array, asize); + for (uint i=0; i< asize; i++){ + BooleanEdge oprand1 = array[i]; + BooleanEdge carray [asize -1]; + uint index = 0; + for( uint j =0; j< asize; j++){ + if(i != j){ + BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]); + carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2); + } + } + ASSERT(index == asize -1); + newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1); + } + return applyLogicalOperation(SATC_AND, newarray, asize+1); +} + BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { - if(!useAlloyCompiler()){ + if (!useInterpreter()) { BooleanEdge newarray[asize]; switch (op) { case SATC_NOT: { @@ -457,7 +492,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]); } } - + ASSERT(asize != 0); Boolean *boolean = new BooleanLogic(this, op, array, asize); Boolean *b = boolMap.get(boolean); @@ -475,7 +510,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint Boolean *boolean = new BooleanLogic(this, op, array, asize); allBooleans.push(boolean); return BooleanEdge(boolean); - + } } @@ -494,7 +529,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } } Boolean *constraint = new BooleanOrder(order, first, second); - if (!useAlloyCompiler() ){ + if (!useInterpreter() ) { Boolean *b = boolMap.get(constraint); if (b == NULL) { @@ -531,7 +566,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } void CSolver::addConstraint(BooleanEdge constraint) { - if(!useAlloyCompiler()){ + if (!useInterpreter()) { if (isTrue(constraint)) return; else if (isFalse(constraint)) { @@ -569,7 +604,7 @@ void CSolver::addConstraint(BooleanEdge constraint) { replaceBooleanWithTrueNoRemove(constraint); constraint->parents.clear(); } - } else{ + } else { constraints.add(constraint); constraint->parents.clear(); } @@ -601,7 +636,78 @@ void CSolver::inferFixedOrders() { } } +int CSolver::solveIncremental() { + if (isUnSAT()) { + return IS_UNSAT; + } + + + long long startTime = getTimeNano(); + bool deleteTuner = false; + if (tuner == NULL) { + tuner = new DefaultTuner(); + deleteTuner = true; + } + int result = IS_INDETER; + ASSERT (!useInterpreter()); + + 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); + +// IntegerEncodingTransform iet(this); +// iet.doTransform(); + + //Doing element optimization on new constraints +// ElementOpt eop(this); +// eop.doTransform(); + + //Since no new element is added, we assuming adding new constraint + //has no impact on previous encoding decisions +// EncodingGraph eg(this); +// eg.encode(); + + naiveEncodingDecision(this); + // eg.validate(); + //Order of sat solver variables don't change! +// VarOrderingOpt bor(this, satEncoder); +// bor.doTransform(); + + long long time2 = getTimeNano(); + //Encoding newly added constraints + satEncoder->encodeAllSATEncoder(this); + long long time1 = getTimeNano(); + + model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC); + + model_print("Is problem UNSAT after encoding: %d\n", unsat); + + result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout); + model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT"); + time2 = getTimeNano(); + elapsedTime = time2 - startTime; + model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); + + if (deleteTuner) { + delete tuner; + tuner = NULL; + } + return result; +} + int CSolver::solve() { + if (isUnSAT()) { + return IS_UNSAT; + } long long startTime = getTimeNano(); bool deleteTuner = false; if (tuner == NULL) { @@ -609,12 +715,12 @@ int CSolver::solve() { deleteTuner = true; } int result = IS_INDETER; - if(useAlloyCompiler()){ + if (useInterpreter()) { interpreter->encode(); - model_print("Problem encoded in Alloy\n"); + model_print("Problem encoded in Interpreter\n"); result = interpreter->solve(); - model_print("Problem solved by Alloy\n"); - } else{ + model_print("Problem solved by Interpreter\n"); + } else { { SetIteratorOrder *orderit = activeOrders.iterator(); @@ -650,7 +756,7 @@ int CSolver::solve() { eg.encode(); naiveEncodingDecision(this); - // eg.validate(); + // eg.validate(); VarOrderingOpt bor(this, satEncoder); bor.doTransform(); @@ -679,9 +785,29 @@ int CSolver::solve() { return result; } -void CSolver::setAlloyEncoder(){ - if(interpreter == NULL){ - interpreter = new AlloyEnc(this); +void CSolver::setInterpreter(InterpreterType type) { + if (interpreter == NULL) { + switch (type) { + case SATUNE: + break; + case ALLOY: { + interpreter = new AlloyInterpreter(this); + break; + } case Z3: { + interpreter = new SMTInterpreter(this); + break; + } + case MATHSAT: { + interpreter = new MathSATInterpreter(this); + break; + } + case SMTRAT: { + interpreter = new SMTRatInterpreter(this); + break; + } + default: + ASSERT(0); + } } } @@ -703,20 +829,27 @@ uint64_t CSolver::getElementValue(Element *element) { case ELEMSET: case ELEMCONST: case ELEMFUNCRETURN: - return useAlloyCompiler()? interpreter->getValue(element): - getElementValueSATTranslator(this, element); + return useInterpreter() ? interpreter->getValue(element) : + getElementValueSATTranslator(this, element); default: ASSERT(0); } exit(-1); } +void CSolver::freezeElement(Element *e){ + e->freezeElement(); + if(!incrementalMode){ + incrementalMode = true; + } +} + bool CSolver::getBooleanValue(BooleanEdge bedge) { Boolean *boolean = bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: - return useAlloyCompiler()? interpreter->getBooleanValue(boolean): - getBooleanVariableValueSATTranslator(this, boolean); + return useInterpreter() ? interpreter->getBooleanValue(boolean) : + getBooleanVariableValueSATTranslator(this, boolean); default: ASSERT(0); }