From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 23 Jan 2018 21:03:31 +0000 (-0800)
Subject: Adding more checks ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=61d4126f6169c6c55a42db0ba79c1f9a48b11632;p=satune.git

Adding more checks ...
---

diff --git a/src/AST/set.cc b/src/AST/set.cc
index e019b12..585ae6d 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -59,7 +59,7 @@ uint64_t Set::getElement(uint index) {
 		return low + index;
 	else
 		return members->get(index);
-}
+        }
 
 uint Set::getSize() {
 	if (isRange) {
diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 961d810..b226cc1 100644
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -89,7 +89,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 	}
 	bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
 	uint numDomains = predicate->table->numDomains();
-
+        ASSERT(numDomains != 0);
 	VectorEdge *clauses = allocDefVectorEdge();
 
 	uint indices[numDomains];	//setup indices
@@ -269,7 +269,6 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 		switch (function->undefBehavior) {
 		case SATC_UNDEFINEDSETSFLAG: {
 			if (isInRange) {
-				//FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
 				clause = constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]);
 			} else {
 				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
diff --git a/src/csolver.cc b/src/csolver.cc
index b74df47..5d4f56d 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -182,6 +182,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
 	return set;
 }
 
+bool CSolver::itemExistInSet(Set *set, uint64_t item){
+        return set->exists(item);
+}
+
 VarType CSolver::getSetVarType(Set *set) {
 	return set->getType();
 }
diff --git a/src/csolver.h b/src/csolver.h
index 523ac30..e254abb 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -18,12 +18,17 @@ public:
 	/** This function creates a set from lowrange to highrange (inclusive). */
 
 	Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
+        
+        bool itemExistInSet(Set *set, uint64_t item);
 
 	VarType getSetVarType(Set *set);
 
 	Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
-	/** This function creates a mutable set. */
+	/** This function creates a mutable set.
+         * Note: You should use addItem for adding new item to Mutable sets, and
+         * at the end, you should call finalizeMutableSet!
+         */
 
 	MutableSet *createMutableSet(VarType type);