From 61d4126f6169c6c55a42db0ba79c1f9a48b11632 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Tue, 23 Jan 2018 13:03:31 -0800 Subject: [PATCH] Adding more checks ... --- src/AST/set.cc | 2 +- src/Backend/satfunctableencoder.cc | 3 +-- src/csolver.cc | 4 ++++ src/csolver.h | 7 ++++++- 4 files changed, 12 insertions(+), 4 deletions(-) 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); -- 2.34.1