From 99ace3f73ea93950e8a8a38c5aa086f1b535cf48 Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 28 Jun 2017 17:44:32 -0700 Subject: [PATCH] Fixing some bugs, using InUseArray, and completing table-function encoding --- src/AST/element.c | 58 ++++++++++++++++++++-------------- src/AST/element.h | 9 +++--- src/AST/order.c | 2 +- src/Backend/satencoder.c | 20 +++++++++--- src/Backend/satencoder.h | 3 +- src/Encoders/elementencoding.c | 4 ++- src/Encoders/elementencoding.h | 4 ++- src/Encoders/naiveencoder.c | 20 ++++-------- src/Encoders/naiveencoder.h | 2 +- src/csolver.c | 11 +++++++ src/csolver.h | 3 ++ 11 files changed, 86 insertions(+), 50 deletions(-) diff --git a/src/AST/element.c b/src/AST/element.c index 5b9d847..57f7b6a 100644 --- 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; iencArraySize; 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; iencodingArray[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; iencArraySize; 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 646276f..8fab12c 100644 --- 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 cbfeac3..08508b9 100644 --- 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 fa385ae..6b3b0d5 100644 --- 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; iallElements, i); + generateElementEncodingVariables(This,getElementEncoding(element)); + } +} + +void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) { VectorBoolean *constraints=csolver->constraints; uint size=getSizeVectorBoolean(constraints); for(uint i=0;iinputs[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 79e2c52..937db2b 100644 --- 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 7b3ebdd..f0510d6 100644 --- 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 f04ba7e..15025cb 100644 --- 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 4f9db3e..17d1946 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -14,17 +14,17 @@ #include -void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){ +void naiveEncodingDecision(CSolver* csolver){ uint size = getSizeVectorElement(csolver->allElements); for(uint i=0; iallElements, 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;iencodingArray[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 800860c..182e3da 100644 --- 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 5f330fd..7ffd1ec 100644 --- 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 495d386..fd807ae 100644 --- 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 -- 2.34.1