From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 25 Jul 2017 20:00:07 +0000 (-0700)
Subject: Adding a new testcase for circuit-based equals + bug fixes ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=370410b6c810e42b81df32b718b86eb3d5bd4d50;p=satune.git

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

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/elemequalityunsattest.c b/src/Test/elemequalityunsattest.c
deleted file mode 100644
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
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
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);
+}