Adding more checks ...

[satune.git] / src / Backend / satfunctableencoder.cc

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));