Test case for table-based predicate + fixing bugs

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index 6d11998eb24bbdc19c16044e55ac33b2359129e1..5ae30bf256d1b9761d589579f56adae167c7b393 100644 (file)
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -89,49 +89,46 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
        }
 
        Edge undefConstraint = encodeConstraintSATEncoder (This, constraint->undefStatus);
-       
+       printCNF(undefConstraint);
        bool notfinished=true;
        while(notfinished) {
                Edge carray[numDomains];
                TableEntry* tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
                bool isInRange = tableEntry!=NULL;
-               bool ignoreEntry = generateNegation == tableEntry->output;
-               ASSERT(predicate->undefinedbehavior == UNDEFINEDSETSFLAG || predicate->undefinedbehavior == FLAGIFFUNDEFINED);
-               //Include this in the set of terms
+               if(isInRange && generateNegation == tableEntry->output)
+                       goto NEXT;
+               Edge clause;
                for(uint i=0;i<numDomains;i++) {
-                       Element * elem = getArrayElement(&constraint->inputs, i);
-                       carray[i] = getElementValueConstraint(This, elem, vals[i]);
+                               Element * elem = getArrayElement(&constraint->inputs, i);
+                               carray[i] = getElementValueConstraint(This, elem, vals[i]);
                }
-
-               Edge clause;
+       
                switch(predicate->undefinedbehavior) {
-                       case UNDEFINEDSETSFLAG: {
-                               if (isInRange && !ignoreEntry) {
+                       case UNDEFINEDSETSFLAG:
+                               if(isInRange){
                                        clause=constraintAND(This->cnf, numDomains, carray);
-                               } else if(!isInRange) {
+                               }else{
                                        clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
                                }
                                break;
-                       }
-                       case FLAGIFFUNDEFINED: {
-                               if (isInRange && !ignoreEntry) {
-                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
-                               } else if(!isInRange) {
+                       case FLAGIFFUNDEFINED:
+                               if(isInRange){
+                                       clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint));
+                               }else{
                                        clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
                                }
                                break;
-                       }
+
                        default:
                                ASSERT(0);
-               }
+               }       
 #ifdef TRACE_DEBUG
                model_print("added clause in predicate table enumeration ...\n");
                printCNF(clause);
                model_print("\n");
 #endif
                pushVectorEdge(clauses, clause);
-               
-               
+NEXT:  
                notfinished=false;
                for(uint i=0;i<numDomains; i++) {
                        uint index=++indices[i];
@@ -237,7 +234,6 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
                TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
                bool isInRange = tableEntry!=NULL;
                ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
-               //Include this in the set of terms
                for(uint i=0;i<numDomains;i++) {
                        Element * elem = getArrayElement(&elemFunc->inputs, i);
                        carray[i] = getElementValueConstraint(This, elem, vals[i]);

diff --git a/src/Test/tablepredicencodetest.c b/src/Test/tablepredicencodetest.c
new file mode 100644 (file)
index 0000000..536879e
--- /dev/null
+++ b/src/Test/tablepredicencodetest.c
@@ -0,0 +1,66 @@
+#include "csolver.h"
+/**
+ * e1 = {1, 2}
+ * e2={1, 3, 5, 7}
+ * e3 = {6, 10, 19}
+ * e4= p(e1, e2, e3) 
+ *     1 5 6 => T
+ *     2 3 19 => T
+ *     1 3 19 => F
+ *     2 7 10 => F
+ *     1 7 6 => F
+ *     2 5 6 => T
+ * e1 == e2
+ * e3 >= e2 
+ * Result: e1=1, e2=1, e3=6 OR 10 OR 19, overflow=1
+ */
+int main(int numargs, char ** argv) {
+       CSolver * solver=allocCSolver();
+       uint64_t set1[]={1, 2};
+       uint64_t set2[]={1, 3, 5, 7};
+       uint64_t set3[]={6, 10, 19};
+       Set * s1=createSet(solver, 0, set1, 2);
+       Set * s2=createSet(solver, 0, set2, 4);
+       Set * s3=createSet(solver, 0, set3, 3);
+       Element * e1=getElementVar(solver, s1);
+       Element * e2=getElementVar(solver, s2);
+       Element * e3=getElementVar(solver, s3);
+       Set * d2[]={s1, s2, s3};
+       //change the overflow flag
+       Table* t1 = createTableForPredicate(solver, d2, 3);
+       uint64_t row1[] = {1, 5, 6};
+       uint64_t row2[] = {2, 3, 19};
+       uint64_t row3[] = {1, 3, 19};
+       uint64_t row4[] = {2, 7, 10};
+       uint64_t row5[] = {1, 7, 6};
+       uint64_t row6[] = {2, 5, 6};
+       addTableEntry(solver, t1, row1, 3, true);
+       addTableEntry(solver, t1, row2, 3, true);
+       addTableEntry(solver, t1, row3, 3, false);
+       addTableEntry(solver, t1, row4, 3, false);
+       addTableEntry(solver, t1, row5, 3, false);
+       addTableEntry(solver, t1, row6, 3, true);
+       Predicate * p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED);
+       Boolean* undef = getBooleanVar(solver , 2);
+       Boolean* b1 =applyPredicateTable(solver, p1, (Element* []){e1, e2, e3}, 3, undef);
+       addConstraint(solver, b1);
+       
+       Set* deq[] = {s3,s2};
+       Predicate* gte = createPredicateOperator(solver, GTE, deq, 2);
+       Element* inputs2 [] = {e3, e2};
+       Boolean* pred = applyPredicate(solver, gte, inputs2, 2);
+       addConstraint(solver, pred);
+       
+       Set * d1[]={s1, s2};
+       Predicate* eq = createPredicateOperator(solver, EQUALS, d1, 2);
+       Boolean* pred2 = applyPredicate(solver, eq,(Element*[]) {e1, e2}, 2);
+       addConstraint(solver, pred2);
+       
+       if (startEncoding(solver)==1)
+               printf("e1=%llu e2=%llu e3=%llu undefFlag:%d\n", 
+                       getElementValue(solver,e1), getElementValue(solver, e2), 
+                       getElementValue(solver, e3), getBooleanValue(solver, undef));
+       else
+               printf("UNSAT\n");
+       deleteSolver(solver);
+}

diff --git a/src/csolver.h b/src/csolver.h
index 6ae5bdf284d912fc80bb26c8a7777c222f74d728..b35f80100b278d6846b77eaefaa3e3aded85e134 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -87,8 +87,7 @@ Predicate * createPredicateTable(CSolver *solver, Table* table, UndefinedBehavio
 
 Table * createTable(CSolver *solver, Set **domains, uint numDomain, Set * range);
 
-Table * createTablePredicate(CSolver *solver, Set **domains, uint numDomain);
-
+Table * createTableForPredicate(CSolver *solver, Set **domains, uint numDomain);
 /** This function adds an input output relation to a table. */
 
 void addTableEntry(CSolver *solver, Table* table, uint64_t* inputs, uint inputSize, uint64_t result);