From: Hamed Date: Tue, 18 Jul 2017 21:01:09 +0000 (-0700) Subject: Adding a elemconst testcase + its bug fixe X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6d0d99cec27718d5e92098793012f12a94ac95b9;p=satune.git Adding a elemconst testcase + its bug fixe --- diff --git a/src/AST/element.h b/src/AST/element.h index beab5af..23e016c 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -49,6 +49,8 @@ static inline ElementEncoding* getElementEncoding(Element* This){ return &((ElementSet*)This)->encoding; case ELEMFUNCRETURN: return &((ElementFunction*)This)->rangeencoding; + case ELEMCONST: + return &((ElementConst*)This)->encoding; default: ASSERT(0); } diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c index 87d19b4..20241b4 100644 --- a/src/Backend/satelemencoder.c +++ b/src/Backend/satelemencoder.c @@ -27,7 +27,7 @@ Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) { ASTNodeType type = GETELEMENTTYPE(elem); - ASSERT(type == ELEMSET || type == ELEMFUNCRETURN); + ASSERT(type == ELEMSET || type == ELEMFUNCRETURN || type == ELEMCONST); ElementEncoding* elemEnc = getElementEncoding(elem); for(uint i=0; iencArraySize; i++){ if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) { diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index 5b2372b..6148074 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -130,6 +130,8 @@ void encodeElementSATEncoder(SATEncoder* encoder, Element *This){ case ELEMSET: generateElementEncoding(encoder, This); return; + case ELEMCONST: + return; default: ASSERT(0); } diff --git a/src/Test/buildconstraintstest.c b/src/Test/buildconstraintstest.c new file mode 100644 index 0000000..e795038 --- /dev/null +++ b/src/Test/buildconstraintstest.c @@ -0,0 +1,47 @@ +#include "csolver.h" + +int main(int numargs, char ** argv) { + CSolver * solver=allocCSolver(); + uint64_t set1[]={0, 1, 2}; + uint64_t setbigarray[]={0, 1, 2, 3, 4}; + + Set * s=createSet(solver, 0, set1, 3); + Set * setbig=createSet(solver, 0, setbigarray, 5); + Element * e1=getElementVar(solver, s); + Element * e2=getElementVar(solver, s); + Set * domain[]={s, s}; + Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2); + Element * inputs[]={e1, e2}; + Boolean * b=applyPredicate(solver, equals, inputs, 2); + addConstraint(solver, b); + + uint64_t set2[] = {2, 3}; + Set* rangef1 = createSet(solver, 1, set2, 2); + Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE); + + Table* table = createTable(solver, domain, 2, s); + uint64_t row1[] = {0, 1}; + uint64_t row2[] = {1, 1}; + uint64_t row3[] = {2, 1}; + uint64_t row4[] = {2, 2}; + addTableEntry(solver, table, row1, 2, 0); + addTableEntry(solver, table, row2, 2, 0); + addTableEntry(solver, table, row3, 2, 2); + addTableEntry(solver, table, row4, 2, 2); + Function * f2 = completeTable(solver, table); //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}; + Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2); + Element* inputs2 [] = {e4, e3}; + Boolean* pred = applyPredicate(solver, equal2, inputs2, 2); + addConstraint(solver, pred); + + if (startEncoding(solver)==1) + printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); + else + printf("UNSAT\n"); + deleteSolver(solver); +} diff --git a/src/Test/cnftest.c b/src/Test/cnftest.c new file mode 100644 index 0000000..6740543 --- /dev/null +++ b/src/Test/cnftest.c @@ -0,0 +1,34 @@ +#include "constraint.h" +#include + +int main(int numargs, char ** argv) { + CNF *cnf=createCNF(); + Edge v1=constraintNewVar(cnf); + Edge v2=constraintNewVar(cnf); + Edge v3=constraintNewVar(cnf); + Edge v4=constraintNewVar(cnf); + + Edge nv1=constraintNegate(v1); + Edge nv2=constraintNegate(v2); + Edge nv3=constraintNegate(v3); + Edge nv4=constraintNegate(v4); + + Edge c1=constraintAND2(cnf, v1, nv2); + Edge c2=constraintAND2(cnf, v3, nv4); + Edge c3=constraintAND2(cnf, nv1, v2); + Edge c4=constraintAND2(cnf, nv3, v4); + Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4)); + printCNF(cor); + printf("\n"); + addConstraintCNF(cnf, cor); + int value=solveCNF(cnf); + if (value==1) { + bool v1v=getValueCNF(cnf, v1); + bool v2v=getValueCNF(cnf, v2); + bool v3v=getValueCNF(cnf, v3); + bool v4v=getValueCNF(cnf, v4); + printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v); + } else + printf("%d\n",value); + deleteCNF(cnf); +} diff --git a/src/Test/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c new file mode 100644 index 0000000..1b6addb --- /dev/null +++ b/src/Test/elemequalityunsattest.c @@ -0,0 +1,22 @@ +#include "csolver.h" + +int main(int numargs, char ** argv) { + CSolver * solver=allocCSolver(); + uint64_t set1[]={0, 1, 2}; + uint64_t set2[]={3, 4}; + Set * s1=createSet(solver, 0, set1, 3); + Set * s2=createSet(solver, 0, set2, 2); + Element * e1=getElementVar(solver, s1); + Element * e2=getElementVar(solver, s2); + Set * domain[]={s1, s2}; + Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2); + Element * inputs[]={e1, e2}; + Boolean *b=applyPredicate(solver, equals, inputs, 2); + addConstraint(solver, b); + + if (startEncoding(solver)==1) + printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); + else + printf("UNSAT\n"); + deleteSolver(solver); +} diff --git a/src/Test/funcencodingtest.c b/src/Test/funcencodingtest.c new file mode 100644 index 0000000..0dacef0 --- /dev/null +++ b/src/Test/funcencodingtest.c @@ -0,0 +1,66 @@ +#include "csolver.h" + +int main(int numargs, char ** argv) { + CSolver * solver=allocCSolver(); + uint64_t set1[]={6}; + uint64_t set2[]={4, 2}; + uint64_t set3[]={3, 1}; + uint64_t set4[]={2, 3, 1}; + uint64_t set5[]={2, 1, 0}; + Set * s1=createSet(solver, 0, set1, 1); + Set * s2=createSet(solver, 0, set2, 2); + Set * s3=createSet(solver, 0, set3, 2); + Set * s4=createSet(solver, 0, set4, 3); + Set * s5=createSet(solver, 0, set5, 3); + Element * e1=getElementVar(solver, s1); + Element * e2=getElementVar(solver, s2); + Element * e7=getElementVar(solver, s5); + Boolean* overflow = getBooleanVar(solver , 2); + Set * d1[]={s1, s2}; + //change the overflow flag + Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE); + Element * in1[]={e1, e2}; + Element * e3 = applyFunction(solver, f1, in1, 2, overflow); + Table* t1 = createTable(solver, d1, 2, s3); + uint64_t row1[] = {6, 2}; + uint64_t row2[] = {6, 4}; + addTableEntry(solver, t1, row1, 2, 3); + addTableEntry(solver, t1, row2, 2, 1); + Function * f2 = completeTable(solver, t1); + Element * e4 = applyFunction(solver, f2, in1, 2, overflow); + + Set *d2[] = {s1}; + Element *in2[]={e1}; + Table* t2 = createTable(solver, d2, 1, s1); + uint64_t row3[] = {6}; + addTableEntry(solver, t2, row3, 1, 6); + Function * f3 = completeTable(solver, t2); + Element * e5 = applyFunction(solver, f3, in2, 1, overflow); + + Set *d3[] = {s2, s3, s1}; + Element *in3[]={e3, e4, e5}; + Table* t3 = createTable(solver, d3, 3, s4); + uint64_t row4[] = {4, 3, 6}; + uint64_t row5[] = {2, 1, 6}; + uint64_t row6[] = {2, 3, 6}; + uint64_t row7[] = {4, 1, 6}; + addTableEntry(solver, t3, row4, 3, 3); + addTableEntry(solver, t3, row5, 3, 1); + addTableEntry(solver, t3, row6, 3, 2); + addTableEntry(solver, t3, row7, 3, 1); + Function * f4 = completeTable(solver, t3); + Element * e6 = applyFunction(solver, f4, in3, 3, overflow); + + Set* deq[] = {s5,s4}; + Predicate* gt = createPredicateOperator(solver, GT, deq, 2); + Element* inputs2 [] = {e7, e6}; + Boolean* pred = applyPredicate(solver, gt, inputs2, 2); + addConstraint(solver, pred); + + if (startEncoding(solver)==1) + printf("e1=%llu e2=%llu e7=%llu\n", + getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7)); + else + printf("UNSAT\n"); + deleteSolver(solver); +} diff --git a/src/Test/ltelemconsttest.c b/src/Test/ltelemconsttest.c new file mode 100644 index 0000000..e058b04 --- /dev/null +++ b/src/Test/ltelemconsttest.c @@ -0,0 +1,21 @@ +#include "csolver.h" + +int main(int numargs, char ** argv){ + CSolver *solver=allocCSolver(); + uint64_t set1[]={5}; + uint64_t set3[]={1, 3, 4, 6}; + Set * s1=createSet(solver, 0, set1, 3); + Set * s3=createSet(solver, 0, set3, 4); + Element * e1=getElementConst(solver, 4, 5); + Element * e2=getElementVar(solver, s3); + Set * domain2[]={s1, s3}; + Predicate *lt=createPredicateOperator(solver, LT, domain2, 2); + Element * inputs2[]={e1, e2}; + 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)); + else + printf("UNSAT\n"); + deleteSolver(solver); +} \ No newline at end of file diff --git a/src/Test/testbuildconstraints.c b/src/Test/testbuildconstraints.c deleted file mode 100644 index e795038..0000000 --- a/src/Test/testbuildconstraints.c +++ /dev/null @@ -1,47 +0,0 @@ -#include "csolver.h" - -int main(int numargs, char ** argv) { - CSolver * solver=allocCSolver(); - uint64_t set1[]={0, 1, 2}; - uint64_t setbigarray[]={0, 1, 2, 3, 4}; - - Set * s=createSet(solver, 0, set1, 3); - Set * setbig=createSet(solver, 0, setbigarray, 5); - Element * e1=getElementVar(solver, s); - Element * e2=getElementVar(solver, s); - Set * domain[]={s, s}; - Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2); - Element * inputs[]={e1, e2}; - Boolean * b=applyPredicate(solver, equals, inputs, 2); - addConstraint(solver, b); - - uint64_t set2[] = {2, 3}; - Set* rangef1 = createSet(solver, 1, set2, 2); - Function * f1 = createFunctionOperator(solver, ADD, domain, 2, setbig, IGNORE); - - Table* table = createTable(solver, domain, 2, s); - uint64_t row1[] = {0, 1}; - uint64_t row2[] = {1, 1}; - uint64_t row3[] = {2, 1}; - uint64_t row4[] = {2, 2}; - addTableEntry(solver, table, row1, 2, 0); - addTableEntry(solver, table, row2, 2, 0); - addTableEntry(solver, table, row3, 2, 2); - addTableEntry(solver, table, row4, 2, 2); - Function * f2 = completeTable(solver, table); //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}; - Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2); - Element* inputs2 [] = {e4, e3}; - Boolean* pred = applyPredicate(solver, equal2, inputs2, 2); - addConstraint(solver, pred); - - if (startEncoding(solver)==1) - printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); - else - printf("UNSAT\n"); - deleteSolver(solver); -} diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c deleted file mode 100644 index 6740543..0000000 --- a/src/Test/testcnf.c +++ /dev/null @@ -1,34 +0,0 @@ -#include "constraint.h" -#include - -int main(int numargs, char ** argv) { - CNF *cnf=createCNF(); - Edge v1=constraintNewVar(cnf); - Edge v2=constraintNewVar(cnf); - Edge v3=constraintNewVar(cnf); - Edge v4=constraintNewVar(cnf); - - Edge nv1=constraintNegate(v1); - Edge nv2=constraintNegate(v2); - Edge nv3=constraintNegate(v3); - Edge nv4=constraintNegate(v4); - - Edge c1=constraintAND2(cnf, v1, nv2); - Edge c2=constraintAND2(cnf, v3, nv4); - Edge c3=constraintAND2(cnf, nv1, v2); - Edge c4=constraintAND2(cnf, nv3, v4); - Edge cor=constraintOR2(cnf, constraintAND2(cnf, c1, c2), constraintAND2(cnf, c3, c4)); - printCNF(cor); - printf("\n"); - addConstraintCNF(cnf, cor); - int value=solveCNF(cnf); - if (value==1) { - bool v1v=getValueCNF(cnf, v1); - bool v2v=getValueCNF(cnf, v2); - bool v3v=getValueCNF(cnf, v3); - bool v4v=getValueCNF(cnf, v4); - printf("%d %u %u %u %u\n", value, v1v, v2v, v3v, v4v); - } else - printf("%d\n",value); - deleteCNF(cnf); -} diff --git a/src/Test/testelementlt.c b/src/Test/testelementlt.c deleted file mode 100644 index e9ddda1..0000000 --- a/src/Test/testelementlt.c +++ /dev/null @@ -1,21 +0,0 @@ -#include "csolver.h" - -int main(int numargs, char ** argv){ - CSolver *solver=allocCSolver(); - uint64_t set1[]={0, 1, 2}; - uint64_t set3[]={1, 3, 4, 5}; - Set * s1=createSet(solver, 0, set1, 3); - Set * s3=createSet(solver, 0, set3, 4); - Element * e1=getElementVar(solver, s1); - Element * e3=getElementVar(solver, s3); - Set * domain2[]={s1, s3}; - Predicate *lt=createPredicateOperator(solver, LT, domain2, 2); - Element * inputs2[]={e1, e3}; - Boolean *b=applyPredicate(solver, lt, inputs2, 2); - addConstraint(solver, b); - if (startEncoding(solver)==1) - printf("e1=%llu e3=%llu\n", getElementValue(solver,e1), getElementValue(solver, e3)); - else - printf("UNSAT\n"); - deleteSolver(solver); -} \ No newline at end of file diff --git a/src/Test/testelemequalityunsat.c b/src/Test/testelemequalityunsat.c deleted file mode 100644 index 1b6addb..0000000 --- a/src/Test/testelemequalityunsat.c +++ /dev/null @@ -1,22 +0,0 @@ -#include "csolver.h" - -int main(int numargs, char ** argv) { - CSolver * solver=allocCSolver(); - uint64_t set1[]={0, 1, 2}; - uint64_t set2[]={3, 4}; - Set * s1=createSet(solver, 0, set1, 3); - Set * s2=createSet(solver, 0, set2, 2); - Element * e1=getElementVar(solver, s1); - Element * e2=getElementVar(solver, s2); - Set * domain[]={s1, s2}; - Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2); - Element * inputs[]={e1, e2}; - Boolean *b=applyPredicate(solver, equals, inputs, 2); - addConstraint(solver, b); - - if (startEncoding(solver)==1) - printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); - else - printf("UNSAT\n"); - deleteSolver(solver); -} diff --git a/src/Test/testfuncencoding.c b/src/Test/testfuncencoding.c deleted file mode 100644 index 0dacef0..0000000 --- a/src/Test/testfuncencoding.c +++ /dev/null @@ -1,66 +0,0 @@ -#include "csolver.h" - -int main(int numargs, char ** argv) { - CSolver * solver=allocCSolver(); - uint64_t set1[]={6}; - uint64_t set2[]={4, 2}; - uint64_t set3[]={3, 1}; - uint64_t set4[]={2, 3, 1}; - uint64_t set5[]={2, 1, 0}; - Set * s1=createSet(solver, 0, set1, 1); - Set * s2=createSet(solver, 0, set2, 2); - Set * s3=createSet(solver, 0, set3, 2); - Set * s4=createSet(solver, 0, set4, 3); - Set * s5=createSet(solver, 0, set5, 3); - Element * e1=getElementVar(solver, s1); - Element * e2=getElementVar(solver, s2); - Element * e7=getElementVar(solver, s5); - Boolean* overflow = getBooleanVar(solver , 2); - Set * d1[]={s1, s2}; - //change the overflow flag - Function * f1 = createFunctionOperator(solver, SUB, d1, 2, s2, IGNORE); - Element * in1[]={e1, e2}; - Element * e3 = applyFunction(solver, f1, in1, 2, overflow); - Table* t1 = createTable(solver, d1, 2, s3); - uint64_t row1[] = {6, 2}; - uint64_t row2[] = {6, 4}; - addTableEntry(solver, t1, row1, 2, 3); - addTableEntry(solver, t1, row2, 2, 1); - Function * f2 = completeTable(solver, t1); - Element * e4 = applyFunction(solver, f2, in1, 2, overflow); - - Set *d2[] = {s1}; - Element *in2[]={e1}; - Table* t2 = createTable(solver, d2, 1, s1); - uint64_t row3[] = {6}; - addTableEntry(solver, t2, row3, 1, 6); - Function * f3 = completeTable(solver, t2); - Element * e5 = applyFunction(solver, f3, in2, 1, overflow); - - Set *d3[] = {s2, s3, s1}; - Element *in3[]={e3, e4, e5}; - Table* t3 = createTable(solver, d3, 3, s4); - uint64_t row4[] = {4, 3, 6}; - uint64_t row5[] = {2, 1, 6}; - uint64_t row6[] = {2, 3, 6}; - uint64_t row7[] = {4, 1, 6}; - addTableEntry(solver, t3, row4, 3, 3); - addTableEntry(solver, t3, row5, 3, 1); - addTableEntry(solver, t3, row6, 3, 2); - addTableEntry(solver, t3, row7, 3, 1); - Function * f4 = completeTable(solver, t3); - Element * e6 = applyFunction(solver, f4, in3, 3, overflow); - - Set* deq[] = {s5,s4}; - Predicate* gt = createPredicateOperator(solver, GT, deq, 2); - Element* inputs2 [] = {e7, e6}; - Boolean* pred = applyPredicate(solver, gt, inputs2, 2); - addConstraint(solver, pred); - - if (startEncoding(solver)==1) - printf("e1=%llu e2=%llu e7=%llu\n", - getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7)); - else - printf("UNSAT\n"); - deleteSolver(solver); -} diff --git a/src/csolver.c b/src/csolver.c index c92aee6..cfef6f4 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -196,6 +196,7 @@ int startEncoding(CSolver* This){ uint64_t getElementValue(CSolver* This, Element* element){ switch(GETELEMENTTYPE(element)){ case ELEMSET: + case ELEMCONST: return getElementValueSATTranslator(This, element); default: ASSERT(0);