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         snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
  24 }
  25
  26 MathSATInterpreter::~MathSATInterpreter(){
  27 }
  28
  29 int MathSATInterpreter::getResult(){
  30         ifstream input(SMTSOLUTIONFILE, ios::in);
  31         string line;
  32         while(getline(input, line)){
  33                 if(line.find("unsat")!= line.npos){
  34                         return IS_UNSAT;
  35                 }
  36                 if(line.find("(") != line.npos){
  37                         char cline [line.size()+1];
  38                         strcpy ( cline, line.c_str() );
  39                         char valuestr [512];
  40                         uint id;
  41                         if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){
  42                                 uint value;
  43                                 if (strcmp (valuestr, "true)") == 0 ){
  44                                         value =1;
  45                                 }else if (strcmp(valuestr, "false)") == 0){
  46                                         value = 0;
  47                                 }else {
  48                                         ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
  49                                 }
  50
  51                                 model_print("Signature%u = %u\n", id, value);
  52                                 sigEnc.setValue(id, value);
  53                         } else {
  54                                 ASSERT(0);
  55                         }
  56                 }
  57         }
  58         return IS_SAT;
  59 }