Adding API for AtMostOneConstraint + bugfix for turning off the optimizations

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 379858685235b90dd9514b4519417696d4bae906..448fb9a7304e6b38a4b891883d151ff805d6a5d2 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -244,10 +244,10 @@ void CSolver::mustHaveValue(Element *element) {
 }
 
 void CSolver::freezeElementsVariables() {
-       
-       for(uint i=0; i< allElements.getSize(); i++){
+
+       for (uint i = 0; i < allElements.getSize(); i++) {
                Element *e = allElements.get(i);
-               if(e->frozen){
+               if (e->frozen) {
                        satEncoder->freezeElementVariables(&e->encoding);
                }
        }
@@ -409,28 +409,30 @@ 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);
-                       }
+BooleanEdge CSolver::applyAtMostOneConstraint (BooleanEdge *array, uint asize) {
+       if(asize == 0 || asize == 1){
+               return getBooleanTrue();
+       }
+       BooleanEdge newarray[asize*(asize-1)];
+       uint newsize = 0;
+       for (uint i = 0; i < asize -1; i++) {
+               for(uint j = i +1; j < asize; j++){
+                       BooleanEdge oprand1 = array[i];
+                       BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
+                       newarray[newsize++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
                }
-               ASSERT(index == asize -1);
-               newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1);
        }
-       return applyLogicalOperation(SATC_AND, newarray, asize+1);
+       return applyLogicalOperation(SATC_AND, newarray, newsize);
+}
+
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
+       BooleanEdge atleastOne = applyLogicalOperation(SATC_OR, array, asize);
+       BooleanEdge atmostOne = applyAtMostOneConstraint (array, asize);
+       return applyLogicalOperation(SATC_AND, atleastOne, atmostOne);
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-       if (!useInterpreter()) {
+       if (!useInterpreter() && !optimizationsOff) {
                BooleanEdge newarray[asize];
                switch (op) {
                case SATC_NOT: {
@@ -530,7 +532,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
                }
        }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       if (!useInterpreter() ) {
+       if (!useInterpreter() && !optimizationsOff ) {
                Boolean *b = boolMap.get(constraint);
 
                if (b == NULL) {
@@ -641,8 +643,8 @@ int CSolver::solveIncremental() {
        if (isUnSAT()) {
                return IS_UNSAT;
        }
-       
-       
+
+
        long long startTime = getTimeNano();
        bool deleteTuner = false;
        if (tuner == NULL) {
@@ -672,7 +674,7 @@ int CSolver::solveIncremental() {
        //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);
@@ -698,7 +700,7 @@ int CSolver::solveIncremental() {
        time2 = getTimeNano();
        elapsedTime = time2 - startTime;
        model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
-       
+
        if (deleteTuner) {
                delete tuner;
                tuner = NULL;
@@ -775,7 +777,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");
@@ -842,9 +844,9 @@ uint64_t CSolver::getElementValue(Element *element) {
        exit(-1);
 }
 
-void CSolver::freezeElement(Element *e){
+void CSolver::freezeElement(Element *e) {
        e->freezeElement();
-       if(!incrementalMode){
+       if (!incrementalMode) {
                incrementalMode = true;
        }
 }