Fixing some bugs + improving the testcase ...

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 458ec796f78853175e9146fe25e44191de568ab7..f5f8f68e323aac242344fdc216eb68995e27a00d 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -22,11 +22,11 @@ inline bool Ptr_equals(void * key1, void * key2) {
        return key1 == key2;
 }
 
-inline unsigned int order_pair_hash_Function(OrderPair* This){
+static inline unsigned int order_pair_hash_Function(OrderPair* This){
        return (uint) (This->first << 2) ^ This->second;
 }
 
-inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
+static inline unsigned int order_pair_equals(OrderPair* key1, OrderPair* key2){
        return key1->first== key2->first && key1->second == key2->second;
 }
 

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index a45eb132cf1eb2c53ae99dd4e5bd259b69ac59cd..5936bbd8e0ca96efda7c215207b31d4436e93795 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -23,8 +23,6 @@ VectorDef(TableEntry, TableEntry *, 4);
 VectorDef(ASTNode, ASTNode *, 4);
 VectorDef(Int, uint64_t, 4);
 
-
-
 HashTableDef(Void, void *, void *);
 HashTableDef(BoolConst, OrderPair *, Constraint *);
 

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index caa8a92bd9dfeaddf92b6df6b6e9291f206303bc..440d1aa1def4b7a30e6f5d0d884b5fecac8b4b7d 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -14,5 +14,23 @@ int main(int numargs, char ** argv) {
        Order * o=createOrder(solver, TOTAL, s);
        Boolean * oc=orderConstraint(solver, o, 1, 2);
        addBoolean(solver, oc);
+       
+       uint64_t set2[] = {2, 3};
+       Set* range = createSet(solver, 1, set2, 2);
+       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, range, IGNORE);
+       /*Table* table = createTable(solver, domain, 2, range);
+       uint64_t row1[] = {0, 1};
+       uint64_t row2[] = {1, 1};
+       addTableEntry(solver, table, row1, 2, 2);
+       addTableEntry(solver, table, row2, 2, 3);
+       Function * f2 = completeTable(solver, table); */
+       Boolean* overflow = getBooleanVar(solver , 2);
+       Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
+       Set* domain2[] = {s,range};
+       Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
+       Element* inputs2 [] = {e1, e3};
+       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
+       addBoolean(solver, pred);
+       startEncoding(solver);
        deleteSolver(solver);
 }

diff --git a/src/csolver.c b/src/csolver.c
index 68fb39fc3855f4ed3472b677e1daa07a5bca7f2a..d63c266c804aa2bf587e76db54bda52d939cafcb 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -171,7 +171,7 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
        return constraint;
 }
 
-void encode(CSolver* solver){
+void startEncoding(CSolver* solver){
        naiveEncodingDecision(solver);
        SATEncoder* satEncoder = allocSATEncoder();
 //     initializeConstraintVars(solver, satEncoder);

diff --git a/src/csolver.h b/src/csolver.h
index fd807aef3fe1204b96efb11bd798479342b22596..bd90bf3054a5cbf85e4b506097391c2786e51d7d 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -113,5 +113,5 @@ Order * createOrder(CSolver *, OrderType type, Set * set);
 Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second);
 
 /** When everything is done, the client calls this function and then csolver starts to encode*/
-void encode(CSolver*);
+void startEncoding(CSolver*);
 #endif