Adding SMT Interpreters

[satune.git] / src / Test / deserializealloytest.cc

diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
index 3cb13feb95f9fc8b3c2147f02d55fe29826081c5..187e384617ebbd1c4a45a2548bc64d92c70d98ce 100644 (file)
--- a/src/Test/deserializealloytest.cc
+++ b/src/Test/deserializealloytest.cc
@@ -1,16 +1,32 @@
 #include "csolver.h"
 
 
 #include "csolver.h"
 
 

+InterpreterType getInterpreterType(char * itype){
+       if(strcmp (itype,"--alloy") == 0){
+               return ALLOY;
+       } else if(strcmp (itype,"--z3") == 0){
+               return Z3;
+       } else if(strcmp (itype,"--smtrat") == 0){
+               return SMTRAT;
+       } else if(strcmp (itype,"--alloy") == 0){
+               return ALLOY;
+       } else {
+               printf("Unknown interpreter type: %s\n", itype);
+               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n");
+               exit(-1);
+       }
+}
+

 int main(int argc, char **argv) {
        printf("%d\n", argc);
        if (argc != 2 && argc != 3) {
                printf("You only specify the name of the file ...\n");
 int main(int argc, char **argv) {
        printf("%d\n", argc);
        if (argc != 2 && argc != 3) {
                printf("You only specify the name of the file ...\n");

-               printf("./run.sh deserializer test.dump [--alloy]\n");
+               printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n");

                exit(-1);
        }
        CSolver *solver; 
        if(argc == 3){
                exit(-1);
        }
        CSolver *solver; 
        if(argc == 3){

-               solver = CSolver::deserialize(argv[1], true);
+               solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));

        } else {
                solver = CSolver::deserialize(argv[1]);
        }
        } else {
                solver = CSolver::deserialize(argv[1]);
        }