Fixing some bugs, using InUseArray, and completing table-function encoding

diff --git a/src/AST/element.c b/src/AST/element.c
index 5b9d847fddcd9512140d70dc810fdb40a12e89f9..57f7b6a5b27abf9ec8cb661295451c272bad6663 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -2,6 +2,8 @@
 #include "structs.h"
 #include "set.h"
 #include "constraint.h"
+#include "function.h"
+#include "table.h"
 
 Element *allocElementSet(Set * s) {
        ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet));
@@ -26,38 +28,48 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
        return &tmp->base;
 }
 
-uint getElementSize(Element* This){
+Set* getElementSet(Element* This){
        switch(GETELEMENTTYPE(This)){
                case ELEMSET:
-                       return getSetSize( ((ElementSet*)This)->set );
-                       break;
+                       return ((ElementSet*)This)->set;
                case ELEMFUNCRETURN:
-                       ASSERT(0);
+                       ;//Nope is needed for label assignment. i.e. next instruction isn't 
+                       Function* func = ((ElementFunction*)This)->function;
+                       switch(GETFUNCTIONTYPE(func)){
+                               case TABLEFUNC:
+                                       return ((FunctionTable*)func)->table->range;
+                               case OPERATORFUNC:
+                                       return ((FunctionOperator*)func)->range;
+                               default:
+                                       ASSERT(0);
+                       }
                default:
                        ASSERT(0);
        }
-       return -1;
+       ASSERT(0);
+       return NULL;
 }
 
+uint getElemEncodingInUseVarsSize(ElementEncoding* This){
+       uint size=0;
+       for(uint i=0; i<This->encArraySize; i++){
+               if(isinUseElement(This, i)){
+                       size++;
+               }
+       }
+       return size;
+}
 
-Constraint * getElementValueConstraint(Element* This, uint64_t value) {
-       switch(GETELEMENTTYPE(This)){
-               case ELEMSET:
-                       ; //Statement is needed for a label and This is a NOPE
-                       uint size = getSetSize(((ElementSet*)This)->set);
-                       //FIXME
-                       for(uint i=0; i<size; i++){
-                               if( getElementEncoding(This)->encodingArray[i]==value){
-                                       return generateBinaryConstraint(getElementEncoding(This)->numVars,
-                                               getElementEncoding(This)->variables, i);
-                               }
-                       }
-                       break;
-               case ELEMFUNCRETURN:
-                       ASSERT(0);
-                       break;
-               default:
-                       ASSERT(0);
+
+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;

diff --git a/src/AST/element.h b/src/AST/element.h
index 646276f4ffeca758776296852c2f257ff168228e..8fab12cc9f573666fb94824df962748d3479836f 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -9,8 +9,7 @@
 #include "boolean.h"
 
 #define GETELEMENTTYPE(o) GETASTNODETYPE(o)
-#define GETELEMENTPARENTS(o) (&((Element*)o)->parents)
-               
+#define GETELEMENTPARENTS(o) (&((Element*)o)->parents)         
 struct Element {
        ASTNode base;
        VectorASTNode parents;
@@ -34,7 +33,7 @@ struct ElementFunction {
 Element * allocElementSet(Set *s);
 Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus);
 void deleteElement(Element *This);
-
+Set* getElementSet(Element* This);
 static inline ElementEncoding* getElementEncoding(Element* This){
        switch(GETELEMENTTYPE(This)){
                case ELEMSET:
@@ -52,6 +51,6 @@ static inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func
        return &func->functionencoding;
 }
 
-uint getElementSize(Element* This);
-Constraint * getElementValueConstraint(Element* This, uint64_t value);
+uint getElemEncodingInUseVarsSize(ElementEncoding* This);
+Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 #endif

diff --git a/src/AST/order.c b/src/AST/order.c
index cbfeac38d3ab0963b1a427263d93e0fa064cf4b9..08508b9e7be6287de8b71c21b87ed8fa9c960628 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -14,7 +14,7 @@ Order* allocOrder(OrderType type, Set * set){
 }
 
 void addOrderConstraint(Order* order, BooleanOrder* constraint){
-       pushVectorBoolean( &order->constraints, (Boolean) constraint);
+       pushVectorBoolean( &order->constraints, (Boolean*) constraint);
 }
 
 void setOrderEncodingType(Order* order, OrderEncodingType type){

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index fa385aed0222d64fe9a96460bd6e01bd29b624bc..6b3b0d5e4f6c9f7ff7f462fbd137b5bd2aa68626 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -23,7 +23,15 @@ void deleteSATEncoder(SATEncoder *This) {
        ourfree(This);
 }
 
-void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
+void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
+       uint size = getSizeVectorElement(csolver->allElements);
+       for(uint i=0; i<size; i++){
+               Element* element = getVectorElement(csolver->allElements, i);
+               generateElementEncodingVariables(This,getElementEncoding(element));
+       }
+}
+
+void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
        VectorBoolean *constraints=csolver->constraints;
        uint size=getSizeVectorBoolean(constraints);
        for(uint i=0;i<size;i++) {
@@ -143,13 +151,17 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
                case ENUMERATEIMPLICATIONS:
                        return encodeEnumTableElemFunctionSATEncoder(encoder, This);
                        break;
+               case CIRCUIT:
+                       ASSERT(0);
+                       break;
                default:
                        ASSERT(0);
        }
        return NULL;
 }
 
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This){
+Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+       //FIXME: for now it just adds/substracts inputs exhustively
        return NULL;
 }
 
@@ -165,10 +177,10 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
                Element* el= getArrayElement(elements, i);
                Constraint* carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                        carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+                        carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[j]);
                }
                Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
-                       getElementValueConstraint((Element*)This, entry->output));
+                       getElementValueBinaryIndexConstraint((Element*)This, entry->output));
                constraints[i]=row;
        }
        Constraint* result = allocArrayConstraint(OR, size, constraints);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 79e2c525b73cd3f92785bcff45415951e73fccd3..937db2bce7533d240a85d03a08a00e01aff65f3f 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -19,7 +19,8 @@ static inline VectorConstraint* getSATEncoderAllConstraints(SATEncoder* ne){
 }
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
-void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
+void initializeConstraintVars(CSolver* csolver, SATEncoder* This);
+void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
 Constraint * getNewVarSATEncoder(SATEncoder *This);
 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index 7b3ebddf6f1c38c4fb6113440cdf583b990f38b3..f0510d6e50d39fc9eb0cddc297300003af6835f2 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -11,6 +11,7 @@ void initElementEncoding(ElementEncoding * This, Element *element) {
        This->encodingArray=NULL;
        This->inUseArray=NULL;
        This->numVars=0;
+       This->encArraySize=0;
 }
 
 void deleteElementEncoding(ElementEncoding *This) {
@@ -24,6 +25,7 @@ void deleteElementEncoding(ElementEncoding *This) {
 
 void allocEncodingArrayElement(ElementEncoding *This, uint size) {
        This->encodingArray=ourcalloc(1, sizeof(uint64_t)*size);
+       This->encArraySize=size;
 }
 
 void allocInUseArrayElement(ElementEncoding *This, uint size) {
@@ -41,7 +43,7 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
 
 void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){
        ASSERT(This->type==BINARYINDEX);
-       uint size = getElementSize(This->element);
+       uint size = getElemEncodingInUseVarsSize(This);
        allocElementConstraintVariables(This, NUMBITS(size-1));
        getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables);
 }

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index f04ba7e8726ccf3af3b1731cf097dd4507cab563..15025cbff3222a3cf2abe3145a52cb7fca098864 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -15,6 +15,7 @@ struct ElementEncoding {
        Constraint ** variables;/* List Variables Used To Encode Element */
        uint64_t * encodingArray;       /* List the Variables in the appropriate order */
        uint64_t * inUseArray;/* Bitmap to track variables in use */
+       uint encArraySize;
        uint numVars;   /* Number of variables */
 };
 
@@ -24,7 +25,8 @@ void deleteElementEncoding(ElementEncoding *This);
 void baseBinaryIndexElementAssign(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
-
+//FIXME:
+//uint addNewVariableToEncodingArray(ElementEncoding* This, uint64_t);
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
        return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
 }

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 4f9db3ef92a449a5fdd6c18819ce60d620cc5dee..17d19467baff447127160aaab420995502bdbf33 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -14,17 +14,17 @@
 #include <strings.h>
 
 
-void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
+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));
                switch(GETELEMENTTYPE(element)){
                        case ELEMSET:
-                               setElementEncodingType(getElementEncoding(element), BINARYINDEX);
-                               //FIXME:Should be moved to SATEncoder
-                               baseBinaryIndexElementAssign(getElementEncoding(element));
-                               generateElementEncodingVariables(encoder,getElementEncoding(element));
-                               //
+                               //FIXME: Move next line to satEncoderInitializer!
+//                             generateElementEncodingVariables(encoder,getElementEncoding(element));
                                break;
                        case ELEMFUNCRETURN: 
                                setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
@@ -54,22 +54,16 @@ void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
 
 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);
-       
-       
 }
 
 

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 800860c2e4e379b260e9b85d1429cf25fdd0dcfe..182e3da1027742255ebfd91755c77c51a75ff9bd 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -11,7 +11,7 @@
  * @param csolver
  * @param encoder
  */
-void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder);
+void naiveEncodingDecision(CSolver* csolver);
 void baseBinaryIndexElementAssign(ElementEncoding *This);
 
 #endif

diff --git a/src/csolver.c b/src/csolver.c
index 5f330fd6112c70074522c17ac116739bf35746d6..7ffd1eca4ab7e7b59282826ad4293caf271b0135 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -7,6 +7,7 @@
 #include "order.h"
 #include "table.h"
 #include "function.h"
+#include "satencoder.h"
 
 CSolver * allocCSolver() {
        CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver));
@@ -169,3 +170,13 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
        pushVectorBoolean(solver->allBooleans,constraint);
        return constraint;
 }
+
+void encode(CSolver* solver){
+       naiveEncodingDecision(solver);
+       SATEncoder* satEncoder = allocSATEncoder();
+       initializeConstraintVars(solver, satEncoder);
+       encodeAllSATEncoder(solver, satEncoder);
+       //For now, let's just delete it, and in future for doing queries 
+       //we may need it.
+       deleteSATEncoder(satEncoder);
+}
\ No newline at end of file

diff --git a/src/csolver.h b/src/csolver.h
index 495d3864dca23ebdca90cab1f7eec52f485e3fa2..fd807aef3fe1204b96efb11bd798479342b22596 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -111,4 +111,7 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 
 /** This function instantiates a boolean on two items in an order. */
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
+
+/** When everything is done, the client calls this function and then csolver starts to encode*/
+void encode(CSolver*);
 #endif