bug fixes
authorHamed Gorjiara <hgorjiar@uci.edu>
Sat, 23 Feb 2019 08:22:32 +0000 (00:22 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Sat, 23 Feb 2019 08:22:32 +0000 (00:22 -0800)
src/Interpreter/alloyinterpreter.cc
src/Interpreter/mathsatinterpreter.cc
src/Interpreter/smtinterpreter.cc
src/Interpreter/smtratinterpreter.cc
src/ccsolver.cc
src/ccsolver.h

index c0e4a60..021b087 100644 (file)
@@ -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);
 }
 
index ce95153..5123efe 100644 (file)
@@ -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;
index 82c887b..7780931 100644 (file)
@@ -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){
index ebe5113..9742bda 100644 (file)
@@ -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(){
index 7acd00f..8eb786d 100644 (file)
@@ -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
+}
index 2051cc9..b10fa71 100644 (file)
@@ -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
 }