Make naive encoding follow AST Tree

[satune.git] / src / Encoders / naiveencoder.c

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 4f9db3ef92a449a5fdd6c18819ce60d620cc5dee..c3dc425dca69370008959228151f8a1cdd513490 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -13,63 +13,79 @@
 #include "order.h"
 #include <strings.h>
 
+void naiveEncodingDecision(CSolver* This) {
+       for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
+               naiveEncodingConstraint(getVectorBoolean(This->constraints, i));
+       }
+}
 
-void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
-       uint size = getSizeVectorElement(csolver->allElements);
-       for(uint i=0; i<size; i++){
-               Element* element = getVectorElement(csolver->allElements, i);
-               switch(GETELEMENTTYPE(element)){
-                       case ELEMSET:
-                               setElementEncodingType(getElementEncoding(element), BINARYINDEX);
-                               //FIXME:Should be moved to SATEncoder
-                               baseBinaryIndexElementAssign(getElementEncoding(element));
-                               generateElementEncodingVariables(encoder,getElementEncoding(element));
-                               //
-                               break;
-                       case ELEMFUNCRETURN: 
-                               setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
-                                       ENUMERATEIMPLICATIONS);
-                               break;
-                       default:
-                               ASSERT(0);
-               }
+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;
+       
+       setElementEncodingType(encoding, BINARYINDEX);
+       baseBinaryIndexElementAssign(encoding);
        
-       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;
-               } 
+       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);
        }
 }
 
 void baseBinaryIndexElementAssign(ElementEncoding *This) {
        Element * element=This->element;
-       ASSERT(element->type == ELEMSET);
-       Set * set= ((ElementSet*)element)->set;
+       Set * set= getElementSet(element);
        ASSERT(set->isRange==false);
        uint size=getSizeVectorInt(set->members);
        uint encSize=NEXTPOW2(size);
        allocEncodingArrayElement(This, encSize);
        allocInUseArrayElement(This, encSize);
-
        for(uint i=0;i<size;i++) {
                This->encodingArray[i]=getVectorInt(set->members, i);
                setInUseElement(This, i);
        }
-       This->numVars = NUMBITS(size-1);
-       This->variables = ourmalloc(sizeof(Constraint*)* This->numVars);
-       
-       
 }
-
-