From 26d02c400dd077f6aa1cc3aecbd021d4b139ca9c Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 11 Jul 2017 12:44:01 -0700 Subject: [PATCH] Rename some functions and cleanup --- src/AST/boolean.c | 12 +++--- src/AST/element.c | 6 +-- src/AST/function.c | 2 +- src/AST/order.c | 4 +- src/AST/predicate.c | 2 +- src/AST/table.c | 4 +- src/Backend/cnfexpr.c | 4 +- src/Backend/constraint.c | 4 +- src/Collections/array.h | 6 +-- src/Collections/vector.h | 16 ++++---- src/Encoders/elementencoding.h | 6 +-- src/Encoders/naiveencoder.c | 4 +- src/Encoders/naiveencoder.h | 5 +-- src/Encoders/orderencoding.c | 2 +- src/Encoders/orderencoding.h | 2 +- src/Test/buildconstraints.c | 6 +-- src/csolver.c | 74 +++++++++++++++++----------------- src/csolver.h | 2 +- 18 files changed, 78 insertions(+), 83 deletions(-) diff --git a/src/AST/boolean.c b/src/AST/boolean.c index 428b5e2..622c8a3 100644 --- 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;iinputs, 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 8855194..f9b7579 100644 --- 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;idomainencoding, (Element *) This); diff --git a/src/AST/function.c b/src/AST/function.c index 2530e93..1aba4b7 100644 --- 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 7e2b187..1499dcb 100644 --- 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 ce446f2..19e1597 100644 --- 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 804d7ac..72d23dd 100644 --- 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 dbbd93f..c2a5bc9 100644 --- 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 7f65364..843f168 100644 --- 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 73d0c32..19a22b3 100644 --- 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 e0ebebd..650f33d 100644 --- 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 797f301..af9696f 100644 --- 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 5b38732..5560526 100644 --- a/src/Encoders/naiveencoder.c +++ b/src/Encoders/naiveencoder.c @@ -13,7 +13,7 @@ #include "order.h" #include - +//BRIAN: MAKE FOLLOW TREE STRUCTURE void naiveEncodingDecision(CSolver* csolver){ uint size = getSizeVectorElement(csolver->allElements); for(uint i=0; itype=ORDER_UNASSIGNED; This->order=order; } diff --git a/src/Encoders/orderencoding.h b/src/Encoders/orderencoding.h index a101ea1..f408d66 100644 --- 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 222d4a1..c4440a7 100644 --- 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 04e3d10..40490d5 100644 --- 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 bd90bf3..827609c 100644 --- 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); -- 2.34.1