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.
11 * Created on February 21, 2019, 12:26 PM
14 #include "mathsatinterpreter.h"
15 #include "solver_interface.h"
17 MathSATInterpreter::MathSATInterpreter(CSolver *solver):
18 SMTInterpreter(solver)
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);
27 MathSATInterpreter::~MathSATInterpreter(){
30 int MathSATInterpreter::getResult(){
31 ifstream input(SMTSOLUTIONFILE, ios::in);
33 while(getline(input, line)){
34 if(line.find("unsat")!= line.npos){
37 if(line.find("(") != line.npos){
38 char cline [line.size()+1];
39 strcpy ( cline, line.c_str() );
42 if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
44 if (strcmp (valuestr, "true)") == 0 ){
46 }else if (strcmp(valuestr, "false)") == 0){
49 ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
52 model_print("Signature%u = %u\n", id, value);
53 sigEnc.setValue(id, value);