5123efef72ba932e8a0bad8d836cfe540603a6b8
[satune.git] / 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 }