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;
}
schedulebuilder->buildSchedule(solution);
- model_free(solution);
+ model_free(solution);
return true;
}
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);
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) {
//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;
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
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
} else {
delete solver;
solver=NULL;
- dprintf(2, "INDETER\n");
+ model_print_err("INDETER\n");
model_print("INDETER\n");
exit(-1);
return NULL;