Adding a new test case for testing FLAGIFFUNDEFINED + bug fixes

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index a4f9a8248dd49334e609bed4185635f7ba760084..c15e822656d64ad7503a454451b1d3bf2a14c492 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -40,7 +40,7 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
                                row=constraintAND(This->cnf, inputNum, carray);
                                break;
                        case FLAGFORCEUNDEFINED:{
-                               Edge undefConst = ((BooleanVar*)constraint->undefStatus)->var;
+                               Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
                                row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst));
                                break;
                        }
@@ -88,7 +88,7 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
                vals[i]=getSetElement(set, indices[i]);
        }
 
-       Edge undefConstraint = ((BooleanVar*) constraint->undefStatus)->var;
+       Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
        
        bool notfinished=true;
        while(notfinished) {
@@ -179,7 +179,7 @@ void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction*
                                break;
                        }
                        case FLAGFORCEUNDEFINED: {
-                               Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
+                               Edge undefConst = encodeConstraintSATEncoder(This, func->overflowstatus);
                                row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
                                break;
                        }
@@ -206,7 +206,6 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
        }
 
        FunctionTable* function =(FunctionTable*)elemFunc->function;
-       model_print("undefBehavior: %d\n", function->undefBehavior);
        switch(function->undefBehavior){
                case IGNOREBEHAVIOR:
                case FLAGFORCEUNDEFINED:
@@ -228,8 +227,7 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                vals[i]=getSetElement(set, indices[i]);
        }
 
-       Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
-       
+       Edge undefConstraint = encodeConstraintSATEncoder(This, elemFunc->overflowstatus);
        bool notfinished=true;
        while(notfinished) {
                Edge carray[numDomains+1];

diff --git a/src/Test/buildconstraintstest.c b/src/Test/buildconstraintstest.c
index 1e336c2861edb411df8e63cd2d1045ac6789c8c1..e7fffe6e4eec37d464507c450087661914124bf6 100644 (file)
--- a/src/Test/buildconstraintstest.c
+++ b/src/Test/buildconstraintstest.c
@@ -25,7 +25,7 @@ int main(int numargs, char ** argv) {
        Set * domain[]={s, s};
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
-       Boolean * b=applyPredicate(solver, equals, inputs, 2, NULL);
+       Boolean * b=applyPredicate(solver, equals, inputs, 2);
        addConstraint(solver, b);
 
        uint64_t set2[] = {2, 3};
@@ -48,7 +48,7 @@ int main(int numargs, char ** argv) {
        Set* domain2[] = {s,rangef1};
        Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
        Element* inputs2 [] = {e4, e3};
-       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2, overflow);
+       Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addConstraint(solver, pred);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c
index ed4fc4d46ea09ff3663cb29312a9b39ec8b41131..bd38ed9183d1711c1c60a05ee4f27c0d80cfb9ee 100644 (file)
--- a/src/Test/elemequalityunsattest.c
+++ b/src/Test/elemequalityunsattest.c
@@ -17,7 +17,7 @@ int main(int numargs, char ** argv) {
        Set * domain[]={s1, s2};
        Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
        Element * inputs[]={e1, e2};
-       Boolean *b=applyPredicate(solver, equals, inputs, 2, NULL);
+       Boolean *b=applyPredicate(solver, equals, inputs, 2);
        addConstraint(solver, b);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/funcencodingtest.c b/src/Test/funcencodingtest.c
index c1162ee0d2264da792f2b2a84fc27941d5ddd9b1..4962f3f027fc48f593de5f31402b9fea557a4bd5 100644 (file)
--- a/src/Test/funcencodingtest.c
+++ b/src/Test/funcencodingtest.c
@@ -70,7 +70,7 @@ int main(int numargs, char ** argv) {
        Set* deq[] = {s5,s4};
        Predicate* gt = createPredicateOperator(solver, GT, deq, 2);
        Element* inputs2 [] = {e7, e6};
-       Boolean* pred = applyPredicate(solver, gt, inputs2, 2, overflow);
+       Boolean* pred = applyPredicate(solver, gt, inputs2, 2);
        addConstraint(solver, pred);
        
        if (startEncoding(solver)==1)

diff --git a/src/Test/ltelemconsttest.c b/src/Test/ltelemconsttest.c
index f96be921ebd12c803a296ebf5ad14a45feb26757..382394900345f7c13706915d199ad6cebe7223c6 100644 (file)
--- a/src/Test/ltelemconsttest.c
+++ b/src/Test/ltelemconsttest.c
@@ -16,7 +16,7 @@ int main(int numargs, char ** argv){
        Set * domain2[]={s1, s3};
        Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
        Element * inputs2[]={e1, e2};
-       Boolean *b=applyPredicate(solver, lt, inputs2, 2, NULL);
+       Boolean *b=applyPredicate(solver, lt, inputs2, 2);
        addConstraint(solver, b);
        if (startEncoding(solver)==1)
                printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));

diff --git a/src/Test/tablefuncencodetest.c b/src/Test/tablefuncencodetest.c
new file mode 100644 (file)
index 0000000..9d5abed
--- /dev/null
+++ b/src/Test/tablefuncencodetest.c
@@ -0,0 +1,47 @@
+#include "csolver.h"
+/**
+ * e1 = {1, 2}
+ * e2={3, 5, 7}
+ * e3= f(e1, e2) 
+ *     1 5 => 7
+ *     2 3 => 5
+ * e4 = {6, 10, 19}
+ * e4 <= e3
+ * Result: e1=1, e2=5, e4=6, overflow=0
+ */
+int main(int numargs, char ** argv) {
+       CSolver * solver=allocCSolver();
+       uint64_t set1[]={1, 2};
+       uint64_t set2[]={3, 5, 7};
+       uint64_t set3[]={6, 10, 19};
+       Set * s1=createSet(solver, 0, set1, 2);
+       Set * s2=createSet(solver, 0, set2, 3);
+       Set * s3=createSet(solver, 0, set3, 3);
+       Element * e1=getElementVar(solver, s1);
+       Element * e2=getElementVar(solver, s2);
+       Element * e4=getElementVar(solver, s3);
+       Boolean* overflow = getBooleanVar(solver , 2);
+       Set * d1[]={s1, s2};
+       //change the overflow flag
+       Table* t1 = createTable(solver, d1, 2, s2);
+       uint64_t row1[] = {1, 5};
+       uint64_t row2[] = {2, 3};
+       addTableEntry(solver, t1, row1, 2, 7);
+       addTableEntry(solver, t1, row2, 2, 5);
+       Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);    
+       Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow);
+       
+       Set* deq[] = {s3,s2};
+       Predicate* lte = createPredicateOperator(solver, LTE, deq, 2);
+       Element* inputs2 [] = {e4, e3};
+       Boolean* pred = applyPredicate(solver, lte, inputs2, 2);
+       addConstraint(solver, pred);
+       
+       if (startEncoding(solver)==1)
+               printf("e1=%llu e2=%llu e4=%llu overFlow:%d\n", 
+                       getElementValue(solver,e1), getElementValue(solver, e2), 
+                       getElementValue(solver, e4), getBooleanValue(solver, overflow));
+       else
+               printf("UNSAT\n");
+       deleteSolver(solver);
+}

diff --git a/src/csolver.c b/src/csolver.c
index 2f3210d5f2036b179c25e4718cc84661f1b0d16b..78c60831ac83a481c9b5ed5d083ca0d531086f43 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -164,7 +164,10 @@ Element * applyFunction(CSolver *This, Function * function, Element ** array, ui
        return element;
 }
 
-Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus) {
+Boolean * applyPredicate(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs) {
+       return applyPredicateTable(This, predicate, inputs, numInputs, NULL);
+}
+Boolean * applyPredicateTable(CSolver *This, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus) {
        Boolean* boolean= allocBooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
        pushVectorBoolean(This->allBooleans, boolean);
        return boolean;

diff --git a/src/csolver.h b/src/csolver.h
index 2a3fea0332de425893522cee00255e7c2ff6e5ce..6ae5bdf284d912fc80bb26c8a7777c222f74d728 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -103,7 +103,9 @@ Element * applyFunction(CSolver *, Function * function, Element ** array, uint n
 
 /** This function applies a predicate to the Elements in its input. */
 
-Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
+Boolean * applyPredicateTable(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs, Boolean* undefinedStatus);
+
+Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs, uint numInputs);
 
 /** This function applies a logical operation to the Booleans in its input. */