Resolving Conflicts ... Still there're errors that should be fixed

diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h
index 8bb5cc29e38f084af9aab49ade951030fb2718a7..f4610d05eeaa7398d9dd2bbf56ddb8dd08650f8e 100644 (file)
--- a/src/Collections/hashtable.h
+++ b/src/Collections/hashtable.h
@@ -20,6 +20,9 @@
 #include "mymemory.h"
 #include "common.h"
 
+#define HT_DEFAULT_FACTOR 0.75
+#define HT_INITIAL_CAPACITY 16
+
 /**
  * @brief A simple, custom hash table
  *

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index fec9d75cc539b3e256fc34781266a8183ddbfead..dc6d66573c4f3c10bd355136dc493dab327941ca 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -10,6 +10,7 @@ ArrayDef(Element, Element *);
 ArrayDef(Boolean, Boolean *);
 ArrayDef(Set, Set *);
 
+
 VectorDef(Table, Table *, 4);
 VectorDef(Set, Set *, 4);
 VectorDef(Boolean, Boolean *, 4);
@@ -20,6 +21,8 @@ VectorDef(Element, Element *, 4);
 VectorDef(Order, Order *, 4);
 VectorDef(TableEntry, TableEntry *, 4);
 VectorDef(ASTNode, ASTNode *, 4);
+VectorDef(FunctionEncoding, FunctionEncoding *, 4);
+VectorDef(ElementEncoding, ElementEncoding *, 4);
 VectorDef(Int, uint64_t, 4);
 
 
@@ -31,5 +34,11 @@ inline bool Ptr_equals(void * key1, void * key2) {
        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 --git a/src/Encoders/encodings.c b/src/Encoders/encodings.c
new file mode 100644 (file)
index 0000000..27d393e
--- /dev/null
+++ b/src/Encoders/encodings.c
@@ -0,0 +1,57 @@
+#include "encodings.h"
+#include "elementencoding.h"
+#include "functionencoding.h"
+#include "element.h"
+#include "common.h"
+#include "boolean.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; i<size; i++){
+               Element* element = getVectorElement(csolver->allElements, 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; i<size; i++){
+               Boolean* predicate = getVectorBoolean(csolver->allBooleans, 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
+}
\ No newline at end of file

diff --git a/src/Encoders/encodings.h b/src/Encoders/encodings.h
new file mode 100644 (file)
index 0000000..30c611c
--- /dev/null
+++ b/src/Encoders/encodings.h
@@ -0,0 +1,29 @@
+
+#ifndef NAIVEENCODINGASSIGNMENT_H
+#define NAIVEENCODINGASSIGNMENT_H
+#include "classlist.h"
+#include "structs.h"
+#include "csolver.h"
+#include "mymemory.h"
+
+
+#define GETVECTORFUNCTIONENCODING(o) (&((Encodings*)o)->funcEncoding)
+#define GETVECTORELEMENTENCODING(o) (&((Encodings*)o)->elemEncoding)
+
+struct Encodings{
+       HashTableVoidToFuncEncod* voidToFuncEncode;
+       HashTableElemToEncod* elemToEncode;
+       VectorFunctionEncoding funcEncoding;
+       VectorElementEncoding elemEncoding;
+};
+
+Encodings* allocEncodings();
+
+//For now, This function just simply goes through elements/functions and 
+//assigns a predefined Encoding to each of them
+void assignEncoding(CSolver* csolver, Encodings* This);
+void encodeFunctionsElements(Encodings* This);
+void deleteEncodings(Encodings* This);
+
+#endif /* NAIVEENCODINGASSIGNMENT_H */
+

diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h
index 486d5eb13baf64d4a8bbdb751ef294ae5b06e688..c7cf27e3c0743cf17b26225f614518195f00cd8f 100644 (file)
--- a/src/Encoders/functionencoding.h
+++ b/src/Encoders/functionencoding.h
@@ -24,4 +24,5 @@ struct FunctionEncoding {
 void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
 void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
 void deleteFunctionEncoding(FunctionEncoding *This);
+
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index ad8a65072bc3549730929b0230f656855d53b3f7..ca83383b33ec4f2275b373dffa115aec79ff7d63 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -23,3 +23,54 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) {
                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; i<size; i++){
+               TableEntry* entry = getVectorTableEntry(&table->entries, i);
+               //FIXME: generate Constraints
+       }
+       
+}
+
+void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This){
+       
+}
\ No newline at end of file

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index db4aeb94ef0b661c3fe50e71776b11f81dbbf0ed..d3df611a51c177462633c9e5b78ea63323f48c47 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -2,4 +2,9 @@
 #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

diff --git a/src/classlist.h b/src/classlist.h
index 3c7d071a66221d25dffd679d5465284efe7cc769..f9aa831660e074755b9773d518af5bfff4569b81 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -82,6 +82,9 @@ typedef struct OrderEncoding OrderEncoding;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 
+struct Encodings;
+typedef struct Encodings Encodings;
+
 typedef unsigned int uint;
 typedef uint64_t VarType;
 #endif