Adding a new testcase for circuit-based equals + bug fixes ...

diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
index 94b990980136383d01e834127498092439d3c71b..1df9c61de5477ad77c992495845b010e3ffda63c 100644 (file)
--- a/src/Backend/satfuncopencoder.c
+++ b/src/Backend/satfuncopencoder.c
@@ -212,11 +212,14 @@ Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
        PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
        ASSERT(getSizeArraySet(&predicate->domains) == 2);
        Element *elem0 = getArrayElement( &constraint->inputs, 0);
+       encodeElementSATEncoder(This, elem0);
        Element *elem1 = getArrayElement( &constraint->inputs, 1);
+       encodeElementSATEncoder(This, elem1);
        ElementEncoding *ee0=getElementEncoding(elem0);
        ElementEncoding *ee1=getElementEncoding(elem1);
        ASSERT(ee0->numVars==ee1->numVars);
        uint numVars=ee0->numVars;
+       ASSERT(numVars != 0);
        Edge carray[numVars];
        for (uint i=0; i<numVars; i++) {
                carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);

diff --git a/src/Encoders/naiveencoder.c b/src/Encoders/naiveencoder.c
index 6fe0ac84ce400abc3e7ecbe5eaa5f17d40eed2e1..3bb927cf722abd076bfb1f0b71260ca35baa7fcf 100644 (file)
--- a/src/Encoders/naiveencoder.c
+++ b/src/Encoders/naiveencoder.c
@@ -61,7 +61,7 @@ void naiveEncodingPredicate(BooleanPredicate * This) {
 void naiveEncodingElement(Element * This) {
        ElementEncoding * encoding = getElementEncoding(This);
        if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
-               setElementEncodingType(encoding, UNARY);
+               setElementEncodingType(encoding, BINARYINDEX);
                encodingArrayInitialization(encoding);
        }
        

diff --git a/src/Test/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c
deleted file mode 100644 (file)
index bd38ed9..0000000
--- a/src/Test/elemequalityunsattest.c
+++ /dev/null
@@ -1,28 +0,0 @@
-#include "csolver.h"
-/**
- * e1 = {0, 1, 2}
- * e2 = {3, 4}
- * e1 == e2
- * 
- * Result: UNSAT
- */
-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/elemequalsattest.c b/src/Test/elemequalsattest.c
new file mode 100644 (file)
index 0000000..718dc67
--- /dev/null
+++ b/src/Test/elemequalsattest.c
@@ -0,0 +1,33 @@
+#include "csolver.h"
+/**
+ * e1 = {0, 1, 2}
+ * e2 = {3, 1, 7}
+ * e1 == e2
+ * 
+ * Result (Enumeration):
+ *     e1=1 e2=1
+ * Result (circuit):
+ *     e1=0 e2=3 
+ *     e1=1 e2=1 
+ *     e1=2 e2=7 
+ */
+int main(int numargs, char ** argv) {
+       CSolver * solver=allocCSolver();
+       uint64_t set1[]={0, 1, 2};
+       uint64_t set2[]={3, 1, 7};
+       Set * s1=createSet(solver, 0, set1, 3);
+       Set * s2=createSet(solver, 0, set2, 3);
+       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/elemequalunsattest.c b/src/Test/elemequalunsattest.c
new file mode 100644 (file)
index 0000000..bd38ed9
--- /dev/null
+++ b/src/Test/elemequalunsattest.c
@@ -0,0 +1,28 @@
+#include "csolver.h"
+/**
+ * e1 = {0, 1, 2}
+ * e2 = {3, 4}
+ * e1 == e2
+ * 
+ * Result: UNSAT
+ */
+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);
+}