Adding a elemconst testcase + its bug fixe

diff --git a/src/AST/element.h b/src/AST/element.h
index beab5af1e17aa065249afbae95a96c2109ab50d7..23e016cb0cc2a902a35d7c97b128fd1733031637 100644 (file)
--- 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 87d19b4ae31b5747cdfe46b45876beca6eb8e8b5..20241b46f35863767528abe089c38ba8dcd0d52c 100644 (file)
--- 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; i<elemEnc->encArraySize; i++){
                if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 5b2372b1cb626b2c6e969cc34e0a996b116c9d34..6148074c749c06b6fdf6164af3ff7cd9f6cb4646 100644 (file)
--- 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 (file)
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 (file)
index 0000000..6740543
--- /dev/null
+++ b/src/Test/cnftest.c
@@ -0,0 +1,34 @@
+#include "constraint.h"
+#include <stdio.h>
+
+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 (file)
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 (file)
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 (file)
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 (file)
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 (file)
index 6740543..0000000
--- a/src/Test/testcnf.c
+++ /dev/null
@@ -1,34 +0,0 @@
-#include "constraint.h"
-#include <stdio.h>
-
-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 (file)
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 (file)
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 (file)
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 c92aee6b6b6b94cdaa47d546d24ca5ee102d099a..cfef6f4f8af780dba58f393bf47eaa856e1cab7b 100644 (file)
--- 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);