Testing one-hot encoding + fixing bugs ...

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index 20241b46f35863767528abe089c38ba8dcd0d52c..ab597a6a0d032152e64781ca9ad0e896ce7a2f36 100644 (file)
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -3,6 +3,7 @@
 #include "common.h"
 #include "ops.h"
 #include "element.h"
+#include "set.h"
 
 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) { 
        switch(getElementEncoding(elem)->type){
@@ -39,14 +40,14 @@ Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint
 
 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {
        ASTNodeType type = GETELEMENTTYPE(elem);
-       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST);
        ElementEncoding* elemEnc = getElementEncoding(elem);
        for(uint i=0; i<elemEnc->encArraySize; i++){
                if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
-                       return elemEnc->variables[i];
+                       return (elemEnc->numVars == 0) ? E_True: elemEnc->variables[i];
                }
        }
-       return E_BOGUS;
+       return E_False;
 }
 
 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
@@ -100,8 +101,8 @@ void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 }
 
-void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
-       allocElementConstraintVariables(encoding, encoding->encArraySize);
+void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) { 
+       allocElementConstraintVariables(encoding, getSetSize( getElementSet(encoding->element)));
        getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);        
        for(uint i=0;i<encoding->numVars;i++) {
                for(uint j=i+1;j<encoding->numVars;j++) {

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a872b62dd4992a6ca034e7bf68a0b08781a5fd08..a9c89fe6c781410b3c7f22702613768a05ecc8c5 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -8,7 +8,7 @@
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=elemEnc->numVars-1;i>=0;i--) {
                index=index<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
@@ -19,7 +19,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint64_t value=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
@@ -36,7 +36,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding*
 
 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
-       for(int i=elemEnc->numVars-1;i>=0;i--) {
+       for(uint i=0; i< elemEnc->numVars; i++) {
                if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
@@ -61,11 +61,9 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
                return getSetElement(getElementSet(element), 0);
        switch(elemEnc->type){
                case ONEHOT:
-                       getElementValueOneHotSATTranslator(This, elemEnc);
-                       break;
+                       return getElementValueOneHotSATTranslator(This, elemEnc);
                case UNARY:
-                       getElementValueUnarySATTranslator(This, elemEnc);
-                       break;
+                       return getElementValueUnarySATTranslator(This, elemEnc);
                case BINARYINDEX:
                        return getElementValueBinaryIndexSATTranslator(This, elemEnc);
                case ONEHOTBINARY:

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index ef0e29e3b2b93c1fd2030b6c4a65871d79f9855c..d5b88d7027429ef493fa20bfef37621a31c8cb8d 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -61,8 +61,8 @@ void naiveEncodingPredicate(BooleanPredicate * This) {
 void naiveEncodingElement(Element * This) {
        ElementEncoding * encoding = getElementEncoding(This);
        if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, BINARYINDEX);
-               baseBinaryIndexElementAssign(encoding);
+               setElementEncodingType(encoding, ONEHOT);
+               encodingArrayInitialization(encoding);
        }
        
        if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
@@ -77,7 +77,7 @@ void naiveEncodingElement(Element * This) {
        }
 }
 
-void baseBinaryIndexElementAssign(ElementEncoding *This) {
+void encodingArrayInitialization(ElementEncoding *This) {
        Element * element=This->element;
        Set * set= getElementSet(element);
        ASSERT(set->isRange==false);

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 3d92e1203ebfff677312b3d7bf1156d23d6fb0fd..20f2943ce26a093dd3e22199ad624566f8fb5d73 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -14,6 +14,6 @@ void naiveEncodingConstraint(Boolean * This);
 void naiveEncodingLogicOp(BooleanLogic * This);
 void naiveEncodingPredicate(BooleanPredicate * This);
 void naiveEncodingElement(Element * This);
-void baseBinaryIndexElementAssign(ElementEncoding *This);
+void encodingArrayInitialization(ElementEncoding *This);
 
 #endif

diff --git a/src/Test/tablefuncencodetest.c b/src/Test/tablefuncencodetest.c
index 9d5abeddde1b4bae21c2fb2de0b9338ac50f6a65..13337ea84a53088b727b435048d2b24a869a3164 100644 (file)
--- a/src/Test/tablefuncencodetest.c
+++ b/src/Test/tablefuncencodetest.c
@@ -5,9 +5,13 @@
  * e3= f(e1, e2) 
  *     1 5 => 7
  *     2 3 => 5
+ *     1 7 => 1
+ *     2 7 => 2
+ *     2 5 => 3
+ *     1 3 => 4
  * e4 = {6, 10, 19}
  * e4 <= e3
- * Result: e1=1, e2=5, e4=6, overflow=0
+ * Result: e1=1, e2=5, e3=7, e4=6, overflow=0
  */
 int main(int numargs, char ** argv) {
        CSolver * solver=allocCSolver();
@@ -26,8 +30,16 @@ int main(int numargs, char ** argv) {
        Table* t1 = createTable(solver, d1, 2, s2);
        uint64_t row1[] = {1, 5};
        uint64_t row2[] = {2, 3};
+       uint64_t row3[] = {1, 7};
+       uint64_t row4[] = {2, 7};
+       uint64_t row5[] = {2, 5};
+       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, row5, 2, 3);
+       addTableEntry(solver, t1, row6, 2, 4);
        Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);    
        Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow);
        
@@ -38,8 +50,8 @@ int main(int numargs, char ** argv) {
        addConstraint(solver, pred);
        
        if (startEncoding(solver)==1)
-               printf("e1=%llu e2=%llu e4=%llu overFlow:%d\n", 
-                       getElementValue(solver,e1), getElementValue(solver, e2), 
+               printf("e1=%llu e2=%llu e3=%llu e4=%llu overFlow:%d\n", 
+                       getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e3),
                        getElementValue(solver, e4), getBooleanValue(solver, overflow));
        else
                printf("UNSAT\n");

diff --git a/src/csolver.c b/src/csolver.c
index 78c60831ac83a481c9b5ed5d083ca0d531086f43..d440aadc593c1d8ce9ec0b4e0b846cc6f8d976aa 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -210,6 +210,7 @@ uint64_t getElementValue(CSolver* This, Element* element){
        switch(GETELEMENTTYPE(element)){
                case ELEMSET:
                case ELEMCONST:
+               case ELEMFUNCRETURN:
                        return getElementValueSATTranslator(This, element);
                default:
                        ASSERT(0);