bug fixes

diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
index c0e4a6094d97b8784fb8680eba9656f3e454d088..021b0878ed339fd6ee1b509095c24b101d57462b 100644 (file)
--- a/src/Interpreter/alloyinterpreter.cc
+++ b/src/Interpreter/alloyinterpreter.cc
@@ -101,6 +101,7 @@ void AlloyInterpreter::dumpHeader(){
 }
 
 void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+       model_print("Calling Alloy...\n");
        snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
 }
 

diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
index ce951533e36af5d9b703c8e65d47f4c923430829..5123efef72ba932e8a0bad8d836cfe540603a6b8 100644 (file)
--- a/src/Interpreter/mathsatinterpreter.cc
+++ b/src/Interpreter/mathsatinterpreter.cc
@@ -20,7 +20,8 @@ MathSATInterpreter::MathSATInterpreter(CSolver *solver):
 }
 
 void MathSATInterpreter::compileRunCommand(char * command , size_t size){
-       snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+       model_print("Calling MathSAT...\n");
+       snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
 MathSATInterpreter::~MathSATInterpreter(){
@@ -38,7 +39,7 @@ int MathSATInterpreter::getResult(){
                        strcpy ( cline, line.c_str() );
                        char valuestr [512];
                        uint id;
-                       if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){
+                       if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
                                uint value;
                                if (strcmp (valuestr, "true)") == 0 ){
                                        value =1;

diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc
index 82c887b244afa77156e97461382af4c395dc3a06..778093155da4386b04520a0382ddb054788d3f0f 100644 (file)
--- a/src/Interpreter/smtinterpreter.cc
+++ b/src/Interpreter/smtinterpreter.cc
@@ -101,7 +101,8 @@ void SMTInterpreter::dumpHeader(){
 }
 
 void SMTInterpreter::compileRunCommand(char * command, size_t size){
-       snprintf(command, size, "./z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+       model_print("Calling Z3...\n");
+       snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
 string SMTInterpreter::negateConstraint(string constr){

diff --git a/src/Interpreter/smtratinterpreter.cc b/src/Interpreter/smtratinterpreter.cc
index ebe51135e3039f0d8e0fd14a89c03f5177172892..9742bda9669dfc26a4075c2386ab76def426b5e5 100644 (file)
--- a/src/Interpreter/smtratinterpreter.cc
+++ b/src/Interpreter/smtratinterpreter.cc
@@ -19,7 +19,8 @@ SMTRatInterpreter::SMTRatInterpreter(CSolver *solver):
 }
 
 void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
-       snprintf(command, size, "timeout %u ./smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
+       model_print("Calling SMTRat...\n");
+       snprintf(command, size, "./run.sh timeout %u smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
 SMTRatInterpreter::~SMTRatInterpreter(){

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index 7acd00f4f4eb00ac48c9163e36527d6ea03b078b..8eb786dfb74013119be684c174e32f91a0d9931e 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -135,7 +135,6 @@ void printConstraints(void *solver) {
 }
 
 
-
 void serialize(void *solver) {
        CCSOLVER(solver)->serialize();
 }
@@ -151,4 +150,4 @@ void setInterpreter(void *solver, unsigned int type){
 
 void *clone(void *solver) {
        return CCSOLVER(solver)->clone();
-}
\ No newline at end of file
+}

diff --git a/src/ccsolver.h b/src/ccsolver.h
index 2051cc91b9126e2e8b8ccfbdd61c6cb9eca46df0..b10fa71681fc2bad67fd63fe6c6fce9e146b1398 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -41,7 +41,7 @@ int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
-void setAlloyEncoder(void *solver);
+void setInterpreter(void *solver, unsigned int type);
 void *clone(void *solver);
 #ifdef __cplusplus
 }