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 > 4) {
  23                 printf("You only specify the name of the file ...\n");
  24                 printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
  25                 exit(-1);
  26         }
  27         CSolver *solver;
  28         if(argc >= 3){
  29                 solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
  30                 if(argc == 4){
  31                         solver->setSatSolverTimeout(atol(argv[3]));
  32                 }
  33         } else {
  34                 solver = CSolver::deserialize(argv[1]);
  35         }
  36         int value = solver->solve();
  37         if (value == 1) {
  38                 printf("%s is SAT\n", argv[1]);
  39         } else {
  40                 printf("%s is UNSAT\n", argv[1]);
  41         }
  42         delete solver;
  43         return 1;
  44
  45 }