From bb1e3e7741fe70469395ccc223364deef16c3f8e Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 19 Jul 2017 19:06:35 -0700 Subject: [PATCH] Using hashset for tableEntries + adding handlers for different undefBehaviors for FunctionTable --- src/AST/element.c | 1 + src/AST/table.c | 25 +++-- src/AST/table.h | 3 +- src/AST/tableentry.c | 1 + src/AST/tableentry.h | 1 + src/Backend/satfuncencoder.c | 174 +++++++++++++++++++++++++++++------ src/Backend/satfuncencoder.h | 2 + src/Collections/hashset.h | 44 ++++----- src/Collections/structs.c | 24 +++++ src/Collections/structs.h | 2 +- 10 files changed, 220 insertions(+), 57 deletions(-) diff --git a/src/AST/element.c b/src/AST/element.c index 6926ce0..8a7d28f 100644 --- a/src/AST/element.c +++ b/src/AST/element.c @@ -18,6 +18,7 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr ElementFunction* This = (ElementFunction*) ourmalloc(sizeof(ElementFunction)); GETELEMENTTYPE(This)= ELEMFUNCRETURN; This->function=function; + ASSERT(GETBOOLEANTYPE(overflowstatus) == BOOLEANVAR); This->overflowstatus = overflowstatus; initArrayInitElement(&This->inputs, array, numArrays); initDefVectorASTNode(GETELEMENTPARENTS(This)); diff --git a/src/AST/table.c b/src/AST/table.c index f212ff9..a4606ff 100644 --- a/src/AST/table.c +++ b/src/AST/table.c @@ -8,25 +8,38 @@ Table * allocTable(Set **domains, uint numDomain, Set * range){ Table* This = (Table*) ourmalloc(sizeof(Table)); initArrayInitSet(&This->domains, domains, numDomain); - initDefVectorTableEntry(&This->entries); + This->entrie= allocHashSetTableEntry(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR); This->range =range; return This; } void addNewTableEntry(Table* This, uint64_t* inputs, uint inputSize, uint64_t result){ ASSERT(getSizeArraySet( &This->domains) == inputSize); +#ifdef CONFIG_ASSERT if(This->range==NULL) ASSERT(result == true || result == false); - pushVectorTableEntry(&This->entries, allocTableEntry(inputs, inputSize, result)); +#endif + TableEntry* tb = allocTableEntry(inputs, inputSize, result); + ASSERT(!containsHashSetTableEntry(This->entrie, tb)); + bool status= addHashSetTableEntry(This->entrie, tb); + ASSERT(status); +} + +TableEntry* getTableEntryFromTable(Table* table, uint64_t* inputs, uint inputSize){ + TableEntry* temp = allocTableEntry(inputs, inputSize, -1); + TableEntry* result= getHashSetTableEntry(table->entrie, temp); + deleteTableEntry(temp); + return result; } void deleteTable(Table* This){ deleteInlineArraySet(&This->domains); - uint size = getSizeVectorTableEntry(&This->entries); - for(uint i=0; ientries, i)); + HSIteratorTableEntry* iterator = iteratorTableEntry(This->entrie); + while(hasNextTableEntry(iterator)){ + deleteTableEntry( nextTableEntry(iterator) ); } - deleteVectorArrayTableEntry(&This->entries); + deleteIterTableEntry(iterator); + deleteHashSetTableEntry(This->entrie); ourfree(This); } diff --git a/src/AST/table.h b/src/AST/table.h index d2df3a4..f465a47 100644 --- a/src/AST/table.h +++ b/src/AST/table.h @@ -7,10 +7,11 @@ struct Table { ArraySet domains; Set * range; - VectorTableEntry entries; + HashSetTableEntry* entrie; }; Table * allocTable(Set ** domains, uint numDomain, Set * range); void addNewTableEntry(Table * This, uint64_t * inputs, uint inputSize, uint64_t result); +TableEntry* getTableEntryFromTable(Table* table, uint64_t* inputs, uint inputSize); void deleteTable(Table * This); #endif diff --git a/src/AST/tableentry.c b/src/AST/tableentry.c index 9992af7..4fb74a5 100644 --- a/src/AST/tableentry.c +++ b/src/AST/tableentry.c @@ -4,6 +4,7 @@ TableEntry* allocTableEntry(uint64_t* inputs, uint inputSize, uint64_t result){ TableEntry* te = (TableEntry*) ourmalloc(sizeof(TableEntry)+inputSize*sizeof(uint64_t)); te->output=result; + te->inputSize=inputSize; memcpy(te->inputs, inputs, inputSize * sizeof(uint64_t)); return te; } diff --git a/src/AST/tableentry.h b/src/AST/tableentry.h index 63c6fde..1901e53 100644 --- a/src/AST/tableentry.h +++ b/src/AST/tableentry.h @@ -18,6 +18,7 @@ #include "mymemory.h" struct TableEntry { uint64_t output; + uint inputSize; uint64_t inputs[]; }; diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c index 87be4b7..683336f 100644 --- a/src/Backend/satfuncencoder.c +++ b/src/Backend/satfuncencoder.c @@ -9,8 +9,9 @@ #include "set.h" #include "element.h" #include "common.h" -Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ - VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries); + +Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ + Table* table = ((PredicateTable*)constraint->predicate)->table; FunctionEncodingType encType = constraint->encoding.type; ArrayElement* inputs = &constraint->inputs; uint inputNum =getSizeArrayElement(inputs); @@ -18,15 +19,13 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co for(uint i=0; ientrie); bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE; Edge constraints[size]; - for(uint i=0; ientrie); + uint i=0; + while(hasNextTableEntry(iterator)){ + TableEntry* entry = nextTableEntry(iterator); if(generateNegation == entry->output) { //Skip the irrelevant entries continue; @@ -36,12 +35,16 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co Element* el = getArrayElement(inputs, j); carray[j] = getElementValueConstraint(This, el, entry->inputs[j]); } - constraints[i]=constraintAND(This->cnf, inputNum, carray); + constraints[i++]=constraintAND(This->cnf, inputNum, carray); } Edge result=constraintOR(This->cnf, size, constraints); return generateNegation ? constraintNegate(result) : result; } +Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ + //FIXME + return E_NULL; +} Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) { switch(constraint->encoding.type){ @@ -251,23 +254,18 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* deleteVectorEdge(clauses); } -void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* func){ -#ifdef TRACE_DEBUG - model_print("Enumeration Table functions ...\n"); -#endif - //FIXME: HANDLE UNDEFINED BEHAVIORS - ASSERT(GETFUNCTIONTYPE(func->function)==TABLEFUNC); +void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){ + UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior; + ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED); ArrayElement* elements= &func->inputs; - for(uint i=0; ifunction))->table; - uint size = getSizeVectorTableEntry(&table->entries); - Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries - for(uint i=0; ientries, i); + uint size = getSizeHashSetTableEntry(table->entrie); + Edge constraints[size]; + HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie); + uint i=0; + while(hasNextTableEntry(iterator)) { + TableEntry* entry = nextTableEntry(iterator); + ASSERT(entry!=NULL); uint inputNum = getSizeArrayElement(elements); Edge carray[inputNum]; for(uint j=0; jinputs[j]); } Edge output = getElementValueConstraint(This, (Element*)func, entry->output); - Edge row= constraintIMPLIES(This->cnf, constraintAND(This->cnf, inputNum, carray), output); - constraints[i]=row; + Edge row; + switch(undefStatus ){ + case IGNOREBEHAVIOR: { + row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output); + break; + } + case FLAGFORCEUNDEFINED: { + Edge undefConst = ((BooleanVar*)func->overflowstatus)->var; + row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst))); + break; + } + default: + ASSERT(0); + + } + constraints[i++]=row; } + deleteIterTableEntry(iterator); addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints)); } + +void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){ +#ifdef TRACE_DEBUG + model_print("Enumeration Table functions ...\n"); +#endif + ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC); + //First encode children + ArrayElement* elements= &elemFunc->inputs; + for(uint i=0; iundefBehavior){ + case IGNOREBEHAVIOR: + case FLAGFORCEUNDEFINED: + return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc); + default: + break; + } + + uint numDomains=getSizeArraySet(&function->table->domains); + + VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses + + uint indices[numDomains]; //setup indices + bzero(indices, sizeof(uint)*numDomains); + + uint64_t vals[numDomains]; //setup value array + for(uint i=0;itable->domains, i); + vals[i]=getSetElement(set, indices[i]); + } + + Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var; + + bool notfinished=true; + while(notfinished) { + Edge carray[numDomains+1]; + TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains); + bool isInRange = tableEntry!=NULL; + bool needClause = isInRange; + if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) { + needClause=true; + } + + if (needClause) { + //Include this in the set of terms + for(uint i=0;iinputs, i); + carray[i] = getElementValueConstraint(This, elem, vals[i]); + } + if (isInRange) { + carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output); + } + + Edge clause; + switch(function->undefBehavior) { + case UNDEFINEDSETSFLAG: { + if (isInRange) { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]); + } else { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); + } + break; + } + case FLAGIFFUNDEFINED: { + if (isInRange) { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint))); + } else { + clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint); + } + break; + } + default: + ASSERT(0); + } +#ifdef TRACE_DEBUG + model_print("added clause in table enumeration ...\n"); + printCNF(clause); + model_print("\n"); +#endif + pushVectorEdge(clauses, clause); + } + + notfinished=false; + for(uint i=0;itable->domains, i); + + if (index < getSetSize(set)) { + vals[i]=getSetElement(set, index); + notfinished=true; + break; + } else { + indices[i]=0; + vals[i]=getSetElement(set, 0); + } + } + } + + Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses)); + addConstraintCNF(This->cnf, cor); + deleteVectorEdge(clauses); + +} diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncencoder.h index 02dc858..8b8a9a2 100644 --- a/src/Backend/satfuncencoder.h +++ b/src/Backend/satfuncencoder.h @@ -1,11 +1,13 @@ #ifndef SATFUNCENCODER_H #define SATFUNCENCODER_H +Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This); void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); +void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* encoder, ElementFunction* This); Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint); Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint); diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index 0fe1386..f647c38 100644 --- a/src/Collections/hashset.h +++ b/src/Collections/hashset.h @@ -42,20 +42,20 @@ \ HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ void deleteHashSet ## Name(struct HashSet ## Name * set); \ - HashSet ## Name * copy ## Name(HashSet ## Name * set); \ - void resetSet ## Name(HashSet ## Name * set); \ - bool add ## Name(HashSet ## Name * set,_Key key); \ - _Key getSet ## Name(HashSet ## Name * set,_Key key); \ - _Key getFirstKey ## Name(HashSet ## Name * set); \ - bool containsSet ## Name(HashSet ## Name * set,_Key key); \ - bool removeSet ## Name(HashSet ## Name * set,_Key key); \ - unsigned int getSizeSet ## Name(HashSet ## Name * set); \ - bool isEmpty ## Name(HashSet ## Name * set); \ + HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set); \ + void resetHashSet ## Name(HashSet ## Name * set); \ + bool addHashSet ## Name(HashSet ## Name * set,_Key key); \ + _Key getHashSet ## Name(HashSet ## Name * set,_Key key); \ + _Key getHashSetFirstKey ## Name(HashSet ## Name * set); \ + bool containsHashSet ## Name(HashSet ## Name * set,_Key key); \ + bool removeHashSet ## Name(HashSet ## Name * set,_Key key); \ + unsigned int getSizeHashSet ## Name(HashSet ## Name * set); \ + bool isEmptyHashSet ## Name(HashSet ## Name * set); \ HSIterator ## Name * iterator ## Name(HashSet ## Name * set); #define HashSetImpl(Name, _Key, hash_function, equals) \ - HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \ + HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals, ourfree); \ HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set) { \ HSIterator ## Name * hsit = (HSIterator ## Name *)ourmalloc(sizeof(HSIterator ## Name)); \ hsit->curr=_curr; \ @@ -84,7 +84,7 @@ \ void removeIter ## Name(HSIterator ## Name *hsit) { \ _Key k=hsit->last->key; \ - removeSet ## Name(hsit->set, k); \ + removeHashSet ## Name(hsit->set, k); \ } \ \ HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ @@ -106,16 +106,16 @@ ourfree(set); \ } \ \ - HashSet ## Name * copy ## Name(HashSet ## Name * set) { \ + HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set) { \ HashSet ## Name *copy=allocHashSet ## Name(getCapacity ## Name ## Set(set->table), getLoadFactor ## Name ## Set(set->table)); \ HSIterator ## Name * it=iterator ## Name(set); \ while(hasNext ## Name(it)) \ - add ## Name(copy, next ## Name(it)); \ + addHashSet ## Name(copy, next ## Name(it)); \ deleteIter ## Name(it); \ return copy; \ } \ \ - void resetSet ## Name(HashSet ## Name * set) { \ + void resetHashSet ## Name(HashSet ## Name * set) { \ LinkNode ## Name *tmp=set->list; \ while(tmp!=NULL) { \ LinkNode ## Name *tmpnext=tmp->next; \ @@ -126,7 +126,7 @@ reset ## Name ## Set(set->table); \ } \ \ - bool add ## Name(HashSet ## Name * set,_Key key) { \ + bool addHashSet ## Name(HashSet ## Name * set,_Key key) { \ LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ if (val==NULL) { \ LinkNode ## Name * newnode=(LinkNode ## Name *)ourmalloc(sizeof(struct LinkNode ## Name)); \ @@ -144,7 +144,7 @@ return false; \ } \ \ - _Key getSet ## Name(HashSet ## Name * set,_Key key) { \ + _Key getHashSet ## Name(HashSet ## Name * set,_Key key) { \ LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ if (val!=NULL) \ return val->key; \ @@ -152,15 +152,15 @@ return NULL; \ } \ \ - _Key getFirstKey ## Name(HashSet ## Name * set) { \ + _Key getHashSetFirstKey ## Name(HashSet ## Name * set) { \ return set->list->key; \ } \ \ - bool containsSet ## Name(HashSet ## Name * set,_Key key) { \ + bool containsHashSet ## Name(HashSet ## Name * set,_Key key) { \ return get ## Name ## Set(set->table, key)!=NULL; \ } \ \ - bool removeSet ## Name(HashSet ## Name * set,_Key key) { \ + bool removeHashSet ## Name(HashSet ## Name * set,_Key key) { \ LinkNode ## Name * oldlinknode; \ oldlinknode=get ## Name ## Set(set->table, key); \ if (oldlinknode==NULL) { \ @@ -180,12 +180,12 @@ return true; \ } \ \ - unsigned int getSizeSet ## Name(HashSet ## Name * set) { \ + unsigned int getSizeHashSet ## Name(HashSet ## Name * set) { \ return getSizeTable ## Name ## Set(set->table); \ } \ \ - bool isEmpty ## Name(HashSet ## Name * set) { \ - return getSizeSet ## Name(set)==0; \ + bool isEmptyHashSet ## Name(HashSet ## Name * set) { \ + return getSizeHashSet ## Name(set)==0; \ } \ \ HSIterator ## Name * iterator ## Name(HashSet ## Name * set) { \ diff --git a/src/Collections/structs.c b/src/Collections/structs.c index 64821c9..3bd5e4a 100644 --- a/src/Collections/structs.c +++ b/src/Collections/structs.c @@ -1,6 +1,7 @@ #include "structs.h" #include "mymemory.h" #include "orderpair.h" +#include "tableentry.h" VectorImpl(Table, Table *, 4); VectorImpl(Set, Set *, 4); @@ -29,4 +30,27 @@ static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){ return key1->first== key2->first && key1->second == key2->second; } +static inline unsigned int table_entry_hash_Function(TableEntry* This){ + //http://isthe.com/chongo/tech/comp/fnv/ + unsigned int h = 2166136261; + const unsigned int FNV_PRIME = 16777619; + for(uint i=0; iinputSize; i++){ + h ^= This->inputs[i]; + h *= FNV_PRIME; + } + return h; +} + +static inline bool table_entry_equals(TableEntry* key1, TableEntry* key2){ + if(key1->inputSize != key2->inputSize) + return false; + for(uint i=0; iinputSize; i++) + if(key1->inputs[i]!=key2->inputs[i]) + return false; + return true; +} + HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree); +HashSetImpl(TableEntry, TableEntry*, table_entry_hash_Function, table_entry_equals); + + diff --git a/src/Collections/structs.h b/src/Collections/structs.h index 3a4e81a..97d97e5 100644 --- a/src/Collections/structs.h +++ b/src/Collections/structs.h @@ -25,5 +25,5 @@ HashTableDef(Void, void *, void *); HashTableDef(OrderPair, OrderPair *, OrderPair *); HashSetDef(Void, void *); - +HashSetDef(TableEntry, TableEntry*); #endif -- 2.34.1