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));
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; i<size; i++){
- deleteTableEntry(getVectorTableEntry(&This->entries, i));
+ HSIteratorTableEntry* iterator = iteratorTableEntry(This->entrie);
+ while(hasNextTableEntry(iterator)){
+ deleteTableEntry( nextTableEntry(iterator) );
}
- deleteVectorArrayTableEntry(&This->entries);
+ deleteIterTableEntry(iterator);
+ deleteHashSetTableEntry(This->entrie);
ourfree(This);
}
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
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;
}
#include "mymemory.h"
struct TableEntry {
uint64_t output;
+ uint inputSize;
uint64_t inputs[];
};
#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);
for(uint i=0; i<inputNum; i++){
encodeElementSATEncoder(This, getArrayElement(inputs, i));
}
-
- //WARNING: THIS ASSUMES PREDICATE TABLE IS COMPLETE...SEEMS UNLIKELY TO BE SAFE IN MANY CASES...
- //WONDER WHAT BEST WAY TO HANDLE THIS IS...
-
- uint size = getSizeVectorTableEntry(entries);
+ uint size = getSizeHashSetTableEntry(table->entrie);
bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
Edge constraints[size];
- for(uint i=0; i<size; i++){
- TableEntry* entry = getVectorTableEntry(entries, i);
+ HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
+ uint i=0;
+ while(hasNextTableEntry(iterator)){
+ TableEntry* entry = nextTableEntry(iterator);
if(generateNegation == entry->output) {
//Skip the irrelevant entries
continue;
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){
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; i<getSizeArrayElement(elements); i++){
- Element *elem = getArrayElement( elements, i);
- encodeElementSATEncoder(This, elem);
- }
-
Table* table = ((FunctionTable*) (func->function))->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; i<size; i++) {
- TableEntry* entry = getVectorTableEntry(&table->entries, 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; j<inputNum; j++){
carray[j] = getElementValueConstraint(This, el, entry->inputs[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; i<getSizeArrayElement(elements); i++){
+ Element *elem = getArrayElement( elements, i);
+ encodeElementSATEncoder(This, elem);
+ }
+
+ FunctionTable* function =(FunctionTable*)elemFunc;
+ switch(function->undefBehavior){
+ 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;i<numDomains; i++) {
+ Set * set=getArraySet(&function->table->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;i<numDomains;i++) {
+ Element * elem = getArrayElement(&elemFunc->inputs, 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;i<numDomains; i++) {
+ uint index=++indices[i];
+ Set * set=getArraySet(&function->table->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);
+
+}
#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);
\
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; \
\
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) { \
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; \
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)); \
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; \
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) { \
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) { \
#include "structs.h"
#include "mymemory.h"
#include "orderpair.h"
+#include "tableentry.h"
VectorImpl(Table, Table *, 4);
VectorImpl(Set, Set *, 4);
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; i<This->inputSize; 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; i<key1->inputSize; 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);
+
+
HashTableDef(OrderPair, OrderPair *, OrderPair *);
HashSetDef(Void, void *);
-
+HashSetDef(TableEntry, TableEntry*);
#endif
projects / satune.git / commitdiff