src/Interpreter/mathsatinterpreter.cc

   1 /*
   2  * To change this license header, choose License Headers in Project Properties.
   3  * To change this template file, choose Tools | Templates
   4  * and open the template in the editor.
   5  */
   6
   7 /*
   8  * File:   smtsolvers.cc
   9  * Author: hamed
  10  *
  11  * Created on February 21, 2019, 12:26 PM
  12  */
  13
  14 #include "mathsatinterpreter.h"
  15 #include "solver_interface.h"
  16
  17 MathSATInterpreter::MathSATInterpreter(CSolver *solver) :
  18         SMTInterpreter(solver)
  19 {
  20 }
  21
  22 void MathSATInterpreter::compileRunCommand(char *command, size_t size) {
  23         model_print("Calling MathSAT...\n");
  24         snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
  25 }
  26
  27 MathSATInterpreter::~MathSATInterpreter() {
  28 }
  29
  30 int MathSATInterpreter::getResult() {
  31         ifstream input(SMTSOLUTIONFILE, ios::in);
  32         string line;
  33         while (getline(input, line)) {
  34                 if (line.find("unsat") != line.npos) {
  35                         return IS_UNSAT;
  36                 }
  37                 if (line.find("(") != line.npos) {
  38                         char cline [line.size() + 1];
  39                         strcpy ( cline, line.c_str() );
  40                         char valuestr [512];
  41                         uint id;
  42                         if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)) {
  43                                 uint value;
  44                                 if (strcmp (valuestr, "true)") == 0 ) {
  45                                         value = 1;
  46                                 } else if (strcmp(valuestr, "false)") == 0) {
  47                                         value = 0;
  48                                 } else {
  49                                         ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
  50                                 }
  51
  52                                 model_print("Signature%u = %u\n", id, value);
  53                                 sigEnc.setValue(id, value);
  54                         } else {
  55                                 ASSERT(0);
  56                         }
  57                 }
  58         }
  59         return IS_SAT;
  60 }