FunctionType type;
virtual ~Function() {}
virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
+ virtual Set * getRange() = 0;
CMEMALLOC;
};
uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
bool isInRangeFunction(uint64_t val);
Function *clone(CSolver *solver, CloneMap *map);
+ Set * getRange() {return range;}
CMEMALLOC;
};
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
Function *clone(CSolver *solver, CloneMap *map);
+ Set * getRange();
CMEMALLOC;
};
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
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();
break;
}
bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
- uint numDomains = predicate->table->domains.getSize();
+ uint numDomains = predicate->table->numDomains();
VectorEdge *clauses = allocDefVectorEdge();
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;
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);
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();
break;
}
- uint numDomains = function->table->domains.getSize();
+ uint numDomains = function->table->numDomains();
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
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]);
}
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);