Incremental solver works and the test case passes
authorHamed Gorjiara <hgorjiar@uci.edu>
Fri, 14 Jun 2019 03:27:06 +0000 (20:27 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Fri, 14 Jun 2019 03:27:06 +0000 (20:27 -0700)
src/AST/element.cc
src/AST/element.h
src/ASTTransform/elementopt.cc
src/Backend/constraint.cc
src/Backend/constraint.h
src/Backend/satelemencoder.cc
src/Backend/satencoder.cc
src/Backend/satencoder.h
src/Test/incrementaltest.cc [new file with mode: 0644]
src/csolver.cc
src/csolver.h

index f182cd2..8044966 100644 (file)
@@ -9,7 +9,8 @@
 Element::Element(ASTNodeType _type) :
        ASTNode(_type),
        encoding(this),
-       anyValue(false) {
+       anyValue(false),
+       frozen(false){
 }
 
 ElementSet::ElementSet(Set *s) :
index 91d677f..166078a 100644 (file)
@@ -15,6 +15,8 @@ public:
        Vector<ASTNode *> 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 {
index 22a6dbe..413d5dd 100644 (file)
@@ -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) {
index f92c223..5246101 100644 (file)
@@ -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);
index 8d2666c..f623571 100644 (file)
@@ -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);
index 3f26b5c..aa73924 100644 (file)
@@ -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));
index 00219ef..5312b4f 100755 (executable)
@@ -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;
 }
index 1f8253a..11387a8 100644 (file)
@@ -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 (file)
index 0000000..c71645d
--- /dev/null
@@ -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;
+}
index a02227e..d1c6d33 100644 (file)
@@ -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) {
index 0ff566e..6996e42 100644 (file)
@@ -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<Boolean *> allBooleans;
@@ -223,6 +236,7 @@ private:
        SATEncoder *satEncoder;
        bool unsat;
        bool booleanVarUsed;
+       bool incrementalMode;
        Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;