implemented communication with solver

Former-commit-id: 8e34e17722

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -10,6 +10,7 @@
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 
+#include "src/solver/SmtSolver.h"
 #include "src/solver/Smt2SmtSolver.h"
 
 #include "src/utility/graph.h"
@@ -1072,7 +1073,6 @@ namespace storm {
             // Then, compute the subset of states that has a probability of 0 or 1, respectively.
             std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, storm::storage::BitVector(model.getNumberOfStates(),true), targetStates);
             storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
-            std::cout << "states with prob 0" << statesWithProbability0 << std::endl;
             storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
             storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
             
@@ -1142,9 +1142,6 @@ namespace storm {
             //now lets add the actual transitions
             for (storm::storage::sparse::state_type state = 0; state < flexibleMatrix.getNumberOfRows(); ++state){
                 storm::RationalFunction reachProbability(oneStepProbabilities[state]);
-                if(!reachProbability.isZero()){
-                    std::cout << "non zero " << state << ":  " << reachProbability << std::endl;
-                }
                 for(auto const& transition : flexibleMatrix.getRow(state)){
                     reachProbability += transition.getValue() * stateProbVars[transition.getColumn()];
                 }
@@ -1187,8 +1184,17 @@ namespace storm {
                 solver.add(carl::Constraint<storm::RawPolynomial>(uB,storm::CompareRelation::LEQ));
             }
             
-            flexibleMatrix.print();
-                
+            switch (solver.check()){
+                case storm::solver::SmtSolver::CheckResult::Sat:
+                    std::cout << "sat!" << std::endl;
+                    break;
+                case storm::solver::SmtSolver::CheckResult::Unsat:
+                    std::cout << "unsat!" << std::endl;
+                    break;
+                case storm::solver::SmtSolver::CheckResult::Unknown:
+                    std::cout << "unknown!" << std::endl;
+                    break;
+            }
             
             /*
             //testing stuff...
@@ -1290,7 +1296,7 @@ namespace storm {
                     flexibleMatrix.getRow(*initialStates.begin()).clear();
                 }
             }
-            */
+            
                         std::cout << std::endl << "-----------------------" << std::endl << "testing stuff..." << std::endl;
             std::map<storm::Variable, storm::RationalFunction::CoeffType> testmap;
             

src/settings/modules/Smt2SmtSolverSettings.cpp

@@ -6,14 +6,14 @@ namespace storm {
     namespace settings {
         namespace modules {
             
-            const std::string Smt2SmtSolverSettings::moduleName = "smt2smtsolver";
+            const std::string Smt2SmtSolverSettings::moduleName = "smt2";
             const std::string Smt2SmtSolverSettings::solverCommandOption = "solvercommand";
-            const std::string Smt2SmtSolverSettings::exportSmtLibScriptOption = "exportSmtLibScript";
+            const std::string Smt2SmtSolverSettings::exportScriptOption = "exportscript";
             
             Smt2SmtSolverSettings::Smt2SmtSolverSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, solverCommandOption, true, "If set, this command is used to call the solver and to let the solver know that it should read SMT-LIBv2 commands from standard input. If not set, only a SMT-LIB script file might be exported.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("command", "path to the solver + command line arguments.").setDefaultValueString("").build()).build());
                 
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportSmtLibScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportScriptOption, true, "If set, the SMT-LIBv2 script will be exportet to this file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "path and filename to the location where the script file should be exportet to").setDefaultValueString("").build()).build());
             }
             
             bool Smt2SmtSolverSettings::isSolverCommandSet() const{
@@ -26,12 +26,12 @@ namespace storm {
 
 
             bool Smt2SmtSolverSettings::isExportSmtLibScriptSet() const{
-                return this->getOption(exportSmtLibScriptOption).getHasOptionBeenSet();
+                return this->getOption(exportScriptOption).getHasOptionBeenSet();
             }
 
 
             std::string Smt2SmtSolverSettings::getExportSmtLibScriptPath() const{
-                return this->getOption(solverCommandOption).getArgumentByName("path").getValueAsString();
+                return this->getOption(exportScriptOption).getArgumentByName("path").getValueAsString();
             }
 
 

src/settings/modules/Smt2SmtSolverSettings.h

@@ -55,7 +55,7 @@ namespace storm {
             private:
                 // Define the string names of the options as constants.
                 static const std::string solverCommandOption;
-                static const std::string exportSmtLibScriptOption;
+                static const std::string exportScriptOption;
             };
             
         } // namespace modules

src/solver/Smt2SmtSolver.cpp

@@ -8,6 +8,7 @@
 #include "src/exceptions/IllegalFunctionCallException.h"
 #include "utility/macros.h"
 #include "adapters/CarlAdapter.h"
+#include "exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace solver {
@@ -28,32 +29,42 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
         }
 
-        Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) {
+        Smt2SmtSolver::Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions) : SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown), useCarlExpressions(useCarlExpressions) {
 #ifndef STORM_HAVE_CARL
             STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL");
+#endif
+#ifndef WINDOWS
+            processIdOfSolver=0;
 #endif
             expressionAdapter = std::unique_ptr<storm::adapters::Smt2ExpressionAdapter>(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), true));
             init();
         }
 
         Smt2SmtSolver::~Smt2SmtSolver() {
-            writeCommand("( exit )");
-            //todo make sure that the process exits
+            writeCommand("( exit )", true);
+#ifndef WINDOWS
+            if(processIdOfSolver!=0){
+                //Since the process has been open successfully, it means that we have to close our fds   
+                close(fromSolver);
+                close(toSolver);
+                //todo make sure that the process exits  waitpid kill(pid, ..);
+            }
+#endif
         }
 
         void Smt2SmtSolver::push() {
             expressionAdapter->increaseScope();
-            writeCommand("( push 1 ) ");
+            writeCommand("( push 1 ) ", true);
         }
 
         void Smt2SmtSolver::pop() {
             expressionAdapter->decreaseScope();
-            writeCommand("( pop 1 ) ");
+            writeCommand("( pop 1 ) ", true);
         }
 
         void Smt2SmtSolver::pop(uint_fast64_t n) {
             expressionAdapter->decreaseScope(n);
-            writeCommand("( pop " + std::to_string(n) + " ) ");
+            writeCommand("( pop " + std::to_string(n) + " ) ", true);
         }
 
         void Smt2SmtSolver::reset() {
@@ -74,9 +85,9 @@ namespace storm {
             rightHandSide.gatherVariables(variables);
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
             for (auto declaration : varDeclarations){
-                writeCommand(declaration);
+                writeCommand(declaration, true);
             }
-            writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )");
+            writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
         }
         
         template<>
@@ -90,24 +101,34 @@ namespace storm {
             std::set<storm::Variable> variables = constraint.lhs().gatherVariables();
             std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
             for (auto declaration : varDeclarations){
-                writeCommand(declaration);
+                writeCommand(declaration, true);
             }
-            writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )");
+            writeCommand("( assert " + expressionAdapter->translateExpression(constraint) + " )", true);
         }
         
         
 #endif
 
         SmtSolver::CheckResult Smt2SmtSolver::check() {
-            writeCommand("( check-sat )");
-            if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
-                // todo get the result
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
+            writeCommand("( check-sat )", false);
+#ifdef WINDOWS
+                STORM_LOG_WARN("SMT-LIBv2 Solver can not be started on Windows as this is not yet implemented. Assume that the check-result is \"unknown\"");
+                return SmtSolver::CheckResult::Unknown;
+#else
+                
+            if (processIdOfSolver!=0){
+                auto solverOutput = readSolverOutput();
+                STORM_LOG_THROW(solverOutput.size()==1, storm::exceptions::UnexpectedException, "expected a single line of output after smt2 command ( check-sat ). Got " + std::to_string(solverOutput.size()) + " lines of output instead.");
+                solverOutput[0].erase(std::remove_if(solverOutput[0].begin(), solverOutput[0].end(), isspace), solverOutput[0].end()); //remove spaces
+                if(solverOutput[0]=="sat") return SmtSolver::CheckResult::Sat;
+                if(solverOutput[0]=="unsat") return SmtSolver::CheckResult::Unsat;
+                if(solverOutput[0]=="unknown") return SmtSolver::CheckResult::Unknown;
             }
             else{
                 STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\"");
                 return SmtSolver::CheckResult::Unknown;
             }
+#endif
         }
 
         SmtSolver::CheckResult Smt2SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
@@ -123,8 +144,53 @@ namespace storm {
 
         void Smt2SmtSolver::init() {
             if (storm::settings::smt2SmtSolverSettings().isSolverCommandSet()){
-                //todo call the solver!
-                std::string cmd = storm::settings::smt2SmtSolverSettings().getSolverCommand();
+#ifdef WINDOWS
+                STORM_LOG_WARN("opening a thread for the smt solver is not implemented on Windows. Hence, no actual solving will be done")
+#else
+                //for executing the solver we will need the path to the executable file as well as the arguments as a char* array
+                //where the first argument is the path to the executable file and the last is NULL
+                const std::string cmdString = storm::settings::smt2SmtSolverSettings().getSolverCommand();
+                std::vector<std::string> solverCommandVec;
+                boost::split(solverCommandVec, cmdString, boost::is_any_of("\t "));
+                char** solverArgs = new char* [solverCommandVec.size()+1];
+                solverArgs[0] = const_cast<char*>(solverCommandVec[0].substr(0, cmdString.rfind('/')+1).c_str());
+                for(uint_fast64_t argumentIndex = 1; argumentIndex<solverCommandVec.size(); ++argumentIndex){
+                    solverArgs[argumentIndex]=const_cast<char*>(solverCommandVec[argumentIndex].c_str());
+                }
+                solverArgs[solverCommandVec.size()] = NULL;
+                
+                //get the pipes started
+                int pipeIn[2];
+                int pipeOut[2];                
+                const int READ=0;
+                const int WRITE=1;
+                STORM_LOG_THROW(pipe(pipeIn) == 0 && pipe(pipeOut)==0, storm::exceptions::UnexpectedException, "Could not open pipe to new process");
+                
+                //now start the child process, i.e., the solver
+                pid_t pid = fork();
+                STORM_LOG_THROW(pid>=0, storm::exceptions::UnexpectedException, "Could not start new process for the smt solver");
+                if (pid == 0){
+                    // Child process
+                    // duplicate the fd so that standard input and output will be send to our pipes
+                    dup2(pipeIn[READ], STDIN_FILENO); 
+                    dup2(pipeOut[WRITE], STDOUT_FILENO);
+                    // we can now close everything since our child process will use std in and out to address the pipes
+                    close(pipeIn[READ]);
+                    close(pipeIn[WRITE]); 
+                    close(pipeOut[READ]); 
+                    close(pipeOut[WRITE]); 
+                    
+                    execv(solverCommandVec[0].c_str(), solverArgs); //"-smt2 -in"
+                    // if we reach this point, execl was not successful
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not execute the solver correctly");
+                }
+                // Parent Process
+                toSolver=pipeIn[WRITE];
+                fromSolver=pipeOut[READ];   
+                close(pipeOut[WRITE]);
+                close(pipeIn[READ]);
+                processIdOfSolver=pid;
+#endif  
             }
             else{
                 STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
@@ -133,22 +199,95 @@ namespace storm {
             if (storm::settings::smt2SmtSolverSettings().isExportSmtLibScriptSet()){
                 STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
                 commandFile.open(storm::settings::smt2SmtSolverSettings().getExportSmtLibScriptPath(), std::ios::trunc);
-                STORM_LOG_THROW(commandFile.is_open(), storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
+                isCommandFileOpen=commandFile.is_open();
+                STORM_LOG_THROW(isCommandFileOpen, storm::exceptions::InvalidArgumentException, "The file where the smt2commands should be written to could not be opened");
             }
 
             //some initial commands
-            writeCommand("( set-logic QF_NRA )");
-
+            writeCommand("( set-option :print-success true )", true);
+            writeCommand("( set-logic QF_NRA )", true);
+            //writeCommand("( get-info :name )");
         }
 
-        void Smt2SmtSolver::writeCommand(std::string smt2Command) {
-            if (commandFile.is_open()) {
+        void Smt2SmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) {
+            if (isCommandFileOpen) {
                 commandFile << smt2Command << std::endl;
-            } else{
-                std::cout << "COMMAND FILE IS CLOSED" <<std::endl;
             }
             
-            //todo actually write to the solver
+#ifndef WINDOWS
+            if (processIdOfSolver!=0){
+                write(toSolver, (smt2Command+"\n").c_str(), smt2Command.length()+1);
+                if(expectSuccess){
+                    auto output=readSolverOutput();
+                    STORM_LOG_THROW(output.size()==1, storm::exceptions::UnexpectedException, "expected a single success response after smt2 command " + smt2Command + ". Got " + std::to_string(output.size()) + " lines of output instead.");
+                    output[0].erase(std::remove_if(output[0].begin(), output[0].end(), isspace), output[0].end());
+                    STORM_LOG_THROW(output[0]=="success", storm::exceptions::UnexpectedException, "expected <<success>> response after smt2 command " + smt2Command + ". Got <<" + output[0] + ">> instead");
+                }
+            }
+#endif
+        }
+        
+        std::vector<std::string> Smt2SmtSolver::readSolverOutput(bool waitForOutput){
+#ifndef WINDOWS
+            if (processIdOfSolver==0){
+                STORM_LOG_DEBUG("failed to read solver output as the solver is not running");
+                return std::vector<std::string>();
+            }
+            int bytesReadable;
+            if(waitForOutput){
+                bytesReadable=1;//just assume that there are bytes readable
+            }
+            else if(ioctl(fromSolver, FIONREAD, &bytesReadable)< 0){ //actually obtain the readable bytes
+                STORM_LOG_ERROR("Could not check if the solver has output");
+                return std::vector<std::string>();
+            }
+            std::string solverOutput="";
+            const ssize_t MAX_CHUNK_SIZE=256;
+            char chunk[MAX_CHUNK_SIZE];
+            while(bytesReadable>0){
+                ssize_t chunkSize = read(fromSolver, chunk, MAX_CHUNK_SIZE);
+                STORM_LOG_THROW(chunkSize>=0, storm::exceptions::UnexpectedException, "failed to read solver output");
+                solverOutput += std::string(chunk, chunkSize);
+                if(ioctl(fromSolver, FIONREAD, &bytesReadable)< 0){//obtain the new amount of readable bytes
+                    STORM_LOG_ERROR("Could not check if the solver has output");
+                    return std::vector<std::string>();
+                }
+                if(bytesReadable==0 && solverOutput.back()!='\n'){
+                    STORM_LOG_DEBUG("Solver Output did not end with newline symbol (\\n). Since we assume that this should case, we will wait for more output from the solver");
+                    bytesReadable=1; //we expect more output!
+                }
+            }
+            checkForErrorMessage(solverOutput);
+            std::vector<std::string> solverOutputAsVector;
+            if(solverOutput.length()>0){
+                solverOutput=solverOutput.substr(0,solverOutput.length()-1);
+                boost::split(solverOutputAsVector, solverOutput, boost::is_any_of("\n"));
+                //note: this is a little bit unsafe as \n can be contained within a solver response
+            }
+            return solverOutputAsVector;
+#endif
+        }
+        
+        void Smt2SmtSolver::checkForErrorMessage(const std::string message){
+            size_t errorOccurrance = message.find("error");
+            if (errorOccurrance!=std::string::npos){
+                std::string errorMsg = "An error was detected while checking the solver output. ";
+                STORM_LOG_DEBUG("Detected an error message in the solver response:\n" + message);
+                size_t firstQuoteSign = message.find('\"',errorOccurrance);
+                if(firstQuoteSign!=std::string::npos && message.find("\\\"", firstQuoteSign-1)!=firstQuoteSign-1){
+                    size_t secondQuoteSign = message.find('\"', firstQuoteSign+1);
+                    while(secondQuoteSign!=std::string::npos && message.find("\\\"", secondQuoteSign-1)==secondQuoteSign-1){
+                        secondQuoteSign = message.find('\"',secondQuoteSign+1);
+                    }
+                    if(secondQuoteSign!=std::string::npos){
+                        errorMsg += "The error message was:\n" + message.substr(errorOccurrance,secondQuoteSign-errorOccurrance+1) + ".";
+                        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg);
+                        return;
+                    }
+                }
+                errorMsg += "The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance,200);
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg);
+            }
         }
     }
 }

src/solver/Smt2SmtSolver.h

@@ -3,6 +3,10 @@
 
 #include <iostream>
 #include <fstream>
+#ifndef WINDOWS
+    #include <unistd.h>
+    #include <sys/ioctl.h>
+#endif
 
 #include "storm-config.h"
 #include "src/solver/SmtSolver.h"
@@ -11,7 +15,12 @@
 
 namespace storm {
     namespace solver {
-
+        /*!
+         * This class represents an SMT-LIBv2 conforming solver. 
+         * Any SMT-LIBv2 conforming solver can be called and will be opened as a child process.
+         * It is also possible to export the SMT2 script for later use.
+         * @note The parsing of the solver responses is a little bit crude and might cause bugs (e.g., if a variable name has the infix "error")
+         */
         class Smt2SmtSolver : public SmtSolver {
         public:
 
@@ -31,7 +40,7 @@ namespace storm {
         public:
             /*!
              * Creates a new solver with the given manager.
-             * In addition to storm expressions, this solver also allows carl expressions (but not both).
+             * In addition to storm expressions, this solver also allows carl expressions (but not both to not confuse variables).
              * Hence, there is a flag to chose between the two
              */
             Smt2SmtSolver(storm::expressions::ExpressionManager& manager, bool useCarlExpressions = false);
@@ -79,21 +88,51 @@ namespace storm {
 
 
             /*!
-             * Initializes the solver
+             * Initializes the solver, i.e. opens a new process for it and creates a file stream for the script file  (if demanded)
+             * Moreover, some initial commands are send to the solver
              */
             void init();
 
 
-            /*! Writes the given command to the solver
+            /*! 
+             * Writes the given command to the solver
              * @param smt2Command the command that the solver will receive
+             * @param expectSuccess set this flag to true whenever a success response from the solver is expected.
              */
-            void writeCommand(std::string smt2Command);
+            void writeCommand(std::string smt2Command, bool expectSuccess);
             
+            /*! 
+             * Reads from the solver. The output is checked for an error message and an exception is thrown in that case.
+             * @param waitForOutput if this is true and there is currently no output, we will wait until there is output.
+             * @return the output of the solver. Every entry of the vector corresponds to one output line
+             */
+            std::vector<std::string> readSolverOutput(bool waitForOutput=true);
+            
+            /*! 
+             * Checks if the given message contains an error message and throws an exception.
+             * More precisely, an exception is thrown whenever the word "error" is contained in the message.
+             * This function is directly called when reading the solver output via readSolverOutput()
+             * We will try to parse the message in the SMT-LIBv2 format, i.e.,
+             * ( error "this is the error message from the solver" ) to give some debug information
+             * However, the whole message is always written to the debug log (providing there is an error)
+             * @param message the considered message which should be an output of the solver.
+             */
+            void checkForErrorMessage(const std::string message);
+
+#ifndef WINDOWS
+            // descriptors for the pipe from and to the solver
+            int toSolver;
+            int fromSolver;
+            // A flag storing the Process ID of the solver. If this is zero, then the solver is not running 
+            pid_t processIdOfSolver;
+#endif
             
 
             // a filestream where the commands that we send to the solver will be stored (can be used for debugging purposes)
             std::ofstream commandFile;
 
+            bool isCommandFileOpen;
+            
             // An expression adapter that is used for translating the expression into Smt2's format.
             std::unique_ptr<storm::adapters::Smt2ExpressionAdapter> expressionAdapter;