Fixing bugs + adding descriptions to test cases

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index a9ba7b17e2d9f41be44cf1141503a5d02798431b..a4f9a8248dd49334e609bed4185635f7ba760084 100644 (file)
--- 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 af65c2c00ab7976a8408d94e288ce9828ce5b051..1e336c2861edb411df8e63cd2d1045ac6789c8c1 100644 (file)
--- 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 e433bf729531a4663ca1327f5bf3ad35768d1fb0..ed4fc4d46ea09ff3663cb29312a9b39ec8b41131 100644 (file)
--- 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 e376ca8f6be8ccadff05f7a4a374acea76c51224..c1162ee0d2264da792f2b2a84fc27941d5ddd9b1 100644 (file)
--- 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 7b9384df8e4f91d830e8dca798d6de2a0b526041..a01a7f5642e37f4119e58c9e1273ae21527ece8a 100644 (file)
--- 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 018e36adbbe58e2e77db26e62036ca7f1cd3f7de..f96be921ebd12c803a296ebf5ad14a45feb26757 100644 (file)
--- 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 4970cac92891f178268d8cdee6f02576aa98df89..2b8a98d0a1538d8be482d0aa792b803e28f2ea87 100644 (file)
--- 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};