Fix yield bug

[satcheck.git] / constgen.h

diff --git a/constgen.h b/constgen.h
index 68c02e70a3ca27bcab4da169da5dd05fd7133568..20420bc1bc601242f67b525503bf3457e963f61a 100644 (file)
--- a/constgen.h
+++ b/constgen.h
@@ -46,7 +46,7 @@ struct MC_Stat {
 #endif
 
 class ConstGen {
- public:
+public:
        ConstGen(MCExecution *e);
        ~ConstGen();
        bool process();
@@ -71,13 +71,13 @@ class ConstGen {
 #ifdef STATS
        MC_Stat *curr_stat;
 #endif
-       
+
        MEMALLOC;
- private:
+private:
        Constraint * getRetValueEncoding(EPRecord *record, uint64_t value);
        Constraint * getMemValueEncoding(EPRecord *record, uint64_t value);
        bool subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record);
-       
+
        void addBranchGoal(EPRecord *, Constraint *c);
        void addGoal(EPRecord *, Constraint *c);
        void translateGoals();
@@ -115,7 +115,8 @@ class ConstGen {
        void processLoad(EPRecord *record);
        void processAddresses(EPRecord *record);
        void recordExecCond(EPRecord *record);
-
+       void computeYieldCond(EPRecord *record);
+       
        /** TSO Specific methods */
 #ifdef TSO
        void genTSOTransOrderConstraints();
@@ -124,7 +125,7 @@ class ConstGen {
 #endif
 
        /** These functions build closed groups of memory operations that
-                       can store/load from each other. */
+                       can store/load from each other. */
        void groupMemoryOperations(EPRecord *op);
        void mergeSets(StoreLoadSet *to, StoreLoadSet *from);
 
@@ -136,10 +137,10 @@ class ConstGen {
        void genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec);
 
        /** The hashtable maps an address to the closure set of
-                       memory operations that may touch that address. */
+                       memory operations that may touch that address. */
        StoreLoadSetHashTable *storeloadtable;
        /** This hashtable maps a load to all of the stores it may read
-                       from. */
+                       from. */
        LoadHashTable *loadtable;
 
        MCExecution *execution;
@@ -148,6 +149,7 @@ class ConstGen {
        RecPairTable *rpt;
        uint numconstraints;
        ModelVector<Constraint *> * goalset;
+       ModelVector<EPRecord *> *yieldlist;
        Constraint ** goalvararray;
        ModelVector<Constraint *> * vars;
        BranchTable * branchtable;
@@ -155,9 +157,11 @@ class ConstGen {
        EqualsTable *equalstable;
        ScheduleBuilder *schedulebuilder;
        RecordSet *nonlocaltrans;
+       RecordSet *incompleteexploredbranch;
        LoadHashTable *execcondtable;
        IncrementalSolver *solver;
        RecToIntTable *rectoint;
+       RecToConsTable *yieldtable;
 #ifdef STATS
        ModelVector<struct MC_Stat *> * stats;
 #endif
@@ -167,11 +171,11 @@ class ConstGen {
 };
 
 class RecPair {
- public:
- RecPair(EPRecord *r1, EPRecord *r2) :
-       epr1(r1),
-       epr2(r2),
-       constraint(NULL) {
+public:
+       RecPair(EPRecord *r1, EPRecord *r2) :
+               epr1(r1),
+               epr2(r2),
+               constraint(NULL) {
        }
        EPRecord *epr1;
        EPRecord *epr2;