Binary encoding for ElementSet and table-based ElementFunction

diff --git a/src/AST/element.c b/src/AST/element.c
index a94db4b8d8ac27fbe812a6c44c1c0e2f650553ca..8711529f53f78d2f36b02ff17c6c34c9946f7081 100644 (file)
--- 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; i<size; i++){
+                               if( GETELEMENTENCODING(elemSet)->encodingArray[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<numvars;j++) {
+               carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
+               value=value>>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 b5bc9c1fdfcb7ce5bb21ec1d497a09af33771a50..3a71686c345a7c1f2f6e7006e271d6009dfcbbe4 100644 (file)
--- 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 fc056a2e16b95ef9547af781cd800de6956ec461..afe26ec7a5477e0fbfac0a10b11ffbfe3b7896a2 100644 (file)
--- 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 92315e22818728089a1d543021aea773529122bc..55fb57cb9900b6d7f5b93f38f8fe921c2b34ffe5 100644 (file)
--- 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 ea4b6d21a8d4b9ee0f5410dc11b9ea4c7dae3960..a8af588fb4a67e9f4dff37176c125b4c9a099256 100644 (file)
--- 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; i<size; i++){
     deleteTableEntry(getVectorTableEntry(&table->entries, i));

diff --git a/src/AST/table.h b/src/AST/table.h
index 90f50015071d9c701c9c76310602ee0da1813de4..fa83b06b73e4fe39f9df0d3aae45ec90097b8198 100644 (file)
--- 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 1aa3d3cc9b5f22d90498dcbd0ad915b0e8ab928d..27db299233e94df3495799fa05b450558e14da2c 100644 (file)
--- 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<numvars;j++) {
-               carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
-               value=value>>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 a83a39b782a8f5ddf01b99243a2b40ea49dcf1d7..e1b21d36f69f4ea5ec45ebb646a39b3024e4b16a 100644 (file)
--- 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 4a4bc89670583334c61bfd7adf8208bbd4fb401d..02a9f7f100731a0144d4e32b252fb612f3afc00a 100644 (file)
--- 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 03040ed9103fd03a7f2f55948aff3a3ed0ab03ba..ffdb0d0b87266ebacc7d8347ea421b67f3a9d958 100644 (file)
--- 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 d5ceab6bfde261bebcf7963a99baf3271edd2a58..974772e92f0b8efd468b100def5bbd6181a48664 100644 (file)
--- 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 <strings.h>
 
-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; i<size; i++){
                Element* element = getVectorElement(csolver->allElements, 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;i<num;i++)
+               carray[i]=getNewVar(encoder);
+}
+
+Constraint * getNewVar(NaiveEncoder* encoder) {
+       Constraint* var = allocVarConstraint(VAR, encoder->varindex);
+       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; i<size; i++){
                Element* element = getVectorElement(csolver->allElements, 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; i<size; i++){
                TableEntry* entry = getVectorTableEntry(&table->entries, i);
-               //FIXME: generate Constraints
+               uint inputNum =getSizeArrayElement(elements);
+               Element* el= getArrayElement(elements, i);
+               Constraint* carray[inputNum];
+               for(uint j=0; j<inputNum; j++){
+                        carray[inputNum] = getElementValueConstraint(el, entry->inputs[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 c1623ebdc911d7ba529fe3687471a98e961f4bed..d3c409ce0df66ea402ceaedcf0eed6ad646076b1 100644 (file)
--- 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 3c7d071a66221d25dffd679d5465284efe7cc769..a7078455dae81c0f6d1f95b930f1dc8812e82e07 100644 (file)
--- 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 d9e6d4346dc525e00fa8d676080bc577cdbeab46..5d8c389710200942c30681065f12a367696d430a 100644 (file)
--- 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 5f330fd6112c70074522c17ac116739bf35746d6..ccb19f013f6dad5999c9b1a18a8a8f0c69d6118a 100644 (file)
--- 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 495d3864dca23ebdca90cab1f7eec52f485e3fa2..0bd2088831d9b68bf53e0793c5e88423f042e6cf 100644 (file)
--- 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. */