Edits

diff --git a/src/AST/element.cc b/src/AST/element.cc
index fd308122caee3b28cd5a71226d4f591872113f57..589e3f50130a25e8514cd6476ee8d16ba89d7598 100644 (file)
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -38,14 +38,7 @@ Set *getElementSet(Element *This) {
                return ((ElementConst *)This)->set;
        case ELEMFUNCRETURN: {
                Function *func = ((ElementFunction *)This)->function;
-               switch (func->type) {
-               case TABLEFUNC:
-                       return ((FunctionTable *)func)->table->range;
-               case OPERATORFUNC:
-                       return ((FunctionOperator *)func)->range;
-               default:
-                       ASSERT(0);
-               }
+               return func->getRange();
        }
        default:
                ASSERT(0);

diff --git a/src/AST/function.cc b/src/AST/function.cc
index d6b2d3af814c02d589722406614ef101b2c7f0b4..a882580e957e7e67a5f8d4f5f04d6960c83af1a9 100644 (file)
--- a/src/AST/function.cc
+++ b/src/AST/function.cc
@@ -60,3 +60,7 @@ Function *FunctionTable::clone(CSolver *solver, CloneMap *map) {
        map->put(this, f);
        return f;
 }
+
+Set * FunctionTable::getRange() {
+       return table->getRange();
+}

diff --git a/src/AST/function.h b/src/AST/function.h
index fcb5068ad7703b296130450f6cebad838edacae5..f34c02eaa5b062fc02ad0928cee839dcc93c7d14 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -12,6 +12,7 @@ public:
        FunctionType type;
        virtual ~Function() {}
        virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
+       virtual Set * getRange() = 0;
        CMEMALLOC;
 };
 
@@ -25,6 +26,7 @@ public:
        uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
        bool isInRangeFunction(uint64_t val);
        Function *clone(CSolver *solver, CloneMap *map);
+       Set * getRange() {return range;}
        CMEMALLOC;
 };
 
@@ -34,6 +36,7 @@ public:
        UndefinedBehavior undefBehavior;
        FunctionTable (Table *table, UndefinedBehavior behavior);
        Function *clone(CSolver *solver, CloneMap *map);
+       Set * getRange();
        CMEMALLOC;
 };
 

diff --git a/src/AST/table.h b/src/AST/table.h
index 39b561ce386b38f6efee7a1b7dd20864cccdeffe..6c7926e80e04f42c1437b9d10df5132198efb3a8 100644 (file)
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -11,10 +11,20 @@ public:
        TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
        Table *clone(CSolver *solver, CloneMap *map);
        ~Table();
+       Set * getRange() {return range;}
+       
+       Set * getDomain(uint i) {return domains.get(i);}
+       uint numDomains() {return domains.getSize();}
+ 
+       SetIteratorTableEntry * getEntries() {return entries->iterator();}
+       uint getSize() {return entries->getSize();}
+
+       CMEMALLOC;
+       
+ private:
        Array<Set *> domains;
        Set *range;
        HashsetTableEntry *entries;
-       CMEMALLOC;
 };
 
 #endif

diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 0ec498afea604ad82c97f3cf5b3563bcaac2f112..c8d53d168936ed2a9c883b7caaf4a92faa98163e 100644 (file)
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -18,13 +18,13 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
        FunctionEncodingType encType = constraint->encoding.type;
        Array<Element *> *inputs = &constraint->inputs;
        uint inputNum = inputs->getSize();
-       uint size = table->entries->getSize();
+       uint size = table->getSize();
        bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
        Edge constraints[size];
        Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
        printCNF(undefConst);
        model_print("**\n");
-       SetIteratorTableEntry *iterator = table->entries->iterator();
+       SetIteratorTableEntry *iterator = table->getEntries();
        uint i = 0;
        while (iterator->hasNext()) {
                TableEntry *entry = iterator->next();
@@ -88,7 +88,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                break;
        }
        bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
-       uint numDomains = predicate->table->domains.getSize();
+       uint numDomains = predicate->table->numDomains();
 
        VectorEdge *clauses = allocDefVectorEdge();
 
@@ -97,7 +97,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = predicate->table->domains.get(i);
+               Set *set = predicate->table->getDomain(i);
                vals[i] = set->getElement(indices[i]);
        }
        bool hasOverflow = false;
@@ -150,7 +150,7 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = predicate->table->domains.get(i);
+                       Set *set = predicate->table->getDomain(i);
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);
@@ -181,9 +181,9 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func)
        ASSERT(undefStatus == SATC_IGNOREBEHAVIOR || undefStatus == SATC_FLAGFORCEUNDEFINED);
        Array<Element *> *elements = &func->inputs;
        Table *table = ((FunctionTable *) (func->function))->table;
-       uint size = table->entries->getSize();
+       uint size = table->getSize();
        Edge constraints[size];
-       SetIteratorTableEntry *iterator = table->entries->iterator();
+       SetIteratorTableEntry *iterator = table->getEntries();
        uint i = 0;
        while (iterator->hasNext()) {
                TableEntry *entry = iterator->next();
@@ -237,7 +237,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                break;
        }
 
-       uint numDomains = function->table->domains.getSize();
+       uint numDomains = function->table->numDomains();
 
        VectorEdge *clauses = allocDefVectorEdge();     // Setup array of clauses
 
@@ -246,7 +246,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 
        uint64_t vals[numDomains];//setup value array
        for (uint i = 0; i < numDomains; i++) {
-               Set *set = function->table->domains.get(i);
+               Set *set = function->table->getDomain(i);
                vals[i] = set->getElement(indices[i]);
        }
 
@@ -300,7 +300,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
                notfinished = false;
                for (uint i = 0; i < numDomains; i++) {
                        uint index = ++indices[i];
-                       Set *set = function->table->domains.get(i);
+                       Set *set = function->table->getDomain(i);
 
                        if (index < set->getSize()) {
                                vals[i] = set->getElement(index);