Rename some functions and cleanup

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 428b5e2fe6b24456a97b2179638087ba314159f8..622c8a338ca83df1c21eee3eaec19bb4dccfc8bf 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -9,7 +9,7 @@ Boolean* allocBooleanVar(VarType t) {
        GETBOOLEANTYPE(This)=BOOLEANVAR;
        This->vtype=t;
        This->var=E_NULL;
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
        return & This->base;
 }
 
@@ -20,7 +20,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        This->first=first;
        This->second=second;
        pushVectorBoolean(&order->constraints, &This->base);
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
        return & This -> base;
 }
 
@@ -28,8 +28,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
        BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
        GETBOOLEANTYPE(This)= PREDICATEOP;
        This->predicate=predicate;
-       allocInlineArrayInitElement(&This->inputs, inputs, numInputs);
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initArrayInitElement(&This->inputs, inputs, numInputs);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
 
        for(uint i=0;i<numInputs;i++) {
                pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
@@ -41,8 +41,8 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
        BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
-       allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
-       allocInlineArrayInitBoolean(&This->inputs, array, asize);
+       initDefVectorBoolean(GETBOOLEANPARENTS(This));
+       initArrayInitBoolean(&This->inputs, array, asize);
        pushVectorBoolean(solver->allBooleans, (Boolean *) This);
        return & This->base;
 }

diff --git a/src/AST/element.c b/src/AST/element.c
index 8855194e934edac8c9a6912fbb07ad39781bfd11..f9b7579a2cc8d1693f6c51bb8228ad0943ba3412 100644 (file)
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -9,7 +9,7 @@ Element *allocElementSet(Set * s) {
        ElementSet * This=(ElementSet *)ourmalloc(sizeof(ElementSet));
        GETELEMENTTYPE(This)= ELEMSET;
        This->set=s;
-       allocInlineDefVectorASTNode(GETELEMENTPARENTS(This));
+       initDefVectorASTNode(GETELEMENTPARENTS(This));
        initElementEncoding(&This->encoding, (Element *) This);
        return &This->base;
 }
@@ -19,8 +19,8 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
        GETELEMENTTYPE(This)= ELEMFUNCRETURN;
        This->function=function;
        This->overflowstatus = overflowstatus;
-       allocInlineArrayInitElement(&This->inputs, array, numArrays);
-       allocInlineDefVectorASTNode(GETELEMENTPARENTS(This));
+       initArrayInitElement(&This->inputs, array, numArrays);
+       initDefVectorASTNode(GETELEMENTPARENTS(This));
        for(uint i=0;i<numArrays;i++)
                pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) This);
        initElementEncoding(&This->domainencoding, (Element *) This);

diff --git a/src/AST/function.c b/src/AST/function.c
index 2530e93663494e1c391815441abd1d27fa3b2412..1aba4b78050a23b0c588a2d27df8b4da470434f6 100644 (file)
--- a/src/AST/function.c
+++ b/src/AST/function.c
@@ -6,7 +6,7 @@
 Function* allocFunctionOperator(ArithOp op, Set ** domain, uint numDomain, Set * range, OverFlowBehavior overflowbehavior) {
        FunctionOperator* This = (FunctionOperator*) ourmalloc(sizeof(FunctionOperator));
        GETFUNCTIONTYPE(This)=OPERATORFUNC;
-       allocInlineArrayInitSet(&This->domains, domain, numDomain);
+       initArrayInitSet(&This->domains, domain, numDomain);
        This->op=op;
        This->overflowbehavior = overflowbehavior;
        This->range=range;

diff --git a/src/AST/order.c b/src/AST/order.c
index 7e2b1877c426af69421278e7bcf394763245e5e9..1499dcb16be20425d260c1f9db2b1341a08055f7 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -6,9 +6,9 @@
 Order* allocOrder(OrderType type, Set * set){
        Order* This = (Order*)ourmalloc(sizeof(Order));
        This->set=set;
-       allocInlineDefVectorBoolean(& This->constraints);
+       initDefVectorBoolean(& This->constraints);
        This->type=type;
-       allocOrderEncoding(& This->order, This);
+       initOrderEncoding(& This->order, This);
        This->boolsToConstraints = NULL;
        return This;
 }

diff --git a/src/AST/predicate.c b/src/AST/predicate.c
index ce446f2af23ee5cce2183550a0eb5fc4ec204c85..19e159760ddc897931494f1782826c64319489c3 100644 (file)
--- a/src/AST/predicate.c
+++ b/src/AST/predicate.c
@@ -5,7 +5,7 @@
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){
        PredicateOperator* This = ourmalloc(sizeof(PredicateOperator));
        GETPREDICATETYPE(This)=OPERATORPRED;
-       allocInlineArrayInitSet(&This->domains, domain, numDomain);
+       initArrayInitSet(&This->domains, domain, numDomain);
        This->op=op;
        return &This->base;
 }

diff --git a/src/AST/table.c b/src/AST/table.c
index 804d7ac8be9dc094fba4a41dd80f4c54e3bbd6b0..72d23ddf7f1f9b8d06427f072e9ae7dcaec8fe56 100644 (file)
--- a/src/AST/table.c
+++ b/src/AST/table.c
@@ -7,8 +7,8 @@
 
 Table * allocTable(Set **domains, uint numDomain, Set * range){
        Table* This = (Table*) ourmalloc(sizeof(Table));
-       allocInlineArrayInitSet(&This->domains, domains, numDomain);
-       allocInlineDefVectorTableEntry(&This->entries);
+       initArrayInitSet(&This->domains, domains, numDomain);
+       initDefVectorTableEntry(&This->entries);
        This->range =range;
        return This;
 }

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index dbbd93f53d51e6143db4a1bdbda6bf1102c2f4df..c2a5bc9f9d3769c8592419e7069c358ab1f6e2db 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -117,7 +117,7 @@ CNFExpr * allocCNFExprBool(bool isTrue) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=0;
        This->isTrue=isTrue;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        return This;
 }
@@ -126,7 +126,7 @@ CNFExpr * allocCNFExprLiteral(Literal l) {
        CNFExpr *This=ourmalloc(sizeof(CNFExpr));
        This->litSize=1;
        This->isTrue=false;
-       allocInlineVectorLitVector(&This->clauses, 2);
+       initVectorLitVector(&This->clauses, 2);
        initLitVector(&This->singletons);
        addLiteralLitVector(&This->singletons, l);
        return This;

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 7f65364f357945557178915547e194ede587a797..843f1685c48c99779d118c5037d42a68d960e83b 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -56,8 +56,8 @@ CNF * createCNF() {
        cnf->size=0;
        cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
        cnf->enableMatching=true;
-       allocInlineDefVectorEdge(& cnf->constraints);
-       allocInlineDefVectorEdge(& cnf->args);
+       initDefVectorEdge(& cnf->constraints);
+       initDefVectorEdge(& cnf->args);
        cnf->solver=allocIncrementalSolver();
        return cnf;
 }

diff --git a/src/Collections/array.h b/src/Collections/array.h
index 73d0c32124a7cb873724179c2001aeeaa90103e4..19a22b3cdb7c947a70204f05623dfd53aa9a8212 100644 (file)
--- a/src/Collections/array.h
+++ b/src/Collections/array.h
@@ -37,12 +37,12 @@
        static inline void deleteInlineArray ## name(Array ## name *This) {                                     \
                ourfree(This->array);                                                                                                                                                                                           \
        }                                                                                                                                                                                                                                                                                       \
-       static inline void allocInlineArray ## name(Array ## name * This, uint size) {                  \
+       static inline void initArray ## name(Array ## name * This, uint size) {                 \
                This->size = size;                                                                                                                                                                                                      \
                This->array = (type *) ourcalloc(1, sizeof(type) * size);                                               \
        }                                                                                                                                                                                                                                                                                       \
-       static inline void allocInlineArrayInit ## name(Array ## name * This, type *array, uint size) { \
-               allocInlineArray ##name(This, size);                                                                                                                            \
+       static inline void initArrayInit ## name(Array ## name * This, type *array, uint size) { \
+               initArray ##name(This, size);                                                                                                                                                           \
                memcpy(This->array, array, size * sizeof(type));                                                                                \
        }
 

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index e0ebebd035ac76afe61573a902f184109a8d69c6..650f33dc8352b3cea81983de89eb53af0a0054e7 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -23,9 +23,9 @@
        void clearVector ## name(Vector ## name *vector);                     \
        void deleteVectorArray ## name(Vector ## name *vector);                                                         \
        type * exposeArray ## name(Vector ## name * vector);                                                                    \
-       void allocInlineVector ## name(Vector ## name * vector, uint capacity); \
-       void allocInlineDefVector ## name(Vector ## name * vector);                                             \
-       void allocInlineVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
+       void initVector ## name(Vector ## name * vector, uint capacity); \
+       void initDefVector ## name(Vector ## name * vector);                                            \
+       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
 #define VectorImpl(name, type, defcap)                                  \
        Vector ## name * allocDefVector ## name() {                           \
@@ -91,16 +91,16 @@
        void deleteVectorArray ## name(Vector ## name *vector) {                                                        \
                ourfree(vector->array);                                             \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
+       void initVector ## name(Vector ## name * vector, uint capacity) { \
                vector->size = 0;                                                      \
                vector->capacity = capacity;                                                                                                                                                                                    \
                vector->array = (type *) ourmalloc(sizeof(type) * capacity);                            \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineDefVector ## name(Vector ## name * vector) {                                    \
-               allocInlineVector ## name(vector, defcap);                                                                                                      \
+       void initDefVector ## name(Vector ## name * vector) {                                   \
+               initVector ## name(vector, defcap);                                                                                                     \
        }                                                                                                                                                                                                                                                                                       \
-       void allocInlineVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {     \
-               allocInlineVector ##name(vector, capacity);                                                                                                     \
+       void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {    \
+               initVector ##name(vector, capacity);                                                                                                    \
                vector->size=capacity;                                                                                                                                                                                  \
                memcpy(vector->array, array, capacity * sizeof(type));  \
        }

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 797f301c6ca3d67284d5b6d0d356045a374e703f..af9696f691e06ead7be9555bfce0e0e6bb3c95e8 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -25,6 +25,9 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
+void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
+void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
+
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
        return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
 }
@@ -33,7 +36,4 @@ static inline void setInUseElement(ElementEncoding *This, uint offset) {
        This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
 }
 
-void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
-
 #endif

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 5b38732e6382e337f83b08bdcbb17d2138a3c874..5560526c2e5f9aec00d64b445722bc44ffca38ef 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -13,7 +13,7 @@
 #include "order.h"
 #include <strings.h>
 
-
+//BRIAN: MAKE FOLLOW TREE STRUCTURE
 void naiveEncodingDecision(CSolver* csolver){
        uint size = getSizeVectorElement(csolver->allElements);
        for(uint i=0; i<size; i++){
@@ -57,5 +57,3 @@ void baseBinaryIndexElementAssign(ElementEncoding *This) {
                setInUseElement(This, i);
        }
 }
-
-

diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
index 182e3da1027742255ebfd91755c77c51a75ff9bd..2b9fb87516c302ea1214f1c2a8958dea5a4e7ce8 100644 (file)
--- a/src/Encoders/naiveencoder.h
+++ b/src/Encoders/naiveencoder.h
@@ -3,11 +3,8 @@
 #include "classlist.h"
 #include "structs.h"
 
-
-
 /**
- *For now, This function just simply goes through elements/functions and 
- *assigns a predefined Encoding to each of them 
+ * The NaiveEncoder assigns a predefined Encoding to each Element and Function.
  * @param csolver
  * @param encoder
  */

diff --git a/src/Encoders/orderencoding.c b/src/Encoders/orderencoding.c
index 161704b5228978808eface4698b65af763afa742..1f1d93f514b8bc133f7ef12a855449a809fba402 100644 (file)
--- a/src/Encoders/orderencoding.c
+++ b/src/Encoders/orderencoding.c
@@ -1,6 +1,6 @@
 #include "orderencoding.h"
 
-void allocOrderEncoding(OrderEncoding * This, Order *order) {
+void initOrderEncoding(OrderEncoding * This, Order *order) {
        This->type=ORDER_UNASSIGNED;
        This->order=order;
 }

diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h
index a101ea105699fa2571fe7e0cdb53d41b18b1ee7f..f408d665dd405b208ff0f3be4e4e39e2b6e30fcc 100644 (file)
--- a/src/Encoders/orderencoding.h
+++ b/src/Encoders/orderencoding.h
@@ -13,7 +13,7 @@ struct OrderEncoding {
        Order *order;
 };
 
-void allocOrderEncoding(OrderEncoding * This, Order *order);
+void initOrderEncoding(OrderEncoding * This, Order *order);
 void deleteOrderEncoding(OrderEncoding *This);
 
 #endif

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 222d4a11c74aec994f48ca90dc3e512d4c196656..c4440a7aade9bf54036b1c1dd8392e6cf687f45b 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -10,10 +10,10 @@ int main(int numargs, char ** argv) {
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
        Boolean * b=applyPredicate(solver, equals, inputs, 2);
-       addBoolean(solver, b);
+       addConstraint(solver, b);
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
-       addBoolean(solver, oc);
+       addConstraint(solver, oc);
                
        uint64_t set2[] = {2, 3};
        Set* rangef1 = createSet(solver, 1, set2, 2);
@@ -37,7 +37,7 @@ int main(int numargs, char ** argv) {
        Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
        Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
-       addBoolean(solver, pred);
+       addConstraint(solver, pred);
        
        startEncoding(solver);
        deleteSolver(solver);

diff --git a/src/csolver.c b/src/csolver.c
index 04e3d1070fe75fd917a599399ea0e95eac668ae3..40490d535c4ddc7723fa99cd6e7470b029e7cc8a 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -10,16 +10,16 @@
 #include "satencoder.h"
 
 CSolver * allocCSolver() {
-       CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver));
-       tmp->constraints=allocDefVectorBoolean();
-       tmp->allBooleans=allocDefVectorBoolean();
-       tmp->allSets=allocDefVectorSet();
-       tmp->allElements=allocDefVectorElement();
-       tmp->allPredicates = allocDefVectorPredicate();
-       tmp->allTables = allocDefVectorTable();
-       tmp->allOrders = allocDefVectorOrder();
-       tmp->allFunctions = allocDefVectorFunction();
-       return tmp;
+       CSolver * This=(CSolver *) ourmalloc(sizeof(CSolver));
+       This->constraints=allocDefVectorBoolean();
+       This->allBooleans=allocDefVectorBoolean();
+       This->allSets=allocDefVectorSet();
+       This->allElements=allocDefVectorElement();
+       This->allPredicates = allocDefVectorPredicate();
+       This->allTables = allocDefVectorTable();
+       This->allOrders = allocDefVectorOrder();
+       This->allFunctions = allocDefVectorFunction();
+       return This;
 }
 
 /** This function tears down the solver and the entire AST */
@@ -89,11 +89,11 @@ MutableSet * createMutableSet(CSolver * This, VarType type) {
        return set;
 }
 
-void addItem(CSolver *solver, MutableSet * set, uint64_t element) {
+void addItem(CSolver *This, MutableSet * set, uint64_t element) {
        addElementMSet(set, element);
 }
 
-uint64_t createUniqueItem(CSolver *solver, MutableSet * set) {
+uint64_t createUniqueItem(CSolver *This, MutableSet * set) {
        uint64_t element=set->low++;
        addElementMSet(set, element);
        return element;
@@ -105,76 +105,76 @@ Element * getElementVar(CSolver *This, Set * set) {
        return element;
 }
 
-Boolean * getBooleanVar(CSolver *solver, VarType type) {
+Boolean * getBooleanVar(CSolver *This, VarType type) {
        Boolean* boolean= allocBooleanVar(type);
-       pushVectorBoolean(solver->allBooleans, boolean);
+       pushVectorBoolean(This->allBooleans, boolean);
        return boolean;
 }
 
-Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior) {
+Function * createFunctionOperator(CSolver *This, ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior) {
        Function* function = allocFunctionOperator(op, domain, numDomain, range, overflowbehavior);
-       pushVectorFunction(solver->allFunctions, function);
+       pushVectorFunction(This->allFunctions, function);
        return function;
 }
 
-Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) {
+Predicate * createPredicateOperator(CSolver *This, CompOp op, Set ** domain, uint numDomain) {
        Predicate* predicate= allocPredicateOperator(op, domain,numDomain);
-       pushVectorPredicate(solver->allPredicates, predicate);
+       pushVectorPredicate(This->allPredicates, predicate);
        return predicate;
 }
 
-Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range) {
+Table * createTable(CSolver *This, Set **domains, uint numDomain, Set * range) {
        Table* table= allocTable(domains,numDomain,range);
-       pushVectorTable(solver->allTables, table);
+       pushVectorTable(This->allTables, table);
        return table;
 }
 
-void addTableEntry(CSolver *solver, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) {
+void addTableEntry(CSolver *This, Table* table, uint64_t* inputs, uint inputSize, uint64_t result) {
        addNewTableEntry(table,inputs, inputSize,result);
 }
 
-Function * completeTable(CSolver *solver, Table * table) {
+Function * completeTable(CSolver *This, Table * table) {
        Function* function = allocFunctionTable(table);
-       pushVectorFunction(solver->allFunctions,function);
+       pushVectorFunction(This->allFunctions,function);
        return function;
 }
 
-Element * applyFunction(CSolver *solver, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
+Element * applyFunction(CSolver *This, Function * function, Element ** array, uint numArrays, Boolean * overflowstatus) {
        Element* element= allocElementFunction(function,array,numArrays,overflowstatus);
-       pushVectorElement(solver->allElements, element);
+       pushVectorElement(This->allElements, element);
        return element;
 }
 
-Boolean * applyPredicate(CSolver *solver, Predicate * predicate, Element ** inputs, uint numInputs) {
+Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs) {
        Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs);
-       pushVectorBoolean(solver->allBooleans, boolean);
+       pushVectorBoolean(This->allBooleans, boolean);
        return boolean;
 }
 
-Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array, uint asize) {
-       return allocBooleanLogicArray(solver, op, array, asize);
+Boolean * applyLogicalOperation(CSolver *This, LogicOp op, Boolean ** array, uint asize) {
+       return allocBooleanLogicArray(This, op, array, asize);
 }
 
-void addBoolean(CSolver *This, Boolean * constraint) {
+void addConstraint(CSolver *This, Boolean * constraint) {
        pushVectorBoolean(This->constraints, constraint);
 }
 
-Order * createOrder(CSolver *solver, OrderType type, Set * set) {
+Order * createOrder(CSolver *This, OrderType type, Set * set) {
        Order* order = allocOrder(type, set);
-       pushVectorOrder(solver->allOrders, order);
+       pushVectorOrder(This->allOrders, order);
        return order;
 }
 
-Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64_t second) {
+Boolean * orderConstraint(CSolver *This, Order * order, uint64_t first, uint64_t second) {
        Boolean* constraint = allocBooleanOrder(order, first, second);
-       pushVectorBoolean(solver->allBooleans,constraint);
+       pushVectorBoolean(This->allBooleans,constraint);
        return constraint;
 }
 
-void startEncoding(CSolver* solver){
-       naiveEncodingDecision(solver);
+void startEncoding(CSolver* This){
+       naiveEncodingDecision(This);
        SATEncoder* satEncoder = allocSATEncoder();
-       encodeAllSATEncoder(solver, satEncoder);
+       encodeAllSATEncoder(This, satEncoder);
        int result= solveCNF(satEncoder->cnf);
        model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);
        for(uint i=1; i<=satEncoder->cnf->solver->solutionsize; i++){

diff --git a/src/csolver.h b/src/csolver.h
index bd90bf3054a5cbf85e4b506097391c2786e51d7d..827609c94abe3094f0d70c93add5e89949f44ec7 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -104,7 +104,7 @@ Boolean * applyLogicalOperation(CSolver *, LogicOp op, Boolean ** array, uint as
 /** This function adds a boolean constraint to the set of constraints
     to be satisfied */
 
-void addBoolean(CSolver *, Boolean * constraint);
+void addConstraint(CSolver *, Boolean * constraint);
 
 /** This function instantiates an order of type type over the set set. */
 Order * createOrder(CSolver *, OrderType type, Set * set);