projects
/
satcheck.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Fix yield bug
[satcheck.git]
/
constgen.h
diff --git
a/constgen.h
b/constgen.h
index 8669a7f98bcc3aaa13e40c7c792d7c2c965e04d3..20420bc1bc601242f67b525503bf3457e963f61a 100644
(file)
--- a/
constgen.h
+++ b/
constgen.h
@@
-115,7
+115,8
@@
private:
void processLoad(EPRecord *record);
void processAddresses(EPRecord *record);
void recordExecCond(EPRecord *record);
void processLoad(EPRecord *record);
void processAddresses(EPRecord *record);
void recordExecCond(EPRecord *record);
-
+ void computeYieldCond(EPRecord *record);
+
/** TSO Specific methods */
#ifdef TSO
void genTSOTransOrderConstraints();
/** TSO Specific methods */
#ifdef TSO
void genTSOTransOrderConstraints();
@@
-148,6
+149,7
@@
private:
RecPairTable *rpt;
uint numconstraints;
ModelVector<Constraint *> * goalset;
RecPairTable *rpt;
uint numconstraints;
ModelVector<Constraint *> * goalset;
+ ModelVector<EPRecord *> *yieldlist;
Constraint ** goalvararray;
ModelVector<Constraint *> * vars;
BranchTable * branchtable;
Constraint ** goalvararray;
ModelVector<Constraint *> * vars;
BranchTable * branchtable;
@@
-155,9
+157,11
@@
private:
EqualsTable *equalstable;
ScheduleBuilder *schedulebuilder;
RecordSet *nonlocaltrans;
EqualsTable *equalstable;
ScheduleBuilder *schedulebuilder;
RecordSet *nonlocaltrans;
+ RecordSet *incompleteexploredbranch;
LoadHashTable *execcondtable;
IncrementalSolver *solver;
RecToIntTable *rectoint;
LoadHashTable *execcondtable;
IncrementalSolver *solver;
RecToIntTable *rectoint;
+ RecToConsTable *yieldtable;
#ifdef STATS
ModelVector<struct MC_Stat *> * stats;
#endif
#ifdef STATS
ModelVector<struct MC_Stat *> * stats;
#endif