Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SmtlibSmtSolver.cpp
Go to the documentation of this file.
1#include <errno.h>
2#include <signal.h>
3#include <sys/ioctl.h>
4#include <sys/types.h>
5#include <sys/wait.h>
6#include <unistd.h>
7
9
17#include "storm/io/file.h"
21
22#include <boost/algorithm/string.hpp>
23
24namespace storm {
25namespace solver {
26
30
32 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
33}
34
36 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
37}
38
40 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
41}
42
44 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
45}
46
48 : SmtSolver(manager), isCommandFileOpen(false), expressionAdapter(nullptr), useCarlExpressions(useCarlExpressions) {
49#ifndef STORM_HAVE_CARL
50 STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalArgumentException, "Tried to use carl expressions but storm is not linked with CARL");
51#endif
52
53 processIdOfSolver = 0;
54 this->expressionAdapter =
55 std::unique_ptr<storm::adapters::Smt2ExpressionAdapter>(new storm::adapters::Smt2ExpressionAdapter(this->getManager(), this->useReadableVarNames));
56 init();
57}
58
60 writeCommand("( exit )",
61 false); // do not wait for success because it does not matter at this point and may cause problems if the solver is not running properly
62
63 if (processIdOfSolver != 0) {
64 // Since the process has been opened successfully, it means that we have to close our fds
65 close(fromSolver);
66 close(toSolver);
67 kill(processIdOfSolver, SIGTERM);
68 waitpid(processIdOfSolver, nullptr, 0); // make sure the process has exited
69 }
70}
71
73 expressionAdapter->increaseScope();
74 writeCommand("( push 1 ) ", true);
75}
76
78 expressionAdapter->decreaseScope();
79 writeCommand("( pop 1 ) ", true);
80}
81
82void SmtlibSmtSolver::pop(uint_fast64_t n) {
83 expressionAdapter->decreaseScope(n);
84 writeCommand("( pop " + std::to_string(n) + " ) ", true);
85}
86
88 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
89}
90
92 STORM_LOG_THROW(!useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
93 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
94}
95
96#ifdef STORM_HAVE_CARL
97void SmtlibSmtSolver::add(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation, storm::RationalFunction const& rightHandSide) {
98 STORM_LOG_THROW(useCarlExpressions, storm::exceptions::IllegalFunctionCallException, "This solver was initialized without allowing carl expressions");
99 // if some of the occurring variables are not declared yet, we will have to.
100 std::set<storm::RationalFunctionVariable> variables;
101 leftHandSide.gatherVariables(variables);
102 rightHandSide.gatherVariables(variables);
103 std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variables);
104 for (auto declaration : varDeclarations) {
105 writeCommand(declaration, true);
106 }
107 writeCommand("( assert " + expressionAdapter->translateExpression(leftHandSide, relation, rightHandSide) + " )", true);
108}
109
110void SmtlibSmtSolver::add(const storm::RationalFunctionVariable& variable, bool value) {
111 STORM_LOG_THROW((variable.type() == carl::VariableType::VT_BOOL), storm::exceptions::IllegalArgumentException,
112 "Tried to add a constraint that consists of a non-boolean variable.");
113 std::set<storm::RationalFunctionVariable> variableSet;
114 variableSet.insert(variable);
115 std::vector<std::string> const varDeclarations = expressionAdapter->checkForUndeclaredVariables(variableSet);
116 for (auto declaration : varDeclarations) {
117 writeCommand(declaration, true);
118 }
119 std::string varName = carl::VariablePool::getInstance().getName(variable, this->useReadableVarNames);
120 if (value) {
121 writeCommand("( assert " + varName + " )", true);
122 } else {
123 writeCommand("( assert (not " + varName + ") )", true);
124 }
125}
126
127#endif
128
130 writeCommand("( check-sat )", false);
131
132 if (processIdOfSolver != 0) {
133 auto solverOutput = readSolverOutput();
135 solverOutput.size() == 1, storm::exceptions::UnexpectedException,
136 "expected a single line of output after smt2 command ( check-sat ). Got " + std::to_string(solverOutput.size()) + " lines of output instead.");
137 solverOutput[0].erase(std::remove_if(solverOutput[0].begin(), solverOutput[0].end(), ::isspace), solverOutput[0].end()); // remove spaces
138 if (solverOutput[0] == "sat")
140 if (solverOutput[0] == "unsat")
142 if (solverOutput[0] == "unknown")
144 // if we reach this point, something unexpected happened. Lets return unknown and print some debug output
145 STORM_LOG_DEBUG("unexpected solver output: " << solverOutput[0] << ". Returning result 'unknown'");
147 } else {
148 STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving is done... Assume that the result is \"unknown\"");
150 }
151}
152
153SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const&) {
154 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
155}
156
157SmtSolver::CheckResult SmtlibSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const&) {
158 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "functionality not (yet) implemented");
159}
160
161void SmtlibSmtSolver::init() {
162 if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isSolverCommandSet()) {
163 signal(SIGPIPE, SIG_IGN);
164 this->needsRestart = false;
165
166 // for executing the solver we will need the path to the executable file as well as the arguments as a char* array
167 // where the first argument is the path to the executable file and the last is NULL
168 const std::string cmdString = storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getSolverCommand();
169 std::vector<std::string> solverCommandVec;
170 boost::split(solverCommandVec, cmdString, boost::is_any_of("\t "));
171 char** solverArgs = new char*[solverCommandVec.size() + 1];
172 solverArgs[0] = const_cast<char*>(solverCommandVec[0].substr(0, cmdString.rfind('/') + 1).c_str());
173 for (uint_fast64_t argumentIndex = 1; argumentIndex < solverCommandVec.size(); ++argumentIndex) {
174 solverArgs[argumentIndex] = const_cast<char*>(solverCommandVec[argumentIndex].c_str());
175 }
176 solverArgs[solverCommandVec.size()] = NULL;
177
178 // get the pipes started
179 int pipeIn[2];
180 int pipeOut[2];
181 const int READ = 0;
182 const int WRITE = 1;
183 STORM_LOG_THROW(pipe(pipeIn) == 0 && pipe(pipeOut) == 0, storm::exceptions::UnexpectedException, "Could not open pipe to new process");
184
185 // now start the child process, i.e., the solver
186 pid_t pid = fork();
187 STORM_LOG_THROW(pid >= 0, storm::exceptions::UnexpectedException, "Could not start new process for the smt solver");
188 if (pid == 0) {
189 // Child process
190 // duplicate the fd so that standard input and output will be send to our pipes
191 dup2(pipeIn[READ], STDIN_FILENO);
192 dup2(pipeOut[WRITE], STDOUT_FILENO);
193 dup2(pipeOut[WRITE], STDERR_FILENO);
194 // we can now close everything since our child process will use std in and out to address the pipes
195 close(pipeIn[READ]);
196 close(pipeIn[WRITE]);
197 close(pipeOut[READ]);
198 close(pipeOut[WRITE]);
199
200 execv(solverCommandVec[0].c_str(), solverArgs); //"-smt2 -in"
201 // if we reach this point, execl was not successful
202 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not execute the solver correctly");
203 }
204 // Parent Process
205 toSolver = pipeIn[WRITE];
206 fromSolver = pipeOut[READ];
207 close(pipeOut[WRITE]);
208 close(pipeIn[READ]);
209 processIdOfSolver = pid;
210
211 } else {
212 STORM_LOG_WARN("No SMT-LIBv2 Solver Command specified, which means that no actual SMT solving can be done");
213 }
214
215 if (storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().isExportSmtLibScriptSet()) {
216 STORM_LOG_DEBUG("The SMT-LIBv2 commands are exportet to the given file");
217 storm::io::openFile(storm::settings::getModule<storm::settings::modules::Smt2SmtSolverSettings>().getExportSmtLibScriptPath(), commandFile);
218 isCommandFileOpen = true;
219 // TODO also close file
220 }
221
222 // some initial commands
223 writeCommand("( set-option :print-success true )", true);
224 writeCommand("( set-logic QF_NRA )", true);
225 // writeCommand("( get-info :name )");
226}
227
229 return this->needsRestart;
230}
231
232void SmtlibSmtSolver::writeCommand(std::string smt2Command, bool expectSuccess) {
233 if (isCommandFileOpen) {
234 commandFile << smt2Command << '\n';
235 }
236
237 if (processIdOfSolver != 0) {
238 if (write(toSolver, (smt2Command + "\n").c_str(), smt2Command.length() + 1) < 0) {
239 STORM_LOG_DEBUG("Was not able to write " << smt2Command << "to the solver.");
240 }
241 if (expectSuccess) {
242 auto output = readSolverOutput();
243 STORM_LOG_THROW(output.size() == 1, storm::exceptions::UnexpectedException,
244 "expected a single success response after smt2 command " + smt2Command + ". Got " + std::to_string(output.size()) +
245 " lines of output instead.");
246 output[0].erase(std::remove_if(output[0].begin(), output[0].end(), ::isspace), output[0].end());
247 STORM_LOG_THROW(output[0] == "success", storm::exceptions::UnexpectedException,
248 "expected <<success>> response after smt2 command " + smt2Command + ". Got <<" + output[0] + ">> instead");
249 }
250 }
251}
252
253std::vector<std::string> SmtlibSmtSolver::readSolverOutput(bool waitForOutput) {
254 if (processIdOfSolver == 0) {
255 STORM_LOG_DEBUG("failed to read solver output as the solver is not running");
256 return std::vector<std::string>();
257 }
258 int bytesReadable;
259 if (waitForOutput) {
260 bytesReadable = 1; // just assume that there are bytes readable
261 } else if (ioctl(fromSolver, FIONREAD, &bytesReadable) < 0) { // actually obtain the readable bytes
262 STORM_LOG_ERROR("Could not check if the solver has output");
263 return std::vector<std::string>();
264 }
265 std::string solverOutput = "";
266 const ssize_t MAX_CHUNK_SIZE = 256;
267 char chunk[MAX_CHUNK_SIZE];
268 while (bytesReadable > 0) {
269 ssize_t chunkSize = read(fromSolver, chunk, MAX_CHUNK_SIZE);
270 STORM_LOG_THROW(chunkSize >= 0, storm::exceptions::UnexpectedException, "failed to read solver output");
271 solverOutput += std::string(chunk, chunkSize);
272 if (ioctl(fromSolver, FIONREAD, &bytesReadable) < 0) { // obtain the new amount of readable bytes
273 STORM_LOG_ERROR("Could not check if the solver has output");
274 return std::vector<std::string>();
275 }
276 if (bytesReadable == 0 && solverOutput.back() != '\n') {
278 "Solver Output '"
279 << solverOutput
280 << "' did not end with newline symbol (\\n). Since we assume that this should be the case, we will wait for more output from the solver");
281 bytesReadable = 1; // we expect more output!
282 }
283 if (bytesReadable > 0) {
284 pid_t w = waitpid(processIdOfSolver, nullptr, WNOHANG);
285 if (w != 0) {
286 STORM_LOG_WARN_COND(w > 0, "Error when checking whether the solver is still running. Will assume that solver has terminated.");
287 STORM_LOG_WARN("The solver exited unexpectedly when reading output: " << solverOutput);
288 solverOutput += "terminated";
289 this->needsRestart = true;
290 this->processIdOfSolver = 0;
291 bytesReadable = 0;
292 }
293 }
294 }
295 checkForErrorMessage(solverOutput);
296 std::vector<std::string> solverOutputAsVector;
297 if (solverOutput.length() > 0) {
298 solverOutput = solverOutput.substr(0, solverOutput.length() - 1);
299 boost::split(solverOutputAsVector, solverOutput, boost::is_any_of("\n"));
300 // note: this is a little bit unsafe as \n can be contained within a solver response
301 }
302 return solverOutputAsVector;
303}
304
305void SmtlibSmtSolver::checkForErrorMessage(const std::string message) {
306 size_t errorOccurrance = message.find("error");
307 // do not throw an exception for timeout or memout errors
308 if (message.find("timeout") != std::string::npos) {
309 STORM_LOG_INFO("SMT solver answered: '" << message << "' and I am interpreting this as timeout ");
310 this->needsRestart = true;
311 this->processIdOfSolver = 0;
312 } else if (message.find("memory") != std::string::npos) {
313 STORM_LOG_INFO("SMT solver answered: '" << message << "' and I am interpreting this as out of memory ");
314 this->needsRestart = true;
315 this->processIdOfSolver = 0;
316 } else if (errorOccurrance != std::string::npos) {
317 this->needsRestart = true;
318 std::string errorMsg = "An error was detected while checking the solver output. ";
319 STORM_LOG_DEBUG("Detected an error message in the solver response:\n" + message);
320 size_t firstQuoteSign = message.find('\"', errorOccurrance);
321 if (firstQuoteSign != std::string::npos && message.find("\\\"", firstQuoteSign - 1) != firstQuoteSign - 1) {
322 size_t secondQuoteSign = message.find('\"', firstQuoteSign + 1);
323 while (secondQuoteSign != std::string::npos && message.find("\\\"", secondQuoteSign - 1) == secondQuoteSign - 1) {
324 secondQuoteSign = message.find('\"', secondQuoteSign + 1);
325 }
326 if (secondQuoteSign != std::string::npos) {
327 errorMsg += "The error message was: <<" + message.substr(errorOccurrance, secondQuoteSign - errorOccurrance + 1) + ">>.";
328 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg);
329 return;
330 }
331 }
332 errorMsg += "The error message could not be parsed correctly. Snippet:\n" + message.substr(errorOccurrance, 200);
333 STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, errorMsg);
334 }
335}
336} // namespace solver
337} // namespace storm
This class is responsible for managing a set of typed variables and all expressions using these varia...
The base class for all model references.
Definition SmtSolver.h:31
An interface that captures the functionality of an SMT solver.
Definition SmtSolver.h:22
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
Definition SmtSolver.cpp:79
CheckResult
possible check results
Definition SmtSolver.h:25
virtual bool getBooleanValue(storm::expressions::Variable const &variable) const override
SmtlibModelReference(storm::expressions::ExpressionManager const &manager)
virtual std::string toString() const override
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const &variable) const override
virtual double getRationalValue(storm::expressions::Variable const &variable) const override
virtual CheckResult check() override
Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.
virtual void push() override
Pushes a backtracking point on the solver's stack.
virtual void reset() override
Removes all assertions from the solver's stack.
virtual void add(storm::expressions::Expression const &assertion) override
Adds an assertion to the solver's stack.
virtual CheckResult checkWithAssumptions(std::set< storm::expressions::Expression > const &assumptions) override
Checks whether the conjunction of assertions that are currently on the solver's stack together with t...
SmtlibSmtSolver(storm::expressions::ExpressionManager &manager, bool useCarlExpressions=false)
Creates a new solver with the given manager.
virtual void pop() override
Pops a backtracking point from the solver's stack.
#define STORM_LOG_INFO(message)
Definition logging.h:24
#define STORM_LOG_WARN(message)
Definition logging.h:25
#define STORM_LOG_DEBUG(message)
Definition logging.h:18
#define STORM_LOG_ERROR(message)
Definition logging.h:26
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
void openFile(std::string const &filepath, std::ofstream &filestream, bool append=false, bool silent=false)
Open the given file for writing.
Definition file.h:18
LabParser.cpp.
carl::Relation CompareRelation
carl::Variable RationalFunctionVariable