Commit after resolving conflicts

diff --combined src/AST/boolean.c
index 0d3e8929d8d25d3e0131d70c0f86935f0d7688cc,1a46ccd6a118c32bbd680119af35a894e51b1052..831a20042cb0f507a48e28e81dc285449fa08455
--- 1/src/AST/boolean.c
--- 2/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@@ -1,11 -1,10 +1,12 @@@
  #include "boolean.h"
 +#include "structs.h"
 +#include "csolver.h"
  
  Boolean* allocBoolean(VarType t) {
        BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar));
        GETBOOLEANTYPE(tmp)=BOOLEANVAR;
        tmp->vtype=t;
+       tmp->var=NULL;
        return & tmp->base;
  }
  
@@@ -18,33 -17,6 +19,33 @@@ Boolean* allocBooleanOrder(Order* order
        return & tmp -> base;
  }
  
 +Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs){
 +    BooleanPredicate* bp = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
 +    GETBOOLEANTYPE(bp)= PREDICATEOP;
 +    bp->predicate=predicate;
 +    bp->inputs= allocVectorArrayElement (numInputs,inputs);
 +    return & bp->base;
 +}
 +
 +Boolean * allocBooleanLogic(LogicOp op, Boolean * left, Boolean* right){
 +    BooleanLogic* bl = (BooleanLogic*) ourmalloc(sizeof(BooleanLogic));
 +    GETBOOLEANTYPE(bl) = LOGICOP;
 +    bl->op=op;
 +    bl->left=left;
 +    bl->right=right;
 +    return &bl->base;
 +}
 +Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
 +    ASSERT(asize>=2);
 +    Boolean* boolean = allocBooleanLogic(op,array[0], array[1]);
 +    pushVectorBoolean(solver->allBooleans,boolean);
 +    for(uint i=2; i<asize; i++){
 +      boolean=allocBooleanLogic(op,boolean, array[i]);
 +      pushVectorBoolean(solver->allBooleans,boolean);
 +    }
 +    return boolean;
 +}
 +
  void deleteBoolean(Boolean * This) {
        ourfree(This);
  }

diff --combined src/AST/boolean.h
index fd59a21b213c6b631aae0b894b7f2745723566f0,860365f891b3b8edff3f628da504ad0dac2fc421..0222fc74e930c10e6cb93cb19051d633bf0ce6fb
--- 1/src/AST/boolean.h
--- 2/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@@ -3,7 -3,6 +3,7 @@@
  #include "classlist.h"
  #include "mymemory.h"
  #include "ops.h"
 +#include "structs.h"
  
  /** 
                This is a little sketchy, but apparently legit.
@@@ -25,6 -24,7 +25,7 @@@ struct BooleanOrder 
  struct BooleanVar {
        Boolean base;
        VarType vtype;
+       Constraint * var;
  };
  
  struct BooleanLogic {
@@@ -41,26 -41,10 +42,26 @@@ struct BooleanComp 
        Boolean * right;
  };
  
 +struct BooleanPredicate{
 +    Boolean base;
 +    Predicate * predicate;
 +    VectorElement* inputs;
 +};
  
  
  Boolean * allocBoolean(VarType t);
  Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second);
 +Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint numInputs);
 +Boolean * allocBooleanLogic(LogicOp op, Boolean * left, Boolean* right);
 +/**
 + * This function also save new boooleans to solver->allbooleans
 + * @param solver
 + * @param op
 + * @param array
 + * @param asize
 + * @return 
 + */
 +Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize);
  void deleteBoolean(Boolean * This);
  
  #endif

diff --combined src/AST/element.c
index 903256d61f7e5fd1555fe77aae066eebbe00c6a3,df29cfecc00e69d3a22ba7a4038e2b478a5e14f3..3746d250f10e748119f485fd14ecc082de9940d2
--- 1/src/AST/element.c
--- 2/src/AST/element.c
+++ b/src/AST/element.c
@@@ -1,22 -1,12 +1,23 @@@
  #include "element.h"
 -
 +#include "structs.h"
- 
- Element *allocElementSet(Set * s) {
-       ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet));
++//FIXME: ELEMENTSET?
+ Element *allocElement(Set * s) {
+       Element * tmp=(Element *)ourmalloc(sizeof(Element));
 +      GETELEMENTTYPE(tmp)= ELEMSET;
        tmp->set=s;
-       return &tmp->base;
+       tmp->encoding=NULL;
+       return tmp;
  }
  
 +Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus){
 +    ElementFunction* ef = (ElementFunction*) ourmalloc(sizeof(ElementFunction));
 +    GETELEMENTTYPE(ef)= ELEMFUNCRETURN;
 +    ef->function=function;
 +    ef->overflowstatus = overflowstatus;
 +    ef->Elements = allocVectorArrayElement(numArrays, array);
 +    return &ef->base;
 +}
 +
  void deleteElement(Element *This) {
        ourfree(This);
  }

diff --combined src/AST/element.h
index 4119b7d2f3dede9555fc7767167a3ae9882ac6af,91d19dba19fe6830d63334f2630ca594a08dde4d..0a23d8889d2a88d9a310934b3ea3788374cdfa8c
--- 1/src/AST/element.h
--- 2/src/AST/element.h
+++ b/src/AST/element.h
@@@ -2,28 -2,12 +2,31 @@@
  #define ELEMENT_H
  #include "classlist.h"
  #include "mymemory.h"
 +#include "ops.h"
 +#include "structs.h"
  
 +#define GETELEMENTTYPE(o) (((Element*)o)->type)
 +
++//FIXME:TALK ABOUT ELEMENT
  struct Element {
-       ElementType type;
++      ElementType type;
+       Set * set;
+       ElementEncoding * encoding;
  };
  
- Element * allocElementSet(Set *s);
 +struct ElementSet {
 +    Element base;
 +    Set * set;
 +};
 +
 +struct ElementFunction{
 +    Element base;
 +    Function * function;
 +    VectorElement* Elements;
 +    Boolean * overflowstatus;
 +};
 +
+ Element * allocElement(Set *s);
 +Element* allocElementFunction(Function * function, Element ** array, uint numArrays, Boolean * overflowstatus);
  void deleteElement(Element *This);
  #endif

diff --combined src/AST/ops.h
index adbef8dda52ede93bcce7c6ace8fdaca57eba28d,b330d1bedfd77a1a5cdc53508ada60dfb2bd51ad..9fa296630bc46bc415cf1af1a7d9c437dd8f67a0
--- 1/src/AST/ops.h
--- 2/src/AST/ops.h
+++ b/src/AST/ops.h
@@@ -1,6 -1,6 +1,6 @@@
  #ifndef OPS_H
  #define OPS_H
- enum LogicOp {AND, OR, NOT, XOR, IMPLIES};
+ enum LogicOp {L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES};
  typedef enum LogicOp LogicOp;
  
  enum ArithOp {ADD, SUB};
@@@ -23,12 -23,9 +23,12 @@@ typedef enum OrderType OrderType
  enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW};
  typedef enum OverFlowBehavior OverFlowBehavior;
  
 -enum BooleanType {ORDERCONST, BOOLEANVAR, LOGICOP, COMPARE};
 +enum BooleanType {ORDERCONST, BOOLEANVAR, LOGICOP, COMPARE, PREDICATEOP};
  typedef enum BooleanType BooleanType;
  
  enum FunctionType {TABLEFUNC, OPERATORFUNC};
  typedef enum FunctionType FunctionType;
 +
 +enum ElementType {ELEMSET, ELEMFUNCRETURN};
 +typedef enum ElementType ElementType;
  #endif

diff --combined src/classlist.h
index 14f43f80c57f857c7547a156fe796b3d30ab9054,237d529be962f45906e0fc00918247152f05e74b..3306ffe311b5e148e13824f9f5931109e7961704
--- 1/src/classlist.h
--- 2/src/classlist.h
+++ b/src/classlist.h
@@@ -18,6 -18,9 +18,9 @@@
  
  struct CSolver;
  typedef struct CSolver CSolver;
+ struct SATEncoder;
+ typedef struct SATEncoder SATEncoder;
+ 
  
  struct Constraint;
  typedef struct Constraint Constraint;
@@@ -26,7 -29,6 +29,7 @@@ typedef struct BooleanOrder BooleanOrde
  typedef struct BooleanVar BooleanVar;
  typedef struct BooleanLogic BooleanLogic;
  typedef struct BooleanComp BooleanComp;
 +typedef struct BooleanPredicate BooleanPredicate;
  
  struct Boolean;
  typedef struct Boolean Boolean;
@@@ -36,12 -38,8 +39,11 @@@ typedef struct IncrementalSolver Increm
  
  struct Set;
  typedef struct Set Set;
- 
  typedef struct Set MutableSet;
  
 +typedef struct ElementFunction ElementFunction;
 +typedef struct ElementSet ElementSet;
 +
  struct Element;
  typedef struct Element Element;
  
@@@ -66,6 -64,9 +68,9 @@@ typedef struct ElementEncoding ElementE
  struct FunctionEncoding;
  typedef struct FunctionEncoding FunctionEncoding;
  
+ struct OrderEncoding;
+ typedef struct OrderEncoding OrderEncoding;
+ 
  struct TableEntry;
  typedef struct TableEntry TableEntry;
  

diff --combined src/csolver.c
index 2ec12db45a0df213637b75f2c89b5e44cc8acc74,a7af8d304d1a66bcb3029967d992f6a0294a46ea..b35680caae5b7a7a8f29710d32cdc2cae4c3edbf
--- 1/src/csolver.c
--- 2/src/csolver.c
+++ b/src/csolver.c
@@@ -30,33 -30,38 +30,38 @@@ void deleteSolver(CSolver *This) 
        for(uint i=0;i<size;i++) {
                deleteBoolean(getVectorBoolean(This->allBooleans, i));
        }
- 
        deleteVectorBoolean(This->allBooleans);
  
        size=getSizeVectorSet(This->allSets);
        for(uint i=0;i<size;i++) {
                deleteSet(getVectorSet(This->allSets, i));
        }
- 
        deleteVectorSet(This->allSets);
  
        size=getSizeVectorElement(This->allElements);
        for(uint i=0;i<size;i++) {
                deleteElement(getVectorElement(This->allElements, i));
        }
+       deleteVectorElement(This->allElements);
+ 
        size=getSizeVectorTable(This->allTables);
        for(uint i=0;i<size;i++) {
                deleteTable(getVectorTable(This->allTables, i));
        }
+       deleteVectorTable(This->allTables);
+       
        size=getSizeVectorPredicate(This->allPredicates);
        for(uint i=0;i<size;i++) {
                deletePredicate(getVectorPredicate(This->allPredicates, i));
        }
+       deleteVectorPredicate(This->allPredicates);
+ 
        size=getSizeVectorOrder(This->allOrders);
        for(uint i=0;i<size;i++) {
                deleteOrder(getVectorOrder(This->allOrders, i));
        }
        deleteVectorOrder(This->allOrders);
+       
        size=getSizeVectorFunction(This->allFunctions);
        for(uint i=0;i<size;i++) {
                deleteFunction(getVectorFunction(This->allFunctions, i));
@@@ -94,7 -99,7 +99,7 @@@ uint64_t createUniqueItem(CSolver *solv
  }
  
  Element * getElementVar(CSolver *This, Set * set) {
-       Element * element=allocElementSet(set);
+       Element * element=allocElement(set);
        pushVectorElement(This->allElements, element);
        return element;
  }
@@@ -134,19 -139,15 +139,19 @@@ Function * completeTable(CSolver *solve
  }
  
  Element * applyFunction(CSolver *solver, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
 -      return NULL;
 +    Element* element= allocElementFunction(function,array,numArrays,overflowstatus);
 +    pushVectorElement(solver->allElements, element);
 +    return element;
  }
  
  Boolean * applyPredicate(CSolver *solver, Predicate * predicate, Element ** inputs, uint numInputs) {
 -      return NULL;
 +    Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
 +    pushVectorBoolean(solver->allBooleans, boolean);
 +    return boolean;
  }
  
 -Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array) {
 -      return NULL;
 +Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array, uint asize) {
 +    return allocBooleanLogicArray(solver, op, array, asize);
  }
  
  void addBoolean(CSolver *This, Boolean * constraint) {