X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=schedulebuilder.cc;h=68a4b77f115e5b6ff87571eeee1f5121eea786b6;hb=HEAD;hp=9e7d3debe71c6bc181ad5bc0da64b573e1fabf03;hpb=086658309f67c28dc254b06bda5bafa8c3e191d6;p=satcheck.git

diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index 9e7d3de..68a4b77 100644
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -13,6 +13,7 @@
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"
+#include "model.h"
 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
 	cg(cgen),
@@ -31,20 +32,20 @@ void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
 	case LOAD: {
 		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
 		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
-		model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+		model_print("rd=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
 	break;
 	case STORE: {
 		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
 		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
-		model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+		model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
 	break;
 	case RMW: {
 		StoreLoadSet * sls=cgen->getStoreLoadSet(r);
 		model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
-		model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
-		model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+		model_print("rd=%llu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
+		model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
 	}
 	break;
 	default:
@@ -69,7 +70,6 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 			EPRecord *next=processRecord(record, satsolution);
 #ifdef TSO
 			if (next != NULL) {
-
 				if (next->getType()==STORE) {
 					stores[index]->push_back(next);
 					next=getNextRecord(next);
@@ -84,6 +84,9 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 			}
 #endif
 			if (next!=record) {
+#ifdef DUMP_SAT_SCHEDULE
+				neatPrint(record, cg, satsolution);
+#endif
 				threads[index]=next;
 				index=index-1;
 			}
@@ -111,6 +114,10 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 		if (earliest == NULL)
 			break;
 
+#ifdef DUMP_SAT_SCHEDULE
+		neatPrint(earliest, cg, satsolution);
+#endif
+
 		for(uint index=0;index<threads.size();index++) {
 			EPRecord *record=threads[index];
 			if (record==earliest) {
@@ -215,6 +222,8 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
 	case LABEL:
 		break;
 	case YIELD:
+		if (model->params.noexecyields)
+			return NULL;
 		break;
 	default:
 		ASSERT(0);