2 testcases are added + their bugs are fixed ...

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 4e1ba3ef36be39ea2ebe4e5f69255c89e282c22f..741806ea2cd350debe590ecc720e62c80edb8dc0 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -136,7 +136,8 @@ Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate *
                        }
                }
        }
-
+       if(getSizeVectorEdge(clauses) == 0)
+               return E_False;
        Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
        deleteVectorEdge(clauses);
        return generateNegation ? constraintNegate(cor) : cor;

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index f30ebd025371ad0aba37c0fe212eee407c3f71e2..e795038dfcacbb48a1d1dab6347f4b20773ae0fb 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -41,5 +41,7 @@ int main(int numargs, char ** argv) {
        
        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/elemequalityunsat.c b/src/Test/elemequalityunsat.c
new file mode 100644 (file)
index 0000000..1b6addb
--- /dev/null
+++ b/src/Test/elemequalityunsat.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/elemlt.c b/src/Test/elemlt.c
new file mode 100644 (file)
index 0000000..e9ddda1
--- /dev/null
+++ b/src/Test/elemlt.c
@@ -0,0 +1,21 @@
+#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