Make naive encoding follow AST Tree

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index af9696f691e06ead7be9555bfce0e0e6bb3c95e8..385f5c27d1fe66a4408987cc13a1995f2479119b 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -21,6 +21,7 @@ struct ElementEncoding {
 };
 
 void initElementEncoding(ElementEncoding *This, Element *element);
+static inline ElementEncodingType getElementEncodingType(ElementEncoding * This) {return This->type;}
 void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);

diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h
index 41d99761e6958309e66f946e1e428c2e89639cbb..fa8729e086ef1ebde07ef1aaa6e088f020401cc0 100644 (file)
--- a/src/Encoders/functionencoding.h
+++ b/src/Encoders/functionencoding.h
@@ -24,6 +24,7 @@ struct FunctionEncoding {
 void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
 void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
 void setFunctionEncodingType(FunctionEncoding* encoding, FunctionEncodingType type);
+static inline FunctionEncodingType getFunctionEncodingType(FunctionEncoding* This) {return This->type;}
 void deleteFunctionEncoding(FunctionEncoding *This);
 
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 5560526c2e5f9aec00d64b445722bc44ffca38ef..c3dc425dca69370008959228151f8a1cdd513490 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -13,34 +13,66 @@
 #include "order.h"
 #include <strings.h>
 
-//BRIAN: MAKE FOLLOW TREE STRUCTURE
-void naiveEncodingDecision(CSolver* csolver){
-       uint size = getSizeVectorElement(csolver->allElements);
-       for(uint i=0; i<size; i++){
-               Element* element = getVectorElement(csolver->allElements, i);
-               //Whether it's a ElementFunction or ElementSet we should do the followings:
-               setElementEncodingType(getElementEncoding(element), BINARYINDEX);
-               baseBinaryIndexElementAssign(getElementEncoding(element));
-               if(GETELEMENTTYPE(element) == ELEMFUNCRETURN){
-                       setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
-                               ENUMERATEIMPLICATIONS);
-               }
+void naiveEncodingDecision(CSolver* This) {
+       for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
+               naiveEncodingConstraint(getVectorBoolean(This->constraints, i));
+       }
+}
+
+void naiveEncodingConstraint(Boolean * This) {
+       switch(GETBOOLEANTYPE(This)) {
+       case BOOLEANVAR: {
+               return;
+       }
+       case ORDERCONST: {
+               setOrderEncodingType( ((BooleanOrder*)This)->order, PAIRWISE );
+               return;
        }
+       case LOGICOP: {
+               naiveEncodingLogicOp((BooleanLogic *) This);
+       }
+       case PREDICATEOP: {
+               naiveEncodingPredicate((BooleanPredicate *) This);
+               return;
+       }
+       default:
+               ASSERT(0);
+       }
+}
+
+void naiveEncodingLogicOp(BooleanLogic * This) {
+       for(uint i=0; i < getSizeArrayBoolean(&This->inputs); i++) {
+               naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
+       }
+}
+
+void naiveEncodingPredicate(BooleanPredicate * This) {
+       FunctionEncoding * encoding = getPredicateFunctionEncoding(This);
+       if (getFunctionEncodingType(encoding) != FUNC_UNASSIGNED)
+               return;
+
+       setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
+       for(uint i=0; i < getSizeArrayElement(&This->inputs); i++) {
+               Element * element=getArrayElement(&This->inputs, i);
+               naiveEncodingElement(element);
+       }
+}
+
+void naiveEncodingElement(Element * This) {
+       ElementEncoding * encoding = getElementEncoding(This);
+       if (getElementEncodingType(encoding) != ELEM_UNASSIGNED)
+               return;
        
-       size = getSizeVectorBoolean(csolver->allBooleans);
-       for(uint i=0; i<size; i++){
-               Boolean* boolean = getVectorBoolean(csolver->allBooleans, i);
-               switch(GETBOOLEANTYPE(boolean)){
-                       case PREDICATEOP:
-                               setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean),
-                                       ENUMERATEIMPLICATIONS);
-                               break;
-                       case ORDERCONST:
-                               setOrderEncodingType( ((BooleanOrder*)boolean)->order, PAIRWISE );
-                               break;
-                       default:
-                               continue;
-               } 
+       setElementEncodingType(encoding, BINARYINDEX);
+       baseBinaryIndexElementAssign(encoding);
+       
+       if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
+               ElementFunction *function=(ElementFunction *) This;
+               for(uint i=0; i < getSizeArrayElement(&function->inputs); i++) {
+                       Element * element=getArrayElement(&function->inputs, i);
+                       naiveEncodingElement(element);
+               }
+               setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
        }
 }
 

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 2b9fb87516c302ea1214f1c2a8958dea5a4e7ce8..3d92e1203ebfff677312b3d7bf1156d23d6fb0fd 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -8,7 +8,12 @@
  * @param csolver
  * @param encoder
  */
+
 void naiveEncodingDecision(CSolver* csolver);
+void naiveEncodingConstraint(Boolean * This);
+void naiveEncodingLogicOp(BooleanLogic * This);
+void naiveEncodingPredicate(BooleanPredicate * This);
+void naiveEncodingElement(Element * This);
 void baseBinaryIndexElementAssign(ElementEncoding *This);
 
 #endif