From 3a8a8fde847fb3197d24286084d97b4f6a01183e Mon Sep 17 00:00:00 2001 From: Hamed Date: Thu, 20 Jul 2017 18:11:26 -0700 Subject: [PATCH] Test case for table-based predicate + fixing bugs --- src/Backend/satfunctableencoder.c | 38 ++++++++---------- src/Test/tablepredicencodetest.c | 66 +++++++++++++++++++++++++++++++ src/csolver.h | 3 +- 3 files changed, 84 insertions(+), 23 deletions(-) create mode 100644 src/Test/tablepredicencodetest.c diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c index 6d11998..5ae30bf 100644 --- 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;iinputs, 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;itable, vals, numDomains); bool isInRange = tableEntry!=NULL; ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED); - //Include this in the set of terms for(uint i=0;iinputs, i); carray[i] = getElementValueConstraint(This, elem, vals[i]); diff --git a/src/Test/tablepredicencodetest.c b/src/Test/tablepredicencodetest.c new file mode 100644 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 6ae5bdf..b35f801 100644 --- 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); -- 2.34.1