edits

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 0efe7a138a1da5edfd310fc9784e6c751ee76286..5342c4f62ab6bede6a0e67d0998ce8d6d628ea21 100644 (file)
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -273,8 +273,6 @@ void SATEncoder::generateElementEncoding(Element *element) {
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
        if(encoding->numVars == 0)
                return;
 void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
        if(encoding->numVars == 0)
                return;

-       Edge carray[encoding->numVars];
-       int size = 0;

        int index = -1;
        for(uint i= encoding->encArraySize-1; i>=0; i--){
                if(encoding->isinUseElement(i)){
        int index = -1;
        for(uint i= encoding->encArraySize-1; i>=0; i--){
                if(encoding->isinUseElement(i)){


@@ -285,17 +283,14 @@ void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
                }
        }
        if( index != -1 ){
                }
        }
        if( index != -1 ){

-               carray[size++] = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index);
+               addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));

        }
        index = index == -1? encoding->encArraySize-1 : index-1;
        }
        index = index == -1? encoding->encArraySize-1 : index-1;

-       for(int i= index; i>=0; i--){
+       for(int i= index; i>=0; i--) {

                if (!encoding->isinUseElement(i)){
                if (!encoding->isinUseElement(i)){

-                       carray[size++] = constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i));
+                       addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));

                }
        }
                }
        }

-       if(size > 0){
-               addConstraintCNF(cnf, constraintAND(cnf, size, carray));
-       }

 }
 
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
 }
 
 void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){


@@ -304,6 +299,7 @@ void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
        model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
        Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset);
        Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset));
        model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
        Edge lowerbound = generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, maxvalueminusoffset);
        Edge upperbound = constraintNegate(generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, minvalueminusoffset));

-       addConstraintCNF(cnf, constraintAND2(cnf, lowerbound, upperbound));
+       addConstraintCNF(cnf, lowerbound);
+       addConstraintCNF(cnf, upperbound);

 }
 
 }