From: Hamed Date: Fri, 23 Jun 2017 07:26:08 +0000 (-0700) Subject: Resolving Conflicts ... Still there're errors that should be fixed X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ddc4141470ead8ab7bfa6047a6a6a0ac1766a91f;p=satune.git Resolving Conflicts ... Still there're errors that should be fixed --- ddc4141470ead8ab7bfa6047a6a6a0ac1766a91f diff --cc src/Collections/structs.h index 112fc08,fec9d75..dc6d665 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@@ -4,20 -4,24 +4,27 @@@ #include "hashtable.h" #include "hashset.h" #include "classlist.h" + #include "array.h" - VectorDef(Int, uint64_t, 4); + ArrayDef(Element, Element *); + ArrayDef(Boolean, Boolean *); + ArrayDef(Set, Set *); + ++ + VectorDef(Table, Table *, 4); + VectorDef(Set, Set *, 4); VectorDef(Boolean, Boolean *, 4); VectorDef(Constraint, Constraint *, 4); - VectorDef(Set, Set *, 4); - VectorDef(Element, Element *, 4); - VectorDef(TableEntry, TableEntry *, 4); + VectorDef(Function, Function *, 4); VectorDef(Predicate, Predicate *, 4); - VectorDef(Table, Table *, 4); + VectorDef(Element, Element *, 4); VectorDef(Order, Order *, 4); - VectorDef(Function, Function *, 4); + VectorDef(TableEntry, TableEntry *, 4); VectorDef(ASTNode, ASTNode *, 4); +VectorDef(FunctionEncoding, FunctionEncoding *, 4); +VectorDef(ElementEncoding, ElementEncoding *, 4); + VectorDef(Int, uint64_t, 4); + inline unsigned int Ptr_hash_function(void * hash) { return (unsigned int)((uint64_t)hash >> 4); @@@ -27,10 -31,5 +34,11 @@@ inline bool Ptr_equals(void * key1, voi return key1 == key2; } +HashTableDef(Void, void *, void *, Ptr_hash_function, Ptr_equals); +HashTableDef(ElemToEncod, Element *, ElementEncoding *, Ptr_hash_function, Ptr_equals); +HashTableDef(VoidToFuncEncod, void *, FunctionEncoding *, Ptr_hash_function, Ptr_equals); + +HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); + + #endif diff --cc src/Encoders/encodings.c index f86389d,0000000..27d393e mode 100644,000000..100644 --- a/src/Encoders/encodings.c +++ b/src/Encoders/encodings.c @@@ -1,57 -1,0 +1,57 @@@ +#include "encodings.h" +#include "elementencoding.h" +#include "functionencoding.h" +#include "element.h" +#include "common.h" +#include "boolean.h" - #include "naiveelementencoder.h" ++#include "naiveencoder.h" + +Encodings* allocEncodings(){ + Encodings* This = (Encodings*) ourmalloc(sizeof(Encodings)); + allocInlineDefVectorElementEncoding(GETVECTORELEMENTENCODING(This)); + allocInlineDefVectorFunctionEncoding(GETVECTORFUNCTIONENCODING(This)); + This->elemToEncode= allocHashTableElemToEncod(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + This->voidToFuncEncode= allocHashTableVoidToFuncEncod(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); + return This; +} + +void deleteEncodings(Encodings* This){ + deleteVectorArrayFunctionEncoding(GETVECTORFUNCTIONENCODING(This)); + deleteVectorArrayElementEncoding(GETVECTORELEMENTENCODING(This)); + deleteHashTableElemToEncod(This->elemToEncode); + deleteHashTableVoidToFuncEncod(This->voidToFuncEncode); + ourfree(This); +} + +void assignEncoding(CSolver* csolver, Encodings* This){ + uint size = getSizeVectorElement(csolver->allElements); + for(uint i=0; iallElements, i); + if(GETELEMENTTYPE(element)==ELEMSET){ + ElementEncoding* eencoding = allocElementEncoding( BINARYINDEX, element); + baseBinaryIndexElementAssign(eencoding); + pushVectorElementEncoding(GETVECTORELEMENTENCODING(This) , eencoding); + putElemToEncod(This->elemToEncode, element, eencoding); + }else if (GETELEMENTTYPE(element)==ELEMFUNCRETURN){ + FunctionEncoding* fencoding = allocFunctionEncoding( ENUMERATEIMPLICATIONS, element); + pushVectorFunctionEncoding(GETVECTORFUNCTIONENCODING(This) , fencoding); + putVoidToFuncEncod(This->voidToFuncEncode,element, fencoding); + }else + ASSERT(0); + } + + size = getSizeVectorBoolean(csolver->allBooleans); + for(uint i=0; iallBooleans, i); + if(GETBOOLEANTYPE(predicate)==PREDICATEOP){ + FunctionEncoding* fencoding = allocPredicateEncoding(ENUMERATEIMPLICATIONS, predicate); + pushVectorFunctionEncoding(GETVECTORFUNCTIONENCODING(This), fencoding); + putVoidToFuncEncod(This->voidToFuncEncode, predicate,fencoding); + }else + ASSERT(0); + } +} + +void encodeFunctionsElements(Encodings* This){ + //call encoding for each element/predicate +} diff --cc src/Encoders/functionencoding.h index dc52aa7,486d5eb..c7cf27e --- a/src/Encoders/functionencoding.h +++ b/src/Encoders/functionencoding.h @@@ -21,8 -21,7 +21,8 @@@ struct FunctionEncoding ElementPredicate op; }; - FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function); - FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate); + void initFunctionEncoding(FunctionEncoding *encoding, Element *function); + void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate); void deleteFunctionEncoding(FunctionEncoding *This); + #endif diff --cc src/Encoders/naiveencoder.c index 0000000,ad8a650..ca83383 mode 000000,100644..100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@@ -1,0 -1,25 +1,76 @@@ + #include "naiveencoder.h" + #include "elementencoding.h" + #include "element.h" + #include "functionencoding.h" + #include "function.h" + #include "set.h" + #include "common.h" + #include "structs.h" + #include + + void baseBinaryIndexElementAssign(ElementEncoding *This) { + Element * element=This->element; + ASSERT(element->type == ELEMSET); + Set * set= ((ElementSet*)element)->set; + 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); + } + } ++ ++ ++void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This){ ++ if(This->isFunction) { ++ ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN); ++ if(This->type==CIRCUIT){ ++ naiveEncodeCircuitFunction(encodings, This); ++ } else if( This->type == ENUMERATEIMPLICATIONS){ ++ naiveEncodeEnumeratedFunction(encodings, This); ++ } else ++ ASSERT(0); ++ ++ }else { ++ ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP); ++ BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate; ++ //FIXME ++ ++ } ++} ++ ++ ++void naiveEncodeCircuitFunction(Encodings* encodings, FunctionEncoding* This){ ++ ++} ++ ++void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This){ ++ ElementFunction* ef =(ElementFunction*)This->op.function; ++ Function * function = ef->function; ++ if(GETFUNCTIONTYPE(function)==TABLEFUNC){ ++ naiveEncodeEnumTableFunc(encodings, ef); ++ }else if (GETFUNCTIONTYPE(function)== OPERATORFUNC){ ++ naiveEncodeEnumOperatingFunc(encodings, ef); ++ }else ++ ASSERT(0); ++} ++ ++void naiveEncodeEnumTableFunc(Encodings* encodings, 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 ++ } ++ ++} ++ ++void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This){ ++ ++} diff --cc src/Encoders/naiveencoder.h index 0000000,db4aeb9..d3df611 mode 000000,100644..100644 --- a/src/Encoders/naiveencoder.h +++ b/src/Encoders/naiveencoder.h @@@ -1,0 -1,5 +1,10 @@@ + #ifndef NAIVEELEMENTENCODER_H + #define NAIVEELEMENTENCODER_H + #include "classlist.h" + void baseBinaryIndexElementAssign(ElementEncoding *This); ++void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This); ++void naiveEncodeCircuitFunction(Encodings* encodings,FunctionEncoding* This); ++void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This); ++void naiveEncodeEnumTableFunc(Encodings* encodings, ElementFunction* This); ++void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This); + #endif