From: Hamed Date: Thu, 20 Jul 2017 22:03:11 +0000 (-0700) Subject: Adding a new test case for testing FLAGIFFUNDEFINED + bug fixes X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=057db1c3a09d6caef13bee02791ce7d9f3789d29;p=satune.git Adding a new test case for testing FLAGIFFUNDEFINED + bug fixes --- diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c index a4f9a82..c15e822 100644 --- 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 1e336c2..e7fffe6 100644 --- 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 ed4fc4d..bd38ed9 100644 --- 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 c1162ee..4962f3f 100644 --- 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 f96be92..3823949 100644 --- 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 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 2f3210d..78c6083 100644 --- 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 2a3fea0..6ae5bdf 100644 --- 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. */