Add some comments for Hamed

diff --git a/src/AST/element.c b/src/AST/element.c
index f5cd301fd7df13fc493cd6ec34a12edcaaf6a392..8379983390ced6078568f48c60cb0e3f0856dd73 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -50,6 +50,11 @@ 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);

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 94d19c811e946c9fe69eabf2a585c29009c83eac..24859bee2adc4439e0ca40676da73898f03f3b5d 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -22,6 +22,13 @@ void deleteSATEncoder(SATEncoder *This) {
 }
 
 void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
+       /** We really should not walk the free list to generate constraint
+                       variables...walk the constraint tree instead.  Or even better
+                       yet, just do this as you need to during the encodeAllSATEncoder
+                       walk.  */
+
+       FIXME!!!!(); // Make sure Hamed sees comment above
+
        uint size = getSizeVectorElement(csolver->allElements);
        for(uint i=0; i<size; i++){
                Element* element = getVectorElement(csolver->allElements, i);
@@ -174,7 +181,10 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
                Element* el= getArrayElement(elements, i);
                Constraint* carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                        carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[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]);
                }
                Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
                        getElementValueBinaryIndexConstraint((Element*)This, entry->output));