From 73415104c9001d8154b226d320c5963d1364b858 Mon Sep 17 00:00:00 2001 From: Hamed Date: Mon, 26 Jun 2017 19:16:29 -0700 Subject: [PATCH] Binary encoding for ElementSet and table-based ElementFunction --- src/AST/element.c | 48 ++++++++++++++++++ src/AST/element.h | 15 +++++- src/AST/set.c | 8 +++ src/AST/set.h | 1 + src/AST/table.c | 19 +++---- src/AST/table.h | 6 +-- src/Backend/constraint.c | 10 ---- src/Backend/constraint.h | 2 +- src/Encoders/elementencoding.c | 27 ++++++++++ src/Encoders/elementencoding.h | 5 ++ src/Encoders/naiveencoder.c | 90 +++++++++++++++++++++++++--------- src/Encoders/naiveencoder.h | 27 +++++++--- src/classlist.h | 2 + src/common.h | 1 + src/csolver.c | 2 +- src/csolver.h | 2 +- 16 files changed, 210 insertions(+), 55 deletions(-) diff --git a/src/AST/element.c b/src/AST/element.c index a94db4b..8711529 100644 --- a/src/AST/element.c +++ b/src/AST/element.c @@ -1,5 +1,7 @@ #include "element.h" #include "structs.h" +#include "set.h" +#include "constraint.h" Element *allocElementSet(Set * s) { ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet)); @@ -24,6 +26,52 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr return &tmp->base; } +uint getElementSize(Element* This){ + switch(GETELEMENTTYPE(This)){ + case ELEMSET: + return getSetSize( ((ElementSet*)This)->set ); + break; + case ELEMFUNCRETURN: + ASSERT(0); + default: + ASSERT(0); + } + return -1; +} + + +Constraint * getElementValueConstraint(Element* This, uint64_t value) { + switch(GETELEMENTTYPE(This)){ + case ELEMSET: + ; //Statement is needed for a label and This is a NOPE + ElementSet* elemSet= ((ElementSet*)This); + uint size = getSetSize(elemSet->set); + for(uint i=0; iencodingArray[i]==value){ + return generateBinaryConstraint(GETELEMENTENCODING(elemSet)->numVars, + GETELEMENTENCODING(elemSet)->variables, i); + } + } + break; + case ELEMFUNCRETURN: + break; + default: + ASSERT(0); + } + ASSERT(0); + return NULL; +} + +Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) { + Constraint *carray[numvars]; + for(uint j=0;j>1; + } + + return allocArrayConstraint(AND, numvars, carray); +} + void deleteElement(Element *This) { switch(GETELEMENTTYPE(This)) { case ELEMFUNCRETURN: { diff --git a/src/AST/element.h b/src/AST/element.h index b5bc9c1..3a71686 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -6,10 +6,20 @@ #include "astnode.h" #include "functionencoding.h" #include "elementencoding.h" +#include "boolean.h" #define GETELEMENTTYPE(o) GETASTNODETYPE(o) #define GETELEMENTPARENTS(o) (&((Element*)o)->parents) - +#define GETELEMENTENCODING(e) (GETELEMENTTYPE(e)==ELEMSET? \ + &((ElementSet*)e)->encoding: \ + GETELEMENTTYPE(e)==ELEMFUNCRETURN? \ + &((ElementFunction*)e)->domainencoding: NULL) +// Should be called on the element or boolean +#define GETFUNCTIONENCODING(f) (GETASTNODETYPE(f) == ELEMFUNCRETURN? \ + &((ElementFunction*)f)->functionencoding: \ + GETASTNODETYPE(f) == PREDICATEOP? \ + &((BooleanPredicate*)f)->encoding: NULL) + struct Element { ASTNode base; VectorASTNode parents; @@ -33,4 +43,7 @@ struct ElementFunction { Element * allocElementSet(Set *s); Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus); void deleteElement(Element *This); + +uint getElementSize(Element* This); +Constraint * getElementValueConstraint(Element* This, uint64_t value); #endif diff --git a/src/AST/set.c b/src/AST/set.c index fc056a2..afe26ec 100644 --- a/src/AST/set.c +++ b/src/AST/set.c @@ -21,6 +21,14 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { return tmp; } +uint getSetSize(Set* set){ + if(set->isRange){ + return set->high- set->low+1; + }else{ + return getSizeVectorInt(set->members); + } +} + void deleteSet(Set * set) { if (!set->isRange) deleteVectorInt(set->members); diff --git a/src/AST/set.h b/src/AST/set.h index 92315e2..55fb57c 100644 --- a/src/AST/set.h +++ b/src/AST/set.h @@ -23,6 +23,7 @@ struct Set { Set *allocSet(VarType t, uint64_t * elements, uint num); Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); +uint getSetSize(Set* set); void deleteSet(Set *set); #endif/* SET_H */ diff --git a/src/AST/table.c b/src/AST/table.c index ea4b6d2..a8af588 100644 --- a/src/AST/table.c +++ b/src/AST/table.c @@ -3,23 +3,24 @@ #include "structs.h" #include "tableentry.h" #include "set.h" +#include "mutableset.h" -Table * allocTable(Set **domains, uint numDomain, Set * range){ - Table* table = (Table*) ourmalloc(sizeof(Table)); - allocInlineArrayInitSet(&table->domains, domains, numDomain); - allocInlineDefVectorTableEntry(&table->entries); - table->range =range; - return table; +Table * allocTable(Element **domains, uint numDomain, Element * range){ + Table* table = (Table*) ourmalloc(sizeof(Table)); + allocInlineArrayInitElement(&table->domains, domains, numDomain); + allocInlineDefVectorTableEntry(&table->entries); + table->range =range; + return table; } void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result){ - ASSERT(getSizeVectorSet( table->domains) == inputSize); - pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result)); + ASSERT(getSizeArrayElement( &table->domains) == inputSize); + pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result)); } void deleteTable(Table* table){ - deleteInlineArraySet(&table->domains); + deleteInlineArrayElement(&table->domains); uint size = getSizeVectorTableEntry(&table->entries); for(uint i=0; ientries, i)); diff --git a/src/AST/table.h b/src/AST/table.h index 90f5001..fa83b06 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -5,12 +5,12 @@ #include "structs.h" struct Table { - ArraySet domains; - Set * range; + ArrayElement domains; + Element * range; VectorTableEntry entries; }; -Table * allocTable(Set **domains, uint numDomain, Set * range); +Table * allocTable(Element **domains, uint numDomain, Element * range); void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result); void deleteTable(Table* table); #endif diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c index 1aa3d3c..27db299 100644 --- a/src/Backend/constraint.c +++ b/src/Backend/constraint.c @@ -186,16 +186,6 @@ Constraint * cloneConstraint(Constraint * This) { } } -Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) { - Constraint *carray[numvars]; - for(uint j=0;j>1; - } - - return allocArrayConstraint(AND, numvars, carray); -} - /** Generates a constraint to ensure that all encodings are less than value */ Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) { Constraint *orarray[numvars]; diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index a83a39b..e1b21d3 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -47,7 +47,7 @@ Constraint *negateConstraint(Constraint * c); extern Constraint ctrue; extern Constraint cfalse; -Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value); +Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value); Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c index 4a4bc89..02a9f7f 100644 --- a/src/Encoders/elementencoding.c +++ b/src/Encoders/elementencoding.c @@ -1,4 +1,7 @@ #include "elementencoding.h" +#include "common.h" +#include "naiveencoder.h" +#include "element.h" void initElementEncoding(ElementEncoding * This, Element *element) { This->element=element; @@ -26,6 +29,30 @@ void allocInUseArrayElement(ElementEncoding *This, uint size) { This->inUseArray=ourcalloc(1, size >> 6); } +void allocElementConstraintVariables(ElementEncoding* This, uint numVars){ + This->numVars = numVars; + This->variables = ourmalloc(sizeof(Constraint*) * numVars); +} + void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){ This->type = type; } + +void generateBinaryIndexEncodingVars(NaiveEncoder* encoder, ElementEncoding* This){ + ASSERT(This->type==BINARYINDEX); + uint size = getElementSize(This->element); + allocElementConstraintVariables(This, NUMBITS(size-1)); + getArrayNewVars(encoder, This->numVars, This->variables); +} + +void generateElementEncodingVariables(NaiveEncoder* encoder, ElementEncoding* This){ + ASSERT(This->type!=ELEM_UNASSIGNED); + ASSERT(This->variables==NULL); + switch(This->type){ + case BINARYINDEX: + generateBinaryIndexEncodingVars(encoder, This); + break; + default: + ASSERT(0); + } +} \ No newline at end of file diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index 03040ed..ffdb0d0 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -1,6 +1,7 @@ #ifndef ELEMENTENCODING_H #define ELEMENTENCODING_H #include "classlist.h" +#include "naiveencoder.h" enum ElementEncodingType { ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL @@ -31,4 +32,8 @@ static inline bool isinUseElement(ElementEncoding *This, uint offset) { static inline void setInUseElement(ElementEncoding *This, uint offset) { This->inUseArray[(offset>>6)] |= 1 << (offset & 63); } + +void generateBinaryIndexEncodingVars(NaiveEncoder* encode, ElementEncoding* This); +void generateElementEncodingVariables(NaiveEncoder* encoder, ElementEncoding* This); + #endif diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c index d5ceab6..974772e 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -9,19 +9,30 @@ #include "csolver.h" #include "boolean.h" #include "table.h" +#include "tableentry.h" +#include "constraint.h" #include -void naiveEncodingDecision(CSolver* csolver){ +NaiveEncoder* allocNaiveEncoder(){ + NaiveEncoder* encoder = (NaiveEncoder*) ourmalloc(sizeof(NaiveEncoder)); + allocInlineDefVectorConstraint(GETNAIVEENCODERALLCONSTRAINTS(encoder)); + allocInlineDefVectorConstraint(GETNAIVEENCODERVARS(encoder)); + encoder->varindex=0; + return encoder; +} + +void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){ uint size = getSizeVectorElement(csolver->allElements); for(uint i=0; iallElements, i); switch(GETELEMENTTYPE(element)){ case ELEMSET: - setElementEncodingType(&((ElementSet*)element)->encoding, BINARYINDEX); - baseBinaryIndexElementAssign(&((ElementSet*)element)->encoding); + setElementEncodingType(GETELEMENTENCODING(element), BINARYINDEX); + baseBinaryIndexElementAssign(GETELEMENTENCODING(element)); + generateElementEncodingVariables(encoder,GETELEMENTENCODING(element)); break; case ELEMFUNCRETURN: - setFunctionEncodingType(&((ElementFunction*)element)->functionencoding, ENUMERATEIMPLICATIONS); + setFunctionEncodingType(GETFUNCTIONENCODING(element), ENUMERATEIMPLICATIONS); break; default: ASSERT(0); @@ -33,7 +44,7 @@ void naiveEncodingDecision(CSolver* csolver){ Boolean* predicate = getVectorBoolean(csolver->allBooleans, i); switch(GETBOOLEANTYPE(predicate)){ case PREDICATEOP: - setFunctionEncodingType(&((BooleanPredicate*)predicate)->encoding, ENUMERATEIMPLICATIONS); + setFunctionEncodingType(GETFUNCTIONENCODING(predicate), ENUMERATEIMPLICATIONS); break; default: continue; @@ -41,6 +52,22 @@ void naiveEncodingDecision(CSolver* csolver){ } } + +void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray) { + for(uint i=0;ivarindex); + Constraint* notVar = allocVarConstraint(NOTVAR, encoder->varindex); + setNegConstraint(var, notVar); + setNegConstraint(notVar, var); + pushVectorConstraint(GETNAIVEENCODERVARS(encoder), var); + encoder->varindex++; + return var; +} + void baseBinaryIndexElementAssign(ElementEncoding *This) { Element * element=This->element; ASSERT(element->type == ELEMSET); @@ -55,16 +82,22 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) { This->encodingArray[i]=getVectorInt(set->members, i); setInUseElement(This, i); } + This->numVars = NUMBITS(size-1); + This->variables = ourmalloc(sizeof(Constraint*)* This->numVars); + + } void encode(CSolver* csolver){ + NaiveEncoder* encoder = allocNaiveEncoder(); + naiveEncodingDecision( csolver, encoder); uint size = getSizeVectorElement(csolver->allElements); for(uint i=0; iallElements, i); switch(GETELEMENTTYPE(element)){ case ELEMFUNCRETURN: - naiveEncodeFunctionPredicate(&((ElementFunction*)element)->functionencoding); + naiveEncodeFunctionPredicate(encoder, GETFUNCTIONENCODING(element)); break; default: continue; @@ -76,7 +109,7 @@ void encode(CSolver* csolver){ Boolean* predicate = getVectorBoolean(csolver->allBooleans, i); switch(GETBOOLEANTYPE(predicate)){ case PREDICATEOP: - naiveEncodeFunctionPredicate(&((BooleanPredicate*)predicate)->encoding); + naiveEncodeFunctionPredicate(encoder, GETFUNCTIONENCODING(predicate)); break; default: continue; @@ -84,15 +117,15 @@ void encode(CSolver* csolver){ } } -void naiveEncodeFunctionPredicate(FunctionEncoding *This){ +void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This){ if(This->isFunction) { ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN); switch(This->type){ case ENUMERATEIMPLICATIONS: - naiveEncodeEnumeratedFunction(This); + naiveEncodeEnumeratedFunction(encoder, This); break; case CIRCUIT: - naiveEncodeCircuitFunction(This); + naiveEncodeCircuitFunction(encoder, This); break; default: ASSERT(0); @@ -105,38 +138,49 @@ void naiveEncodeFunctionPredicate(FunctionEncoding *This){ } } - -void naiveEncodeCircuitFunction(FunctionEncoding* This){ - -} - -void naiveEncodeEnumeratedFunction(FunctionEncoding* This){ +void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This){ ElementFunction* ef =(ElementFunction*)This->op.function; - Function * function = ef->function; - switch(GETFUNCTIONTYPE(function)){ + switch(GETFUNCTIONTYPE(ef->function)){ case TABLEFUNC: - naiveEncodeEnumTableFunc(ef); + naiveEncodeEnumTableFunc(encoder, ef); break; case OPERATORFUNC: - naiveEncodeEnumOperatingFunc(ef); + naiveEncodeEnumOperatingFunc(encoder, ef); break; default: ASSERT(0); } } -void naiveEncodeEnumTableFunc(ElementFunction* This){ +void naiveEncodeEnumTableFunc(NaiveEncoder* encoder, ElementFunction* This){ ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC); ArrayElement* elements= &This->inputs; Table* table = ((FunctionTable*) (This->function))->table; uint size = getSizeVectorTableEntry(&table->entries); for(uint i=0; ientries, i); - //FIXME: generate Constraints + uint inputNum =getSizeArrayElement(elements); + Element* el= getArrayElement(elements, i); + Constraint* carray[inputNum]; + for(uint j=0; jinputs[j]); + } + Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), + getElementValueConstraint(table->range, entry->output)); + pushVectorConstraint( GETNAIVEENCODERALLCONSTRAINTS(encoder), row); } } -void naiveEncodeEnumOperatingFunc(ElementFunction* This){ +void naiveEncodeEnumOperatingFunc(NaiveEncoder* encoder, ElementFunction* This){ + +} + + +void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This){ +} + +void deleteNaiveEncoder(NaiveEncoder* encoder){ + deleteVectorArrayConstraint(&encoder->vars); } \ No newline at end of file diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h index c1623eb..d3c409c 100644 --- a/src/Encoders/naiveencoder.h +++ b/src/Encoders/naiveencoder.h @@ -1,15 +1,30 @@ #ifndef NAIVEELEMENTENCODER_H #define NAIVEELEMENTENCODER_H #include "classlist.h" +#include "structs.h" +#define GETNAIVEENCODERVARS(ne) (&((NaiveEncoder*)ne)->vars) +#define GETNAIVEENCODERALLCONSTRAINTS(ne) (&((NaiveEncoder*)ne)->allConstraints) + +struct NaiveEncoder{ + uint varindex; + VectorConstraint vars; + VectorConstraint allConstraints; +}; + +NaiveEncoder* allocNaiveEncoder(); +Constraint* getNewVar(NaiveEncoder* encoder); +void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray); //For now, This function just simply goes through elements/functions and //assigns a predefined Encoding to each of them -void naiveEncodingDecision(CSolver* csolver); +void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder); void encode(CSolver* csolver); void baseBinaryIndexElementAssign(ElementEncoding *This); -void naiveEncodeFunctionPredicate( FunctionEncoding *This); -void naiveEncodeCircuitFunction(FunctionEncoding* This); -void naiveEncodeEnumeratedFunction(FunctionEncoding* This); -void naiveEncodeEnumTableFunc(ElementFunction* This); -void naiveEncodeEnumOperatingFunc(ElementFunction* This); +void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This); +void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This); +void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This); +void naiveEncodeEnumTableFunc(NaiveEncoder* encoder, ElementFunction* This); +void naiveEncodeEnumOperatingFunc(NaiveEncoder* encoder, ElementFunction* This); + +void deleteNaiveEncoder(NaiveEncoder* encoder); #endif diff --git a/src/classlist.h b/src/classlist.h index 3c7d071..a707845 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -82,6 +82,8 @@ typedef struct OrderEncoding OrderEncoding; struct TableEntry; typedef struct TableEntry TableEntry; +struct NaiveEncoder; +typedef struct NaiveEncoder NaiveEncoder; typedef unsigned int uint; typedef uint64_t VarType; #endif diff --git a/src/common.h b/src/common.h index d9e6d43..5d8c389 100644 --- a/src/common.h +++ b/src/common.h @@ -33,6 +33,7 @@ extern int switch_alloc; #define model_print printf #define NEXTPOW2(x) (1<<(sizeof(uint)*8-__builtin_clz(x-1))) +#define NUMBITS(x) ((x==0) ? 0 : 8*sizeof(x)-__builtin_clz(x)) #ifdef CONFIG_DEBUG #define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0) diff --git a/src/csolver.c b/src/csolver.c index 5f330fd..ccb19f0 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -122,7 +122,7 @@ Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, u return predicate; } -Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) { +Table * createTable(CSolver *solver, Element **domains, uint numDomain, Element * range) { Table* table= allocTable(domains,numDomain,range); pushVectorTable(solver->allTables, table); return table; diff --git a/src/csolver.h b/src/csolver.h index 495d386..0bd2088 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -79,7 +79,7 @@ Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, u /** This function creates an empty instance table.*/ -Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range); +Table * createTable(CSolver *solver, Element **domains, uint numDomain, Element * range); /** This function adds an input output relation to a table. */ -- 2.34.1