From 370410b6c810e42b81df32b718b86eb3d5bd4d50 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 25 Jul 2017 13:00:07 -0700
Subject: [PATCH] Adding a new testcase for circuit-based equals + bug fixes
 ...

---
 src/Backend/satfuncopencoder.c                |  3 ++
 src/Encoders/naiveencoder.c                   |  2 +-
 src/Test/elemequalsattest.c                   | 33 +++++++++++++++++++
 ...ualityunsattest.c => elemequalunsattest.c} |  0
 4 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 src/Test/elemequalsattest.c
 rename src/Test/{elemequalityunsattest.c => elemequalunsattest.c} (100%)

diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
index 94b9909..1df9c61 100644
--- 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 6fe0ac8..3bb927c 100644
--- 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/elemequalsattest.c b/src/Test/elemequalsattest.c
new file mode 100644
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/elemequalityunsattest.c b/src/Test/elemequalunsattest.c
similarity index 100%
rename from src/Test/elemequalityunsattest.c
rename to src/Test/elemequalunsattest.c
-- 
2.34.1