projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
18aa569
)
Edits
author
bdemsky
<bdemsky@uci.edu>
Fri, 8 Sep 2017 02:38:42 +0000
(19:38 -0700)
committer
bdemsky
<bdemsky@uci.edu>
Fri, 8 Sep 2017 02:38:42 +0000
(19:38 -0700)
src/AST/element.cc
patch
|
blob
|
history
src/AST/function.cc
patch
|
blob
|
history
src/AST/function.h
patch
|
blob
|
history
src/AST/table.h
patch
|
blob
|
history
src/Backend/satfunctableencoder.cc
patch
|
blob
|
history
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;
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);
}
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;
}
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;}
FunctionType type;
virtual ~Function() {}
virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
+ virtual Set * getRange() = 0;
CMEMALLOC;
};
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);
uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
bool isInRangeFunction(uint64_t val);
Function *clone(CSolver *solver, CloneMap *map);
+ Set * getRange() {return range;}
CMEMALLOC;
};
CMEMALLOC;
};
@@
-34,6
+36,7
@@
public:
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
Function *clone(CSolver *solver, CloneMap *map);
UndefinedBehavior undefBehavior;
FunctionTable (Table *table, UndefinedBehavior behavior);
Function *clone(CSolver *solver, CloneMap *map);
+ Set * getRange();
CMEMALLOC;
};
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();
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;
Array<Set *> domains;
Set *range;
HashsetTableEntry *entries;
- CMEMALLOC;
};
#endif
};
#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();
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");
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();
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;
break;
}
bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
- uint numDomains = predicate->table->
domains.getSize
();
+ uint numDomains = predicate->table->
numDomains
();
VectorEdge *clauses = allocDefVectorEdge();
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++) {
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;
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];
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);
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;
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];
Edge constraints[size];
- SetIteratorTableEntry *iterator = table->
entries->iterator
();
+ SetIteratorTableEntry *iterator = table->
getEntries
();
uint i = 0;
while (iterator->hasNext()) {
TableEntry *entry = iterator->next();
uint i = 0;
while (iterator->hasNext()) {
TableEntry *entry = iterator->next();
@@
-237,7
+237,7
@@
void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
break;
}
break;
}
- uint numDomains = function->table->
domains.getSize
();
+ uint numDomains = function->table->
numDomains
();
VectorEdge *clauses = allocDefVectorEdge(); // Setup array of clauses
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++) {
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]);
}
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];
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);
if (index < set->getSize()) {
vals[i] = set->getElement(index);