GETBOOLEANTYPE(This)=BOOLEANVAR;
This->vtype=t;
This->var=E_NULL;
- allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+ initDefVectorBoolean(GETBOOLEANPARENTS(This));
return & This->base;
}
This->first=first;
This->second=second;
pushVectorBoolean(&order->constraints, &This->base);
- allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
+ initDefVectorBoolean(GETBOOLEANPARENTS(This));
return & This -> base;
}
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);
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;
}
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;
}
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);
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;
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;
}
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;
}
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;
}
CNFExpr *This=ourmalloc(sizeof(CNFExpr));
This->litSize=0;
This->isTrue=isTrue;
- allocInlineVectorLitVector(&This->clauses, 2);
+ initVectorLitVector(&This->clauses, 2);
initLitVector(&This->singletons);
return This;
}
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;
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;
}
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)); \
}
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() { \
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)); \
}
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;
}
This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
}
-void generateBinaryIndexEncodingVars(SATEncoder* encode, ElementEncoding* This);
-void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This);
-
#endif
#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++){
setInUseElement(This, i);
}
}
-
-
#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
*/
#include "orderencoding.h"
-void allocOrderEncoding(OrderEncoding * This, Order *order) {
+void initOrderEncoding(OrderEncoding * This, Order *order) {
This->type=ORDER_UNASSIGNED;
This->order=order;
}
Order *order;
};
-void allocOrderEncoding(OrderEncoding * This, Order *order);
+void initOrderEncoding(OrderEncoding * This, Order *order);
void deleteOrderEncoding(OrderEncoding *This);
#endif
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);
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);
#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 */
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;
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++){
/** 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);