X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=constgen.cc;h=2f3375b23070d0cd9ccde22677440b042b0ca6ac;hb=fc4a3bc4e90fad4f37ac0e44e33bb90d7a5749c3;hp=cf584646b340ce7d160aba52c1e49e1e8fb797ab;hpb=e3e2836db3e10d5d1b7a262c7b34f247af076b7a;p=satcheck.git

diff --git a/constgen.cc b/constgen.cc
index cf58464..2f3375b 100644
--- a/constgen.cc
+++ b/constgen.cc
@@ -192,7 +192,7 @@ bool ConstGen::canReuseEncoding() {
 		Constraint *var=goalvararray[i];
 		if (var != NULL) {
 			if (solution[var->getVar()]) {
-				//				if (goalvararray[i] != NULL)
+				//if (goalvararray[i] != NULL)
 				//model_print("SAT clearing goal %d.\n", i);
 
 				goalvararray[i]=NULL;
@@ -201,7 +201,7 @@ bool ConstGen::canReuseEncoding() {
 	}
 
 	schedulebuilder->buildSchedule(solution);
-	model_free(solution);	
+	model_free(solution);
 
 	return true;
 }
@@ -308,7 +308,7 @@ void ConstGen::printEventGraph() {
 	sprintf(buffer, "eventgraph%u.dot",schedule_graph);
 	schedule_graph++;
 	int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
-	dprintf(file, "digraph eventgraph {\n");
+	model_dprintf(file, "digraph eventgraph {\n");
 	
 	EPRecord *first=execution->getEPRecord(MCID_FIRST);
 	printRecord(first, file);
@@ -318,19 +318,19 @@ void ConstGen::printEventGraph() {
 		printRecord(record, file);
 	}
 
-	dprintf(file, "}\n");
+	model_dprintf(file, "}\n");
 	close(file);
 }
 
 void ConstGen::doPrint(EPRecord *record, int file) {
-	dprintf(file, "%lu[label=\"",(uintptr_t)record);
+	model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
 	record->print(file);
-	dprintf(file, "\"];\n");
+	model_dprintf(file, "\"];\n");
 	if (record->getNextRecord()!=NULL)
-		dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
+		model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
 	
 	if (record->getChildRecord()!=NULL)
-		dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
+		model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
 }
 
 void ConstGen::printRecord(EPRecord *record, int file) {
@@ -362,7 +362,7 @@ void ConstGen::printRecord(EPRecord *record, int file) {
 				//runs code
 				if (branchdir->getFirstRecord()!=NULL) {
 					workstack->push_back(branchdir->getFirstRecord());
-					dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
+					model_dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
 				}
 			}
 			return;
@@ -746,6 +746,15 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
 				Constraint *c13=getOrderConstraint(t1rec, t3rec);
 #ifdef TSO
 				Constraint *c32=getOrderConstraint(t3rec, t2rec);
+				if (!c32->isFalse()) {
+					//Have a store->load that could be reordered, need to generate other constraint
+					Constraint *c12=getOrderConstraint(t1rec, t2rec);
+					Constraint *c23=getOrderConstraint(t2rec, t3rec);
+					Constraint *c31=getOrderConstraint(t3rec, t1rec);
+					Constraint *slarray[] = {c31, c23, c12};
+					Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
+					ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
+				}
 				Constraint * array[]={c21, c32, c13};
 				Constraint *intratransorder=new Constraint(OR, 3, array);
 #else
@@ -759,6 +768,16 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
 				Constraint *c02=getOrderConstraint(t0rec, t2rec);
 #ifdef TSO
 				Constraint *c10=getOrderConstraint(t1rec, t0rec);
+
+				if (!c10->isFalse()) {
+					//Have a store->load that could be reordered, need to generate other constraint
+					Constraint *c01=getOrderConstraint(t0rec, t1rec);
+					Constraint *c12=getOrderConstraint(t1rec, t2rec);
+					Constraint *c20=getOrderConstraint(t2rec, t0rec);
+					Constraint *slarray[] = {c01, c12, c20};
+					Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
+					ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
+				}
 				Constraint * array[]={c10, c21, c02};
 				Constraint *intratransorder=new Constraint(OR, 3, array);
 #else
@@ -859,7 +878,7 @@ bool * ConstGen::runSolver() {
 	} else {
 		delete solver;
 		solver=NULL;
-		dprintf(2, "INDETER\n");
+		model_print_err("INDETER\n");
 		model_print("INDETER\n");
 		exit(-1);
 		return NULL;