Document interface

[satcheck.git] / constgen.cc

diff --git a/constgen.cc b/constgen.cc
index cf584646b340ce7d160aba52c1e49e1e8fb797ab..2f3375b23070d0cd9ccde22677440b042b0ca6ac 100644 (file)
--- 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;