Fix some bugs, Moving backend codes to SATEncoder

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 411af2604b771835682316e1d191c7d56c1b600d..297c3835d007f9d808bd8b2c8a4d03b8a0b8bb48 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -51,4 +51,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
 void deleteBoolean(Boolean * This);
 
+inline FunctionEncoding* getPredicateFunctionEncoding(BooleanPredicate* func){
+       return &func->encoding;
+}
+
 #endif

diff --git a/src/AST/element.c b/src/AST/element.c
index f219072f4c8621f76411bbe5510ef48fde4959ba..5b9d847fddcd9512140d70dc810fdb40a12e89f9 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -44,16 +44,17 @@ 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);
+                       uint size = getSetSize(((ElementSet*)This)->set);
+                       //FIXME
                        for(uint i=0; i<size; i++){
-                               if( getElementEncoding(elemSet)->encodingArray[i]==value){
-                                       return generateBinaryConstraint(getElementEncoding(elemSet)->numVars,
-                                               getElementEncoding(elemSet)->variables, i);
+                               if( getElementEncoding(This)->encodingArray[i]==value){
+                                       return generateBinaryConstraint(getElementEncoding(This)->numVars,
+                                               getElementEncoding(This)->variables, i);
                                }
                        }
                        break;
                case ELEMFUNCRETURN:
+                       ASSERT(0);
                        break;
                default:
                        ASSERT(0);

diff --git a/src/AST/element.h b/src/AST/element.h
index c0eeaf52c906e3b913224d257271a548608d3e5d..3f9693a9a591f1b61d9c606399a24c3faa3e8ca1 100644 (file)
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -47,6 +47,11 @@ inline ElementEncoding* getElementEncoding(Element* This){
        return NULL;
 }
 
+
+inline FunctionEncoding* getElementFunctionEncoding(ElementFunction* func){
+       return &func->functionencoding;
+}
+
 uint getElementSize(Element* This);
 Constraint * getElementValueConstraint(Element* This, uint64_t value);
 #endif

diff --git a/src/AST/table.c b/src/AST/table.c
index a8af588fb4a67e9f4dff37176c125b4c9a099256..a0b1e6f451e085a5ad3a1c84a8bc128609e61e0e 100644 (file)
--- a/src/AST/table.c
+++ b/src/AST/table.c
@@ -6,9 +6,9 @@
 #include "mutableset.h"
 
 
-Table * allocTable(Element **domains, uint numDomain, Element * range){
+Table * allocTable(Set **domains, uint numDomain, Set * range){
        Table* table = (Table*) ourmalloc(sizeof(Table));
-       allocInlineArrayInitElement(&table->domains, domains, numDomain);
+       allocInlineArrayInitSet(&table->domains, domains, numDomain);
        allocInlineDefVectorTableEntry(&table->entries);
        table->range =range;
        return table;
@@ -20,7 +20,7 @@ void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t r
 }
 
 void deleteTable(Table* table){
-  deleteInlineArrayElement(&table->domains);
+  deleteInlineArraySet(&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 fa83b06b73e4fe39f9df0d3aae45ec90097b8198..90f50015071d9c701c9c76310602ee0da1813de4 100644 (file)
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -5,12 +5,12 @@
 #include "structs.h"
 
 struct Table {
-       ArrayElement domains;
-       Element * range;
+       ArraySet domains;
+       Set * range;
        VectorTableEntry entries;
 };
 
-Table * allocTable(Element **domains, uint numDomain, Element * range);
+Table * allocTable(Set **domains, uint numDomain, Set * range);
 void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result);
 void deleteTable(Table* table);
 #endif

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 37d3bc7f4847b35c1fb2432a7dbc82464e344a16..325b614c18cf593927f904125c93002010008904 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -4,9 +4,16 @@
 #include "boolean.h"
 #include "constraint.h"
 #include "common.h"
+#include "element.h"
+#include "function.h"
+#include "tableentry.h"
+#include "table.h"
+
 
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
+       allocInlineDefVectorConstraint(getSATEncoderAllConstraints(This));
+       allocInlineDefVectorConstraint(getSATEncoderVars(This));
        This->varcount=1;
        return This;
 }
@@ -22,6 +29,20 @@ void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
                Boolean *constraint=getVectorBoolean(constraints, i);
                encodeConstraintSATEncoder(This, constraint);
        }
+       
+       size = getSizeVectorElement(csolver->allElements);
+       for(uint i=0; i<size; i++){
+               Element* element = getVectorElement(csolver->allElements, i);
+               switch(GETELEMENTTYPE(element)){
+                       case ELEMFUNCRETURN: 
+                               encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
+                               break;
+                       default:        
+                               continue;
+                               //ElementSets that aren't used in any constraints/functions
+                               //will be eliminated.
+               }
+       }
 }
 
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
@@ -40,11 +61,17 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
        }
 }
 
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
+       for(uint i=0;i<num;i++)
+               carray[i]=getNewVarSATEncoder(encoder);
+}
+
 Constraint * getNewVarSATEncoder(SATEncoder *This) {
        Constraint * var=allocVarConstraint(VAR, This->varcount);
        Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
        setNegConstraint(var, varneg);
        setNegConstraint(varneg, var);
+       pushVectorConstraint(getSATEncoderVars(This), var);
        return var;
 }
 
@@ -92,5 +119,56 @@ Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint)
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
        //TO IMPLEMENT
+       
+       return NULL;
+}
+
+Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
+       switch(GETFUNCTIONTYPE(This->function)){
+               case TABLEFUNC:
+                       return encodeTableElementFunctionSATEncoder(encoder, This);
+               case OPERATORFUNC:
+                       return encodeOperatorElementFunctionSATEncoder(encoder, This);
+               default:
+                       ASSERT(0);
+       }
+       //FIXME
+       return NULL;
+}
+
+Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
+       switch(getElementFunctionEncoding(This)->type){
+               case ENUMERATEIMPLICATIONS:
+                       return encodeEnumTableElemFunctionSATEncoder(encoder, This);
+                       break;
+               default:
+                       ASSERT(0);
+       }
+       //FIXME
        return NULL;
 }
+
+Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This){
+       return NULL;
+}
+
+Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* 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);
+               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((Element*)This, entry->output));
+               pushVectorConstraint( getSATEncoderAllConstraints(encoder), row);
+       }
+       //FIXME
+       return NULL;
+}
\ No newline at end of file

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 5382bc505acb2830887938b75576ce7465a3a0b9..dcc65462d087ceb02f9e7ccc9856c181c33a5eb3 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -2,18 +2,34 @@
 #define SATENCODER_H
 
 #include "classlist.h"
+#include "structs.h"
 
 struct SATEncoder {
        uint varcount;
+       //regarding managing memory 
+       VectorConstraint vars;
+       VectorConstraint allConstraints;
 };
 
+inline VectorConstraint* getSATEncoderVars(SATEncoder* ne){
+       return &ne->vars;
+}
+inline VectorConstraint* getSATEncoderAllConstraints(SATEncoder* ne){
+       return &ne->allConstraints;
+}
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
 Constraint * getNewVarSATEncoder(SATEncoder *This);
+void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+
+Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This);
+Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
 #endif

diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c
index fc76a4ad14d69c6d7dae6cb42b687d2b4f505eb0..7b3ebddf6f1c38c4fb6113440cdf583b990f38b3 100644 (file)
--- a/src/Encoders/elementencoding.c
+++ b/src/Encoders/elementencoding.c
@@ -2,6 +2,7 @@
 #include "common.h"
 #include "naiveencoder.h"
 #include "element.h"
+#include "satencoder.h"
 
 void initElementEncoding(ElementEncoding * This, Element *element) {
        This->element=element;
@@ -38,14 +39,14 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type){
        This->type = type;
 }
 
-void generateBinaryIndexEncodingVars(NaiveEncoder* encoder, ElementEncoding* This){
+void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This){
        ASSERT(This->type==BINARYINDEX);
        uint size = getElementSize(This->element);
        allocElementConstraintVariables(This, NUMBITS(size-1));
-       getArrayNewVars(encoder, This->numVars, This->variables);
+       getArrayNewVarsSATEncoder(encoder, This->numVars, This->variables);
 }
 
-void generateElementEncodingVariables(NaiveEncoder* encoder, ElementEncoding* This){
+void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){
        ASSERT(This->type!=ELEM_UNASSIGNED);
        ASSERT(This->variables==NULL);
        switch(This->type){

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index ffdb0d0b87266ebacc7d8347ea421b67f3a9d958..f04ba7e8726ccf3af3b1731cf097dd4507cab563 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -33,7 +33,7 @@ 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);
+void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
+void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
 
 #endif

diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h
index 60690e3857a0626433a16fa255e17bb510215649..a3521396f04abef9689b7371f4905e88b430dd14 100644 (file)
--- a/src/Encoders/functionencoding.h
+++ b/src/Encoders/functionencoding.h
@@ -21,18 +21,6 @@ struct FunctionEncoding {
        ElementPredicate op;
 };
 
-inline FunctionEncoding* getFunctionEncoding(ASTNode func){
-       switch(GETASTNODETYPE(func)){
-               case ELEMFUNCRETURN:
-                       return &((ElementFunction*)func)->functionencoding;
-               case PREDICATEOP:
-                       return &((BooleanPredicate*)func)->encoding;
-               default:
-                       ASSERT(0);
-       }
-       return NULL;
-}
-
 void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
 void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
 void setFunctionEncodingType(FunctionEncoding* encoding, FunctionEncodingType type);

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index a4f46a550d6a53a1465973805ffe1d51adc8f939..1ea5857176e637142619cb3f1afc55924245e7cc 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -10,30 +10,24 @@
 #include "boolean.h"
 #include "table.h"
 #include "tableentry.h"
-//THIS FILE SHOULD HAVE NOTHING TO DO WITH CONSTRAINTS...
-//#include "constraint.h"
 #include <strings.h>
 
-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){
+void naiveEncodingDecision(CSolver* csolver, SATEncoder* 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(getElementEncoding(element), BINARYINDEX);
+                               //FIXME:Should be moved to SATEncoder
                                baseBinaryIndexElementAssign(getElementEncoding(element));
                                generateElementEncodingVariables(encoder,getElementEncoding(element));
+                               //
                                break;
                        case ELEMFUNCRETURN: 
-                               setFunctionEncodingType(getFunctionEncoding(element), ENUMERATEIMPLICATIONS);
+                               setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
+                                       ENUMERATEIMPLICATIONS);
                                break;
                        default:
                                ASSERT(0);
@@ -45,7 +39,8 @@ void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){
                Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
                switch(GETBOOLEANTYPE(predicate)){
                        case PREDICATEOP:
-                               setFunctionEncodingType(getFunctionEncoding(predicate), ENUMERATEIMPLICATIONS);
+                               setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)predicate),
+                                       ENUMERATEIMPLICATIONS);
                                break;
                        default:
                                continue;
@@ -53,28 +48,6 @@ void naiveEncodingDecision(CSolver* csolver, NaiveEncoder* encoder){
        }
 }
 
-
-// THIS SHOULD NOT BE HERE
-/*
-void getArrayNewVars(NaiveEncoder* encoder, uint num, Constraint **carray) {
-       for(uint i=0;i<num;i++)
-               carray[i]=getNewVar(encoder);
-}
-*/
-
-// THIS SHOULD NOT BE HERE
-/*
-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);
@@ -96,98 +69,3 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) {
 }
 
 
-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(encoder, getFunctionEncoding(element));
-                               break;
-                       default:
-                               continue;
-               }
-       }
-       
-       size = getSizeVectorBoolean(csolver->allBooleans);
-       for(uint i=0; i<size; i++){
-               Boolean* predicate = getVectorBoolean(csolver->allBooleans, i);
-               switch(GETBOOLEANTYPE(predicate)){
-                       case PREDICATEOP:
-                               naiveEncodeFunctionPredicate(encoder, getFunctionEncoding(predicate));
-                               break;
-                       default:
-                               continue;
-               } 
-       }
-}
-
-void naiveEncodeFunctionPredicate(NaiveEncoder* encoder, FunctionEncoding *This){
-       if(This->isFunction) {
-               ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN);
-               switch(This->type){
-                       case ENUMERATEIMPLICATIONS:
-                               naiveEncodeEnumeratedFunction(encoder, This);
-                               break;
-                       case CIRCUIT:
-                               naiveEncodeCircuitFunction(encoder, This);
-                               break;
-                       default:
-                               ASSERT(0);
-               }
-       }else {
-               ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP);
-               BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate;
-               //FIXME
-               
-       }
-}
-
-void naiveEncodeEnumeratedFunction(NaiveEncoder* encoder, FunctionEncoding* This){
-       ElementFunction* ef =(ElementFunction*)This->op.function;
-       switch(GETFUNCTIONTYPE(ef->function)){
-               case TABLEFUNC:
-                       naiveEncodeEnumTableFunc(encoder, ef);
-                       break;
-               case OPERATORFUNC:
-                       naiveEncodeEnumOperatingFunc(encoder, ef);
-                       break;
-               default:
-                       ASSERT(0);
-       } 
-}
-
-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);
-               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(NaiveEncoder* encoder, ElementFunction* This){
-       
-}
-
-
-void naiveEncodeCircuitFunction(NaiveEncoder* encoder, FunctionEncoding* This){
-       
-}
-
-void deleteNaiveEncoder(NaiveEncoder* encoder){
-       deleteVectorArrayConstraint(&encoder->vars);
-}

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index d3c409ce0df66ea402ceaedcf0eed6ad646076b1..800860c2e4e379b260e9b85d1429cf25fdd0dcfe 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -3,28 +3,15 @@
 #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, NaiveEncoder* encoder);
-void encode(CSolver* csolver);
+/**
+ *For now, This function just simply goes through elements/functions and 
+ *assigns a predefined Encoding to each of them 
+ * @param csolver
+ * @param encoder
+ */
+void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder);
 void baseBinaryIndexElementAssign(ElementEncoding *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 a7078455dae81c0f6d1f95b930f1dc8812e82e07..3c7d071a66221d25dffd679d5465284efe7cc769 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -82,8 +82,6 @@ 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/csolver.c b/src/csolver.c
index ccb19f013f6dad5999c9b1a18a8a8f0c69d6118a..5f330fd6112c70074522c17ac116739bf35746d6 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, Element **domains, uint numDomain, Element * range) {
+Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) {
        Table* table= allocTable(domains,numDomain,range);
        pushVectorTable(solver->allTables, table);
        return table;

diff --git a/src/csolver.h b/src/csolver.h
index 0bd2088831d9b68bf53e0793c5e88423f042e6cf..495d3864dca23ebdca90cab1f7eec52f485e3fa2 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, Element **domains, uint numDomain, Element * range);
+Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range);
 
 /** This function adds an input output relation to a table. */