projects
/
satcheck.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
40913ce
)
Halt execution at yield with -Y to simplify SAT formula
author
bdemsky
<bdemsky@uci.edu>
Wed, 21 Dec 2016 23:10:42 +0000
(15:10 -0800)
committer
bdemsky
<bdemsky@uci.edu>
Wed, 21 Dec 2016 23:10:42 +0000
(15:10 -0800)
constgen.cc
patch
|
blob
|
history
mcexecution.cc
patch
|
blob
|
history
diff --git
a/constgen.cc
b/constgen.cc
index e7f8c2d68004928529c2441d2024b0fe7208d85d..368cb6823d8cce01715fd4723478953b8fbddd3a 100644
(file)
--- a/
constgen.cc
+++ b/
constgen.cc
@@
-347,7
+347,8
@@
void ConstGen::printRecord(EPRecord *record, int file) {
doPrint(record,file);
if (record->getType()==LOOPENTER) {
doPrint(record,file);
if (record->getType()==LOOPENTER) {
- workstack->push_back(record->getNextRecord());
+ if (record->getNextRecord()!=NULL)
+ workstack->push_back(record->getNextRecord());
workstack->push_back(record->getChildRecord());
return;
}
workstack->push_back(record->getChildRecord());
return;
}
@@
-1975,7
+1976,8
@@
void ConstGen::traverseRecord(EPRecord *record, bool initial) {
processRecord(record);
}
if (record->getType()==LOOPENTER) {
processRecord(record);
}
if (record->getType()==LOOPENTER) {
- workstack->push_back(record->getNextRecord());
+ if (record->getNextRecord()!=NULL)
+ workstack->push_back(record->getNextRecord());
workstack->push_back(record->getChildRecord());
return;
}
workstack->push_back(record->getChildRecord());
return;
}
diff --git
a/mcexecution.cc
b/mcexecution.cc
index 59ea44aeb34d6b091b004c8e9f55385c67862bbf..65df7ce8218a6f74d2d416f2316ae7742204809c 100644
(file)
--- a/
mcexecution.cc
+++ b/
mcexecution.cc
@@
-842,6
+842,9
@@
void MCExecution::threadFinish() {
void MCExecution::threadYield() {
getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
void MCExecution::threadYield() {
getOrCreateCurrRecord(YIELD, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
+ if (model->params.noexecyields) {
+ threadFinish();
+ }
}
/** @brief Thread yield. */
}
/** @brief Thread yield. */