From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 7 Jul 2017 01:12:21 +0000 (-0700)
Subject: Fixing some bugs + improving the testcase ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=3c17d1f92ba70983fdd020de0a3875f11cce7647;p=satune.git

Fixing some bugs + improving the testcase ...
---

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 458ec79..f5f8f68 100644
--- 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 a45eb13..5936bbd 100644
--- 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 caa8a92..440d1aa 100644
--- 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 68fb39f..d63c266 100644
--- 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 fd807ae..bd90bf3 100644
--- 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