From 6d0d99cec27718d5e92098793012f12a94ac95b9 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 14:01:09 -0700
Subject: [PATCH] Adding a elemconst testcase + its bug fixe

---
 src/AST/element.h                                    |  2 ++
 src/Backend/satelemencoder.c                         |  2 +-
 src/Backend/satencoder.c                             |  2 ++
 ...testbuildconstraints.c => buildconstraintstest.c} |  0
 src/Test/{testcnf.c => cnftest.c}                    |  0
 ...stelemequalityunsat.c => elemequalityunsattest.c} |  0
 src/Test/{testfuncencoding.c => funcencodingtest.c}  |  0
 src/Test/{testelementlt.c => ltelemconsttest.c}      | 12 ++++++------
 src/csolver.c                                        |  1 +
 9 files changed, 12 insertions(+), 7 deletions(-)
 rename src/Test/{testbuildconstraints.c => buildconstraintstest.c} (100%)
 rename src/Test/{testcnf.c => cnftest.c} (100%)
 rename src/Test/{testelemequalityunsat.c => elemequalityunsattest.c} (100%)
 rename src/Test/{testfuncencoding.c => funcencodingtest.c} (100%)
 rename src/Test/{testelementlt.c => ltelemconsttest.c} (61%)

diff --git a/src/AST/element.h b/src/AST/element.h
index beab5af..23e016c 100644
--- 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 87d19b4..20241b4 100644
--- 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 5b2372b..6148074 100644
--- 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/testbuildconstraints.c b/src/Test/buildconstraintstest.c
similarity index 100%
rename from src/Test/testbuildconstraints.c
rename to src/Test/buildconstraintstest.c
diff --git a/src/Test/testcnf.c b/src/Test/cnftest.c
similarity index 100%
rename from src/Test/testcnf.c
rename to src/Test/cnftest.c
diff --git a/src/Test/testelemequalityunsat.c b/src/Test/elemequalityunsattest.c
similarity index 100%
rename from src/Test/testelemequalityunsat.c
rename to src/Test/elemequalityunsattest.c
diff --git a/src/Test/testfuncencoding.c b/src/Test/funcencodingtest.c
similarity index 100%
rename from src/Test/testfuncencoding.c
rename to src/Test/funcencodingtest.c
diff --git a/src/Test/testelementlt.c b/src/Test/ltelemconsttest.c
similarity index 61%
rename from src/Test/testelementlt.c
rename to src/Test/ltelemconsttest.c
index e9ddda1..e058b04 100644
--- a/src/Test/testelementlt.c
+++ b/src/Test/ltelemconsttest.c
@@ -2,19 +2,19 @@
 
 int main(int numargs, char ** argv){
 	CSolver *solver=allocCSolver();
-	uint64_t set1[]={0, 1, 2};
-	uint64_t set3[]={1, 3, 4, 5};
+	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=getElementVar(solver, s1);
-	Element * e3=getElementVar(solver, s3);
+	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, e3};
+	Element * inputs2[]={e1, e2};
 	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));
+		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
 	else
 		printf("UNSAT\n");
 	deleteSolver(solver);
diff --git a/src/csolver.c b/src/csolver.c
index c92aee6..cfef6f4 100644
--- 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);
-- 
2.34.1