From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 20 Jul 2017 19:21:19 +0000 (-0700)
Subject: Fixing bugs + adding descriptions to test cases
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=039d671a9982e507c509a5540a357c7e7938c7ed

Fixing bugs + adding descriptions to test cases
---

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index a9ba7b1..a4f9a82 100644
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -205,7 +205,8 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
 		encodeElementSATEncoder(This, elem);
 	}
 
-	FunctionTable* function =(FunctionTable*)elemFunc;
+	FunctionTable* function =(FunctionTable*)elemFunc->function;
+	model_print("undefBehavior: %d\n", function->undefBehavior);
 	switch(function->undefBehavior){
 		case IGNOREBEHAVIOR:
 		case FLAGFORCEUNDEFINED:
diff --git a/src/Test/buildconstraintstest.c b/src/Test/buildconstraintstest.c
index af65c2c..1e336c2 100644
--- a/src/Test/buildconstraintstest.c
+++ b/src/Test/buildconstraintstest.c
@@ -1,5 +1,18 @@
 #include "csolver.h"
 
+/**
+ * e1={0, 1, 2}
+ * e2={0, 1, 2}
+ * e1 == e2
+ * e3= e1+e2 {0, 1, 2, 3, 4}
+ * e4 = f(e1, e2)
+ *	0 1 => 0
+ *	1 1 => 0
+ *	2 1 => 2
+ *	2 2 => 2
+ * e3 == e4
+ * Result: UNSAT!
+ */
 int main(int numargs, char ** argv) {
 	CSolver * solver=allocCSolver();
 	uint64_t set1[]={0, 1, 2};
@@ -12,8 +25,7 @@ int main(int numargs, char ** argv) {
 	Set * domain[]={s, s};
 	Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
 	Element * inputs[]={e1, e2};
-	Boolean* overflow = getBooleanVar(solver , 2);
-	Boolean * b=applyPredicate(solver, equals, inputs, 2, overflow);
+	Boolean * b=applyPredicate(solver, equals, inputs, 2, NULL);
 	addConstraint(solver, b);
 
 	uint64_t set2[] = {2, 3};
@@ -30,7 +42,7 @@ int main(int numargs, char ** argv) {
 	addTableEntry(solver, table, row3, 2, 2);
 	addTableEntry(solver, table, row4, 2, 2);
 	Function * f2 = completeTable(solver, table, IGNOREBEHAVIOR); //its range would be as same as s
-	
+	Boolean* overflow = getBooleanVar(solver , 2);	
 	Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
 	Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
 	Set* domain2[] = {s,rangef1};
diff --git a/src/Test/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c
index e433bf7..ed4fc4d 100644
--- a/src/Test/elemequalityunsattest.c
+++ b/src/Test/elemequalityunsattest.c
@@ -1,5 +1,11 @@
 #include "csolver.h"
-
+/**
+ * e1 = {0, 1, 2}
+ * e2 = {3, 4}
+ * e1 == e2
+ * 
+ * Result: UNSAT
+ */
 int main(int numargs, char ** argv) {
 	CSolver * solver=allocCSolver();
 	uint64_t set1[]={0, 1, 2};
diff --git a/src/Test/funcencodingtest.c b/src/Test/funcencodingtest.c
index e376ca8..c1162ee 100644
--- a/src/Test/funcencodingtest.c
+++ b/src/Test/funcencodingtest.c
@@ -1,5 +1,21 @@
 #include "csolver.h"
-
+/**
+ * e1 = {6}
+ * e2={4, 2}
+ * e3=Fsub(e1,e2) {4, 2}
+ * e4= f(e1, e2) 
+ *	6 2 => 3
+ *	6 4 => 1
+ * e5 = f(e1)=>e1 {6}
+ * e6 = (e3, e4, e5) {2, 3, 1}
+ *	4 3 6 => 3
+ *	2 1 6 => 1
+ *	2 3 6 => 2
+ *	4 1 6 => 1
+ * e7 = {2, 1, 0}
+ * e7 > e6
+ * Result: e1=6, e2=4, e7=2
+ */
 int main(int numargs, char ** argv) {
 	CSolver * solver=allocCSolver();
 	uint64_t set1[]={6};
diff --git a/src/Test/logicopstest.c b/src/Test/logicopstest.c
index 7b9384d..a01a7f5 100644
--- a/src/Test/logicopstest.c
+++ b/src/Test/logicopstest.c
@@ -4,9 +4,7 @@
  * b1 AND b2=>b3
  * !b3 OR b4
  * b1 XOR b4
- * @param numargs
- * @param argv
- * @return 
+ * Result: b1=1 b2=0 b3=0 b4=0 
  */
 int main(int numargs, char** argv){
 	CSolver * solver=allocCSolver();
diff --git a/src/Test/ltelemconsttest.c b/src/Test/ltelemconsttest.c
index 018e36a..f96be92 100644
--- a/src/Test/ltelemconsttest.c
+++ b/src/Test/ltelemconsttest.c
@@ -1,5 +1,10 @@
 #include "csolver.h"
-
+/**
+ * e1 = 5
+ * e2 = {1, 3, 4, 6}
+ * e1 < e2
+ * Result: e1=5 e2=6
+ */
 int main(int numargs, char ** argv){
 	CSolver *solver=allocCSolver();
 	uint64_t set1[]={5};
diff --git a/src/Test/ordertest.c b/src/Test/ordertest.c
index 4970cac..2b8a98d 100644
--- a/src/Test/ordertest.c
+++ b/src/Test/ordertest.c
@@ -1,6 +1,11 @@
 
 #include "csolver.h"
-
+/**
+ * TotalOrder(5, 1, 4)
+ * 5 => 1
+ * 1 => 4
+ * Result: O(5,1)=0 O(1,4)=0 O(5,4)=0 O(1,5)=1 O(1111,5)=2
+ */
 int main(int numargs, char ** argv) {
 	CSolver * solver=allocCSolver();
 	uint64_t set1[]={5, 1, 4};