From: bdemsky <bdemsky@uci.edu>
Date: Thu, 29 Jun 2017 06:46:28 +0000 (-0700)
Subject: Add some comments for Hamed
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8e0ff7564e815489b3fbc3af442c098926ed3a51;p=satune.git

Add some comments for Hamed
---

diff --git a/src/AST/element.c b/src/AST/element.c
index f5cd301..8379983 100644
--- 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 94d19c8..24859be 100644
--- 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));