src/bin/
src/lib_cons_comp.so
/src/mymemory.cc
+.*
+*.dSYM
\ No newline at end of file
BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
GETBOOLEANTYPE(This)= PREDICATEOP;
This->predicate=predicate;
- This->inputs= allocVectorArrayElement (numInputs,inputs);
+ allocInlineArrayInitElement(&This->inputs, inputs, numInputs);
allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
for(uint i=0;i<numInputs;i++) {
pushVectorASTNode(GETELEMENTPARENTS(inputs[i]), (ASTNode *)This);
}
+ initPredicateEncoding(&This->encoding, (Boolean *) This);
+
return & This->base;
}
Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
- This->array = ourmalloc(sizeof(Boolean *)*asize);
- memcpy(This->array, array, sizeof(Boolean *)*asize);
- for(uint i=0;i<asize;i++) {
- pushVectorBoolean(GETBOOLEANPARENTS(array[i]), (Boolean *)This);
- }
+ allocInlineArrayInitBoolean(&This->inputs, array, asize);
pushVectorBoolean(solver->allBooleans, (Boolean *) This);
return & This->base;
}
void deleteBoolean(Boolean * This) {
switch(GETBOOLEANTYPE(This)){
- case PREDICATEOP:
- deleteVectorArrayElement( ((BooleanPredicate*)This)->inputs );
- break;
- default:
- break;
+ case PREDICATEOP: {
+ BooleanPredicate *bp=(BooleanPredicate *)This;
+ deleteInlineArrayElement(& bp->inputs );
+ deleteFunctionEncoding(& bp->encoding);
+ break;
+ }
+ default:
+ break;
}
deleteVectorArrayBoolean(GETBOOLEANPARENTS(This));
ourfree(This);
#include "ops.h"
#include "structs.h"
#include "astnode.h"
+#include "functionencoding.h"
/**
This is a little sketchy, but apparently legit.
struct BooleanLogic {
Boolean base;
LogicOp op;
- Boolean ** array;
- uint numArray;
+ ArrayBoolean inputs;
};
struct BooleanPredicate {
Boolean base;
Predicate * predicate;
- VectorElement* inputs;
+ FunctionEncoding encoding;
+ ArrayElement inputs;
};
Boolean * allocBoolean(VarType t);
ElementSet * tmp=(ElementSet *)ourmalloc(sizeof(ElementSet));
GETELEMENTTYPE(tmp)= ELEMSET;
tmp->set=s;
- tmp->encoding=NULL;
allocInlineDefVectorASTNode(GETELEMENTPARENTS(tmp));
+ initElementEncoding(&tmp->encoding, (Element *) tmp);
return &tmp->base;
}
GETELEMENTTYPE(tmp)= ELEMFUNCRETURN;
tmp->function=function;
tmp->overflowstatus = overflowstatus;
- tmp->Elements = allocVectorArrayElement(numArrays, array);
+ allocInlineArrayInitElement(&tmp->inputs, array, numArrays);
allocInlineDefVectorASTNode(GETELEMENTPARENTS(tmp));
for(uint i=0;i<numArrays;i++)
pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) tmp);
+ initElementEncoding(&tmp->domainencoding, (Element *) tmp);
+ initFunctionEncoding(&tmp->functionencoding, (Element *) tmp);
return &tmp->base;
}
void deleteElement(Element *This) {
+ switch(GETELEMENTTYPE(This)) {
+ case ELEMFUNCRETURN: {
+ ElementFunction *ef = (ElementFunction *) This;
+ deleteInlineArrayElement(&ef->inputs);
+ deleteElementEncoding(&ef->domainencoding);
+ deleteFunctionEncoding(&ef->functionencoding);
+ break;
+ }
+ case ELEMSET: {
+ ElementSet *es = (ElementSet *) This;
+ deleteElementEncoding(&es->encoding);
+ break;
+ }
+ default:
+ ;
+ }
deleteVectorArrayASTNode(GETELEMENTPARENTS(This));
+
ourfree(This);
}
#include "mymemory.h"
#include "structs.h"
#include "astnode.h"
+#include "functionencoding.h"
+#include "elementencoding.h"
#define GETELEMENTTYPE(o) GETASTNODETYPE(o)
#define GETELEMENTPARENTS(o) (&((Element*)o)->parents)
struct ElementSet {
Element base;
Set * set;
- ElementEncoding * encoding;
+ ElementEncoding encoding;
};
struct ElementFunction {
Element base;
Function * function;
- VectorElement* Elements;
+ ArrayElement inputs;
Boolean * overflowstatus;
+ FunctionEncoding functionencoding;
+ ElementEncoding domainencoding;
};
Element * allocElementSet(Set *s);
Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior){
FunctionOperator* This = (FunctionOperator*) ourmalloc(sizeof(FunctionOperator));
GETFUNCTIONTYPE(This)=OPERATORFUNC;
- This->numDomains=numDomain;
- This->domains = ourmalloc(numDomain * sizeof(Set *));
- memcpy(This->domains, domain, numDomain * sizeof(Set *));
+ allocInlineArrayInitSet(&This->domains, domain, numDomain);
This->op=op;
This->overflowbehavior = overflowbehavior;
This->range=range;
case TABLEFUNC:
break;
case OPERATORFUNC:
- ourfree(((FunctionOperator*) This)->domains);
+ deleteInlineArraySet(&((FunctionOperator*) This)->domains);
break;
default:
ASSERT(0);
struct FunctionOperator {
Function base;
ArithOp op;
- uint numDomains;
- Set ** domains;
+ ArraySet domains;
Set * range;
OverFlowBehavior overflowbehavior;
};
enum PredicateType {TABLEPRED, OPERATORPRED};
typedef enum PredicateType PredicateType;
-enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, TABLEPREDICATEOP, ELEMSET, ELEMFUNCRETURN};
+enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, ELEMSET, ELEMFUNCRETURN};
typedef enum ASTNodeType ASTNodeType;
#endif
Order* allocOrder(OrderType type, Set * set){
- Order* order = (Order*)ourmalloc(sizeof(Order));
- order->set=set;
- order->constraints = allocDefVectorBoolean();
- order->type=type;
- return order;
+ Order* order = (Order*)ourmalloc(sizeof(Order));
+ order->set=set;
+ allocInlineDefVectorBoolean(& order->constraints);
+ order->type=type;
+ return order;
}
void deleteOrder(Order* order){
- uint size = getSizeVectorBoolean( order->constraints );
- for(uint i=0; i<size; i++){
- deleteBoolean( getVectorBoolean(order->constraints, i) );
- }
- deleteSet( order->set);
- ourfree(order);
-}
\ No newline at end of file
+ deleteVectorArrayBoolean(& order->constraints);
+ ourfree(order);
+}
struct Order {
OrderType type;
Set * set;
- VectorBoolean* constraints;
+ VectorBoolean constraints;
};
Order* allocOrder(OrderType type, Set * set);
#include "predicate.h"
-#include "structs.h"
-
Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain){
PredicateOperator* predicate = ourmalloc(sizeof(PredicateOperator));
GETPREDICATETYPE(predicate)=OPERATORPRED;
- predicate->numDomains=numDomain;
- predicate->domains = ourmalloc(numDomain * sizeof(Set *));
- memcpy(predicate->domains, domain, numDomain * sizeof(Set *));
+ allocInlineArrayInitSet(&predicate->domains, domain, numDomain);
predicate->op=op;
return &predicate->base;
}
switch(GETPREDICATETYPE(predicate)) {
case OPERATORPRED: {
PredicateOperator * operpred=(PredicateOperator *) predicate;
- ourfree(operpred->domains);
+ deleteInlineArraySet(&operpred->domains);
break;
}
case TABLEPRED: {
#include "classlist.h"
#include "mymemory.h"
#include "ops.h"
-
+#include "structs.h"
#define GETPREDICATETYPE(o) (((Predicate *)(o))->type)
struct PredicateOperator {
Predicate base;
CompOp op;
- Set ** domains;
- uint numDomains;
+ ArraySet domains;
};
struct PredicateTable {
Table * allocTable(Set **domains, uint numDomain, Set * range){
Table* table = (Table*) ourmalloc(sizeof(Table));
- table->numDomains=numDomain;
- table->domains = ourmalloc(numDomain*sizeof(Set *));
- memcpy(table->domains, domains, numDomain * sizeof(Set *));
+ allocInlineArrayInitSet(&table->domains, domains, numDomain);
+ allocInlineDefVectorTableEntry(&table->entries);
table->range =range;
- return table;
+ return table;
}
void addNewTableEntry(Table* table, uint64_t* inputs, uint inputSize, uint64_t result){
ASSERT(getSizeVectorSet( table->domains) == inputSize);
- pushVectorTableEntry(table->entries, allocTableEntry(inputs, inputSize, result));
+ pushVectorTableEntry(&table->entries, allocTableEntry(inputs, inputSize, result));
}
void deleteTable(Table* table){
- ourfree(table->domains);
- uint size = getSizeVectorTableEntry(table->entries);
- for(uint i=0; i<size; i++){
- deleteTableEntry(getVectorTableEntry(table->entries, i));
- }
- deleteVectorTableEntry(table->entries);
- ourfree(table);
+ deleteInlineArraySet(&table->domains);
+ uint size = getSizeVectorTableEntry(&table->entries);
+ for(uint i=0; i<size; i++){
+ deleteTableEntry(getVectorTableEntry(&table->entries, i));
+ }
+ deleteVectorArrayTableEntry(&table->entries);
+ ourfree(table);
}
#include "structs.h"
struct Table {
- Set ** domains;
+ ArraySet domains;
Set * range;
- uint numDomains;
- VectorTableEntry* entries;
+ VectorTableEntry entries;
};
Table * allocTable(Set **domains, uint numDomain, Set * range);
#include "tableentry.h"
+#include <string.h>
TableEntry* allocTableEntry(uint64_t* inputs, uint inputSize, uint64_t result){
- TableEntry* te = (TableEntry*) ourmalloc(sizeof(TableEntry)+inputSize*sizeof(uint64_t));
- te->output=result;
- for(int i=0; i<inputSize; i++){
- te->inputs[i]=inputs[i];
- }
- return te;
+ TableEntry* te = (TableEntry*) ourmalloc(sizeof(TableEntry)+inputSize*sizeof(uint64_t));
+ te->output=result;
+ memcpy(te->inputs, inputs, inputSize * sizeof(uint64_t));
+ return te;
}
void deleteTableEntry(TableEntry* tableEntry){
- ourfree(tableEntry);
-}
\ No newline at end of file
+ ourfree(tableEntry);
+}
void deleteConstraint(Constraint *);
void printConstraint(Constraint * c);
void dumpConstraint(Constraint * c, IncrementalSolver *solver);
-inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
+static inline uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;}
VectorConstraint * simplify(Constraint * c);
-inline CType getType(Constraint * c) {return c->type;}
-inline bool isFalse(Constraint * c) {return c->type==FALSE;}
-inline bool isTrue(Constraint * c) {return c->type==TRUE;}
+static inline CType getType(Constraint * c) {return c->type;}
+static inline bool isFalse(Constraint * c) {return c->type==FALSE;}
+static inline bool isTrue(Constraint * c) {return c->type==TRUE;}
void internalfreeConstraint(Constraint * c);
void freerecConstraint(Constraint * c);
Constraint * cloneConstraint(Constraint * c);
-inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
+static inline void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;}
Constraint *negateConstraint(Constraint * c);
extern Constraint ctrue;
#include "csolver.h"
#include "boolean.h"
#include "constraint.h"
+#include "common.h"
SATEncoder * allocSATEncoder() {
SATEncoder *This=ourmalloc(sizeof (SATEncoder));
return encodeVarSATEncoder(This, (BooleanVar *) constraint);
case LOGICOP:
return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
+ case PREDICATEOP:
+ return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
+ default:
+ model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
+ exit(-1);
}
}
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
- return NULL;
-}
-
Constraint * getNewVarSATEncoder(SATEncoder *This) {
Constraint * var=allocVarConstraint(VAR, This->varcount);
Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
}
Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
- /*
- Constraint *left=encodeConstraintSATEncoder(This, constraint->left);
- Constraint *right=NULL;
- if (constraint->right!=NULL)
- right=encodeConstraintSATEncoder(This, constraint->right);
+ Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
+ for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
+ array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
+
switch(constraint->op) {
case L_AND:
- return allocConstraint(AND, left, right);
+ return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
case L_OR:
- return allocConstraint(OR, left, right);
+ return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
case L_NOT:
- return negateConstraint(allocConstraint(OR, left, NULL));
+ ASSERT(constraint->numArray==1);
+ return negateConstraint(array[0]);
case L_XOR: {
- Constraint * nleft=negateConstraint(cloneConstraint(left));
- Constraint * nright=negateConstraint(cloneConstraint(right));
+ ASSERT(constraint->numArray==2);
+ Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
+ Constraint * nright=negateConstraint(cloneConstraint(array[1]));
return allocConstraint(OR,
- allocConstraint(AND, left, nright),
- allocConstraint(AND, nleft, right));
+ allocConstraint(AND, array[0], nright),
+ allocConstraint(AND, nleft, array[1]));
}
case L_IMPLIES:
- return allocConstraint(IMPLIES, left, right);
- }*/
+ ASSERT(constraint->numArray==2);
+ return allocConstraint(IMPLIES, array[0], array[1]);
+ default:
+ model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
+ exit(-1);
+ }
+}
+
+Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
+ //TO IMPLEMENT
+ return NULL;
+}
+
+Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+ //TO IMPLEMENT
return NULL;
}
uint varcount;
};
-
SATEncoder * allocSATEncoder();
void deleteSATEncoder(SATEncoder *This);
void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint);
Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint);
-
+Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
#endif
sp_before_semi = ignore
sp_before_semi_for_empty = ignore
sp_after_semi_for_empty = ignore
-sp_before_nl_cont = ignore
\ No newline at end of file
+sp_before_nl_cont = ignore
\ No newline at end of file
--- /dev/null
+#ifndef ARRAY_H
+#define ARRAY_H
+
+#define ArrayDef(name, type) \
+ struct Array ## name { \
+ type * array; \
+ uint size; \
+ }; \
+ typedef struct Array ## name Array ## name; \
+ static inline Array ## name * allocArray ## name(uint size) { \
+ Array ## name * tmp = (Array ## name *)ourmalloc(sizeof(type)); \
+ tmp->size = size; \
+ tmp->array = (type *) ourcalloc(1, sizeof(type) * size); \
+ return tmp; \
+ } \
+ static inline Array ## name * allocArrayInit ## name(type * array, uint size) { \
+ Array ## name * tmp = allocArray ## name(size); \
+ memcpy(tmp->array, array, size * sizeof(type)); \
+ return tmp; \
+ } \
+ static inline type getArray ## name(Array ## name * This, uint index) { \
+ return This->array[index]; \
+ } \
+ static inline void setArray ## name(Array ## name * This, uint index, type item) { \
+ This->array[index]=item; \
+ } \
+ static inline uint getSizeArray ## name(Array ## name *This) { \
+ return This->size; \
+ } \
+ static inline void deleteArray ## name(Array ## name *This) { \
+ ourfree(This->array); \
+ ourfree(This); \
+ } \
+ static inline type * exposeCArray ## name(Array ## name * This) { \
+ return This->array; \
+ } \
+ static inline void deleteInlineArray ## name(Array ## name *This) { \
+ ourfree(This->array); \
+ } \
+ static inline void allocInlineArray ## 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); \
+ memcpy(This->array, array, size * sizeof(type)); \
+ }
+
+#endif
#include "structs.h"
#include "mymemory.h"
-VectorImpl(Int, uint64_t, 4);
+VectorImpl(Table, Table *, 4);
+VectorImpl(Set, Set *, 4);
VectorImpl(Boolean, Boolean *, 4);
VectorImpl(Constraint, Constraint *, 4);
-VectorImpl(Set, Set *, 4);
+VectorImpl(Function, Function *, 4);
+VectorImpl(Predicate, Predicate *, 4);
VectorImpl(Element, Element *, 4);
+VectorImpl(Order, Order *, 4);
+VectorImpl(TableEntry, TableEntry *, 4);
VectorImpl(ASTNode, ASTNode *, 4);
-HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals);
-HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals);
+VectorImpl(Int, uint64_t, 4);
#include "hashtable.h"
#include "hashset.h"
#include "classlist.h"
+#include "array.h"
-VectorDef(Int, uint64_t, 4);
+ArrayDef(Element, Element *);
+ArrayDef(Boolean, Boolean *);
+ArrayDef(Set, Set *);
+
+
+VectorDef(Table, Table *, 4);
+VectorDef(Set, Set *, 4);
VectorDef(Boolean, Boolean *, 4);
VectorDef(Constraint, Constraint *, 4);
-VectorDef(Set, Set *, 4);
-VectorDef(Element, Element *, 4);
-VectorDef(TableEntry, TableEntry *, 4);
+VectorDef(Function, Function *, 4);
VectorDef(Predicate, Predicate *, 4);
-VectorDef(Table, Table *, 4);
+VectorDef(Element, Element *, 4);
VectorDef(Order, Order *, 4);
-VectorDef(Function, Function *, 4);
+VectorDef(TableEntry, TableEntry *, 4);
VectorDef(ASTNode, ASTNode *, 4);
VectorDef(FunctionEncoding, FunctionEncoding *, 4);
VectorDef(ElementEncoding, ElementEncoding *, 4);
+VectorDef(Int, uint64_t, 4);
+
inline unsigned int Ptr_hash_function(void * hash) {
return (unsigned int)((uint64_t)hash >> 4);
HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals);
+
#endif
return allocVector ## name(defcap); \
} \
Vector ## name * allocVector ## name(uint capacity) { \
- Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(type)); \
+ Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
tmp->size = 0; \
tmp->capacity = capacity; \
tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity); \
} \
Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \
Vector ## name * tmp = allocVector ## name(capacity); \
- memcpy(tmp->array, array, capacity * sizeof(type)); \
+ tmp->size=capacity; \
+ memcpy(tmp->array, array, capacity * sizeof(type)); \
return tmp; \
} \
void pushVector ## name(Vector ## name *vector, type item) { \
} \
void allocInlineVectorArray ## name(Vector ## name * vector, uint capacity, type * array) { \
allocInlineVector ##name(vector, capacity); \
- memcpy(vector->array, array, capacity * sizeof(type)); \
+ vector->size=capacity; \
+ memcpy(vector->array, array, capacity * sizeof(type)); \
}
#endif
#include "elementencoding.h"
-ElementEncoding * allocElementEncoding(ElementEncodingType type, Element *element) {
- ElementEncoding * This=ourmalloc(sizeof(ElementEncoding));
+void initElementEncoding(ElementEncoding * This, Element *element) {
This->element=element;
- This->type=type;
+ This->type=ELEM_UNASSIGNED;
This->variables=NULL;
This->encodingArray=NULL;
+ This->inUseArray=NULL;
This->numVars=0;
- return This;
}
void deleteElementEncoding(ElementEncoding *This) {
ourfree(This->encodingArray);
if (This->inUseArray!=NULL)
ourfree(This->inUseArray);
- ourfree(This);
}
void allocEncodingArrayElement(ElementEncoding *This, uint size) {
#include "classlist.h"
enum ElementEncodingType {
- ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
+ ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
};
typedef enum ElementEncodingType ElementEncodingType;
uint numVars; /* Number of variables */
};
-ElementEncoding * allocElementEncoding(ElementEncodingType type, Element *element);
+void initElementEncoding(ElementEncoding *This, Element *element);
void deleteElementEncoding(ElementEncoding *This);
void baseBinaryIndexElementAssign(ElementEncoding *This);
void allocEncodingArrayElement(ElementEncoding *This, uint size);
void allocInUseArrayElement(ElementEncoding *This, uint size);
-inline bool isinUseElement(ElementEncoding *This, uint offset) {
+static inline bool isinUseElement(ElementEncoding *This, uint offset) {
return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
}
-inline void setInUseElement(ElementEncoding *This, uint offset) {
+static inline void setInUseElement(ElementEncoding *This, uint offset) {
This->inUseArray[(offset>>6)] |= 1 << (offset & 63);
}
#endif
#include "element.h"
#include "common.h"
#include "boolean.h"
-#include "naiveelementencoder.h"
+#include "naiveencoder.h"
Encodings* allocEncodings(){
Encodings* This = (Encodings*) ourmalloc(sizeof(Encodings));
#include "functionencoding.h"
-FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function) {
- FunctionEncoding * This=ourmalloc(sizeof(FunctionEncoding));
+void initFunctionEncoding(FunctionEncoding *This, Element *function) {
This->op.function=function;
- This->type=type;
- return This;
+ This->type=FUNC_UNASSIGNED;
}
-FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate) {
- FunctionEncoding * This=ourmalloc(sizeof(FunctionEncoding));
+void initPredicateEncoding(FunctionEncoding *This, Boolean *predicate) {
This->op.predicate=predicate;
- This->type=type;
- return This;
+ This->type=FUNC_UNASSIGNED;
}
-void deleteFunctionEncoding(FunctionEncoding *fe) {
- ourfree(fe);
+void deleteFunctionEncoding(FunctionEncoding *This) {
}
#include "classlist.h"
enum FunctionEncodingType {
- ENUMERATEIMPLICATIONS, CIRCUIT
+ FUNC_UNASSIGNED, ENUMERATEIMPLICATIONS, CIRCUIT
};
typedef enum FunctionEncodingType FunctionEncodingType;
ElementPredicate op;
};
-FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function);
-FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate);
+void initFunctionEncoding(FunctionEncoding *encoding, Element *function);
+void initPredicateEncoding(FunctionEncoding *encoding, Boolean *predicate);
void deleteFunctionEncoding(FunctionEncoding *This);
#endif
+++ /dev/null
-#include "naiveelementencoder.h"
-#include "elementencoding.h"
-#include "element.h"
-#include "set.h"
-#include "common.h"
-#include "structs.h"
-#include <strings.h>
-
-void baseBinaryIndexElementAssign(ElementEncoding *This) {
- Element * element=This->element;
- ASSERT(element->type == ELEMSET);
- Set * set= ((ElementSet*)element)->set;
- ASSERT(set->isRange==false);
- uint size=getSizeVectorInt(set->members);
- uint encSize=NEXTPOW2(size);
- allocEncodingArrayElement(This, encSize);
- allocInUseArrayElement(This, encSize);
-
- for(uint i=0;i<size;i++) {
- This->encodingArray[i]=getVectorInt(set->members, i);
- setInUseElement(This, i);
- }
-}
-
-
-
+++ /dev/null
-#ifndef NAIVEELEMENTENCODER_H
-#define NAIVEELEMENTENCODER_H
-#include "classlist.h"
-void baseBinaryIndexElementAssign(ElementEncoding *This);
-#endif
--- /dev/null
+#include "naiveencoder.h"
+#include "elementencoding.h"
+#include "element.h"
+#include "functionencoding.h"
+#include "function.h"
+#include "set.h"
+#include "common.h"
+#include "structs.h"
+#include <strings.h>
+
+void baseBinaryIndexElementAssign(ElementEncoding *This) {
+ Element * element=This->element;
+ ASSERT(element->type == ELEMSET);
+ Set * set= ((ElementSet*)element)->set;
+ ASSERT(set->isRange==false);
+ uint size=getSizeVectorInt(set->members);
+ uint encSize=NEXTPOW2(size);
+ allocEncodingArrayElement(This, encSize);
+ allocInUseArrayElement(This, encSize);
+
+ for(uint i=0;i<size;i++) {
+ This->encodingArray[i]=getVectorInt(set->members, i);
+ setInUseElement(This, i);
+ }
+}
+
+
+void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This){
+ if(This->isFunction) {
+ ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN);
+ if(This->type==CIRCUIT){
+ naiveEncodeCircuitFunction(encodings, This);
+ } else if( This->type == ENUMERATEIMPLICATIONS){
+ naiveEncodeEnumeratedFunction(encodings, This);
+ } else
+ ASSERT(0);
+
+ }else {
+ ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP);
+ BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate;
+ //FIXME
+
+ }
+}
+
+
+void naiveEncodeCircuitFunction(Encodings* encodings, FunctionEncoding* This){
+
+}
+
+void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This){
+ ElementFunction* ef =(ElementFunction*)This->op.function;
+ Function * function = ef->function;
+ if(GETFUNCTIONTYPE(function)==TABLEFUNC){
+ naiveEncodeEnumTableFunc(encodings, ef);
+ }else if (GETFUNCTIONTYPE(function)== OPERATORFUNC){
+ naiveEncodeEnumOperatingFunc(encodings, ef);
+ }else
+ ASSERT(0);
+}
+
+void naiveEncodeEnumTableFunc(Encodings* encodings, 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);
+ //FIXME: generate Constraints
+ }
+
+}
+
+void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This){
+
+}
\ No newline at end of file
--- /dev/null
+#ifndef NAIVEELEMENTENCODER_H
+#define NAIVEELEMENTENCODER_H
+#include "classlist.h"
+void baseBinaryIndexElementAssign(ElementEncoding *This);
+void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This);
+void naiveEncodeCircuitFunction(Encodings* encodings,FunctionEncoding* This);
+void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This);
+void naiveEncodeEnumTableFunc(Encodings* encodings, ElementFunction* This);
+void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This);
+#endif
+++ /dev/null
-
-#include "naivefunctionencoder.h"
-#include "functionencoding.h"
-#include "common.h"
-#include "element.h"
-#include "boolean.h"
-#include "function.h"
-#include "table.h"
-#include "tableentry.h"
-
-void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This){
- if(This->isFunction) {
- ASSERT(GETELEMENTTYPE(This->op.function)==ELEMFUNCRETURN);
- if(This->type==CIRCUIT){
- naiveEncodeCircuitFunction(encodings, This);
- } else if( This->type == ENUMERATEIMPLICATIONS){
- naiveEncodeEnumeratedFunction(encodings, This);
- } else
- ASSERT(0);
-
- }else {
- ASSERT(GETBOOLEANTYPE(This->op.predicate) == PREDICATEOP);
- BooleanPredicate* predicate = (BooleanPredicate*)This->op.predicate;
- //FIXME
-
- }
-}
-
-
-void naiveEncodeCircuitFunction(Encodings* encodings, FunctionEncoding* This){
-
-}
-
-void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This){
- ElementFunction* ef =(ElementFunction*)This->op.function;
- Function * function = ef->function;
- if(GETFUNCTIONTYPE(function)==TABLEFUNC){
- naiveEncodeEnumTableFunc(encodings, ef);
- }else if (GETFUNCTIONTYPE(function)== OPERATORFUNC){
- naiveEncodeEnumOperatingFunc(encodings, ef);
- }else
- ASSERT(0);
-}
-
-void naiveEncodeEnumTableFunc(Encodings* encodings, ElementFunction* This){
- ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
- VectorElement* elements= This->Elements;
- Table* table = ((FunctionTable*) This->function)->table;
- uint size = getSizeVectorTableEntry(table->entries);
- for(uint i=0; i<size; i++){
- TableEntry* entry = getVectorTableEntry(table->entries, i);
- //FIXME: generate Constraints
- }
-
-}
-
-void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This){
-
-}
\ No newline at end of file
+++ /dev/null
-
-
-#ifndef NAIVEFUNCTIONENCODER_H
-#define NAIVEFUNCTIONENCODER_H
-#include "encodings.h"
-#include "functionencoding.h"
-
-void naiveEncodeFunctionPredicate(Encodings* encodings, FunctionEncoding *This);
-void naiveEncodeCircuitFunction(Encodings* encodings,FunctionEncoding* This);
-void naiveEncodeEnumeratedFunction(Encodings* encodings, FunctionEncoding* This);
-void naiveEncodeEnumTableFunc(Encodings* encodings, ElementFunction* This);
-void naiveEncodeEnumOperatingFunc(Encodings* encodings, ElementFunction* This);
-#endif /* NAIVEFUNCTIONENCODER_H */
-
debug: CFLAGS += -DCONFIG_DEBUG
debug: all
+test: all
+ make -C Test
+
PHONY += docs
docs: $(C_SOURCES) $(HEADERS)
doxygen
ctags -R
tabbing:
- uncrustify -c C.cfg --no-backup *.c
+ uncrustify -c C.cfg --no-backup *.c */*.c
uncrustify -c C.cfg --no-backup *.h */*.h
wc:
--- /dev/null
+BASE := ..
+
+OBJECTS := $(patsubst %.c, ../bin/%, $(wildcard *.c))
+
+include $(BASE)/common.mk
+
+DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
+
+CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections
+
+all: $(OBJECTS) ../bin/run.sh
+
+-include $(DEPS)
+
+../bin/%: %.c
+ $(CC) -MMD -MF $(@D)/.$(@F).d -o ../bin/$@ $< $(CPPFLAGS) -L$(BASE)/bin/ -l_cons_comp
+
+../bin/run.sh: run.sh
+ cp run.sh ../bin/run.sh
+
+clean::
+ rm -f $(OBJECTS) $(DEPS) ../bin/run.sh
--- /dev/null
+#include "csolver.h"
+
+int main(int numargs, char ** argv) {
+ CSolver * solver=allocCSolver();
+ uint64_t set1[]={0, 1, 2};
+ Set * s=createSet(solver, 0, set1, 3);
+ Element * e1=getElementVar(solver, s);
+ Element * e2=getElementVar(solver, s);
+ Set * domain[]={s, s};
+ Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
+ Element * inputs[]={e1, e2};
+ Boolean * b=applyPredicate(solver, equals, inputs, 2);
+ addBoolean(solver, b);
+ Order * o=createOrder(solver, TOTAL, s);
+ Boolean * oc=orderConstraint(solver, o, 1, 2);
+ addBoolean(solver, oc);
+ deleteSolver(solver);
+}
--- /dev/null
+#!/bin/bash
+
+export LD_LIBRARY_PATH=../bin
+# For Mac OSX
+export DYLD_LIBRARY_PATH=../bin
+
+$@
#include <stdio.h>
#include "config.h"
+/*
extern int model_out;
extern int model_err;
extern int switch_alloc;
#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+*/
+
+#define model_print printf
+
#define NEXTPOW2(x) (1<<(sizeof(uint)*8-__builtin_clz(x-1)))
#ifdef CONFIG_DEBUG
CSolver * allocCSolver();
+/** Delete solver instance. */
+
+void deleteSolver(CSolver * This);
+
/** This function creates a set containing the elements passed in the array. */
Set * createSet(CSolver *, VarType type, uint64_t * elements, uint num);
#include "config.h"
+/*
void * ourmalloc(size_t size);
void ourfree(void *ptr);
void * ourcalloc(size_t count, size_t size);
void * ourrealloc(void *ptr, size_t size);
+*/
+
+static inline void * ourmalloc(size_t size) { return malloc(size); }
+static inline void ourfree(void *ptr) { free(ptr); }
+static inline void * ourcalloc(size_t count, size_t size) { return calloc(count, size); }
+static inline void * ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
#endif/* _MY_MEMORY_H */
projects / satune.git / commitdiff