Adding SMTRat and MathSAT interpreters

diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc
index d87cbd9fbad083de008e8f82a9ce656c82ffc9cd..a5927f71d037ce31dcf03f57356a5b3fddf543d5 100644 (file)
--- 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<returned %d>: %s\n", status, buffer);
+               exit(-1);
        }
        return result;
 }

diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
new file mode 100644 (file)
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 (file)
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 dc8f1cdb9e199c90fb00a868b80e5339fafea626..82c887b244afa77156e97461382af4c395dc3a06 100644 (file)
--- 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 ac62fd712f4128d3e71b43f6d705239785cb2e75..035e76be8c2efd19b1d609117033305352d55e70 100644 (file)
--- a/src/Interpreter/smtinterpreter.h
+++ b/src/Interpreter/smtinterpreter.h
@@ -7,6 +7,9 @@
 #include <iostream>
 #include <fstream>
 
+#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 (file)
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 (file)
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 187e384617ebbd1c4a45a2548bc64d92c70d98ce..cef60f4c9727de506f9146300de1102ab8a53423 100644 (file)
--- 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 2670e4745a24c0371aaa4db082be7890bec86666..1eba56d4bd46afdfa886a9e7b5efbfaa361360a2 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -31,6 +31,8 @@
 #include <stdarg.h>
 #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);
                }