src/Test/deserializealloytest.cc

   1 #include "csolver.h"
   2
   3
   4 InterpreterType getInterpreterType(char * itype){
   5         if(strcmp (itype,"--alloy") == 0){
   6                 return ALLOY;
   7         } else if(strcmp (itype,"--z3") == 0){
   8                 return Z3;
   9         } else if(strcmp (itype,"--smtrat") == 0){
  10                 return SMTRAT;
  11         } else if(strcmp (itype,"--mathsat") == 0){
  12                 return MATHSAT;
  13         } else {
  14                 printf("Unknown interpreter type: %s\n", itype);
  15                 printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
  16                 exit(-1);
  17         }
  18 }
  19
  20 int main(int argc, char **argv) {
  21         printf("%d\n", argc);
  22         if (argc != 2 && argc != 3) {
  23                 printf("You only specify the name of the file ...\n");
  24                 printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
  25                 exit(-1);
  26         }
  27         CSolver *solver;
  28         if(argc == 3){
  29                 solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
  30         } else {
  31                 solver = CSolver::deserialize(argv[1]);
  32         }
  33         int value = solver->solve();
  34         if (value == 1) {
  35                 printf("%s is SAT\n", argv[1]);
  36         } else {
  37                 printf("%s is UNSAT\n", argv[1]);
  38         }
  39         delete solver;
  40         return 1;
  41
  42 }