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);