Resolving Conflicts ... Still there're errors that should be fixed
authorHamed <hamed.gorjiara@gmail.com>
Fri, 23 Jun 2017 07:26:08 +0000 (00:26 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Fri, 23 Jun 2017 07:26:08 +0000 (00:26 -0700)
41 files changed:
.gitignore
src/AST/boolean.c
src/AST/boolean.h
src/AST/element.c
src/AST/element.h
src/AST/function.c
src/AST/function.h
src/AST/ops.h
src/AST/order.c
src/AST/order.h
src/AST/predicate.c
src/AST/predicate.h
src/AST/table.c
src/AST/table.h
src/AST/tableentry.c
src/Backend/constraint.h
src/Backend/satencoder.c
src/Backend/satencoder.h
src/C.cfg
src/Collections/array.h [new file with mode: 0644]
src/Collections/structs.c
src/Collections/structs.h
src/Collections/vector.h
src/Encoders/elementencoding.c
src/Encoders/elementencoding.h
src/Encoders/encodings.c
src/Encoders/functionencoding.c
src/Encoders/functionencoding.h
src/Encoders/naiveelementencoder.c [deleted file]
src/Encoders/naiveelementencoder.h [deleted file]
src/Encoders/naiveencoder.c [new file with mode: 0644]
src/Encoders/naiveencoder.h [new file with mode: 0644]
src/Encoders/naivefunctionencoder.c [deleted file]
src/Encoders/naivefunctionencoder.h [deleted file]
src/Makefile
src/Test/Makefile [new file with mode: 0644]
src/Test/buildconstraints.c [new file with mode: 0644]
src/Test/run.sh [new file with mode: 0755]
src/common.h
src/csolver.h
src/mymemory.h

index 39d4e58..c6f1f57 100644 (file)
@@ -5,3 +5,5 @@ nbproject/
 src/bin/
 src/lib_cons_comp.so
 /src/mymemory.cc
+.*
+*.dSYM
\ No newline at end of file
index 39d7e10..0432b43 100644 (file)
@@ -26,34 +26,35 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
        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);
index 17e29b6..411af26 100644 (file)
@@ -5,6 +5,7 @@
 #include "ops.h"
 #include "structs.h"
 #include "astnode.h"
+#include "functionencoding.h"
 
 /**
     This is a little sketchy, but apparently legit.
@@ -34,14 +35,14 @@ struct BooleanVar {
 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);
index 3cec477..a94db4b 100644 (file)
@@ -5,8 +5,8 @@ Element *allocElementSet(Set * s) {
        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;
 }
 
@@ -15,14 +15,33 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
        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);
 }
index 56079e9..b5bc9c1 100644 (file)
@@ -4,6 +4,8 @@
 #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)
@@ -16,14 +18,16 @@ struct Element {
 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);
index daa3dc3..43adc25 100644 (file)
@@ -6,9 +6,7 @@
 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;
@@ -27,7 +25,7 @@ void deleteFunction(Function* This){
        case TABLEFUNC:
                break;
        case OPERATORFUNC:
-               ourfree(((FunctionOperator*) This)->domains);
+               deleteInlineArraySet(&((FunctionOperator*) This)->domains);
                break;
        default:
                ASSERT(0);
index 50a59ec..2e04320 100644 (file)
@@ -14,8 +14,7 @@ struct Function {
 struct FunctionOperator {
        Function base;
        ArithOp op;
-       uint numDomains;
-       Set ** domains;
+       ArraySet domains;
        Set * range;
        OverFlowBehavior overflowbehavior;
 };
index 427b4f2..1f94cb1 100644 (file)
@@ -32,7 +32,7 @@ typedef enum FunctionType FunctionType;
 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
index 47cc374..d2dc842 100644 (file)
@@ -5,18 +5,14 @@
 
 
 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);
+}
index 7d2bc3c..93b2413 100644 (file)
@@ -7,7 +7,7 @@
 struct Order {
        OrderType type;
        Set * set;
-       VectorBoolean* constraints;
+       VectorBoolean constraints;
 };
 
 Order* allocOrder(OrderType type, Set * set);
index 904fe22..79e81df 100644 (file)
@@ -1,13 +1,9 @@
 #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;
 }
@@ -16,7 +12,7 @@ void deletePredicate(Predicate* predicate){
        switch(GETPREDICATETYPE(predicate)) {
        case OPERATORPRED: {
                PredicateOperator * operpred=(PredicateOperator *) predicate;
-               ourfree(operpred->domains);
+               deleteInlineArraySet(&operpred->domains);
                break;
        }
        case TABLEPRED: {
index c6dd02b..ee432cb 100644 (file)
@@ -3,7 +3,7 @@
 #include "classlist.h"
 #include "mymemory.h"
 #include "ops.h"
-
+#include "structs.h"
 
 #define GETPREDICATETYPE(o) (((Predicate *)(o))->type)
 
@@ -14,8 +14,7 @@ struct Predicate {
 struct PredicateOperator {
        Predicate base;
        CompOp op;
-       Set ** domains;
-       uint numDomains;
+       ArraySet domains;
 };
 
 struct PredicateTable {
index 6482d83..ea4b6d2 100644 (file)
@@ -7,25 +7,24 @@
 
 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);
 }
 
index cff8ec6..90f5001 100644 (file)
@@ -5,10 +5,9 @@
 #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);
index b99d183..9992af7 100644 (file)
@@ -1,14 +1,13 @@
 #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);
+}
index d6e7e86..a83a39b 100644 (file)
@@ -33,15 +33,15 @@ Constraint * allocVarConstraint(CType t, uint var);
 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;
index fafd6a3..37d3bc7 100644 (file)
@@ -3,6 +3,7 @@
 #include "csolver.h"
 #include "boolean.h"
 #include "constraint.h"
+#include "common.h"
 
 SATEncoder * allocSATEncoder() {
        SATEncoder *This=ourmalloc(sizeof (SATEncoder));
@@ -31,13 +32,14 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
                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++);
@@ -54,27 +56,41 @@ Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
 }
 
 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;
 }
index ea5de8b..5382bc5 100644 (file)
@@ -7,7 +7,6 @@ struct SATEncoder {
        uint varcount;
 };
 
-
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(SATEncoder *This, CSolver *csolver);
@@ -16,5 +15,5 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 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
index 9831cf2..9a4c97a 100644 (file)
--- a/src/C.cfg
+++ b/src/C.cfg
@@ -12,4 +12,4 @@ sp_special_semi                           = ignore
 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
diff --git a/src/Collections/array.h b/src/Collections/array.h
new file mode 100644 (file)
index 0000000..73d0c32
--- /dev/null
@@ -0,0 +1,49 @@
+#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
index 4da4995..f776830 100644 (file)
@@ -1,11 +1,14 @@
 #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);
index 112fc08..dc6d665 100644 (file)
@@ -4,20 +4,27 @@
 #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);
@@ -33,4 +40,5 @@ HashTableDef(VoidToFuncEncod, void *, FunctionEncoding *, Ptr_hash_function, Ptr
 
 HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals);
 
+
 #endif
index fa1764e..76da387 100644 (file)
@@ -29,7 +29,7 @@
                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);          \
@@ -37,7 +37,8 @@
        }                                                                     \
        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) {          \
@@ -79,6 +80,7 @@
        }                                                                                                                                                                                                                                                                                       \
        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
index 08385db..217327d 100644 (file)
@@ -1,13 +1,12 @@
 #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) {
@@ -17,7 +16,6 @@ void deleteElementEncoding(ElementEncoding *This) {
                ourfree(This->encodingArray);
        if (This->inUseArray!=NULL)
                ourfree(This->inUseArray);
-       ourfree(This);
 }
 
 void allocEncodingArrayElement(ElementEncoding *This, uint size) {
index bc173ea..1af74be 100644 (file)
@@ -3,7 +3,7 @@
 #include "classlist.h"
 
 enum ElementEncodingType {
-       ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
+       ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, ONEHOTBINARY, BINARYVAL
 };
 
 typedef enum ElementEncodingType ElementEncodingType;
@@ -17,17 +17,17 @@ struct ElementEncoding {
        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
index f86389d..27d393e 100644 (file)
@@ -4,7 +4,7 @@
 #include "element.h"
 #include "common.h"
 #include "boolean.h"
-#include "naiveelementencoder.h"
+#include "naiveencoder.h"
 
 Encodings* allocEncodings(){
        Encodings* This = (Encodings*) ourmalloc(sizeof(Encodings));
index d0f8c3d..32be4ab 100644 (file)
@@ -1,19 +1,14 @@
 #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) {
 }
index dc52aa7..c7cf27e 100644 (file)
@@ -3,7 +3,7 @@
 #include "classlist.h"
 
 enum FunctionEncodingType {
-       ENUMERATEIMPLICATIONS, CIRCUIT
+       FUNC_UNASSIGNED, ENUMERATEIMPLICATIONS, CIRCUIT
 };
 
 typedef enum FunctionEncodingType FunctionEncodingType;
@@ -21,8 +21,8 @@ struct FunctionEncoding {
        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
diff --git a/src/Encoders/naiveelementencoder.c b/src/Encoders/naiveelementencoder.c
deleted file mode 100644 (file)
index 348c54c..0000000
+++ /dev/null
@@ -1,26 +0,0 @@
-#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);
-       }
-}
-
-
-
diff --git a/src/Encoders/naiveelementencoder.h b/src/Encoders/naiveelementencoder.h
deleted file mode 100644 (file)
index db4aeb9..0000000
+++ /dev/null
@@ -1,5 +0,0 @@
-#ifndef NAIVEELEMENTENCODER_H
-#define NAIVEELEMENTENCODER_H
-#include "classlist.h"
-void baseBinaryIndexElementAssign(ElementEncoding *This);
-#endif
diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
new file mode 100644 (file)
index 0000000..ca83383
--- /dev/null
@@ -0,0 +1,76 @@
+#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
diff --git a/src/Encoders/naiveencoder.h b/src/Encoders/naiveencoder.h
new file mode 100644 (file)
index 0000000..d3df611
--- /dev/null
@@ -0,0 +1,10 @@
+#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
diff --git a/src/Encoders/naivefunctionencoder.c b/src/Encoders/naivefunctionencoder.c
deleted file mode 100644 (file)
index 03037fd..0000000
+++ /dev/null
@@ -1,59 +0,0 @@
-
-#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
diff --git a/src/Encoders/naivefunctionencoder.h b/src/Encoders/naivefunctionencoder.h
deleted file mode 100644 (file)
index b0935ac..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-
-
-#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 */
-
index 341a5df..35468a0 100644 (file)
@@ -37,6 +37,9 @@ ${OBJ_DIR}:
 debug: CFLAGS += -DCONFIG_DEBUG
 debug: all
 
+test: all
+       make -C Test
+
 PHONY += docs
 docs: $(C_SOURCES) $(HEADERS)
        doxygen
@@ -63,7 +66,7 @@ tags:
        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:
diff --git a/src/Test/Makefile b/src/Test/Makefile
new file mode 100644 (file)
index 0000000..b3b7cb3
--- /dev/null
@@ -0,0 +1,22 @@
+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
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
new file mode 100644 (file)
index 0000000..caa8a92
--- /dev/null
@@ -0,0 +1,18 @@
+#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);
+}
diff --git a/src/Test/run.sh b/src/Test/run.sh
new file mode 100755 (executable)
index 0000000..9741fe0
--- /dev/null
@@ -0,0 +1,7 @@
+#!/bin/bash
+
+export LD_LIBRARY_PATH=../bin
+# For Mac OSX
+export DYLD_LIBRARY_PATH=../bin
+
+$@
index 9b78485..d9e6d43 100644 (file)
@@ -17,6 +17,7 @@
 #include <stdio.h>
 #include "config.h"
 
+/*
 extern int model_out;
 extern int model_err;
 extern int switch_alloc;
@@ -27,6 +28,10 @@ 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
index 95809dd..495d386 100644 (file)
@@ -34,6 +34,10 @@ struct CSolver {
 
 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);
index 2fa964e..32dfa51 100644 (file)
 
 #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 */