Adding more checks ...
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 23 Jan 2018 21:03:31 +0000 (13:03 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 23 Jan 2018 21:03:31 +0000 (13:03 -0800)
src/AST/set.cc
src/Backend/satfunctableencoder.cc
src/csolver.cc
src/csolver.h

index e019b12..585ae6d 100644 (file)
@@ -59,7 +59,7 @@ uint64_t Set::getElement(uint index) {
                return low + index;
        else
                return members->get(index);
-}
+        }
 
 uint Set::getSize() {
        if (isRange) {
index 961d810..b226cc1 100644 (file)
@@ -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));
index b74df47..5d4f56d 100644 (file)
@@ -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();
 }
index 523ac30..e254abb 100644 (file)
@@ -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);