Adding more checks ...

diff --git a/src/AST/set.cc b/src/AST/set.cc
index e019b12a3c3f333adfbbaf7b79c0485cb09d72d3..585ae6d1068a109cadf9891d555db7548972b44c 100644 (file)
--- 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 961d810f1766b7850b39926d6fd69d471111047d..b226cc17e4cf359ed9ef2d20232bd536a608317f 100644 (file)
--- 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 b74df47f37c6c22cb20c2e5391b2c0d4e09533ea..5d4f56d2e1897b6311e629835e533b54f07891b6 100644 (file)
--- 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 523ac307194534f1c7e35a302247cef2cc8032a7..e254abbc29c8026ddc274166f4b9de23c167c89d 100644 (file)
--- 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);