From: bdemsky <bdemsky@uci.edu>
Date: Fri, 8 Sep 2017 02:38:42 +0000 (-0700)
Subject: Edits
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=65092ed0458d0752b5b8b3defb90d012dca634b1

Edits
---

diff --git a/src/AST/element.cc b/src/AST/element.cc
index fd30812..589e3f5 100644
--- 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 d6b2d3a..a882580 100644
--- 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 fcb5068..f34c02e 100644
--- 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 39b561c..6c7926e 100644
--- 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 0ec498a..c8d53d1 100644
--- 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);