getting two of FIXMEs fixed

diff --git a/src/AST/element.c b/src/AST/element.c
index 8379983390ced6078568f48c60cb0e3f0856dd73..9fc426c1fb686f544f7d20608b258ac8becad41c 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -33,7 +33,7 @@ Set* getElementSet(Element* This){
                case ELEMSET:
                        return ((ElementSet*)This)->set;
                case ELEMFUNCRETURN:
-                       ;//Nope is needed for label assignment. i.e. next instruction isn't 
+                       ;//Nope is needed for label assignment. i.e. next instruction isn't a statement 
                        Function* func = ((ElementFunction*)This)->function;
                        switch(GETFUNCTIONTYPE(func)){
                                case TABLEFUNC:
@@ -50,25 +50,6 @@ Set* getElementSet(Element* This){
        return NULL;
 }
 
-FIXME()!!!!
-
-/** This function belongs in the backend...Elements should not touch
-               binary constraints nor should they touch their encoders... */
-
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
-       ASTNodeType type = GETELEMENTTYPE(This);
-       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
-       ElementEncoding* elemEnc = getElementEncoding(This);
-       for(uint i=0; i<elemEnc->encArraySize; i++){
-               if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
-                       return generateBinaryConstraint(elemEnc->numVars,
-                               elemEnc->variables, i);
-               }
-       }
-       ASSERT(0);
-       return NULL;
-}
-
 void deleteElement(Element *This) {
        switch(GETELEMENTTYPE(This)) {
        case ELEMFUNCRETURN: {

diff --git a/src/AST/element.h b/src/AST/element.h
index 7e4db2880de743381ad9aab76925064f4d72af32..509ee8c3d34566c21faf9f4e8d78d2fca84f6e4d 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -51,5 +51,4 @@ static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func
        return &func->functionencoding;
 }
 
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 #endif

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 24859bee2adc4439e0ca40676da73898f03f3b5d..28dd6af00f65cbd200b61e2fa6530a29eb6bf39a 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -27,7 +27,7 @@ void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
                        yet, just do this as you need to during the encodeAllSATEncoder
                        walk.  */
 
-       FIXME!!!!(); // Make sure Hamed sees comment above
+//     FIXME!!!!(); // Make sure Hamed sees comment above
 
        uint size = getSizeVectorElement(csolver->allElements);
        for(uint i=0; i<size; i++){
@@ -36,6 +36,44 @@ void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
        }
 }
 
+
+Constraint * getElementValueConstraint(Element* This, uint64_t value) {
+       switch(getElementEncoding(This)->type){
+               case ONEHOT:
+                       ASSERT(0);
+                       break;
+               case UNARY:
+                       ASSERT(0);
+                       break;
+               case BINARYINDEX:
+                       ASSERT(0);
+                       break;
+               case ONEHOTBINARY:
+                       return getElementValueBinaryIndexConstraint(This, value);
+                       break;
+               case BINARYVAL:
+                       ASSERT(0);
+                       break;
+               default:
+                       ASSERT(0);
+                       break;
+       }
+       return NULL;
+}
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
+       ASTNodeType type = GETELEMENTTYPE(This);
+       ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
+       ElementEncoding* elemEnc = getElementEncoding(This);
+       for(uint i=0; i<elemEnc->encArraySize; i++){
+               if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
+                       return generateBinaryConstraint(elemEnc->numVars,
+                               elemEnc->variables, i);
+               }
+       }
+       ASSERT(0);
+       return NULL;
+}
+
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        VectorBoolean *constraints=csolver->constraints;
        uint size=getSizeVectorBoolean(constraints);
@@ -181,10 +219,7 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
                Element* el= getArrayElement(elements, i);
                Constraint* carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                       FIXME!!!!();
-                       //This next line should not assume a particular encoding type for the element...  just a generic element encoding function that should choose the appropriate encoding...
-                       
-                       carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[j]);
+                       carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
                }
                Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
                        getElementValueBinaryIndexConstraint((Element*)This, entry->output));

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index b711457687abca5dc0ac9738cb2ad5458bfdb543..2a3901db9bceee5f0364c89cc7fa683abb48b4e7 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -19,6 +19,8 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
+Constraint * getElementValueConstraint(Element* This, uint64_t value);
 
 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);