From 3a614d0deec343d2474efaabaa7220e7bcbed0d0 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Thu, 13 Jun 2019 20:27:06 -0700 Subject: [PATCH] Incremental solver works and the test case passes --- src/AST/element.cc | 3 +- src/AST/element.h | 3 ++ src/ASTTransform/elementopt.cc | 2 +- src/Backend/constraint.cc | 8 +-- src/Backend/constraint.h | 1 + src/Backend/satelemencoder.cc | 9 ++++ src/Backend/satencoder.cc | 13 ++++- src/Backend/satencoder.h | 1 + src/Test/incrementaltest.cc | 38 ++++++++++++++ src/csolver.cc | 90 +++++++++++++++++++++++++++++++++- src/csolver.h | 24 +++++++-- 11 files changed, 179 insertions(+), 13 deletions(-) create mode 100644 src/Test/incrementaltest.cc diff --git a/src/AST/element.cc b/src/AST/element.cc index f182cd2..8044966 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -9,7 +9,8 @@ Element::Element(ASTNodeType _type) : ASTNode(_type), encoding(this), - anyValue(false) { + anyValue(false), + frozen(false){ } ElementSet::ElementSet(Set *s) : diff --git a/src/AST/element.h b/src/AST/element.h index 91d677f..166078a 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -15,6 +15,8 @@ public: Vector parents; ElementEncoding encoding; inline ElementEncoding *getElementEncoding() { return &encoding; } + inline void freezeElement(){frozen = true;} + inline bool isFrozen(){return frozen;} virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}; virtual void serialize(Serializer *serializer) = 0; virtual void print() = 0; @@ -22,6 +24,7 @@ public: virtual Set *getRange() = 0; CMEMALLOC; bool anyValue; + bool frozen; }; class ElementSet : public Element { diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc index 22a6dbe..413d5dd 100644 --- a/src/ASTTransform/elementopt.cc +++ b/src/ASTTransform/elementopt.cc @@ -26,7 +26,7 @@ void ElementOpt::doTransform() { SetIteratorBooleanEdge *iterator = solver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); - if (constraint->type == PREDICATEOP) + if (!solver->isConstraintEncoded(constraint) && constraint->type == PREDICATEOP) workList.push((BooleanPredicate *)constraint.getBoolean()); } while (workList.getSize() != 0) { diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc index f92c223..5246101 100644 --- a/src/Backend/constraint.cc +++ b/src/Backend/constraint.cc @@ -589,6 +589,11 @@ void addClause(CNF *cnf, uint numliterals, int *literals) { addArrayClauseLiteral(cnf->solver, numliterals, literals); } +void freezeVariable(CNF *cnf, Edge e){ + int literal = getEdgeVar(e); + freeze(cnf->solver, literal); +} + void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) { Node *andNode = cnfform.node_ptr; int orvar = getEdgeVar(eorvar); @@ -696,13 +701,10 @@ Edge constraintNewVar(CNF *cnf) { } int solveCNF(CNF *cnf) { - long long startTime = getTimeNano(); - finishedClauses(cnf->solver); long long startSolve = getTimeNano(); model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount); int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver); long long finishTime = getTimeNano(); - cnf->encodeTime = startSolve - startTime; model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0); cnf->solveTime = finishTime - startSolve; model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0); diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 8d2666c..f623571 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -182,6 +182,7 @@ void outputCNF(CNF *cnf, Edge cnfform); void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar); void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p); void addClause(CNF *cnf, uint numliterals, int *literals); +void freezeVariable(CNF *cnf, Edge e); Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value); Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value); Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2); diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc index 3f26b5c..aa73924 100644 --- a/src/Backend/satelemencoder.cc +++ b/src/Backend/satelemencoder.cc @@ -220,6 +220,15 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) { generateAnyValueBinaryValueEncoding(encoding); } +void SATEncoder::freezeElementVariables(ElementEncoding *encoding){ + ASSERT(encoding->element->frozen); + for(uint i=0; i< encoding->numVars; i++){ + Edge e = encoding->variables[i]; + ASSERT(edgeIsVarConst(e)); + freezeVariable(cnf, e); + } +} + void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) { ASSERT(encoding->type == BINARYINDEX); allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1)); diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc index 00219ef..5312b4f 100755 --- a/src/Backend/satencoder.cc +++ b/src/Backend/satencoder.cc @@ -31,6 +31,12 @@ void SATEncoder::resetSATEncoder() { int SATEncoder::solve(long timeout) { cnf->solver->timeout = timeout; + long long startTime = getTimeNano(); + finishedClauses(cnf->solver); + cnf->encodeTime = getTimeNano() - startTime; + if(solver->isIncrementalMode()){ + solver->freezeElementsVariables(); + } return solveCNF(cnf); } @@ -41,8 +47,11 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) { SetIteratorBooleanEdge *iterator = csolver->getConstraints(); while (iterator->hasNext()) { BooleanEdge constraint = iterator->next(); - Edge c = encodeConstraintSATEncoder(constraint); - addConstraintCNF(cnf, c); + if(!csolver->isConstraintEncoded(constraint)){ + Edge c = encodeConstraintSATEncoder(constraint); + addConstraintCNF(cnf, c); + csolver->addEncodedConstraint(constraint); + } } delete iterator; } diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 1f8253a..11387a8 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -19,6 +19,7 @@ public: CNF *getCNF() { return cnf;} long long getSolveTime() { return cnf->solveTime; } long long getEncodeTime() { return cnf->encodeTime; } + void freezeElementVariables(ElementEncoding *encoding); CMEMALLOC; private: diff --git a/src/Test/incrementaltest.cc b/src/Test/incrementaltest.cc new file mode 100644 index 0000000..c71645d --- /dev/null +++ b/src/Test/incrementaltest.cc @@ -0,0 +1,38 @@ +#include "csolver.h" + +#define INPUTSIZE 2 +#define DOMAINSIZE 3 + +int main(int numargs, char **argv) { + CSolver *solver = new CSolver(); + uint64_t set1[] = {3, 1, 2}; + uint64_t set2[] = {3, 1, 7}; + Set *s1 = solver->createSet(0, set1, DOMAINSIZE); + Set *s2 = solver->createSet(0, set2, DOMAINSIZE); + Element *e1 = solver->getElementVar(s1); + Element *e2 = solver->getElementVar(s2); + Predicate *equals = solver->createPredicateOperator(SATC_EQUALS); + Element *inputs[] = {e1, e2}; + BooleanEdge b = solver->applyPredicate(equals, inputs, INPUTSIZE); + solver->addConstraint(b); + solver->freezeElement(e1); + solver->freezeElement(e2); + if (solver->solve() == 1){ + int run = 1; + do{ + printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2)); + for(int i=0; i< INPUTSIZE; i++){ + uint64_t val = solver->getElementValue(inputs[i]); + Element *econst = solver->getElementConst(0, val); + Element * tmpInputs[] = {inputs[i], econst}; + BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE); + solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b)); + } + run++; + }while(solver->solveIncremental() == 1); + printf("After %d runs, there are no more models to find ...\n", run); + }else{ + printf("UNSAT\n"); + } + delete solver; +} diff --git a/src/csolver.cc b/src/csolver.cc index a02227e..d1c6d33 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -39,6 +39,7 @@ CSolver::CSolver() : boolFalse(boolTrue.negate()), unsat(false), booleanVarUsed(false), + incrementalMode(false), tuner(NULL), elapsedTime(0), satsolverTimeout(NOTIMEOUT), @@ -139,6 +140,7 @@ void CSolver::resetSolver() { allOrders.clear(); allFunctions.clear(); constraints.reset(); + encodedConstraints.reset(); activeOrders.reset(); boolMap.reset(); elemMap.reset(); @@ -240,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(); } @@ -623,6 +636,74 @@ 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; @@ -689,7 +770,7 @@ int CSolver::solve() { 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"); @@ -756,6 +837,13 @@ uint64_t CSolver::getElementValue(Element *element) { 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) { diff --git a/src/csolver.h b/src/csolver.h index 0ff566e..6996e42 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -58,7 +58,7 @@ public: Set *getElementRange (Element *element); void mustHaveValue(Element *element); - + BooleanEdge getBooleanTrue(); BooleanEdge getBooleanFalse(); @@ -129,10 +129,19 @@ public: /** When everything is done, the client calls this function and then csolver starts to encode*/ int solve(); - + /** + * Incremental Solving for SATUNE. + * It only supports incremental solving for elements! + * No support for BooleanVar, BooleanOrder or using interpreters + * @return + */ + int solveIncremental(); + /** After getting the solution from the SAT solver, client can get the value of an element via this function*/ uint64_t getElementValue(Element *element); + void freezeElement(Element *e); + /** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/ bool getBooleanValue(BooleanEdge boolean); @@ -154,7 +163,9 @@ public: Tuner *getTuner() { return tuner; } SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); } - + bool isConstraintEncoded(BooleanEdge be) { return encodedConstraints.contains(be);} + void addEncodedConstraint(BooleanEdge be) {encodedConstraints.add(be);} + SATEncoder *getSATEncoder() {return satEncoder;} void replaceBooleanWithTrue(BooleanEdge bexpr); @@ -175,20 +186,22 @@ public: long long getEncodeTime(); long long getSolveTime(); long getSatSolverTimeout() { return satsolverTimeout;} - + bool isIncrementalMode() {return incrementalMode;} + void freezeElementsVariables(); CMEMALLOC; private: void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child); void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child); void handleFunction(ElementFunction *ef, BooleanEdge child); - + //These two functions are helpers if the client has a pointer to a //Boolean object that we have since replaced BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize); BooleanEdge doRewrite(BooleanEdge b); /** This is a vector of constraints that must be satisfied. */ HashsetBooleanEdge constraints; + HashsetBooleanEdge encodedConstraints; /** This is a vector of all boolean structs that we have allocated. */ Vector allBooleans; @@ -223,6 +236,7 @@ private: SATEncoder *satEncoder; bool unsat; bool booleanVarUsed; + bool incrementalMode; Tuner *tuner; long long elapsedTime; long satsolverTimeout; -- 2.34.1