From: Hamed Gorjiara Date: Thu, 21 Feb 2019 23:58:16 +0000 (-0800) Subject: Adding SMTRat and MathSAT interpreters X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=b170f31ca9df1c465adec1c156c5a8b1aa49a3c0 Adding SMTRat and MathSAT interpreters --- diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc index d87cbd9..a5927f7 100644 --- a/src/Interpreter/interpreter.cc +++ b/src/Interpreter/interpreter.cc @@ -56,9 +56,12 @@ int Interpreter::solve(){ } compileRunCommand(buffer, sizeof(buffer)); int status = system(buffer); - if (status == 0) { + if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved //Read data in from results file result = getResult(); + } else { + model_print("Error in running command: %s\n", status, buffer); + exit(-1); } return result; } diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc new file mode 100644 index 0000000..ce95153 --- /dev/null +++ b/src/Interpreter/mathsatinterpreter.cc @@ -0,0 +1,59 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: smtsolvers.cc + * Author: hamed + * + * Created on February 21, 2019, 12:26 PM + */ + +#include "mathsatinterpreter.h" +#include "solver_interface.h" + +MathSATInterpreter::MathSATInterpreter(CSolver *solver): + SMTInterpreter(solver) +{ +} + +void MathSATInterpreter::compileRunCommand(char * command , size_t size){ + snprintf(command, size, "timeout %u ./mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE); +} + +MathSATInterpreter::~MathSATInterpreter(){ +} + +int MathSATInterpreter::getResult(){ + ifstream input(SMTSOLUTIONFILE, ios::in); + string line; + while(getline(input, line)){ + if(line.find("unsat")!= line.npos){ + return IS_UNSAT; + } + if(line.find("(") != line.npos){ + char cline [line.size()+1]; + strcpy ( cline, line.c_str() ); + char valuestr [512]; + uint id; + if (2 == sscanf(cline,"%*[^0123456789]%u%*[^0123456789]%s", &id, valuestr)){ + uint value; + if (strcmp (valuestr, "true)") == 0 ){ + value =1; + }else if (strcmp(valuestr, "false)") == 0){ + value = 0; + }else { + ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value)); + } + + model_print("Signature%u = %u\n", id, value); + sigEnc.setValue(id, value); + } else { + ASSERT(0); + } + } + } + return IS_SAT; +} \ No newline at end of file diff --git a/src/Interpreter/mathsatinterpreter.h b/src/Interpreter/mathsatinterpreter.h new file mode 100644 index 0000000..ef2ec9f --- /dev/null +++ b/src/Interpreter/mathsatinterpreter.h @@ -0,0 +1,31 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: mathsatinterpreter.h + * Author: hamed + * + * Created on February 21, 2019, 12:26 PM + */ + +#ifndef MATHSATINTERPRETER_H +#define MATHSATINTERPRETER_H + +#include "smtinterpreter.h" + + +class MathSATInterpreter: public SMTInterpreter{ +public: + MathSATInterpreter(CSolver *solver); + virtual ~MathSATInterpreter(); +protected: + virtual void compileRunCommand(char * command , size_t size); + virtual int getResult(); +}; + + +#endif /* SMTSOLVERS_H */ + diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc index dc8f1cd..82c887b 100644 --- a/src/Interpreter/smtinterpreter.cc +++ b/src/Interpreter/smtinterpreter.cc @@ -15,9 +15,6 @@ using namespace std; -#define SMTFILENAME "satune.smt" -#define SMTSOLUTIONFILE "solution.sol" - SMTInterpreter::SMTInterpreter(CSolver *_solver): Interpreter(_solver) { @@ -82,7 +79,7 @@ int SMTInterpreter::getResult(){ if(line.find("unsat")!= line.npos){ return IS_UNSAT; } - if(line.find("(define-fun") != line.npos){ + if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){ string valueline; ASSERT(getline(input, valueline)); char cline [line.size()+1]; diff --git a/src/Interpreter/smtinterpreter.h b/src/Interpreter/smtinterpreter.h index ac62fd7..035e76b 100644 --- a/src/Interpreter/smtinterpreter.h +++ b/src/Interpreter/smtinterpreter.h @@ -7,6 +7,9 @@ #include #include +#define SMTFILENAME "satune.smt" +#define SMTSOLUTIONFILE "solution.sol" + class SMTInterpreter: public Interpreter{ public: SMTInterpreter(CSolver *solver); @@ -23,7 +26,7 @@ protected: virtual string negateConstraint(string constr); virtual string encodeBooleanLogic( BooleanLogic *bl); virtual string encodeBooleanVar( BooleanVar *bv); - void extractValue(char *idline, char *valueline); + virtual void extractValue(char *idline, char *valueline); virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature); virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2); }; diff --git a/src/Interpreter/smtratinterpreter.cc b/src/Interpreter/smtratinterpreter.cc new file mode 100644 index 0000000..ebe5113 --- /dev/null +++ b/src/Interpreter/smtratinterpreter.cc @@ -0,0 +1,26 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: smtratinterpreter.cc + * Author: hamed + * + * Created on February 21, 2019, 2:33 PM + */ + +#include "smtratinterpreter.h" + +SMTRatInterpreter::SMTRatInterpreter(CSolver *solver): + SMTInterpreter(solver) +{ +} + +void SMTRatInterpreter::compileRunCommand(char * command , size_t size){ + snprintf(command, size, "timeout %u ./smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE); +} + +SMTRatInterpreter::~SMTRatInterpreter(){ +} diff --git a/src/Interpreter/smtratinterpreter.h b/src/Interpreter/smtratinterpreter.h new file mode 100644 index 0000000..f2afb49 --- /dev/null +++ b/src/Interpreter/smtratinterpreter.h @@ -0,0 +1,27 @@ +/* + * To change this license header, choose License Headers in Project Properties. + * To change this template file, choose Tools | Templates + * and open the template in the editor. + */ + +/* + * File: smtratinterpreter.h + * Author: hamed + * + * Created on February 21, 2019, 2:33 PM + */ + +#ifndef SMTRATINTERPRETER_H +#define SMTRATINTERPRETER_H +#include "smtinterpreter.h" + +class SMTRatInterpreter: public SMTInterpreter{ +public: + SMTRatInterpreter(CSolver *solver); + virtual ~SMTRatInterpreter(); +protected: + void compileRunCommand(char * command , size_t size); +}; + +#endif /* SMTRATINTERPRETER_H */ + diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc index 187e384..cef60f4 100644 --- a/src/Test/deserializealloytest.cc +++ b/src/Test/deserializealloytest.cc @@ -8,11 +8,11 @@ InterpreterType getInterpreterType(char * itype){ return Z3; } else if(strcmp (itype,"--smtrat") == 0){ return SMTRAT; - } else if(strcmp (itype,"--alloy") == 0){ - return ALLOY; + } else if(strcmp (itype,"--mathsat") == 0){ + return MATHSAT; } else { printf("Unknown interpreter type: %s\n", itype); - printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n"); + printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n"); exit(-1); } } @@ -21,7 +21,7 @@ int main(int argc, char **argv) { printf("%d\n", argc); if (argc != 2 && argc != 3) { printf("You only specify the name of the file ...\n"); - printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsmt]\n"); + printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n"); exit(-1); } CSolver *solver; diff --git a/src/csolver.cc b/src/csolver.cc index 2670e47..1eba56d 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -31,6 +31,8 @@ #include #include "alloyinterpreter.h" #include "smtinterpreter.h" +#include "mathsatinterpreter.h" +#include "smtratinterpreter.h" CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -692,8 +694,14 @@ void CSolver::setInterpreter(InterpreterType type){ interpreter = new SMTInterpreter(this); break; } - case MATHSAT: - case SMTRAT: + case MATHSAT:{ + interpreter = new MathSATInterpreter(this); + break; + } + case SMTRAT:{ + interpreter = new SMTRatInterpreter(this); + break; + } default: ASSERT(0); }