Merging + fixing memory bugs

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index a02227e0b82ddedcb52c063ae99bb3611fa8fa2d..17e237888caa78445af6b5cb91b1b9c4ebcfcd39 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -39,6 +39,8 @@ CSolver::CSolver() :
        boolFalse(boolTrue.negate()),
        unsat(false),
        booleanVarUsed(false),
+       incrementalMode(false),
+       optimizationsOff(false),
        tuner(NULL),
        elapsedTime(0),
        satsolverTimeout(NOTIMEOUT),
@@ -139,6 +141,7 @@ void CSolver::resetSolver() {
        allOrders.clear();
        allFunctions.clear();
        constraints.reset();
+       encodedConstraints.reset();
        activeOrders.reset();
        boolMap.reset();
        elemMap.reset();
@@ -240,6 +243,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();
 }
@@ -395,24 +409,24 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
        return applyLogicalOperation(op, newarray, asize);
 }
 
-BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint 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++){
+       for (uint i = 0; i < asize; i++) {
                BooleanEdge oprand1 = array[i];
-               BooleanEdge carray [asize -1];
+               BooleanEdge carray [asize - 1];
                uint index = 0;
-               for( uint j =0; j< asize; j++){
-                       if(i != j){
+               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);
+               ASSERT(index == asize - 1);
+               newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
        }
-       return applyLogicalOperation(SATC_AND, newarray, asize+1);
+       return applyLogicalOperation(SATC_AND, newarray, asize + 1);
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
@@ -553,7 +567,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-       if (!useInterpreter()) {
+       if (!useInterpreter() && !optimizationsOff) {
                if (isTrue(constraint))
                        return;
                else if (isFalse(constraint)) {
@@ -623,6 +637,75 @@ 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());
+       if(!optimizationsOff){
+               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;
@@ -652,36 +735,39 @@ int CSolver::solve() {
                        }
                        delete orderit;
                }
+               long long time1, time2;
+               
                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);
+               model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+               if(!optimizationsOff){
+                       Preprocess pp(this);
+                       pp.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 
-               IntegerEncodingTransform iet(this);
-               iet.doTransform();
+                       DecomposeOrderTransform dot(this);
+                       dot.doTransform();
+                       time1 = getTimeNano();
+                       model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
-               ElementOpt eop(this);
-               eop.doTransform();
+                       IntegerEncodingTransform iet(this);
+                       iet.doTransform();
 
-               EncodingGraph eg(this);
-               eg.encode();
+                       ElementOpt eop(this);
+                       eop.doTransform();
 
+                       EncodingGraph eg(this);
+                       eg.encode();
+               }
                naiveEncodingDecision(this);
                //      eg.validate();
-
-               VarOrderingOpt bor(this, satEncoder);
-               bor.doTransform();
-
-               time2 = getTimeNano();
-               model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               if(!optimizationsOff){
+                       VarOrderingOpt bor(this, satEncoder);
+                       bor.doTransform();
+                       time2 = getTimeNano();
+                       model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+               }
 
                satEncoder->encodeAllSATEncoder(this);
                time1 = getTimeNano();
@@ -756,6 +842,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) {