Fixing some bugs ...

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index f92f1e621d909edaa05fc4401444c58e0d2456eb..0609c7c018d8a24cdc67997a5423a9e47b6efd91 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -268,30 +268,33 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                switch(function->undefBehavior) {
                        case UNDEFINEDSETSFLAG: {
                                if (isInRange) {
+                                       //FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
                                        clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
                                } else {
-                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+                                       addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
                                }
                                break;
                        }
                        case FLAGIFFUNDEFINED: {
                                if (isInRange) {
-                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+                                       addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
                                } else {
-                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+                                       addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
                                }
                                break;
                        }
                        default:
                                ASSERT(0);
                }
+               if(isInRange){
 #ifdef TRACE_DEBUG
-               model_print("added clause in function table enumeration ...\n");
-               printCNF(clause);
-               model_print("\n");
+                       model_print("added clause in function table enumeration ...\n");
+                       printCNF(clause);
+                       model_print("\n");
 #endif
-               pushVectorEdge(clauses, clause);
-
+                       pushVectorEdge(clauses, clause);
+               }
                
                notfinished=false;
                for(uint i=0;i<numDomains; i++) {

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 36c16f2729a7a43bca7e76ad942d3645c07634b1..e8a7f3d6b388c9dd359e1bfc489dcd66506e3c06 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -58,7 +58,6 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        VectorInt* mems = order->set->members;
        HashTableOrderPair* table = order->orderPairTable;
        uint size = getSizeVectorInt(mems);
-       uint csize =0;
        for(uint i=0; i<size; i++){
                uint64_t valueI = getVectorInt(mems, i);
                for(uint j=i+1; j<size;j++){

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a9c89fe6c781410b3c7f22702613768a05ecc8c5..7736f941a0acb29fdb53834fefe609d9174aa02d 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -8,18 +8,19 @@
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
-       for(uint i=elemEnc->numVars-1;i>=0;i--) {
+       for(int i=elemEnc->numVars-1;i>=0;i--) {
                index=index<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
+       model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
        ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
        return elemEnc->encodingArray[index];
 }
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint64_t value=0;
-       for(uint i=elemEnc->numVars-1;i>=0;i--) {
+       for(int i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;

diff --git a/src/Test/tablefuncencodetest.c b/src/Test/tablefuncencodetest.c
index 13337ea84a53088b727b435048d2b24a869a3164..12a589e083f651466d089d0e17dd80d840660363 100644 (file)
--- a/src/Test/tablefuncencodetest.c
+++ b/src/Test/tablefuncencodetest.c
@@ -5,10 +5,10 @@
  * e3= f(e1, e2) 
  *     1 5 => 7
  *     2 3 => 5
- *     1 7 => 1
- *     2 7 => 2
+ *     1 7 => 3
+ *     2 7 => 5
  *     2 5 => 3
- *     1 3 => 4
+ *     1 3 => 5
  * e4 = {6, 10, 19}
  * e4 <= e3
  * Result: e1=1, e2=5, e3=7, e4=6, overflow=0
@@ -36,10 +36,10 @@ int main(int numargs, char ** argv) {
        uint64_t row6[] = {1, 3};
        addTableEntry(solver, t1, row1, 2, 7);
        addTableEntry(solver, t1, row2, 2, 5);
-       addTableEntry(solver, t1, row3, 2, 1);
-       addTableEntry(solver, t1, row4, 2, 2);
+       addTableEntry(solver, t1, row3, 2, 3);
+       addTableEntry(solver, t1, row4, 2, 5);
        addTableEntry(solver, t1, row5, 2, 3);
-       addTableEntry(solver, t1, row6, 2, 4);
+       addTableEntry(solver, t1, row6, 2, 5);
        Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);    
        Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow);