From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Sat, 23 Feb 2019 08:22:32 +0000 (-0800)
Subject: bug fixes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=88522b82efee075d4dbaf75e82231a399bcbb41c

bug fixes
---

diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
index c0e4a60..021b087 100644
--- 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 ce95153..5123efe 100644
--- 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 82c887b..7780931 100644
--- 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 ebe5113..9742bda 100644
--- 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 7acd00f..8eb786d 100644
--- 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 2051cc9..b10fa71 100644
--- 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
 }