projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
6f5e234
)
Freezing bug fix - Incremental SATTune works for Sypet
author
Hamed Gorjiara
<hgorjiar@uci.edu>
Mon, 1 Jul 2019 19:36:24 +0000
(12:36 -0700)
committer
Hamed Gorjiara
<hgorjiar@uci.edu>
Mon, 1 Jul 2019 19:36:24 +0000
(12:36 -0700)
src/Backend/satelemencoder.cc
patch
|
blob
|
history
diff --git
a/src/Backend/satelemencoder.cc
b/src/Backend/satelemencoder.cc
index aa739242d002acb28330e6112a6f702ec7548b41..d924e6a9062e0b900f0e65bdbc5988bb6c2f4b83 100644
(file)
--- a/
src/Backend/satelemencoder.cc
+++ b/
src/Backend/satelemencoder.cc
@@
-227,6
+227,15
@@
void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
ASSERT(edgeIsVarConst(e));
freezeVariable(cnf, e);
}
ASSERT(edgeIsVarConst(e));
freezeVariable(cnf, e);
}
+ for(uint i=0; i< encoding->encArraySize; i++){
+ if(encoding->isinUseElement(i) && encoding->encoding != EENC_NONE && encoding->numVars > 1){
+ Edge e = encoding->edgeArray[i];
+ if(!edgeIsNull(e)){
+ ASSERT(edgeIsVarConst(e));
+ freezeVariable(cnf, e);
+ }
+ }
+ }
}
void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
}
void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
@@
-294,6
+303,9
@@
void SATEncoder::generateElementEncoding(Element *element) {
}
int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
}
int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+ if(encoding->encArraySize == 1){
+ return 1;
+ }
for (int i = encoding->encArraySize - 1; i >= 0; i--) {
if (encoding->isinUseElement(i))
return i + 1;
for (int i = encoding->encArraySize - 1; i >= 0; i--) {
if (encoding->isinUseElement(i))
return i + 1;